Metamath Proof Explorer

Theorem dffun2OLDOLD

Description: Obsolete version of dffun2 as of 11-Dec-2024. (Contributed by NM, 29-Dec-1996) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion dffun2OLDOLD ( Fun 𝐴 ↔ ( Rel 𝐴 ∧ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 𝐴 𝑦 ∧ 𝑥 𝐴 𝑧 ) → 𝑦 = 𝑧 ) ) )

Proof

Step Hyp Ref Expression
1 df-fun ⊢ ( Fun 𝐴 ↔ ( Rel 𝐴 ∧ ( 𝐴 ∘ ◡ 𝐴 ) ⊆ I ) )
2 df-id ⊢ I = { ⟨ 𝑦 , 𝑧 ⟩ ∣ 𝑦 = 𝑧 }
3 2 sseq2i ⊢ ( ( 𝐴 ∘ ◡ 𝐴 ) ⊆ I ↔ ( 𝐴 ∘ ◡ 𝐴 ) ⊆ { ⟨ 𝑦 , 𝑧 ⟩ ∣ 𝑦 = 𝑧 } )
4 df-co ⊢ ( 𝐴 ∘ ◡ 𝐴 ) = { ⟨ 𝑦 , 𝑧 ⟩ ∣ ∃ 𝑥 ( 𝑦 ◡ 𝐴 𝑥 ∧ 𝑥 𝐴 𝑧 ) }
5 4 sseq1i ⊢ ( ( 𝐴 ∘ ◡ 𝐴 ) ⊆ { ⟨ 𝑦 , 𝑧 ⟩ ∣ 𝑦 = 𝑧 } ↔ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ∃ 𝑥 ( 𝑦 ◡ 𝐴 𝑥 ∧ 𝑥 𝐴 𝑧 ) } ⊆ { ⟨ 𝑦 , 𝑧 ⟩ ∣ 𝑦 = 𝑧 } )
6 ssopab2bw ⊢ ( { ⟨ 𝑦 , 𝑧 ⟩ ∣ ∃ 𝑥 ( 𝑦 ◡ 𝐴 𝑥 ∧ 𝑥 𝐴 𝑧 ) } ⊆ { ⟨ 𝑦 , 𝑧 ⟩ ∣ 𝑦 = 𝑧 } ↔ ∀ 𝑦 ∀ 𝑧 ( ∃ 𝑥 ( 𝑦 ◡ 𝐴 𝑥 ∧ 𝑥 𝐴 𝑧 ) → 𝑦 = 𝑧 ) )
7 3 5 6 3bitri ⊢ ( ( 𝐴 ∘ ◡ 𝐴 ) ⊆ I ↔ ∀ 𝑦 ∀ 𝑧 ( ∃ 𝑥 ( 𝑦 ◡ 𝐴 𝑥 ∧ 𝑥 𝐴 𝑧 ) → 𝑦 = 𝑧 ) )
8 vex ⊢ 𝑦 ∈ V
9 vex ⊢ 𝑥 ∈ V
10 8 9 brcnv ⊢ ( 𝑦 ◡ 𝐴 𝑥 ↔ 𝑥 𝐴 𝑦 )
11 10 anbi1i ⊢ ( ( 𝑦 ◡ 𝐴 𝑥 ∧ 𝑥 𝐴 𝑧 ) ↔ ( 𝑥 𝐴 𝑦 ∧ 𝑥 𝐴 𝑧 ) )
12 11 exbii ⊢ ( ∃ 𝑥 ( 𝑦 ◡ 𝐴 𝑥 ∧ 𝑥 𝐴 𝑧 ) ↔ ∃ 𝑥 ( 𝑥 𝐴 𝑦 ∧ 𝑥 𝐴 𝑧 ) )
13 12 imbi1i ⊢ ( ( ∃ 𝑥 ( 𝑦 ◡ 𝐴 𝑥 ∧ 𝑥 𝐴 𝑧 ) → 𝑦 = 𝑧 ) ↔ ( ∃ 𝑥 ( 𝑥 𝐴 𝑦 ∧ 𝑥 𝐴 𝑧 ) → 𝑦 = 𝑧 ) )
14 19.23v ⊢ ( ∀ 𝑥 ( ( 𝑥 𝐴 𝑦 ∧ 𝑥 𝐴 𝑧 ) → 𝑦 = 𝑧 ) ↔ ( ∃ 𝑥 ( 𝑥 𝐴 𝑦 ∧ 𝑥 𝐴 𝑧 ) → 𝑦 = 𝑧 ) )
15 13 14 bitr4i ⊢ ( ( ∃ 𝑥 ( 𝑦 ◡ 𝐴 𝑥 ∧ 𝑥 𝐴 𝑧 ) → 𝑦 = 𝑧 ) ↔ ∀ 𝑥 ( ( 𝑥 𝐴 𝑦 ∧ 𝑥 𝐴 𝑧 ) → 𝑦 = 𝑧 ) )
16 15 albii ⊢ ( ∀ 𝑧 ( ∃ 𝑥 ( 𝑦 ◡ 𝐴 𝑥 ∧ 𝑥 𝐴 𝑧 ) → 𝑦 = 𝑧 ) ↔ ∀ 𝑧 ∀ 𝑥 ( ( 𝑥 𝐴 𝑦 ∧ 𝑥 𝐴 𝑧 ) → 𝑦 = 𝑧 ) )
17 alcom ⊢ ( ∀ 𝑧 ∀ 𝑥 ( ( 𝑥 𝐴 𝑦 ∧ 𝑥 𝐴 𝑧 ) → 𝑦 = 𝑧 ) ↔ ∀ 𝑥 ∀ 𝑧 ( ( 𝑥 𝐴 𝑦 ∧ 𝑥 𝐴 𝑧 ) → 𝑦 = 𝑧 ) )
18 16 17 bitri ⊢ ( ∀ 𝑧 ( ∃ 𝑥 ( 𝑦 ◡ 𝐴 𝑥 ∧ 𝑥 𝐴 𝑧 ) → 𝑦 = 𝑧 ) ↔ ∀ 𝑥 ∀ 𝑧 ( ( 𝑥 𝐴 𝑦 ∧ 𝑥 𝐴 𝑧 ) → 𝑦 = 𝑧 ) )
19 18 albii ⊢ ( ∀ 𝑦 ∀ 𝑧 ( ∃ 𝑥 ( 𝑦 ◡ 𝐴 𝑥 ∧ 𝑥 𝐴 𝑧 ) → 𝑦 = 𝑧 ) ↔ ∀ 𝑦 ∀ 𝑥 ∀ 𝑧 ( ( 𝑥 𝐴 𝑦 ∧ 𝑥 𝐴 𝑧 ) → 𝑦 = 𝑧 ) )
20 alcom ⊢ ( ∀ 𝑦 ∀ 𝑥 ∀ 𝑧 ( ( 𝑥 𝐴 𝑦 ∧ 𝑥 𝐴 𝑧 ) → 𝑦 = 𝑧 ) ↔ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 𝐴 𝑦 ∧ 𝑥 𝐴 𝑧 ) → 𝑦 = 𝑧 ) )
21 7 19 20 3bitri ⊢ ( ( 𝐴 ∘ ◡ 𝐴 ) ⊆ I ↔ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 𝐴 𝑦 ∧ 𝑥 𝐴 𝑧 ) → 𝑦 = 𝑧 ) )
22 21 anbi2i ⊢ ( ( Rel 𝐴 ∧ ( 𝐴 ∘ ◡ 𝐴 ) ⊆ I ) ↔ ( Rel 𝐴 ∧ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 𝐴 𝑦 ∧ 𝑥 𝐴 𝑧 ) → 𝑦 = 𝑧 ) ) )
23 1 22 bitri ⊢ ( Fun 𝐴 ↔ ( Rel 𝐴 ∧ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 𝐴 𝑦 ∧ 𝑥 𝐴 𝑧 ) → 𝑦 = 𝑧 ) ) )