Theorem dffun2 6549

Description: Alternate definition of a function. (Contributed by NM, 29-Dec-1996.) Avoid ax-10 2177, ax-12 2212. (Revised by SN, 19-Dec-2024.) Avoid ax-11 2193. (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 6541	. 2 ⊢ (Fun 𝐴 ↔ (Rel 𝐴 ∧ (𝐴 ∘ ◡𝐴) ⊆ I ))
2		cotrg 6104	. . . 4 ⊢ ((𝐴 ∘ ◡𝐴) ⊆ I ↔ ∀𝑦∀𝑥∀𝑧((𝑦◡𝐴𝑥 ∧ 𝑥𝐴𝑧) → 𝑦 I 𝑧))
3		breq1 5105	. . . . . . . . 9 ⊢ (𝑦 = 𝑤 → (𝑦◡𝐴𝑥 ↔ 𝑤◡𝐴𝑥))
4	3	anbi1d 643	. . . . . . . 8 ⊢ (𝑦 = 𝑤 → ((𝑦◡𝐴𝑥 ∧ 𝑥𝐴𝑧) ↔ (𝑤◡𝐴𝑥 ∧ 𝑥𝐴𝑧)))
5		breq1 5105	. . . . . . . 8 ⊢ (𝑦 = 𝑤 → (𝑦 I 𝑧 ↔ 𝑤 I 𝑧))
6	4, 5	imbi12d 347	. . . . . . 7 ⊢ (𝑦 = 𝑤 → (((𝑦◡𝐴𝑥 ∧ 𝑥𝐴𝑧) → 𝑦 I 𝑧) ↔ ((𝑤◡𝐴𝑥 ∧ 𝑥𝐴𝑧) → 𝑤 I 𝑧)))
7	6	albidv 1952	. . . . . 6 ⊢ (𝑦 = 𝑤 → (∀𝑧((𝑦◡𝐴𝑥 ∧ 𝑥𝐴𝑧) → 𝑦 I 𝑧) ↔ ∀𝑧((𝑤◡𝐴𝑥 ∧ 𝑥𝐴𝑧) → 𝑤 I 𝑧)))
8		breq2 5106	. . . . . . . . 9 ⊢ (𝑥 = 𝑤 → (𝑦◡𝐴𝑥 ↔ 𝑦◡𝐴𝑤))
9		breq1 5105	. . . . . . . . 9 ⊢ (𝑥 = 𝑤 → (𝑥𝐴𝑧 ↔ 𝑤𝐴𝑧))
10	8, 9	anbi12d 644	. . . . . . . 8 ⊢ (𝑥 = 𝑤 → ((𝑦◡𝐴𝑥 ∧ 𝑥𝐴𝑧) ↔ (𝑦◡𝐴𝑤 ∧ 𝑤𝐴𝑧)))
11	10	imbi1d 344	. . . . . . 7 ⊢ (𝑥 = 𝑤 → (((𝑦◡𝐴𝑥 ∧ 𝑥𝐴𝑧) → 𝑦 I 𝑧) ↔ ((𝑦◡𝐴𝑤 ∧ 𝑤𝐴𝑧) → 𝑦 I 𝑧)))
12	11	albidv 1952	. . . . . 6 ⊢ (𝑥 = 𝑤 → (∀𝑧((𝑦◡𝐴𝑥 ∧ 𝑥𝐴𝑧) → 𝑦 I 𝑧) ↔ ∀𝑧((𝑦◡𝐴𝑤 ∧ 𝑤𝐴𝑧) → 𝑦 I 𝑧)))
13	7, 12	alcomw 2077	. . . . 5 ⊢ (∀𝑦∀𝑥∀𝑧((𝑦◡𝐴𝑥 ∧ 𝑥𝐴𝑧) → 𝑦 I 𝑧) ↔ ∀𝑥∀𝑦∀𝑧((𝑦◡𝐴𝑥 ∧ 𝑥𝐴𝑧) → 𝑦 I 𝑧))
14		vex 3454	. . . . . . . . 9 ⊢ 𝑦 ∈ V
15		vex 3454	. . . . . . . . 9 ⊢ 𝑥 ∈ V
16	14, 15	brcnv 5859	. . . . . . . 8 ⊢ (𝑦◡𝐴𝑥 ↔ 𝑥𝐴𝑦)
17	16	anbi1i 636	. . . . . . 7 ⊢ ((𝑦◡𝐴𝑥 ∧ 𝑥𝐴𝑧) ↔ (𝑥𝐴𝑦 ∧ 𝑥𝐴𝑧))
18		vex 3454	. . . . . . . 8 ⊢ 𝑧 ∈ V
19	18	ideq 5829	. . . . . . 7 ⊢ (𝑦 I 𝑧 ↔ 𝑦 = 𝑧)
20	17, 19	imbi12i 353	. . . . . 6 ⊢ (((𝑦◡𝐴𝑥 ∧ 𝑥𝐴𝑧) → 𝑦 I 𝑧) ↔ ((𝑥𝐴𝑦 ∧ 𝑥𝐴𝑧) → 𝑦 = 𝑧))
21	20	3albii 1853	. . . . 5 ⊢ (∀𝑥∀𝑦∀𝑧((𝑦◡𝐴𝑥 ∧ 𝑥𝐴𝑧) → 𝑦 I 𝑧) ↔ ∀𝑥∀𝑦∀𝑧((𝑥𝐴𝑦 ∧ 𝑥𝐴𝑧) → 𝑦 = 𝑧))
22	13, 21	bitri 278	. . . 4 ⊢ (∀𝑦∀𝑥∀𝑧((𝑦◡𝐴𝑥 ∧ 𝑥𝐴𝑧) → 𝑦 I 𝑧) ↔ ∀𝑥∀𝑦∀𝑧((𝑥𝐴𝑦 ∧ 𝑥𝐴𝑧) → 𝑦 = 𝑧))
23	2, 22	bitri 278	. . 3 ⊢ ((𝐴 ∘ ◡𝐴) ⊆ I ↔ ∀𝑥∀𝑦∀𝑧((𝑥𝐴𝑦 ∧ 𝑥𝐴𝑧) → 𝑦 = 𝑧))
24	23	anbi2i 635	. 2 ⊢ ((Rel 𝐴 ∧ (𝐴 ∘ ◡𝐴) ⊆ I ) ↔ (Rel 𝐴 ∧ ∀𝑥∀𝑦∀𝑧((𝑥𝐴𝑦 ∧ 𝑥𝐴𝑧) → 𝑦 = 𝑧)))
25	1, 24	bitri 278	1 ⊢ (Fun 𝐴 ↔ (Rel 𝐴 ∧ ∀𝑥∀𝑦∀𝑧((𝑥𝐴𝑦 ∧ 𝑥𝐴𝑧) → 𝑦 = 𝑧)))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401  ∀wal 1567   ⊆ wss 3895   class class class wbr 5102   I cid 5544  ^◡ccnv 5649   ∘ ccom 5654  Rel wrel 5655  Fun wfun 6533

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-pr 5390

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-br 5103  df-opab 5167  df-id 5545  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-fun 6541

This theorem is used by:  dffun6  6550  dffun4  6552  fununiq  6556  fundif  6590  fliftfun  7321  frrlem9  8316  fprlem1  8322  frrlem15  9765  fpwwe2lem10  10729  fclim  15726  invfun  17945  lmfun  23705  ulmdm  26726  fundmpss  36625  fnsingle  36774  funimage  36783  funpartfun  36800  functhincfun  50678