Theorem dffun2 6524

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

Assertion

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

Distinct variable group:   𝑥,𝐴,𝑦,𝑧

Proof of Theorem dffun2

Dummy variable 𝑤 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-fun 6516	. 2 ⊢ (Fun 𝐴 ↔ (Rel 𝐴 ∧ (𝐴 ∘ ◡𝐴) ⊆ I ))
2		cotrg 6083	. . . 4 ⊢ ((𝐴 ∘ ◡𝐴) ⊆ I ↔ ∀𝑦∀𝑥∀𝑧((𝑦◡𝐴𝑥 ∧ 𝑥𝐴𝑧) → 𝑦 I 𝑧))
3		breq1 5113	. . . . . . . . 9 ⊢ (𝑦 = 𝑤 → (𝑦◡𝐴𝑥 ↔ 𝑤◡𝐴𝑥))
4	3	anbi1d 631	. . . . . . . 8 ⊢ (𝑦 = 𝑤 → ((𝑦◡𝐴𝑥 ∧ 𝑥𝐴𝑧) ↔ (𝑤◡𝐴𝑥 ∧ 𝑥𝐴𝑧)))
5		breq1 5113	. . . . . . . 8 ⊢ (𝑦 = 𝑤 → (𝑦 I 𝑧 ↔ 𝑤 I 𝑧))
6	4, 5	imbi12d 344	. . . . . . 7 ⊢ (𝑦 = 𝑤 → (((𝑦◡𝐴𝑥 ∧ 𝑥𝐴𝑧) → 𝑦 I 𝑧) ↔ ((𝑤◡𝐴𝑥 ∧ 𝑥𝐴𝑧) → 𝑤 I 𝑧)))
7	6	albidv 1920	. . . . . 6 ⊢ (𝑦 = 𝑤 → (∀𝑧((𝑦◡𝐴𝑥 ∧ 𝑥𝐴𝑧) → 𝑦 I 𝑧) ↔ ∀𝑧((𝑤◡𝐴𝑥 ∧ 𝑥𝐴𝑧) → 𝑤 I 𝑧)))
8		breq2 5114	. . . . . . . . 9 ⊢ (𝑥 = 𝑤 → (𝑦◡𝐴𝑥 ↔ 𝑦◡𝐴𝑤))
9		breq1 5113	. . . . . . . . 9 ⊢ (𝑥 = 𝑤 → (𝑥𝐴𝑧 ↔ 𝑤𝐴𝑧))
10	8, 9	anbi12d 632	. . . . . . . 8 ⊢ (𝑥 = 𝑤 → ((𝑦◡𝐴𝑥 ∧ 𝑥𝐴𝑧) ↔ (𝑦◡𝐴𝑤 ∧ 𝑤𝐴𝑧)))
11	10	imbi1d 341	. . . . . . 7 ⊢ (𝑥 = 𝑤 → (((𝑦◡𝐴𝑥 ∧ 𝑥𝐴𝑧) → 𝑦 I 𝑧) ↔ ((𝑦◡𝐴𝑤 ∧ 𝑤𝐴𝑧) → 𝑦 I 𝑧)))
12	11	albidv 1920	. . . . . 6 ⊢ (𝑥 = 𝑤 → (∀𝑧((𝑦◡𝐴𝑥 ∧ 𝑥𝐴𝑧) → 𝑦 I 𝑧) ↔ ∀𝑧((𝑦◡𝐴𝑤 ∧ 𝑤𝐴𝑧) → 𝑦 I 𝑧)))
13	7, 12	alcomw 2045	. . . . 5 ⊢ (∀𝑦∀𝑥∀𝑧((𝑦◡𝐴𝑥 ∧ 𝑥𝐴𝑧) → 𝑦 I 𝑧) ↔ ∀𝑥∀𝑦∀𝑧((𝑦◡𝐴𝑥 ∧ 𝑥𝐴𝑧) → 𝑦 I 𝑧))
14		vex 3454	. . . . . . . . 9 ⊢ 𝑦 ∈ V
15		vex 3454	. . . . . . . . 9 ⊢ 𝑥 ∈ V
16	14, 15	brcnv 5849	. . . . . . . 8 ⊢ (𝑦◡𝐴𝑥 ↔ 𝑥𝐴𝑦)
17	16	anbi1i 624	. . . . . . 7 ⊢ ((𝑦◡𝐴𝑥 ∧ 𝑥𝐴𝑧) ↔ (𝑥𝐴𝑦 ∧ 𝑥𝐴𝑧))
18		vex 3454	. . . . . . . 8 ⊢ 𝑧 ∈ V
19	18	ideq 5819	. . . . . . 7 ⊢ (𝑦 I 𝑧 ↔ 𝑦 = 𝑧)
20	17, 19	imbi12i 350	. . . . . 6 ⊢ (((𝑦◡𝐴𝑥 ∧ 𝑥𝐴𝑧) → 𝑦 I 𝑧) ↔ ((𝑥𝐴𝑦 ∧ 𝑥𝐴𝑧) → 𝑦 = 𝑧))
21	20	3albii 1821	. . . . 5 ⊢ (∀𝑥∀𝑦∀𝑧((𝑦◡𝐴𝑥 ∧ 𝑥𝐴𝑧) → 𝑦 I 𝑧) ↔ ∀𝑥∀𝑦∀𝑧((𝑥𝐴𝑦 ∧ 𝑥𝐴𝑧) → 𝑦 = 𝑧))
22	13, 21	bitri 275	. . . 4 ⊢ (∀𝑦∀𝑥∀𝑧((𝑦◡𝐴𝑥 ∧ 𝑥𝐴𝑧) → 𝑦 I 𝑧) ↔ ∀𝑥∀𝑦∀𝑧((𝑥𝐴𝑦 ∧ 𝑥𝐴𝑧) → 𝑦 = 𝑧))
23	2, 22	bitri 275	. . 3 ⊢ ((𝐴 ∘ ◡𝐴) ⊆ I ↔ ∀𝑥∀𝑦∀𝑧((𝑥𝐴𝑦 ∧ 𝑥𝐴𝑧) → 𝑦 = 𝑧))
24	23	anbi2i 623	. 2 ⊢ ((Rel 𝐴 ∧ (𝐴 ∘ ◡𝐴) ⊆ I ) ↔ (Rel 𝐴 ∧ ∀𝑥∀𝑦∀𝑧((𝑥𝐴𝑦 ∧ 𝑥𝐴𝑧) → 𝑦 = 𝑧)))
25	1, 24	bitri 275	1 ⊢ (Fun 𝐴 ↔ (Rel 𝐴 ∧ ∀𝑥∀𝑦∀𝑧((𝑥𝐴𝑦 ∧ 𝑥𝐴𝑧) → 𝑦 = 𝑧)))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1538   ⊆ wss 3917   class class class wbr 5110   I cid 5535  ^◡ccnv 5640   ∘ ccom 5645  Rel wrel 5646  Fun wfun 6508

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-br 5111  df-opab 5173  df-id 5536  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-fun 6516

This theorem is referenced by:  dffun6  6527  dffun3OLD  6529  dffun4  6530  fundif  6568  fliftfun  7290  frrlem9  8276  fprlem1  8282  frrlem15  9717  fpwwe2lem10  10600  fclim  15526  invfun  17733  lmfun  23275  ulmdm  26309  fundmpss  35761  fununiq  35763  fnsingle  35914  funimage  35923  funpartfun  35938  functhincfun  49442