Theorem dffun2 6548

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 6540	. 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 6532

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 4584  df-pr 4586  df-op 4590  df-br 5103  df-opab 5167  df-id 5545  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-fun 6540

This theorem is used by:  dffun6  6549  dffun4  6551  fununiq  6555  fundif  6589  fliftfun  7320  frrlem9  8313  fprlem1  8319  frrlem15  9762  fpwwe2lem10  10726  fclim  15721  invfun  17940  lmfun  23700  ulmdm  26721  fundmpss  36575  fnsingle  36724  funimage  36733  funpartfun  36750  functhincfun  50601