ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  fununi Structured version   GIF version

Theorem fununi 4910
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 (f A (Fun f g A (fg gf)) → Fun A)
Distinct variable group:   f,g,A

Proof of Theorem fununi
Dummy variables x y z w v are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 funrel 4862 . . . . 5 (Fun f → Rel f)
21adantr 261 . . . 4 ((Fun f g A (fg gf)) → Rel f)
32ralimi 2378 . . 3 (f A (Fun f g A (fg gf)) → f A Rel f)
4 reluni 4403 . . 3 (Rel Af A Rel f)
53, 4sylibr 137 . 2 (f A (Fun f g A (fg gf)) → Rel A)
6 r19.28av 2443 . . . 4 ((Fun f g A (fg gf)) → g A (Fun f (fg gf)))
76ralimi 2378 . . 3 (f A (Fun f g A (fg gf)) → f A g A (Fun f (fg gf)))
8 ssel 2933 . . . . . . . . . . . . 13 (wv → (⟨x, y w → ⟨x, y v))
98anim1d 319 . . . . . . . . . . . 12 (wv → ((⟨x, y w x, z v) → (⟨x, y v x, z v)))
10 dffun4 4856 . . . . . . . . . . . . . . 15 (Fun v ↔ (Rel v xyz((⟨x, y v x, z v) → y = z)))
1110simprbi 260 . . . . . . . . . . . . . 14 (Fun vxyz((⟨x, y v x, z v) → y = z))
121119.21bbi 1448 . . . . . . . . . . . . 13 (Fun vz((⟨x, y v x, z v) → y = z))
131219.21bi 1447 . . . . . . . . . . . 12 (Fun v → ((⟨x, y v x, z v) → y = z))
149, 13syl9r 67 . . . . . . . . . . 11 (Fun v → (wv → ((⟨x, y w x, z v) → y = z)))
1514adantl 262 . . . . . . . . . 10 ((Fun w Fun v) → (wv → ((⟨x, y w x, z v) → y = z)))
16 ssel 2933 . . . . . . . . . . . . 13 (vw → (⟨x, z v → ⟨x, z w))
1716anim2d 320 . . . . . . . . . . . 12 (vw → ((⟨x, y w x, z v) → (⟨x, y w x, z w)))
18 dffun4 4856 . . . . . . . . . . . . . . 15 (Fun w ↔ (Rel w xyz((⟨x, y w x, z w) → y = z)))
1918simprbi 260 . . . . . . . . . . . . . 14 (Fun wxyz((⟨x, y w x, z w) → y = z))
201919.21bbi 1448 . . . . . . . . . . . . 13 (Fun wz((⟨x, y w x, z w) → y = z))
212019.21bi 1447 . . . . . . . . . . . 12 (Fun w → ((⟨x, y w x, z w) → y = z))
2217, 21syl9r 67 . . . . . . . . . . 11 (Fun w → (vw → ((⟨x, y w x, z v) → y = z)))
2322adantr 261 . . . . . . . . . 10 ((Fun w Fun v) → (vw → ((⟨x, y w x, z v) → y = z)))
2415, 23jaod 636 . . . . . . . . 9 ((Fun w Fun v) → ((wv vw) → ((⟨x, y w x, z v) → y = z)))
2524imp 115 . . . . . . . 8 (((Fun w Fun v) (wv vw)) → ((⟨x, y w x, z v) → y = z))
2625ralimi 2378 . . . . . . 7 (v A ((Fun w Fun v) (wv vw)) → v A ((⟨x, y w x, z v) → y = z))
2726ralimi 2378 . . . . . 6 (w A v A ((Fun w Fun v) (wv vw)) → w A v A ((⟨x, y w x, z v) → y = z))
28 funeq 4864 . . . . . . . . . 10 (f = w → (Fun f ↔ Fun w))
29 sseq1 2960 . . . . . . . . . . 11 (f = w → (fgwg))
30 sseq2 2961 . . . . . . . . . . 11 (f = w → (gfgw))
3129, 30orbi12d 706 . . . . . . . . . 10 (f = w → ((fg gf) ↔ (wg gw)))
3228, 31anbi12d 442 . . . . . . . . 9 (f = w → ((Fun f (fg gf)) ↔ (Fun w (wg gw))))
33 sseq2 2961 . . . . . . . . . . 11 (g = v → (wgwv))
34 sseq1 2960 . . . . . . . . . . 11 (g = v → (gwvw))
3533, 34orbi12d 706 . . . . . . . . . 10 (g = v → ((wg gw) ↔ (wv vw)))
3635anbi2d 437 . . . . . . . . 9 (g = v → ((Fun w (wg gw)) ↔ (Fun w (wv vw))))
3732, 36cbvral2v 2535 . . . . . . . 8 (f A g A (Fun f (fg gf)) ↔ w A v A (Fun w (wv vw)))
38 ralcom 2467 . . . . . . . . 9 (f A g A (Fun f (fg gf)) ↔ g A f A (Fun f (fg gf)))
39 orcom 646 . . . . . . . . . . . 12 ((fg gf) ↔ (gf fg))
40 sseq1 2960 . . . . . . . . . . . . 13 (g = w → (gfwf))
41 sseq2 2961 . . . . . . . . . . . . 13 (g = w → (fgfw))
4240, 41orbi12d 706 . . . . . . . . . . . 12 (g = w → ((gf fg) ↔ (wf fw)))
4339, 42syl5bb 181 . . . . . . . . . . 11 (g = w → ((fg gf) ↔ (wf fw)))
4443anbi2d 437 . . . . . . . . . 10 (g = w → ((Fun f (fg gf)) ↔ (Fun f (wf fw))))
45 funeq 4864 . . . . . . . . . . 11 (f = v → (Fun f ↔ Fun v))
46 sseq2 2961 . . . . . . . . . . . 12 (f = v → (wfwv))
47 sseq1 2960 . . . . . . . . . . . 12 (f = v → (fwvw))
4846, 47orbi12d 706 . . . . . . . . . . 11 (f = v → ((wf fw) ↔ (wv vw)))
4945, 48anbi12d 442 . . . . . . . . . 10 (f = v → ((Fun f (wf fw)) ↔ (Fun v (wv vw))))
5044, 49cbvral2v 2535 . . . . . . . . 9 (g A f A (Fun f (fg gf)) ↔ w A v A (Fun v (wv vw)))
5138, 50bitri 173 . . . . . . . 8 (f A g A (Fun f (fg gf)) ↔ w A v A (Fun v (wv vw)))
5237, 51anbi12i 433 . . . . . . 7 ((f A g A (Fun f (fg gf)) f A g A (Fun f (fg gf))) ↔ (w A v A (Fun w (wv vw)) w A v A (Fun v (wv vw))))
53 anidm 376 . . . . . . 7 ((f A g A (Fun f (fg gf)) f A g A (Fun f (fg gf))) ↔ f A g A (Fun f (fg gf)))
54 anandir 525 . . . . . . . . 9 (((Fun w Fun v) (wv vw)) ↔ ((Fun w (wv vw)) (Fun v (wv vw))))
55542ralbii 2326 . . . . . . . 8 (w A v A ((Fun w Fun v) (wv vw)) ↔ w A v A ((Fun w (wv vw)) (Fun v (wv vw))))
56 r19.26-2 2436 . . . . . . . 8 (w A v A ((Fun w (wv vw)) (Fun v (wv vw))) ↔ (w A v A (Fun w (wv vw)) w A v A (Fun v (wv vw))))
5755, 56bitr2i 174 . . . . . . 7 ((w A v A (Fun w (wv vw)) w A v A (Fun v (wv vw))) ↔ w A v A ((Fun w Fun v) (wv vw)))
5852, 53, 573bitr3i 199 . . . . . 6 (f A g A (Fun f (fg gf)) ↔ w A v A ((Fun w Fun v) (wv vw)))
59 eluni 3574 . . . . . . . . . 10 (⟨x, y Aw(⟨x, y w w A))
60 eluni 3574 . . . . . . . . . 10 (⟨x, z Av(⟨x, z v v A))
6159, 60anbi12i 433 . . . . . . . . 9 ((⟨x, y A x, z A) ↔ (w(⟨x, y w w A) v(⟨x, z v v A)))
62 eeanv 1804 . . . . . . . . 9 (wv((⟨x, y w w A) (⟨x, z v v A)) ↔ (w(⟨x, y w w A) v(⟨x, z v v A)))
63 an4 520 . . . . . . . . . . 11 (((⟨x, y w w A) (⟨x, z v v A)) ↔ ((⟨x, y w x, z v) (w A v A)))
64 ancom 253 . . . . . . . . . . 11 (((⟨x, y w x, z v) (w A v A)) ↔ ((w A v A) (⟨x, y w x, z v)))
6563, 64bitri 173 . . . . . . . . . 10 (((⟨x, y w w A) (⟨x, z v v A)) ↔ ((w A v A) (⟨x, y w x, z v)))
66652exbii 1494 . . . . . . . . 9 (wv((⟨x, y w w A) (⟨x, z v v A)) ↔ wv((w A v A) (⟨x, y w x, z v)))
6761, 62, 663bitr2i 197 . . . . . . . 8 ((⟨x, y A x, z A) ↔ wv((w A v A) (⟨x, y w x, z v)))
6867imbi1i 227 . . . . . . 7 (((⟨x, y A x, z A) → y = z) ↔ (wv((w A v A) (⟨x, y w x, z v)) → y = z))
69 19.23v 1760 . . . . . . 7 (w(v((w A v A) (⟨x, y w x, z v)) → y = z) ↔ (wv((w A v A) (⟨x, y w x, z v)) → y = z))
70 r2al 2337 . . . . . . . 8 (w A v A ((⟨x, y w x, z v) → y = z) ↔ wv((w A v A) → ((⟨x, y w x, z v) → y = z)))
71 impexp 250 . . . . . . . . 9 ((((w A v A) (⟨x, y w x, z v)) → y = z) ↔ ((w A v A) → ((⟨x, y w x, z v) → y = z)))
72712albii 1357 . . . . . . . 8 (wv(((w A v A) (⟨x, y w x, z v)) → y = z) ↔ wv((w A v A) → ((⟨x, y w x, z v) → y = z)))
73 19.23v 1760 . . . . . . . . 9 (v(((w A v A) (⟨x, y w x, z v)) → y = z) ↔ (v((w A v A) (⟨x, y w x, z v)) → y = z))
7473albii 1356 . . . . . . . 8 (wv(((w A v A) (⟨x, y w x, z v)) → y = z) ↔ w(v((w A v A) (⟨x, y w x, z v)) → y = z))
7570, 72, 743bitr2ri 198 . . . . . . 7 (w(v((w A v A) (⟨x, y w x, z v)) → y = z) ↔ w A v A ((⟨x, y w x, z v) → y = z))
7668, 69, 753bitr2i 197 . . . . . 6 (((⟨x, y A x, z A) → y = z) ↔ w A v A ((⟨x, y w x, z v) → y = z))
7727, 58, 763imtr4i 190 . . . . 5 (f A g A (Fun f (fg gf)) → ((⟨x, y A x, z A) → y = z))
7877alrimiv 1751 . . . 4 (f A g A (Fun f (fg gf)) → z((⟨x, y A x, z A) → y = z))
7978alrimivv 1752 . . 3 (f A g A (Fun f (fg gf)) → xyz((⟨x, y A x, z A) → y = z))
807, 79syl 14 . 2 (f A (Fun f g A (fg gf)) → xyz((⟨x, y A x, z A) → y = z))
81 dffun4 4856 . 2 (Fun A ↔ (Rel A xyz((⟨x, y A x, z A) → y = z)))
825, 80, 81sylanbrc 394 1 (f A (Fun f g A (fg gf)) → Fun A)
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97   wo 628  wal 1240  wex 1378   wcel 1390  wral 2300  wss 2911  cop 3370   cuni 3571  Rel wrel 4293  Fun wfun 4839
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bnd 1396  ax-4 1397  ax-14 1402  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019  ax-sep 3866  ax-pow 3918  ax-pr 3935
This theorem depends on definitions:  df-bi 110  df-3an 886  df-tru 1245  df-nf 1347  df-sb 1643  df-eu 1900  df-mo 1901  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-ral 2305  df-rex 2306  df-v 2553  df-un 2916  df-in 2918  df-ss 2925  df-pw 3353  df-sn 3373  df-pr 3374  df-op 3376  df-uni 3572  df-iun 3650  df-br 3756  df-opab 3810  df-id 4021  df-rel 4295  df-cnv 4296  df-co 4297  df-fun 4847
This theorem is referenced by:  funcnvuni  4911  fun11uni  4912
  Copyright terms: Public domain W3C validator