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

Theorem fun11iun 5068
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 = 𝐶)
fun11iun.2 B V
Assertion
Ref Expression
fun11iun (x A (B:𝐷1-1𝑆 y A (B𝐶 𝐶B)) → x A B: x A 𝐷1-1𝑆)
Distinct variable groups:   x,A   y,A   y,B   x,𝐶   x,𝑆
Allowed substitution hints:   B(x)   𝐶(y)   𝐷(x,y)   𝑆(y)

Proof of Theorem fun11iun
Dummy variables u v z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 vex 2534 . . . . . . . . . 10 u V
2 eqeq1 2024 . . . . . . . . . . 11 (z = u → (z = Bu = B))
32rexbidv 2301 . . . . . . . . . 10 (z = u → (x A z = Bx A u = B))
41, 3elab 2660 . . . . . . . . 9 (u {zx A z = B} ↔ x A u = B)
5 r19.29 2424 . . . . . . . . . 10 ((x A (B:𝐷1-1𝑆 y A (B𝐶 𝐶B)) x A u = B) → x A ((B:𝐷1-1𝑆 y A (B𝐶 𝐶B)) u = B))
6 nfv 1398 . . . . . . . . . . . 12 x(Fun u Fun u)
7 nfre1 2339 . . . . . . . . . . . . . 14 xx A z = B
87nfab 2160 . . . . . . . . . . . . 13 x{zx A z = B}
9 nfv 1398 . . . . . . . . . . . . 13 x(uv vu)
108, 9nfralxy 2334 . . . . . . . . . . . 12 xv {zx A z = B} (uv vu)
116, 10nfan 1435 . . . . . . . . . . 11 x((Fun u Fun u) v {zx A z = B} (uv vu))
12 f1eq1 5008 . . . . . . . . . . . . . . . 16 (u = B → (u:𝐷1-1𝑆B:𝐷1-1𝑆))
1312biimparc 283 . . . . . . . . . . . . . . 15 ((B:𝐷1-1𝑆 u = B) → u:𝐷1-1𝑆)
14 df-f1 4830 . . . . . . . . . . . . . . . 16 (u:𝐷1-1𝑆 ↔ (u:𝐷𝑆 Fun u))
15 ffun 4970 . . . . . . . . . . . . . . . . 17 (u:𝐷𝑆 → Fun u)
1615anim1i 323 . . . . . . . . . . . . . . . 16 ((u:𝐷𝑆 Fun u) → (Fun u Fun u))
1714, 16sylbi 114 . . . . . . . . . . . . . . 15 (u:𝐷1-1𝑆 → (Fun u Fun u))
1813, 17syl 14 . . . . . . . . . . . . . 14 ((B:𝐷1-1𝑆 u = B) → (Fun u Fun u))
1918adantlr 449 . . . . . . . . . . . . 13 (((B:𝐷1-1𝑆 y A (B𝐶 𝐶B)) u = B) → (Fun u Fun u))
20 vex 2534 . . . . . . . . . . . . . . . 16 v V
21 eqeq1 2024 . . . . . . . . . . . . . . . . 17 (z = v → (z = Bv = B))
2221rexbidv 2301 . . . . . . . . . . . . . . . 16 (z = v → (x A z = Bx A v = B))
2320, 22elab 2660 . . . . . . . . . . . . . . 15 (v {zx A z = B} ↔ x A v = B)
24 fun11iun.1 . . . . . . . . . . . . . . . . . 18 (x = yB = 𝐶)
2524eqeq2d 2029 . . . . . . . . . . . . . . . . 17 (x = y → (v = Bv = 𝐶))
2625cbvrexv 2508 . . . . . . . . . . . . . . . 16 (x A v = By A v = 𝐶)
27 r19.29 2424 . . . . . . . . . . . . . . . . . . 19 ((y A (B𝐶 𝐶B) y A v = 𝐶) → y A ((B𝐶 𝐶B) v = 𝐶))
28 sseq12 2941 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((u = B v = 𝐶) → (uvB𝐶))
2928ancoms 255 . . . . . . . . . . . . . . . . . . . . . . . 24 ((v = 𝐶 u = B) → (uvB𝐶))
30 sseq12 2941 . . . . . . . . . . . . . . . . . . . . . . . 24 ((v = 𝐶 u = B) → (vu𝐶B))
3129, 30orbi12d 694 . . . . . . . . . . . . . . . . . . . . . . 23 ((v = 𝐶 u = B) → ((uv vu) ↔ (B𝐶 𝐶B)))
3231biimprcd 149 . . . . . . . . . . . . . . . . . . . . . 22 ((B𝐶 𝐶B) → ((v = 𝐶 u = B) → (uv vu)))
3332expdimp 246 . . . . . . . . . . . . . . . . . . . . 21 (((B𝐶 𝐶B) v = 𝐶) → (u = B → (uv vu)))
3433rexlimivw 2403 . . . . . . . . . . . . . . . . . . . 20 (y A ((B𝐶 𝐶B) v = 𝐶) → (u = B → (uv vu)))
3534imp 115 . . . . . . . . . . . . . . . . . . 19 ((y A ((B𝐶 𝐶B) v = 𝐶) u = B) → (uv vu))
3627, 35sylan 267 . . . . . . . . . . . . . . . . . 18 (((y A (B𝐶 𝐶B) y A v = 𝐶) u = B) → (uv vu))
3736an32s 490 . . . . . . . . . . . . . . . . 17 (((y A (B𝐶 𝐶B) u = B) y A v = 𝐶) → (uv vu))
3837adantlll 452 . . . . . . . . . . . . . . . 16 ((((B:𝐷1-1𝑆 y A (B𝐶 𝐶B)) u = B) y A v = 𝐶) → (uv vu))
3926, 38sylan2b 271 . . . . . . . . . . . . . . 15 ((((B:𝐷1-1𝑆 y A (B𝐶 𝐶B)) u = B) x A v = B) → (uv vu))
4023, 39sylan2b 271 . . . . . . . . . . . . . 14 ((((B:𝐷1-1𝑆 y A (B𝐶 𝐶B)) u = B) v {zx A z = B}) → (uv vu))
4140ralrimiva 2366 . . . . . . . . . . . . 13 (((B:𝐷1-1𝑆 y A (B𝐶 𝐶B)) u = B) → v {zx A z = B} (uv vu))
4219, 41jca 290 . . . . . . . . . . . 12 (((B:𝐷1-1𝑆 y A (B𝐶 𝐶B)) u = B) → ((Fun u Fun u) v {zx A z = B} (uv vu)))
4342a1i 9 . . . . . . . . . . 11 (x A → (((B:𝐷1-1𝑆 y A (B𝐶 𝐶B)) u = B) → ((Fun u Fun u) v {zx A z = B} (uv vu))))
4411, 43rexlimi 2400 . . . . . . . . . 10 (x A ((B:𝐷1-1𝑆 y A (B𝐶 𝐶B)) u = B) → ((Fun u Fun u) v {zx A z = B} (uv vu)))
455, 44syl 14 . . . . . . . . 9 ((x A (B:𝐷1-1𝑆 y A (B𝐶 𝐶B)) x A u = B) → ((Fun u Fun u) v {zx A z = B} (uv vu)))
464, 45sylan2b 271 . . . . . . . 8 ((x A (B:𝐷1-1𝑆 y A (B𝐶 𝐶B)) u {zx A z = B}) → ((Fun u Fun u) v {zx A z = B} (uv vu)))
4746ralrimiva 2366 . . . . . . 7 (x A (B:𝐷1-1𝑆 y A (B𝐶 𝐶B)) → u {zx A z = B} ((Fun u Fun u) v {zx A z = B} (uv vu)))
48 fun11uni 4891 . . . . . . 7 (u {zx A z = B} ((Fun u Fun u) v {zx A z = B} (uv vu)) → (Fun {zx A z = B} Fun {zx A z = B}))
4947, 48syl 14 . . . . . 6 (x A (B:𝐷1-1𝑆 y A (B𝐶 𝐶B)) → (Fun {zx A z = B} Fun {zx A z = B}))
5049simpld 105 . . . . 5 (x A (B:𝐷1-1𝑆 y A (B𝐶 𝐶B)) → Fun {zx A z = B})
51 fun11iun.2 . . . . . . 7 B V
5251dfiun2 3661 . . . . . 6 x A B = {zx A z = B}
5352funeqi 4844 . . . . 5 (Fun x A B ↔ Fun {zx A z = B})
5450, 53sylibr 137 . . . 4 (x A (B:𝐷1-1𝑆 y A (B𝐶 𝐶B)) → Fun x A B)
55 nfra1 2329 . . . . . . 7 xx A (B:𝐷1-1𝑆 y A (B𝐶 𝐶B))
56 rsp 2343 . . . . . . . . 9 (x A (B:𝐷1-1𝑆 y A (B𝐶 𝐶B)) → (x A → (B:𝐷1-1𝑆 y A (B𝐶 𝐶B))))
571eldm2 4456 . . . . . . . . . . 11 (u dom Bvu, v B)
58 f1dm 5017 . . . . . . . . . . . 12 (B:𝐷1-1𝑆 → dom B = 𝐷)
5958eleq2d 2085 . . . . . . . . . . 11 (B:𝐷1-1𝑆 → (u dom Bu 𝐷))
6057, 59syl5bbr 183 . . . . . . . . . 10 (B:𝐷1-1𝑆 → (vu, v Bu 𝐷))
6160adantr 261 . . . . . . . . 9 ((B:𝐷1-1𝑆 y A (B𝐶 𝐶B)) → (vu, v Bu 𝐷))
6256, 61syl6 29 . . . . . . . 8 (x A (B:𝐷1-1𝑆 y A (B𝐶 𝐶B)) → (x A → (vu, v Bu 𝐷)))
6362imp 115 . . . . . . 7 ((x A (B:𝐷1-1𝑆 y A (B𝐶 𝐶B)) x A) → (vu, v Bu 𝐷))
6455, 63rexbida 2295 . . . . . 6 (x A (B:𝐷1-1𝑆 y A (B𝐶 𝐶B)) → (x A vu, v Bx A u 𝐷))
65 eliun 3631 . . . . . . . 8 (⟨u, v x A Bx Au, v B)
6665exbii 1474 . . . . . . 7 (vu, v x A Bvx Au, v B)
671eldm2 4456 . . . . . . 7 (u dom x A Bvu, v x A B)
68 rexcom4 2550 . . . . . . 7 (x A vu, v Bvx Au, v B)
6966, 67, 683bitr4i 201 . . . . . 6 (u dom x A Bx A vu, v B)
70 eliun 3631 . . . . . 6 (u x A 𝐷x A u 𝐷)
7164, 69, 703bitr4g 212 . . . . 5 (x A (B:𝐷1-1𝑆 y A (B𝐶 𝐶B)) → (u dom x A Bu x A 𝐷))
7271eqrdv 2016 . . . 4 (x A (B:𝐷1-1𝑆 y A (B𝐶 𝐶B)) → dom x A B = x A 𝐷)
73 df-fn 4828 . . . 4 ( x A B Fn x A 𝐷 ↔ (Fun x A B dom x A B = x A 𝐷))
7454, 72, 73sylanbrc 396 . . 3 (x A (B:𝐷1-1𝑆 y A (B𝐶 𝐶B)) → x A B Fn x A 𝐷)
75 rniun 4657 . . . 4 ran x A B = x A ran B
76 f1f 5013 . . . . . . . 8 (B:𝐷1-1𝑆B:𝐷𝑆)
77 frn 4974 . . . . . . . 8 (B:𝐷𝑆 → ran B𝑆)
7876, 77syl 14 . . . . . . 7 (B:𝐷1-1𝑆 → ran B𝑆)
7978adantr 261 . . . . . 6 ((B:𝐷1-1𝑆 y A (B𝐶 𝐶B)) → ran B𝑆)
8079ralimi 2358 . . . . 5 (x A (B:𝐷1-1𝑆 y A (B𝐶 𝐶B)) → x A ran B𝑆)
81 iunss 3668 . . . . 5 ( x A ran B𝑆x A ran B𝑆)
8280, 81sylibr 137 . . . 4 (x A (B:𝐷1-1𝑆 y A (B𝐶 𝐶B)) → x A ran B𝑆)
8375, 82syl5eqss 2962 . . 3 (x A (B:𝐷1-1𝑆 y A (B𝐶 𝐶B)) → ran x A B𝑆)
84 df-f 4829 . . 3 ( x A B: x A 𝐷𝑆 ↔ ( x A B Fn x A 𝐷 ran x A B𝑆))
8574, 83, 84sylanbrc 396 . 2 (x A (B:𝐷1-1𝑆 y A (B𝐶 𝐶B)) → x A B: x A 𝐷𝑆)
8649simprd 107 . . 3 (x A (B:𝐷1-1𝑆 y A (B𝐶 𝐶B)) → Fun {zx A z = B})
8752cnveqi 4433 . . . 4 x A B = {zx A z = B}
8887funeqi 4844 . . 3 (Fun x A B ↔ Fun {zx A z = B})
8986, 88sylibr 137 . 2 (x A (B:𝐷1-1𝑆 y A (B𝐶 𝐶B)) → Fun x A B)
90 df-f1 4830 . 2 ( x A B: x A 𝐷1-1𝑆 ↔ ( x A B: x A 𝐷𝑆 Fun x A B))
9185, 89, 90sylanbrc 396 1 (x A (B:𝐷1-1𝑆 y A (B𝐶 𝐶B)) → x A B: x A 𝐷1-1𝑆)
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97  wb 98   wo 616   = wceq 1226  wex 1358   wcel 1370  {cab 2004  wral 2280  wrex 2281  Vcvv 2531  wss 2890  cop 3349   cuni 3550   ciun 3627  ccnv 4267  dom cdm 4268  ran crn 4269  Fun wfun 4819   Fn wfn 4820  wf 4821  1-1wf1 4822
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 617  ax-5 1312  ax-7 1313  ax-gen 1314  ax-ie1 1359  ax-ie2 1360  ax-8 1372  ax-10 1373  ax-11 1374  ax-i12 1375  ax-bnd 1376  ax-4 1377  ax-13 1381  ax-14 1382  ax-17 1396  ax-i9 1400  ax-ial 1405  ax-i5r 1406  ax-ext 2000  ax-sep 3845  ax-pow 3897  ax-pr 3914  ax-un 4116
This theorem depends on definitions:  df-bi 110  df-3an 873  df-tru 1229  df-nf 1326  df-sb 1624  df-eu 1881  df-mo 1882  df-clab 2005  df-cleq 2011  df-clel 2014  df-nfc 2145  df-ral 2285  df-rex 2286  df-v 2533  df-un 2895  df-in 2897  df-ss 2904  df-pw 3332  df-sn 3352  df-pr 3353  df-op 3355  df-uni 3551  df-iun 3629  df-br 3735  df-opab 3789  df-id 4000  df-xp 4274  df-rel 4275  df-cnv 4276  df-co 4277  df-dm 4278  df-rn 4279  df-fun 4827  df-fn 4828  df-f 4829  df-f1 4830
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator