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

Metamath Proof Explorer

Theorem tz6.12-2

Description: Function value when F is not a function. Theorem 6.12(2) of TakeutiZaring p. 27. (Contributed by NM, 30-Apr-2004) (Proof shortened by Mario Carneiro, 31-Aug-2015) Avoid ax-10 , ax-11 , ax-12 . (Revised by TM, 25-Jan-2026)

Ref Expression
Assertion tz6.12-2 ( ¬ ∃! 𝑥 𝐴 𝐹 𝑥 → ( 𝐹 ‘ 𝐴 ) = ∅ )

Proof

Step Hyp Ref Expression
1 df-fv ⊢ ( 𝐹 ‘ 𝐴 ) = ( ℩ 𝑦 𝐴 𝐹 𝑦 )
2 eu6im ⊢ ( ∃ 𝑧 ∀ 𝑥 ( 𝐴 𝐹 𝑥 ↔ 𝑥 = 𝑧 ) → ∃! 𝑥 𝐴 𝐹 𝑥 )
3 breq2 ⊢ ( 𝑦 = 𝑥 → ( 𝐴 𝐹 𝑦 ↔ 𝐴 𝐹 𝑥 ) )
4 3 eqabcbw ⊢ ( { 𝑦 ∣ 𝐴 𝐹 𝑦 } = { 𝑧 } ↔ ∀ 𝑥 ( 𝐴 𝐹 𝑥 ↔ 𝑥 ∈ { 𝑧 } ) )
5 velsn ⊢ ( 𝑥 ∈ { 𝑧 } ↔ 𝑥 = 𝑧 )
6 5 bibi2i ⊢ ( ( 𝐴 𝐹 𝑥 ↔ 𝑥 ∈ { 𝑧 } ) ↔ ( 𝐴 𝐹 𝑥 ↔ 𝑥 = 𝑧 ) )
7 6 albii ⊢ ( ∀ 𝑥 ( 𝐴 𝐹 𝑥 ↔ 𝑥 ∈ { 𝑧 } ) ↔ ∀ 𝑥 ( 𝐴 𝐹 𝑥 ↔ 𝑥 = 𝑧 ) )
8 4 7 bitri ⊢ ( { 𝑦 ∣ 𝐴 𝐹 𝑦 } = { 𝑧 } ↔ ∀ 𝑥 ( 𝐴 𝐹 𝑥 ↔ 𝑥 = 𝑧 ) )
9 8 exbii ⊢ ( ∃ 𝑧 { 𝑦 ∣ 𝐴 𝐹 𝑦 } = { 𝑧 } ↔ ∃ 𝑧 ∀ 𝑥 ( 𝐴 𝐹 𝑥 ↔ 𝑥 = 𝑧 ) )
10 iotanul2 ⊢ ( ¬ ∃ 𝑧 { 𝑦 ∣ 𝐴 𝐹 𝑦 } = { 𝑧 } → ( ℩ 𝑦 𝐴 𝐹 𝑦 ) = ∅ )
11 9 10 sylnbir ⊢ ( ¬ ∃ 𝑧 ∀ 𝑥 ( 𝐴 𝐹 𝑥 ↔ 𝑥 = 𝑧 ) → ( ℩ 𝑦 𝐴 𝐹 𝑦 ) = ∅ )
12 2 11 nsyl5 ⊢ ( ¬ ∃! 𝑥 𝐴 𝐹 𝑥 → ( ℩ 𝑦 𝐴 𝐹 𝑦 ) = ∅ )
13 1 12 eqtrid ⊢ ( ¬ ∃! 𝑥 𝐴 𝐹 𝑥 → ( 𝐹 ‘ 𝐴 ) = ∅ )