Theorem dffun2

Description: Alternate definition of a function. (Contributed by NM, 29-Dec-1996) Avoid ax-10 , ax-12 . (Revised by SN, 19-Dec-2024) Avoid ax-11 . (Revised by BTernaryTau, 29-Dec-2024)

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

Proof

Step	Hyp	Ref	Expression
1		df-fun	⊢ ( Fun 𝐴 ↔ ( Rel 𝐴 ∧ ( 𝐴 ∘ ◡ 𝐴 ) ⊆ I ) )
2		cotrg	⊢ ( ( 𝐴 ∘ ◡ 𝐴 ) ⊆ I ↔ ∀ 𝑦 ∀ 𝑥 ∀ 𝑧 ( ( 𝑦 ◡ 𝐴 𝑥 ∧ 𝑥 𝐴 𝑧 ) → 𝑦 I 𝑧 ) )
3		breq1	⊢ ( 𝑦 = 𝑤 → ( 𝑦 ◡ 𝐴 𝑥 ↔ 𝑤 ◡ 𝐴 𝑥 ) )
4	3	anbi1d	⊢ ( 𝑦 = 𝑤 → ( ( 𝑦 ◡ 𝐴 𝑥 ∧ 𝑥 𝐴 𝑧 ) ↔ ( 𝑤 ◡ 𝐴 𝑥 ∧ 𝑥 𝐴 𝑧 ) ) )
5		breq1	⊢ ( 𝑦 = 𝑤 → ( 𝑦 I 𝑧 ↔ 𝑤 I 𝑧 ) )
6	4 5	imbi12d	⊢ ( 𝑦 = 𝑤 → ( ( ( 𝑦 ◡ 𝐴 𝑥 ∧ 𝑥 𝐴 𝑧 ) → 𝑦 I 𝑧 ) ↔ ( ( 𝑤 ◡ 𝐴 𝑥 ∧ 𝑥 𝐴 𝑧 ) → 𝑤 I 𝑧 ) ) )
7	6	albidv	⊢ ( 𝑦 = 𝑤 → ( ∀ 𝑧 ( ( 𝑦 ◡ 𝐴 𝑥 ∧ 𝑥 𝐴 𝑧 ) → 𝑦 I 𝑧 ) ↔ ∀ 𝑧 ( ( 𝑤 ◡ 𝐴 𝑥 ∧ 𝑥 𝐴 𝑧 ) → 𝑤 I 𝑧 ) ) )
8		breq2	⊢ ( 𝑥 = 𝑤 → ( 𝑦 ◡ 𝐴 𝑥 ↔ 𝑦 ◡ 𝐴 𝑤 ) )
9		breq1	⊢ ( 𝑥 = 𝑤 → ( 𝑥 𝐴 𝑧 ↔ 𝑤 𝐴 𝑧 ) )
10	8 9	anbi12d	⊢ ( 𝑥 = 𝑤 → ( ( 𝑦 ◡ 𝐴 𝑥 ∧ 𝑥 𝐴 𝑧 ) ↔ ( 𝑦 ◡ 𝐴 𝑤 ∧ 𝑤 𝐴 𝑧 ) ) )
11	10	imbi1d	⊢ ( 𝑥 = 𝑤 → ( ( ( 𝑦 ◡ 𝐴 𝑥 ∧ 𝑥 𝐴 𝑧 ) → 𝑦 I 𝑧 ) ↔ ( ( 𝑦 ◡ 𝐴 𝑤 ∧ 𝑤 𝐴 𝑧 ) → 𝑦 I 𝑧 ) ) )
12	11	albidv	⊢ ( 𝑥 = 𝑤 → ( ∀ 𝑧 ( ( 𝑦 ◡ 𝐴 𝑥 ∧ 𝑥 𝐴 𝑧 ) → 𝑦 I 𝑧 ) ↔ ∀ 𝑧 ( ( 𝑦 ◡ 𝐴 𝑤 ∧ 𝑤 𝐴 𝑧 ) → 𝑦 I 𝑧 ) ) )
13	7 12	alcomw	⊢ ( ∀ 𝑦 ∀ 𝑥 ∀ 𝑧 ( ( 𝑦 ◡ 𝐴 𝑥 ∧ 𝑥 𝐴 𝑧 ) → 𝑦 I 𝑧 ) ↔ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑦 ◡ 𝐴 𝑥 ∧ 𝑥 𝐴 𝑧 ) → 𝑦 I 𝑧 ) )
14		vex	⊢ 𝑦 ∈ V
15		vex	⊢ 𝑥 ∈ V
16	14 15	brcnv	⊢ ( 𝑦 ◡ 𝐴 𝑥 ↔ 𝑥 𝐴 𝑦 )
17	16	anbi1i	⊢ ( ( 𝑦 ◡ 𝐴 𝑥 ∧ 𝑥 𝐴 𝑧 ) ↔ ( 𝑥 𝐴 𝑦 ∧ 𝑥 𝐴 𝑧 ) )
18		vex	⊢ 𝑧 ∈ V
19	18	ideq	⊢ ( 𝑦 I 𝑧 ↔ 𝑦 = 𝑧 )
20	17 19	imbi12i	⊢ ( ( ( 𝑦 ◡ 𝐴 𝑥 ∧ 𝑥 𝐴 𝑧 ) → 𝑦 I 𝑧 ) ↔ ( ( 𝑥 𝐴 𝑦 ∧ 𝑥 𝐴 𝑧 ) → 𝑦 = 𝑧 ) )
21	20	3albii	⊢ ( ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑦 ◡ 𝐴 𝑥 ∧ 𝑥 𝐴 𝑧 ) → 𝑦 I 𝑧 ) ↔ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 𝐴 𝑦 ∧ 𝑥 𝐴 𝑧 ) → 𝑦 = 𝑧 ) )
22	13 21	bitri	⊢ ( ∀ 𝑦 ∀ 𝑥 ∀ 𝑧 ( ( 𝑦 ◡ 𝐴 𝑥 ∧ 𝑥 𝐴 𝑧 ) → 𝑦 I 𝑧 ) ↔ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 𝐴 𝑦 ∧ 𝑥 𝐴 𝑧 ) → 𝑦 = 𝑧 ) )
23	2 22	bitri	⊢ ( ( 𝐴 ∘ ◡ 𝐴 ) ⊆ I ↔ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 𝐴 𝑦 ∧ 𝑥 𝐴 𝑧 ) → 𝑦 = 𝑧 ) )
24	23	anbi2i	⊢ ( ( Rel 𝐴 ∧ ( 𝐴 ∘ ◡ 𝐴 ) ⊆ I ) ↔ ( Rel 𝐴 ∧ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 𝐴 𝑦 ∧ 𝑥 𝐴 𝑧 ) → 𝑦 = 𝑧 ) ) )
25	1 24	bitri	⊢ ( Fun 𝐴 ↔ ( Rel 𝐴 ∧ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 𝐴 𝑦 ∧ 𝑥 𝐴 𝑧 ) → 𝑦 = 𝑧 ) ) )