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-1→wf1 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