NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  fun11iun GIF version

Theorem fun11iun 5305
Description: The union of a chain (with respect to inclusion) of one-to-one functions is a one-to-one function. (Contributed by Mario Carneiro, 20-May-2013.) (Revised by Mario Carneiro, 24-Jun-2015.)
Hypotheses
Ref Expression
fun11iun.1 (x = yB = C)
fun11iun.2 B V
Assertion
Ref Expression
fun11iun (x A (B:D1-1S y A (B C C B)) → x A B:x A D1-1S)
Distinct variable groups:   x,A   y,A   y,B   x,C   x,S
Allowed substitution hints:   B(x)   C(y)   D(x,y)   S(y)

Proof of Theorem fun11iun
Dummy variables u v z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 vex 2862 . . . . . . . . . 10 u V
2 eqeq1 2359 . . . . . . . . . . 11 (z = u → (z = Bu = B))
32rexbidv 2635 . . . . . . . . . 10 (z = u → (x A z = Bx A u = B))
41, 3elab 2985 . . . . . . . . 9 (u {z x A z = B} ↔ x A u = B)
5 r19.29 2754 . . . . . . . . . 10 ((x A (B:D1-1S y A (B C C B)) x A u = B) → x A ((B:D1-1S y A (B C C B)) u = B))
6 nfv 1619 . . . . . . . . . . . 12 x(Fun u Fun u)
7 nfre1 2670 . . . . . . . . . . . . . 14 xx A z = B
87nfab 2493 . . . . . . . . . . . . 13 x{z x A z = B}
9 nfv 1619 . . . . . . . . . . . . 13 x(u v v u)
108, 9nfral 2667 . . . . . . . . . . . 12 xv {z x A z = B} (u v v u)
116, 10nfan 1824 . . . . . . . . . . 11 x((Fun u Fun u) v {z x A z = B} (u v v u))
12 f1eq1 5253 . . . . . . . . . . . . . . . 16 (u = B → (u:D1-1SB:D1-1S))
1312biimparc 473 . . . . . . . . . . . . . . 15 ((B:D1-1S u = B) → u:D1-1S)
14 f1fun 5260 . . . . . . . . . . . . . . . 16 (u:D1-1S → Fun u)
15 df-f1 4792 . . . . . . . . . . . . . . . . 17 (u:D1-1S ↔ (u:D–→S Fun u))
1615simprbi 450 . . . . . . . . . . . . . . . 16 (u:D1-1S → Fun u)
1714, 16jca 518 . . . . . . . . . . . . . . 15 (u:D1-1S → (Fun u Fun u))
1813, 17syl 15 . . . . . . . . . . . . . 14 ((B:D1-1S u = B) → (Fun u Fun u))
1918adantlr 695 . . . . . . . . . . . . 13 (((B:D1-1S y A (B C C B)) u = B) → (Fun u Fun u))
20 vex 2862 . . . . . . . . . . . . . . . . 17 v V
21 eqeq1 2359 . . . . . . . . . . . . . . . . . . 19 (z = v → (z = Bv = B))
2221rexbidv 2635 . . . . . . . . . . . . . . . . . 18 (z = v → (x A z = Bx A v = B))
23 fun11iun.1 . . . . . . . . . . . . . . . . . . . 20 (x = yB = C)
2423eqeq2d 2364 . . . . . . . . . . . . . . . . . . 19 (x = y → (v = Bv = C))
2524cbvrexv 2836 . . . . . . . . . . . . . . . . . 18 (x A v = By A v = C)
2622, 25syl6bb 252 . . . . . . . . . . . . . . . . 17 (z = v → (x A z = By A v = C))
2720, 26elab 2985 . . . . . . . . . . . . . . . 16 (v {z x A z = B} ↔ y A v = C)
28 r19.29 2754 . . . . . . . . . . . . . . . . . 18 ((y A (B C C B) y A v = C) → y A ((B C C B) v = C))
29 sseq12 3294 . . . . . . . . . . . . . . . . . . . . . . . 24 ((u = B v = C) → (u vB C))
3029ancoms 439 . . . . . . . . . . . . . . . . . . . . . . 23 ((v = C u = B) → (u vB C))
31 sseq12 3294 . . . . . . . . . . . . . . . . . . . . . . 23 ((v = C u = B) → (v uC B))
3230, 31orbi12d 690 . . . . . . . . . . . . . . . . . . . . . 22 ((v = C u = B) → ((u v v u) ↔ (B C C B)))
3332biimprcd 216 . . . . . . . . . . . . . . . . . . . . 21 ((B C C B) → ((v = C u = B) → (u v v u)))
3433expdimp 426 . . . . . . . . . . . . . . . . . . . 20 (((B C C B) v = C) → (u = B → (u v v u)))
3534rexlimivw 2734 . . . . . . . . . . . . . . . . . . 19 (y A ((B C C B) v = C) → (u = B → (u v v u)))
3635imp 418 . . . . . . . . . . . . . . . . . 18 ((y A ((B C C B) v = C) u = B) → (u v v u))
3728, 36sylan 457 . . . . . . . . . . . . . . . . 17 (((y A (B C C B) y A v = C) u = B) → (u v v u))
3837an32s 779 . . . . . . . . . . . . . . . 16 (((y A (B C C B) u = B) y A v = C) → (u v v u))
3927, 38sylan2b 461 . . . . . . . . . . . . . . 15 (((y A (B C C B) u = B) v {z x A z = B}) → (u v v u))
4039ralrimiva 2697 . . . . . . . . . . . . . 14 ((y A (B C C B) u = B) → v {z x A z = B} (u v v u))
4140adantll 694 . . . . . . . . . . . . 13 (((B:D1-1S y A (B C C B)) u = B) → v {z x A z = B} (u v v u))
4219, 41jca 518 . . . . . . . . . . . 12 (((B:D1-1S y A (B C C B)) u = B) → ((Fun u Fun u) v {z x A z = B} (u v v u)))
4342a1i 10 . . . . . . . . . . 11 (x A → (((B:D1-1S y A (B C C B)) u = B) → ((Fun u Fun u) v {z x A z = B} (u v v u))))
4411, 43rexlimi 2731 . . . . . . . . . 10 (x A ((B:D1-1S y A (B C C B)) u = B) → ((Fun u Fun u) v {z x A z = B} (u v v u)))
455, 44syl 15 . . . . . . . . 9 ((x A (B:D1-1S y A (B C C B)) x A u = B) → ((Fun u Fun u) v {z x A z = B} (u v v u)))
464, 45sylan2b 461 . . . . . . . 8 ((x A (B:D1-1S y A (B C C B)) u {z x A z = B}) → ((Fun u Fun u) v {z x A z = B} (u v v u)))
4746ralrimiva 2697 . . . . . . 7 (x A (B:D1-1S y A (B C C B)) → u {z x A z = B} ((Fun u Fun u) v {z x A z = B} (u v v u)))
48 fun11uni 5162 . . . . . . 7 (u {z x A z = B} ((Fun u Fun u) v {z x A z = B} (u v v u)) → (Fun {z x A z = B} Fun {z x A z = B}))
4947, 48syl 15 . . . . . 6 (x A (B:D1-1S y A (B C C B)) → (Fun {z x A z = B} Fun {z x A z = B}))
5049simpld 445 . . . . 5 (x A (B:D1-1S y A (B C C B)) → Fun {z x A z = B})
51 fun11iun.2 . . . . . . 7 B V
5251dfiun2 4001 . . . . . 6 x A B = {z x A z = B}
5352funeqi 5128 . . . . 5 (Fun x A B ↔ Fun {z x A z = B})
5450, 53sylibr 203 . . . 4 (x A (B:D1-1S y A (B C C B)) → Fun x A B)
55 nfra1 2664 . . . . . . 7 xx A (B:D1-1S y A (B C C B))
56 rsp 2674 . . . . . . . . 9 (x A (B:D1-1S y A (B C C B)) → (x A → (B:D1-1S y A (B C C B))))
5756imp 418 . . . . . . . 8 ((x A (B:D1-1S y A (B C C B)) x A) → (B:D1-1S y A (B C C B)))
58 eldm2 4899 . . . . . . . . . 10 (u dom Bvu, v B)
59 f1dm 5261 . . . . . . . . . . 11 (B:D1-1S → dom B = D)
6059eleq2d 2420 . . . . . . . . . 10 (B:D1-1S → (u dom Bu D))
6158, 60syl5bbr 250 . . . . . . . . 9 (B:D1-1S → (vu, v Bu D))
6261adantr 451 . . . . . . . 8 ((B:D1-1S y A (B C C B)) → (vu, v Bu D))
6357, 62syl 15 . . . . . . 7 ((x A (B:D1-1S y A (B C C B)) x A) → (vu, v Bu D))
6455, 63rexbida 2629 . . . . . 6 (x A (B:D1-1S y A (B C C B)) → (x A vu, v Bx A u D))
65 eliun 3973 . . . . . . . 8 (u, v x A Bx A u, v B)
6665exbii 1582 . . . . . . 7 (vu, v x A Bvx A u, v B)
67 eldm2 4899 . . . . . . 7 (u dom x A Bvu, v x A B)
68 rexcom4 2878 . . . . . . 7 (x A vu, v Bvx A u, v B)
6966, 67, 683bitr4i 268 . . . . . 6 (u dom x A Bx A vu, v B)
70 eliun 3973 . . . . . 6 (u x A Dx A u D)
7164, 69, 703bitr4g 279 . . . . 5 (x A (B:D1-1S y A (B C C B)) → (u dom x A Bu x A D))
7271eqrdv 2351 . . . 4 (x A (B:D1-1S y A (B C C B)) → dom x A B = x A D)
73 df-fn 4790 . . . 4 (x A B Fn x A D ↔ (Fun x A B dom x A B = x A D))
7454, 72, 73sylanbrc 645 . . 3 (x A (B:D1-1S y A (B C C B)) → x A B Fn x A D)
7565exbii 1582 . . . . . 6 (uu, v x A Bux A u, v B)
76 elrn2 4897 . . . . . 6 (v ran x A Buu, v x A B)
77 rexcom4 2878 . . . . . 6 (x A uu, v Bux A u, v B)
7875, 76, 773bitr4i 268 . . . . 5 (v ran x A Bx A uu, v B)
79 nfv 1619 . . . . . 6 x v S
80 elrn2 4897 . . . . . . . . 9 (v ran Buu, v B)
81 f1f 5258 . . . . . . . . . . 11 (B:D1-1SB:D–→S)
82 frn 5228 . . . . . . . . . . 11 (B:D–→S → ran B S)
8381, 82syl 15 . . . . . . . . . 10 (B:D1-1S → ran B S)
8483sseld 3272 . . . . . . . . 9 (B:D1-1S → (v ran Bv S))
8580, 84syl5bir 209 . . . . . . . 8 (B:D1-1S → (uu, v Bv S))
8685adantr 451 . . . . . . 7 ((B:D1-1S y A (B C C B)) → (uu, v Bv S))
8756, 86syl6 29 . . . . . 6 (x A (B:D1-1S y A (B C C B)) → (x A → (uu, v Bv S)))
8855, 79, 87rexlimd 2735 . . . . 5 (x A (B:D1-1S y A (B C C B)) → (x A uu, v Bv S))
8978, 88syl5bi 208 . . . 4 (x A (B:D1-1S y A (B C C B)) → (v ran x A Bv S))
9089ssrdv 3278 . . 3 (x A (B:D1-1S y A (B C C B)) → ran x A B S)
91 df-f 4791 . . 3 (x A B:x A D–→S ↔ (x A B Fn x A D ran x A B S))
9274, 90, 91sylanbrc 645 . 2 (x A (B:D1-1S y A (B C C B)) → x A B:x A D–→S)
9349simprd 449 . . 3 (x A (B:D1-1S y A (B C C B)) → Fun {z x A z = B})
9452cnveqi 4887 . . . 4 x A B = {z x A z = B}
9594funeqi 5128 . . 3 (Fun x A B ↔ Fun {z x A z = B})
9693, 95sylibr 203 . 2 (x A (B:D1-1S y A (B C C B)) → Fun x A B)
97 df-f1 4792 . 2 (x A B:x A D1-1S ↔ (x A B:x A D–→S Fun x A B))
9892, 96, 97sylanbrc 645 1 (x A (B:D1-1S y A (B C C B)) → x A B:x A D1-1S)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 176   wo 357   wa 358  wex 1541   = wceq 1642   wcel 1710  {cab 2339  wral 2614  wrex 2615  Vcvv 2859   wss 3257  cuni 3891  ciun 3969  cop 4561  ccnv 4771  dom cdm 4772  ran crn 4773  Fun wfun 4775   Fn wfn 4776  –→wf 4777  1-1wf1 4778
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-13 1712  ax-14 1714  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334  ax-nin 4078  ax-xp 4079  ax-cnv 4080  ax-1c 4081  ax-sset 4082  ax-si 4083  ax-ins2 4084  ax-ins3 4085  ax-typlower 4086  ax-sn 4087
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-nan 1288  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-eu 2208  df-mo 2209  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2478  df-ne 2518  df-ral 2619  df-rex 2620  df-reu 2621  df-rmo 2622  df-rab 2623  df-v 2861  df-sbc 3047  df-nin 3211  df-compl 3212  df-in 3213  df-un 3214  df-dif 3215  df-symdif 3216  df-ss 3259  df-pss 3261  df-nul 3551  df-if 3663  df-pw 3724  df-sn 3741  df-pr 3742  df-uni 3892  df-int 3927  df-iun 3971  df-opk 4058  df-1c 4136  df-pw1 4137  df-uni1 4138  df-xpk 4185  df-cnvk 4186  df-ins2k 4187  df-ins3k 4188  df-imak 4189  df-cok 4190  df-p6 4191  df-sik 4192  df-ssetk 4193  df-imagek 4194  df-idk 4195  df-iota 4339  df-0c 4377  df-addc 4378  df-nnc 4379  df-fin 4380  df-lefin 4440  df-ltfin 4441  df-ncfin 4442  df-tfin 4443  df-evenfin 4444  df-oddfin 4445  df-sfin 4446  df-spfin 4447  df-phi 4565  df-op 4566  df-proj1 4567  df-proj2 4568  df-opab 4623  df-br 4640  df-swap 4724  df-co 4726  df-ima 4727  df-id 4767  df-cnv 4785  df-rn 4786  df-dm 4787  df-fun 4789  df-fn 4790  df-f 4791  df-f1 4792
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator