This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nfunsn

Description: If the restriction of a class to a singleton is not a function, then its value is the empty set. (An artifact of our function value definition.) (Contributed by NM, 8-Aug-2010) (Proof shortened by Andrew Salmon, 22-Oct-2011)

Ref Expression
Assertion nfunsn ( ¬ Fun ( 𝐹 ↾ { 𝐴 } ) → ( 𝐹 ‘ 𝐴 ) = ∅ )

Proof

Step Hyp Ref Expression
1 eumo ⊢ ( ∃! 𝑦 𝐴 𝐹 𝑦 → ∃* 𝑦 𝐴 𝐹 𝑦 )
2 vex ⊢ 𝑦 ∈ V
3 2 brresi ⊢ ( 𝑥 ( 𝐹 ↾ { 𝐴 } ) 𝑦 ↔ ( 𝑥 ∈ { 𝐴 } ∧ 𝑥 𝐹 𝑦 ) )
4 velsn ⊢ ( 𝑥 ∈ { 𝐴 } ↔ 𝑥 = 𝐴 )
5 breq1 ⊢ ( 𝑥 = 𝐴 → ( 𝑥 𝐹 𝑦 ↔ 𝐴 𝐹 𝑦 ) )
6 4 5 sylbi ⊢ ( 𝑥 ∈ { 𝐴 } → ( 𝑥 𝐹 𝑦 ↔ 𝐴 𝐹 𝑦 ) )
7 6 biimpa ⊢ ( ( 𝑥 ∈ { 𝐴 } ∧ 𝑥 𝐹 𝑦 ) → 𝐴 𝐹 𝑦 )
8 3 7 sylbi ⊢ ( 𝑥 ( 𝐹 ↾ { 𝐴 } ) 𝑦 → 𝐴 𝐹 𝑦 )
9 8 moimi ⊢ ( ∃* 𝑦 𝐴 𝐹 𝑦 → ∃* 𝑦 𝑥 ( 𝐹 ↾ { 𝐴 } ) 𝑦 )
10 1 9 syl ⊢ ( ∃! 𝑦 𝐴 𝐹 𝑦 → ∃* 𝑦 𝑥 ( 𝐹 ↾ { 𝐴 } ) 𝑦 )
11 tz6.12-2 ⊢ ( ¬ ∃! 𝑦 𝐴 𝐹 𝑦 → ( 𝐹 ‘ 𝐴 ) = ∅ )
12 10 11 nsyl4 ⊢ ( ¬ ( 𝐹 ‘ 𝐴 ) = ∅ → ∃* 𝑦 𝑥 ( 𝐹 ↾ { 𝐴 } ) 𝑦 )
13 12 alrimiv ⊢ ( ¬ ( 𝐹 ‘ 𝐴 ) = ∅ → ∀ 𝑥 ∃* 𝑦 𝑥 ( 𝐹 ↾ { 𝐴 } ) 𝑦 )
14 relres ⊢ Rel ( 𝐹 ↾ { 𝐴 } )
15 13 14 jctil ⊢ ( ¬ ( 𝐹 ‘ 𝐴 ) = ∅ → ( Rel ( 𝐹 ↾ { 𝐴 } ) ∧ ∀ 𝑥 ∃* 𝑦 𝑥 ( 𝐹 ↾ { 𝐴 } ) 𝑦 ) )
16 dffun6 ⊢ ( Fun ( 𝐹 ↾ { 𝐴 } ) ↔ ( Rel ( 𝐹 ↾ { 𝐴 } ) ∧ ∀ 𝑥 ∃* 𝑦 𝑥 ( 𝐹 ↾ { 𝐴 } ) 𝑦 ) )
17 15 16 sylibr ⊢ ( ¬ ( 𝐹 ‘ 𝐴 ) = ∅ → Fun ( 𝐹 ↾ { 𝐴 } ) )
18 17 con1i ⊢ ( ¬ Fun ( 𝐹 ↾ { 𝐴 } ) → ( 𝐹 ‘ 𝐴 ) = ∅ )