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

Theorem fin1a2lem6 10266
Description: Lemma for fin1a2 10276. Establish that ω can be broken into two equipollent pieces. (Contributed by Stefan O'Rear, 7-Nov-2014.)
Hypotheses
Ref Expression
fin1a2lem.b 𝐸 = (𝑥 ∈ ω ↦ (2o ·o 𝑥))
fin1a2lem.aa 𝑆 = (𝑥 ∈ On ↦ suc 𝑥)
Assertion
Ref Expression
fin1a2lem6 (𝑆 ↾ ran 𝐸):ran 𝐸1-1-onto→(ω ∖ ran 𝐸)

Proof of Theorem fin1a2lem6
Dummy variables 𝑎 𝑏 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fin1a2lem.aa . . . 4 𝑆 = (𝑥 ∈ On ↦ suc 𝑥)
21fin1a2lem2 10262 . . 3 𝑆:On–1-1→On
3 fin1a2lem.b . . . . 5 𝐸 = (𝑥 ∈ ω ↦ (2o ·o 𝑥))
43fin1a2lem4 10264 . . . 4 𝐸:ω–1-1→ω
5 f1f 6725 . . . 4 (𝐸:ω–1-1→ω → 𝐸:ω⟶ω)
6 frn 6662 . . . . 5 (𝐸:ω⟶ω → ran 𝐸 ⊆ ω)
7 omsson 7788 . . . . 5 ω ⊆ On
86, 7sstrdi 3947 . . . 4 (𝐸:ω⟶ω → ran 𝐸 ⊆ On)
94, 5, 8mp2b 10 . . 3 ran 𝐸 ⊆ On
10 f1ores 6785 . . 3 ((𝑆:On–1-1→On ∧ ran 𝐸 ⊆ On) → (𝑆 ↾ ran 𝐸):ran 𝐸1-1-onto→(𝑆 “ ran 𝐸))
112, 9, 10mp2an 690 . 2 (𝑆 ↾ ran 𝐸):ran 𝐸1-1-onto→(𝑆 “ ran 𝐸)
129sseli 3931 . . . . . . . . 9 (𝑏 ∈ ran 𝐸𝑏 ∈ On)
131fin1a2lem1 10261 . . . . . . . . 9 (𝑏 ∈ On → (𝑆𝑏) = suc 𝑏)
1412, 13syl 17 . . . . . . . 8 (𝑏 ∈ ran 𝐸 → (𝑆𝑏) = suc 𝑏)
1514eqeq1d 2739 . . . . . . 7 (𝑏 ∈ ran 𝐸 → ((𝑆𝑏) = 𝑎 ↔ suc 𝑏 = 𝑎))
1615rexbiia 3092 . . . . . 6 (∃𝑏 ∈ ran 𝐸(𝑆𝑏) = 𝑎 ↔ ∃𝑏 ∈ ran 𝐸 suc 𝑏 = 𝑎)
174, 5, 6mp2b 10 . . . . . . . . . . . 12 ran 𝐸 ⊆ ω
1817sseli 3931 . . . . . . . . . . 11 (𝑏 ∈ ran 𝐸𝑏 ∈ ω)
19 peano2 7809 . . . . . . . . . . 11 (𝑏 ∈ ω → suc 𝑏 ∈ ω)
2018, 19syl 17 . . . . . . . . . 10 (𝑏 ∈ ran 𝐸 → suc 𝑏 ∈ ω)
213fin1a2lem5 10265 . . . . . . . . . . . 12 (𝑏 ∈ ω → (𝑏 ∈ ran 𝐸 ↔ ¬ suc 𝑏 ∈ ran 𝐸))
2221biimpd 228 . . . . . . . . . . 11 (𝑏 ∈ ω → (𝑏 ∈ ran 𝐸 → ¬ suc 𝑏 ∈ ran 𝐸))
2318, 22mpcom 38 . . . . . . . . . 10 (𝑏 ∈ ran 𝐸 → ¬ suc 𝑏 ∈ ran 𝐸)
2420, 23jca 513 . . . . . . . . 9 (𝑏 ∈ ran 𝐸 → (suc 𝑏 ∈ ω ∧ ¬ suc 𝑏 ∈ ran 𝐸))
25 eleq1 2825 . . . . . . . . . 10 (suc 𝑏 = 𝑎 → (suc 𝑏 ∈ ω ↔ 𝑎 ∈ ω))
26 eleq1 2825 . . . . . . . . . . 11 (suc 𝑏 = 𝑎 → (suc 𝑏 ∈ ran 𝐸𝑎 ∈ ran 𝐸))
2726notbid 318 . . . . . . . . . 10 (suc 𝑏 = 𝑎 → (¬ suc 𝑏 ∈ ran 𝐸 ↔ ¬ 𝑎 ∈ ran 𝐸))
2825, 27anbi12d 632 . . . . . . . . 9 (suc 𝑏 = 𝑎 → ((suc 𝑏 ∈ ω ∧ ¬ suc 𝑏 ∈ ran 𝐸) ↔ (𝑎 ∈ ω ∧ ¬ 𝑎 ∈ ran 𝐸)))
2924, 28syl5ibcom 245 . . . . . . . 8 (𝑏 ∈ ran 𝐸 → (suc 𝑏 = 𝑎 → (𝑎 ∈ ω ∧ ¬ 𝑎 ∈ ran 𝐸)))
3029rexlimiv 3142 . . . . . . 7 (∃𝑏 ∈ ran 𝐸 suc 𝑏 = 𝑎 → (𝑎 ∈ ω ∧ ¬ 𝑎 ∈ ran 𝐸))
31 peano1 7807 . . . . . . . . . . . . . 14 ∅ ∈ ω
323fin1a2lem3 10263 . . . . . . . . . . . . . 14 (∅ ∈ ω → (𝐸‘∅) = (2o ·o ∅))
3331, 32ax-mp 5 . . . . . . . . . . . . 13 (𝐸‘∅) = (2o ·o ∅)
34 2on 8385 . . . . . . . . . . . . . 14 2o ∈ On
35 om0 8422 . . . . . . . . . . . . . 14 (2o ∈ On → (2o ·o ∅) = ∅)
3634, 35ax-mp 5 . . . . . . . . . . . . 13 (2o ·o ∅) = ∅
3733, 36eqtri 2765 . . . . . . . . . . . 12 (𝐸‘∅) = ∅
38 f1fun 6727 . . . . . . . . . . . . . 14 (𝐸:ω–1-1→ω → Fun 𝐸)
394, 38ax-mp 5 . . . . . . . . . . . . 13 Fun 𝐸
40 f1dm 6729 . . . . . . . . . . . . . . 15 (𝐸:ω–1-1→ω → dom 𝐸 = ω)
414, 40ax-mp 5 . . . . . . . . . . . . . 14 dom 𝐸 = ω
4231, 41eleqtrri 2837 . . . . . . . . . . . . 13 ∅ ∈ dom 𝐸
43 fvelrn 7014 . . . . . . . . . . . . 13 ((Fun 𝐸 ∧ ∅ ∈ dom 𝐸) → (𝐸‘∅) ∈ ran 𝐸)
4439, 42, 43mp2an 690 . . . . . . . . . . . 12 (𝐸‘∅) ∈ ran 𝐸
4537, 44eqeltrri 2835 . . . . . . . . . . 11 ∅ ∈ ran 𝐸
46 eleq1 2825 . . . . . . . . . . 11 (𝑎 = ∅ → (𝑎 ∈ ran 𝐸 ↔ ∅ ∈ ran 𝐸))
4745, 46mpbiri 258 . . . . . . . . . 10 (𝑎 = ∅ → 𝑎 ∈ ran 𝐸)
4847necon3bi 2968 . . . . . . . . 9 𝑎 ∈ ran 𝐸𝑎 ≠ ∅)
49 nnsuc 7802 . . . . . . . . 9 ((𝑎 ∈ ω ∧ 𝑎 ≠ ∅) → ∃𝑏 ∈ ω 𝑎 = suc 𝑏)
5048, 49sylan2 594 . . . . . . . 8 ((𝑎 ∈ ω ∧ ¬ 𝑎 ∈ ran 𝐸) → ∃𝑏 ∈ ω 𝑎 = suc 𝑏)
51 eleq1 2825 . . . . . . . . . . . . 13 (𝑎 = suc 𝑏 → (𝑎 ∈ ω ↔ suc 𝑏 ∈ ω))
52 eleq1 2825 . . . . . . . . . . . . . 14 (𝑎 = suc 𝑏 → (𝑎 ∈ ran 𝐸 ↔ suc 𝑏 ∈ ran 𝐸))
5352notbid 318 . . . . . . . . . . . . 13 (𝑎 = suc 𝑏 → (¬ 𝑎 ∈ ran 𝐸 ↔ ¬ suc 𝑏 ∈ ran 𝐸))
5451, 53anbi12d 632 . . . . . . . . . . . 12 (𝑎 = suc 𝑏 → ((𝑎 ∈ ω ∧ ¬ 𝑎 ∈ ran 𝐸) ↔ (suc 𝑏 ∈ ω ∧ ¬ suc 𝑏 ∈ ran 𝐸)))
5554anbi1d 631 . . . . . . . . . . 11 (𝑎 = suc 𝑏 → (((𝑎 ∈ ω ∧ ¬ 𝑎 ∈ ran 𝐸) ∧ 𝑏 ∈ ω) ↔ ((suc 𝑏 ∈ ω ∧ ¬ suc 𝑏 ∈ ran 𝐸) ∧ 𝑏 ∈ ω)))
56 simplr 767 . . . . . . . . . . . 12 (((suc 𝑏 ∈ ω ∧ ¬ suc 𝑏 ∈ ran 𝐸) ∧ 𝑏 ∈ ω) → ¬ suc 𝑏 ∈ ran 𝐸)
5721adantl 483 . . . . . . . . . . . 12 (((suc 𝑏 ∈ ω ∧ ¬ suc 𝑏 ∈ ran 𝐸) ∧ 𝑏 ∈ ω) → (𝑏 ∈ ran 𝐸 ↔ ¬ suc 𝑏 ∈ ran 𝐸))
5856, 57mpbird 257 . . . . . . . . . . 11 (((suc 𝑏 ∈ ω ∧ ¬ suc 𝑏 ∈ ran 𝐸) ∧ 𝑏 ∈ ω) → 𝑏 ∈ ran 𝐸)
5955, 58syl6bi 253 . . . . . . . . . 10 (𝑎 = suc 𝑏 → (((𝑎 ∈ ω ∧ ¬ 𝑎 ∈ ran 𝐸) ∧ 𝑏 ∈ ω) → 𝑏 ∈ ran 𝐸))
6059com12 32 . . . . . . . . 9 (((𝑎 ∈ ω ∧ ¬ 𝑎 ∈ ran 𝐸) ∧ 𝑏 ∈ ω) → (𝑎 = suc 𝑏𝑏 ∈ ran 𝐸))
6160impr 456 . . . . . . . 8 (((𝑎 ∈ ω ∧ ¬ 𝑎 ∈ ran 𝐸) ∧ (𝑏 ∈ ω ∧ 𝑎 = suc 𝑏)) → 𝑏 ∈ ran 𝐸)
62 simprr 771 . . . . . . . . 9 (((𝑎 ∈ ω ∧ ¬ 𝑎 ∈ ran 𝐸) ∧ (𝑏 ∈ ω ∧ 𝑎 = suc 𝑏)) → 𝑎 = suc 𝑏)
6362eqcomd 2743 . . . . . . . 8 (((𝑎 ∈ ω ∧ ¬ 𝑎 ∈ ran 𝐸) ∧ (𝑏 ∈ ω ∧ 𝑎 = suc 𝑏)) → suc 𝑏 = 𝑎)
6450, 61, 63reximssdv 3166 . . . . . . 7 ((𝑎 ∈ ω ∧ ¬ 𝑎 ∈ ran 𝐸) → ∃𝑏 ∈ ran 𝐸 suc 𝑏 = 𝑎)
6530, 64impbii 208 . . . . . 6 (∃𝑏 ∈ ran 𝐸 suc 𝑏 = 𝑎 ↔ (𝑎 ∈ ω ∧ ¬ 𝑎 ∈ ran 𝐸))
6616, 65bitri 275 . . . . 5 (∃𝑏 ∈ ran 𝐸(𝑆𝑏) = 𝑎 ↔ (𝑎 ∈ ω ∧ ¬ 𝑎 ∈ ran 𝐸))
67 f1fn 6726 . . . . . . 7 (𝑆:On–1-1→On → 𝑆 Fn On)
682, 67ax-mp 5 . . . . . 6 𝑆 Fn On
69 fvelimab 6901 . . . . . 6 ((𝑆 Fn On ∧ ran 𝐸 ⊆ On) → (𝑎 ∈ (𝑆 “ ran 𝐸) ↔ ∃𝑏 ∈ ran 𝐸(𝑆𝑏) = 𝑎))
7068, 9, 69mp2an 690 . . . . 5 (𝑎 ∈ (𝑆 “ ran 𝐸) ↔ ∃𝑏 ∈ ran 𝐸(𝑆𝑏) = 𝑎)
71 eldif 3911 . . . . 5 (𝑎 ∈ (ω ∖ ran 𝐸) ↔ (𝑎 ∈ ω ∧ ¬ 𝑎 ∈ ran 𝐸))
7266, 70, 713bitr4i 303 . . . 4 (𝑎 ∈ (𝑆 “ ran 𝐸) ↔ 𝑎 ∈ (ω ∖ ran 𝐸))
7372eqriv 2734 . . 3 (𝑆 “ ran 𝐸) = (ω ∖ ran 𝐸)
74 f1oeq3 6761 . . 3 ((𝑆 “ ran 𝐸) = (ω ∖ ran 𝐸) → ((𝑆 ↾ ran 𝐸):ran 𝐸1-1-onto→(𝑆 “ ran 𝐸) ↔ (𝑆 ↾ ran 𝐸):ran 𝐸1-1-onto→(ω ∖ ran 𝐸)))
7573, 74ax-mp 5 . 2 ((𝑆 ↾ ran 𝐸):ran 𝐸1-1-onto→(𝑆 “ ran 𝐸) ↔ (𝑆 ↾ ran 𝐸):ran 𝐸1-1-onto→(ω ∖ ran 𝐸))
7611, 75mpbi 229 1 (𝑆 ↾ ran 𝐸):ran 𝐸1-1-onto→(ω ∖ ran 𝐸)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 205  wa 397   = wceq 1541  wcel 2106  wne 2941  wrex 3071  cdif 3898  wss 3901  c0 4273  cmpt 5179  dom cdm 5624  ran crn 5625  cres 5626  cima 5627  Oncon0 6306  suc csuc 6308  Fun wfun 6477   Fn wfn 6478  wf 6479  1-1wf1 6480  1-1-ontowf1o 6482  cfv 6483  (class class class)co 7341  ωcom 7784  2oc2o 8365   ·o comu 8369
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2708  ax-rep 5233  ax-sep 5247  ax-nul 5254  ax-pr 5376  ax-un 7654
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-ral 3063  df-rex 3072  df-reu 3351  df-rab 3405  df-v 3444  df-sbc 3731  df-csb 3847  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-pss 3920  df-nul 4274  df-if 4478  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4857  df-iun 4947  df-br 5097  df-opab 5159  df-mpt 5180  df-tr 5214  df-id 5522  df-eprel 5528  df-po 5536  df-so 5537  df-fr 5579  df-we 5581  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-pred 6242  df-ord 6309  df-on 6310  df-lim 6311  df-suc 6312  df-iota 6435  df-fun 6485  df-fn 6486  df-f 6487  df-f1 6488  df-fo 6489  df-f1o 6490  df-fv 6491  df-ov 7344  df-oprab 7345  df-mpo 7346  df-om 7785  df-2nd 7904  df-frecs 8171  df-wrecs 8202  df-recs 8276  df-rdg 8315  df-1o 8371  df-2o 8372  df-oadd 8375  df-omul 8376
This theorem is referenced by:  fin1a2lem7  10267
  Copyright terms: Public domain W3C validator