Theorem dffun2

Description: Alternate definition of a function. (Contributed by NM, 29-Dec-1996)

	Ref	Expression
Assertion	dffun2	⊢ ( 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 𝐴 ∧ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 𝐴 𝑦 ∧ 𝑥 𝐴 𝑧 ) → 𝑦 = 𝑧 ) ) )