Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  fununi Structured version   Visualization version   GIF version

Theorem fununi 6399
 Description: The union of a chain (with respect to inclusion) of functions is a function. (Contributed by NM, 10-Aug-2004.)
Assertion
Ref Expression
fununi (∀𝑓𝐴 (Fun 𝑓 ∧ ∀𝑔𝐴 (𝑓𝑔𝑔𝑓)) → Fun 𝐴)
Distinct variable group:   𝑓,𝑔,𝐴

Proof of Theorem fununi
Dummy variables 𝑥 𝑦 𝑧 𝑣 𝑤 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 funrel 6341 . . . . 5 (Fun 𝑓 → Rel 𝑓)
21adantr 484 . . . 4 ((Fun 𝑓 ∧ ∀𝑔𝐴 (𝑓𝑔𝑔𝑓)) → Rel 𝑓)
32ralimi 3128 . . 3 (∀𝑓𝐴 (Fun 𝑓 ∧ ∀𝑔𝐴 (𝑓𝑔𝑔𝑓)) → ∀𝑓𝐴 Rel 𝑓)
4 reluni 5655 . . 3 (Rel 𝐴 ↔ ∀𝑓𝐴 Rel 𝑓)
53, 4sylibr 237 . 2 (∀𝑓𝐴 (Fun 𝑓 ∧ ∀𝑔𝐴 (𝑓𝑔𝑔𝑓)) → Rel 𝐴)
6 r19.28v 3152 . . . 4 ((Fun 𝑓 ∧ ∀𝑔𝐴 (𝑓𝑔𝑔𝑓)) → ∀𝑔𝐴 (Fun 𝑓 ∧ (𝑓𝑔𝑔𝑓)))
76ralimi 3128 . . 3 (∀𝑓𝐴 (Fun 𝑓 ∧ ∀𝑔𝐴 (𝑓𝑔𝑔𝑓)) → ∀𝑓𝐴𝑔𝐴 (Fun 𝑓 ∧ (𝑓𝑔𝑔𝑓)))
8 ssel 3908 . . . . . . . . . . . 12 (𝑤𝑣 → (⟨𝑥, 𝑦⟩ ∈ 𝑤 → ⟨𝑥, 𝑦⟩ ∈ 𝑣))
98anim1d 613 . . . . . . . . . . 11 (𝑤𝑣 → ((⟨𝑥, 𝑦⟩ ∈ 𝑤 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑣) → (⟨𝑥, 𝑦⟩ ∈ 𝑣 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑣)))
10 dffun4 6336 . . . . . . . . . . . . . 14 (Fun 𝑣 ↔ (Rel 𝑣 ∧ ∀𝑥𝑦𝑧((⟨𝑥, 𝑦⟩ ∈ 𝑣 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑣) → 𝑦 = 𝑧)))
1110simprbi 500 . . . . . . . . . . . . 13 (Fun 𝑣 → ∀𝑥𝑦𝑧((⟨𝑥, 𝑦⟩ ∈ 𝑣 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑣) → 𝑦 = 𝑧))
121119.21bbi 2187 . . . . . . . . . . . 12 (Fun 𝑣 → ∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝑣 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑣) → 𝑦 = 𝑧))
131219.21bi 2186 . . . . . . . . . . 11 (Fun 𝑣 → ((⟨𝑥, 𝑦⟩ ∈ 𝑣 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑣) → 𝑦 = 𝑧))
149, 13syl9r 78 . . . . . . . . . 10 (Fun 𝑣 → (𝑤𝑣 → ((⟨𝑥, 𝑦⟩ ∈ 𝑤 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑣) → 𝑦 = 𝑧)))
1514adantl 485 . . . . . . . . 9 ((Fun 𝑤 ∧ Fun 𝑣) → (𝑤𝑣 → ((⟨𝑥, 𝑦⟩ ∈ 𝑤 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑣) → 𝑦 = 𝑧)))
16 ssel 3908 . . . . . . . . . . . 12 (𝑣𝑤 → (⟨𝑥, 𝑧⟩ ∈ 𝑣 → ⟨𝑥, 𝑧⟩ ∈ 𝑤))
1716anim2d 614 . . . . . . . . . . 11 (𝑣𝑤 → ((⟨𝑥, 𝑦⟩ ∈ 𝑤 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑣) → (⟨𝑥, 𝑦⟩ ∈ 𝑤 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑤)))
18 dffun4 6336 . . . . . . . . . . . . . 14 (Fun 𝑤 ↔ (Rel 𝑤 ∧ ∀𝑥𝑦𝑧((⟨𝑥, 𝑦⟩ ∈ 𝑤 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑤) → 𝑦 = 𝑧)))
1918simprbi 500 . . . . . . . . . . . . 13 (Fun 𝑤 → ∀𝑥𝑦𝑧((⟨𝑥, 𝑦⟩ ∈ 𝑤 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑤) → 𝑦 = 𝑧))
201919.21bbi 2187 . . . . . . . . . . . 12 (Fun 𝑤 → ∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝑤 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑤) → 𝑦 = 𝑧))
212019.21bi 2186 . . . . . . . . . . 11 (Fun 𝑤 → ((⟨𝑥, 𝑦⟩ ∈ 𝑤 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑤) → 𝑦 = 𝑧))
2217, 21syl9r 78 . . . . . . . . . 10 (Fun 𝑤 → (𝑣𝑤 → ((⟨𝑥, 𝑦⟩ ∈ 𝑤 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑣) → 𝑦 = 𝑧)))
2322adantr 484 . . . . . . . . 9 ((Fun 𝑤 ∧ Fun 𝑣) → (𝑣𝑤 → ((⟨𝑥, 𝑦⟩ ∈ 𝑤 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑣) → 𝑦 = 𝑧)))
2415, 23jaod 856 . . . . . . . 8 ((Fun 𝑤 ∧ Fun 𝑣) → ((𝑤𝑣𝑣𝑤) → ((⟨𝑥, 𝑦⟩ ∈ 𝑤 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑣) → 𝑦 = 𝑧)))
2524imp 410 . . . . . . 7 (((Fun 𝑤 ∧ Fun 𝑣) ∧ (𝑤𝑣𝑣𝑤)) → ((⟨𝑥, 𝑦⟩ ∈ 𝑤 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑣) → 𝑦 = 𝑧))
26252ralimi 3129 . . . . . 6 (∀𝑤𝐴𝑣𝐴 ((Fun 𝑤 ∧ Fun 𝑣) ∧ (𝑤𝑣𝑣𝑤)) → ∀𝑤𝐴𝑣𝐴 ((⟨𝑥, 𝑦⟩ ∈ 𝑤 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑣) → 𝑦 = 𝑧))
27 funeq 6344 . . . . . . . . . 10 (𝑓 = 𝑤 → (Fun 𝑓 ↔ Fun 𝑤))
28 sseq1 3940 . . . . . . . . . . 11 (𝑓 = 𝑤 → (𝑓𝑔𝑤𝑔))
29 sseq2 3941 . . . . . . . . . . 11 (𝑓 = 𝑤 → (𝑔𝑓𝑔𝑤))
3028, 29orbi12d 916 . . . . . . . . . 10 (𝑓 = 𝑤 → ((𝑓𝑔𝑔𝑓) ↔ (𝑤𝑔𝑔𝑤)))
3127, 30anbi12d 633 . . . . . . . . 9 (𝑓 = 𝑤 → ((Fun 𝑓 ∧ (𝑓𝑔𝑔𝑓)) ↔ (Fun 𝑤 ∧ (𝑤𝑔𝑔𝑤))))
32 sseq2 3941 . . . . . . . . . . 11 (𝑔 = 𝑣 → (𝑤𝑔𝑤𝑣))
33 sseq1 3940 . . . . . . . . . . 11 (𝑔 = 𝑣 → (𝑔𝑤𝑣𝑤))
3432, 33orbi12d 916 . . . . . . . . . 10 (𝑔 = 𝑣 → ((𝑤𝑔𝑔𝑤) ↔ (𝑤𝑣𝑣𝑤)))
3534anbi2d 631 . . . . . . . . 9 (𝑔 = 𝑣 → ((Fun 𝑤 ∧ (𝑤𝑔𝑔𝑤)) ↔ (Fun 𝑤 ∧ (𝑤𝑣𝑣𝑤))))
3631, 35cbvral2vw 3408 . . . . . . . 8 (∀𝑓𝐴𝑔𝐴 (Fun 𝑓 ∧ (𝑓𝑔𝑔𝑓)) ↔ ∀𝑤𝐴𝑣𝐴 (Fun 𝑤 ∧ (𝑤𝑣𝑣𝑤)))
37 ralcom 3307 . . . . . . . . 9 (∀𝑓𝐴𝑔𝐴 (Fun 𝑓 ∧ (𝑓𝑔𝑔𝑓)) ↔ ∀𝑔𝐴𝑓𝐴 (Fun 𝑓 ∧ (𝑓𝑔𝑔𝑓)))
38 orcom 867 . . . . . . . . . . . 12 ((𝑓𝑔𝑔𝑓) ↔ (𝑔𝑓𝑓𝑔))
39 sseq1 3940 . . . . . . . . . . . . 13 (𝑔 = 𝑤 → (𝑔𝑓𝑤𝑓))
40 sseq2 3941 . . . . . . . . . . . . 13 (𝑔 = 𝑤 → (𝑓𝑔𝑓𝑤))
4139, 40orbi12d 916 . . . . . . . . . . . 12 (𝑔 = 𝑤 → ((𝑔𝑓𝑓𝑔) ↔ (𝑤𝑓𝑓𝑤)))
4238, 41syl5bb 286 . . . . . . . . . . 11 (𝑔 = 𝑤 → ((𝑓𝑔𝑔𝑓) ↔ (𝑤𝑓𝑓𝑤)))
4342anbi2d 631 . . . . . . . . . 10 (𝑔 = 𝑤 → ((Fun 𝑓 ∧ (𝑓𝑔𝑔𝑓)) ↔ (Fun 𝑓 ∧ (𝑤𝑓𝑓𝑤))))
44 funeq 6344 . . . . . . . . . . 11 (𝑓 = 𝑣 → (Fun 𝑓 ↔ Fun 𝑣))
45 sseq2 3941 . . . . . . . . . . . 12 (𝑓 = 𝑣 → (𝑤𝑓𝑤𝑣))
46 sseq1 3940 . . . . . . . . . . . 12 (𝑓 = 𝑣 → (𝑓𝑤𝑣𝑤))
4745, 46orbi12d 916 . . . . . . . . . . 11 (𝑓 = 𝑣 → ((𝑤𝑓𝑓𝑤) ↔ (𝑤𝑣𝑣𝑤)))
4844, 47anbi12d 633 . . . . . . . . . 10 (𝑓 = 𝑣 → ((Fun 𝑓 ∧ (𝑤𝑓𝑓𝑤)) ↔ (Fun 𝑣 ∧ (𝑤𝑣𝑣𝑤))))
4943, 48cbvral2vw 3408 . . . . . . . . 9 (∀𝑔𝐴𝑓𝐴 (Fun 𝑓 ∧ (𝑓𝑔𝑔𝑓)) ↔ ∀𝑤𝐴𝑣𝐴 (Fun 𝑣 ∧ (𝑤𝑣𝑣𝑤)))
5037, 49bitri 278 . . . . . . . 8 (∀𝑓𝐴𝑔𝐴 (Fun 𝑓 ∧ (𝑓𝑔𝑔𝑓)) ↔ ∀𝑤𝐴𝑣𝐴 (Fun 𝑣 ∧ (𝑤𝑣𝑣𝑤)))
5136, 50anbi12i 629 . . . . . . 7 ((∀𝑓𝐴𝑔𝐴 (Fun 𝑓 ∧ (𝑓𝑔𝑔𝑓)) ∧ ∀𝑓𝐴𝑔𝐴 (Fun 𝑓 ∧ (𝑓𝑔𝑔𝑓))) ↔ (∀𝑤𝐴𝑣𝐴 (Fun 𝑤 ∧ (𝑤𝑣𝑣𝑤)) ∧ ∀𝑤𝐴𝑣𝐴 (Fun 𝑣 ∧ (𝑤𝑣𝑣𝑤))))
52 anidm 568 . . . . . . 7 ((∀𝑓𝐴𝑔𝐴 (Fun 𝑓 ∧ (𝑓𝑔𝑔𝑓)) ∧ ∀𝑓𝐴𝑔𝐴 (Fun 𝑓 ∧ (𝑓𝑔𝑔𝑓))) ↔ ∀𝑓𝐴𝑔𝐴 (Fun 𝑓 ∧ (𝑓𝑔𝑔𝑓)))
53 anandir 676 . . . . . . . . 9 (((Fun 𝑤 ∧ Fun 𝑣) ∧ (𝑤𝑣𝑣𝑤)) ↔ ((Fun 𝑤 ∧ (𝑤𝑣𝑣𝑤)) ∧ (Fun 𝑣 ∧ (𝑤𝑣𝑣𝑤))))
54532ralbii 3134 . . . . . . . 8 (∀𝑤𝐴𝑣𝐴 ((Fun 𝑤 ∧ Fun 𝑣) ∧ (𝑤𝑣𝑣𝑤)) ↔ ∀𝑤𝐴𝑣𝐴 ((Fun 𝑤 ∧ (𝑤𝑣𝑣𝑤)) ∧ (Fun 𝑣 ∧ (𝑤𝑣𝑣𝑤))))
55 r19.26-2 3138 . . . . . . . 8 (∀𝑤𝐴𝑣𝐴 ((Fun 𝑤 ∧ (𝑤𝑣𝑣𝑤)) ∧ (Fun 𝑣 ∧ (𝑤𝑣𝑣𝑤))) ↔ (∀𝑤𝐴𝑣𝐴 (Fun 𝑤 ∧ (𝑤𝑣𝑣𝑤)) ∧ ∀𝑤𝐴𝑣𝐴 (Fun 𝑣 ∧ (𝑤𝑣𝑣𝑤))))
5654, 55bitr2i 279 . . . . . . 7 ((∀𝑤𝐴𝑣𝐴 (Fun 𝑤 ∧ (𝑤𝑣𝑣𝑤)) ∧ ∀𝑤𝐴𝑣𝐴 (Fun 𝑣 ∧ (𝑤𝑣𝑣𝑤))) ↔ ∀𝑤𝐴𝑣𝐴 ((Fun 𝑤 ∧ Fun 𝑣) ∧ (𝑤𝑣𝑣𝑤)))
5751, 52, 563bitr3i 304 . . . . . 6 (∀𝑓𝐴𝑔𝐴 (Fun 𝑓 ∧ (𝑓𝑔𝑔𝑓)) ↔ ∀𝑤𝐴𝑣𝐴 ((Fun 𝑤 ∧ Fun 𝑣) ∧ (𝑤𝑣𝑣𝑤)))
58 eluni 4803 . . . . . . . . . 10 (⟨𝑥, 𝑦⟩ ∈ 𝐴 ↔ ∃𝑤(⟨𝑥, 𝑦⟩ ∈ 𝑤𝑤𝐴))
59 eluni 4803 . . . . . . . . . 10 (⟨𝑥, 𝑧⟩ ∈ 𝐴 ↔ ∃𝑣(⟨𝑥, 𝑧⟩ ∈ 𝑣𝑣𝐴))
6058, 59anbi12i 629 . . . . . . . . 9 ((⟨𝑥, 𝑦⟩ ∈ 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐴) ↔ (∃𝑤(⟨𝑥, 𝑦⟩ ∈ 𝑤𝑤𝐴) ∧ ∃𝑣(⟨𝑥, 𝑧⟩ ∈ 𝑣𝑣𝐴)))
61 exdistrv 1956 . . . . . . . . 9 (∃𝑤𝑣((⟨𝑥, 𝑦⟩ ∈ 𝑤𝑤𝐴) ∧ (⟨𝑥, 𝑧⟩ ∈ 𝑣𝑣𝐴)) ↔ (∃𝑤(⟨𝑥, 𝑦⟩ ∈ 𝑤𝑤𝐴) ∧ ∃𝑣(⟨𝑥, 𝑧⟩ ∈ 𝑣𝑣𝐴)))
62 an4 655 . . . . . . . . . . 11 (((⟨𝑥, 𝑦⟩ ∈ 𝑤𝑤𝐴) ∧ (⟨𝑥, 𝑧⟩ ∈ 𝑣𝑣𝐴)) ↔ ((⟨𝑥, 𝑦⟩ ∈ 𝑤 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑣) ∧ (𝑤𝐴𝑣𝐴)))
6362biancomi 466 . . . . . . . . . 10 (((⟨𝑥, 𝑦⟩ ∈ 𝑤𝑤𝐴) ∧ (⟨𝑥, 𝑧⟩ ∈ 𝑣𝑣𝐴)) ↔ ((𝑤𝐴𝑣𝐴) ∧ (⟨𝑥, 𝑦⟩ ∈ 𝑤 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑣)))
64632exbii 1850 . . . . . . . . 9 (∃𝑤𝑣((⟨𝑥, 𝑦⟩ ∈ 𝑤𝑤𝐴) ∧ (⟨𝑥, 𝑧⟩ ∈ 𝑣𝑣𝐴)) ↔ ∃𝑤𝑣((𝑤𝐴𝑣𝐴) ∧ (⟨𝑥, 𝑦⟩ ∈ 𝑤 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑣)))
6560, 61, 643bitr2i 302 . . . . . . . 8 ((⟨𝑥, 𝑦⟩ ∈ 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐴) ↔ ∃𝑤𝑣((𝑤𝐴𝑣𝐴) ∧ (⟨𝑥, 𝑦⟩ ∈ 𝑤 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑣)))
6665imbi1i 353 . . . . . . 7 (((⟨𝑥, 𝑦⟩ ∈ 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐴) → 𝑦 = 𝑧) ↔ (∃𝑤𝑣((𝑤𝐴𝑣𝐴) ∧ (⟨𝑥, 𝑦⟩ ∈ 𝑤 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑣)) → 𝑦 = 𝑧))
67 19.23v 1943 . . . . . . 7 (∀𝑤(∃𝑣((𝑤𝐴𝑣𝐴) ∧ (⟨𝑥, 𝑦⟩ ∈ 𝑤 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑣)) → 𝑦 = 𝑧) ↔ (∃𝑤𝑣((𝑤𝐴𝑣𝐴) ∧ (⟨𝑥, 𝑦⟩ ∈ 𝑤 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑣)) → 𝑦 = 𝑧))
68 r2al 3166 . . . . . . . 8 (∀𝑤𝐴𝑣𝐴 ((⟨𝑥, 𝑦⟩ ∈ 𝑤 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑣) → 𝑦 = 𝑧) ↔ ∀𝑤𝑣((𝑤𝐴𝑣𝐴) → ((⟨𝑥, 𝑦⟩ ∈ 𝑤 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑣) → 𝑦 = 𝑧)))
69 impexp 454 . . . . . . . . 9 ((((𝑤𝐴𝑣𝐴) ∧ (⟨𝑥, 𝑦⟩ ∈ 𝑤 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑣)) → 𝑦 = 𝑧) ↔ ((𝑤𝐴𝑣𝐴) → ((⟨𝑥, 𝑦⟩ ∈ 𝑤 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑣) → 𝑦 = 𝑧)))
70692albii 1822 . . . . . . . 8 (∀𝑤𝑣(((𝑤𝐴𝑣𝐴) ∧ (⟨𝑥, 𝑦⟩ ∈ 𝑤 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑣)) → 𝑦 = 𝑧) ↔ ∀𝑤𝑣((𝑤𝐴𝑣𝐴) → ((⟨𝑥, 𝑦⟩ ∈ 𝑤 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑣) → 𝑦 = 𝑧)))
71 19.23v 1943 . . . . . . . . 9 (∀𝑣(((𝑤𝐴𝑣𝐴) ∧ (⟨𝑥, 𝑦⟩ ∈ 𝑤 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑣)) → 𝑦 = 𝑧) ↔ (∃𝑣((𝑤𝐴𝑣𝐴) ∧ (⟨𝑥, 𝑦⟩ ∈ 𝑤 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑣)) → 𝑦 = 𝑧))
7271albii 1821 . . . . . . . 8 (∀𝑤𝑣(((𝑤𝐴𝑣𝐴) ∧ (⟨𝑥, 𝑦⟩ ∈ 𝑤 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑣)) → 𝑦 = 𝑧) ↔ ∀𝑤(∃𝑣((𝑤𝐴𝑣𝐴) ∧ (⟨𝑥, 𝑦⟩ ∈ 𝑤 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑣)) → 𝑦 = 𝑧))
7368, 70, 723bitr2ri 303 . . . . . . 7 (∀𝑤(∃𝑣((𝑤𝐴𝑣𝐴) ∧ (⟨𝑥, 𝑦⟩ ∈ 𝑤 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑣)) → 𝑦 = 𝑧) ↔ ∀𝑤𝐴𝑣𝐴 ((⟨𝑥, 𝑦⟩ ∈ 𝑤 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑣) → 𝑦 = 𝑧))
7466, 67, 733bitr2i 302 . . . . . 6 (((⟨𝑥, 𝑦⟩ ∈ 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐴) → 𝑦 = 𝑧) ↔ ∀𝑤𝐴𝑣𝐴 ((⟨𝑥, 𝑦⟩ ∈ 𝑤 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑣) → 𝑦 = 𝑧))
7526, 57, 743imtr4i 295 . . . . 5 (∀𝑓𝐴𝑔𝐴 (Fun 𝑓 ∧ (𝑓𝑔𝑔𝑓)) → ((⟨𝑥, 𝑦⟩ ∈ 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐴) → 𝑦 = 𝑧))
7675alrimiv 1928 . . . 4 (∀𝑓𝐴𝑔𝐴 (Fun 𝑓 ∧ (𝑓𝑔𝑔𝑓)) → ∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐴) → 𝑦 = 𝑧))
7776alrimivv 1929 . . 3 (∀𝑓𝐴𝑔𝐴 (Fun 𝑓 ∧ (𝑓𝑔𝑔𝑓)) → ∀𝑥𝑦𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐴) → 𝑦 = 𝑧))
787, 77syl 17 . 2 (∀𝑓𝐴 (Fun 𝑓 ∧ ∀𝑔𝐴 (𝑓𝑔𝑔𝑓)) → ∀𝑥𝑦𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐴) → 𝑦 = 𝑧))
79 dffun4 6336 . 2 (Fun 𝐴 ↔ (Rel 𝐴 ∧ ∀𝑥𝑦𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐴) → 𝑦 = 𝑧)))
805, 78, 79sylanbrc 586 1 (∀𝑓𝐴 (Fun 𝑓 ∧ ∀𝑔𝐴 (𝑓𝑔𝑔𝑓)) → Fun 𝐴)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399   ∨ wo 844  ∀wal 1536  ∃wex 1781   ∈ wcel 2111  ∀wral 3106   ⊆ wss 3881  ⟨cop 4531  ∪ cuni 4800  Rel wrel 5524  Fun wfun 6318 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pr 5295 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ral 3111  df-rex 3112  df-v 3443  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-if 4426  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-iun 4883  df-br 5031  df-opab 5093  df-id 5425  df-rel 5526  df-cnv 5527  df-co 5528  df-fun 6326 This theorem is referenced by:  funcnvuni  7620  fun11uni  7621  fiun  7628  axdc3lem2  9864
 Copyright terms: Public domain W3C validator