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

Theorem fin1a2lem6 9865
 Description: Lemma for fin1a2 9875. 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 9861 . . 3 𝑆:On–1-1→On
3 fin1a2lem.b . . . . 5 𝐸 = (𝑥 ∈ ω ↦ (2o ·o 𝑥))
43fin1a2lem4 9863 . . . 4 𝐸:ω–1-1→ω
5 f1f 6560 . . . 4 (𝐸:ω–1-1→ω → 𝐸:ω⟶ω)
6 frn 6504 . . . . 5 (𝐸:ω⟶ω → ran 𝐸 ⊆ ω)
7 omsson 7583 . . . . 5 ω ⊆ On
86, 7sstrdi 3904 . . . 4 (𝐸:ω⟶ω → ran 𝐸 ⊆ On)
94, 5, 8mp2b 10 . . 3 ran 𝐸 ⊆ On
10 f1ores 6616 . . 3 ((𝑆:On–1-1→On ∧ ran 𝐸 ⊆ On) → (𝑆 ↾ ran 𝐸):ran 𝐸1-1-onto→(𝑆 “ ran 𝐸))
112, 9, 10mp2an 691 . 2 (𝑆 ↾ ran 𝐸):ran 𝐸1-1-onto→(𝑆 “ ran 𝐸)
129sseli 3888 . . . . . . . . 9 (𝑏 ∈ ran 𝐸𝑏 ∈ On)
131fin1a2lem1 9860 . . . . . . . . 9 (𝑏 ∈ On → (𝑆𝑏) = suc 𝑏)
1412, 13syl 17 . . . . . . . 8 (𝑏 ∈ ran 𝐸 → (𝑆𝑏) = suc 𝑏)
1514eqeq1d 2760 . . . . . . 7 (𝑏 ∈ ran 𝐸 → ((𝑆𝑏) = 𝑎 ↔ suc 𝑏 = 𝑎))
1615rexbiia 3174 . . . . . 6 (∃𝑏 ∈ ran 𝐸(𝑆𝑏) = 𝑎 ↔ ∃𝑏 ∈ ran 𝐸 suc 𝑏 = 𝑎)
174, 5, 6mp2b 10 . . . . . . . . . . . 12 ran 𝐸 ⊆ ω
1817sseli 3888 . . . . . . . . . . 11 (𝑏 ∈ ran 𝐸𝑏 ∈ ω)
19 peano2 7601 . . . . . . . . . . 11 (𝑏 ∈ ω → suc 𝑏 ∈ ω)
2018, 19syl 17 . . . . . . . . . 10 (𝑏 ∈ ran 𝐸 → suc 𝑏 ∈ ω)
213fin1a2lem5 9864 . . . . . . . . . . . 12 (𝑏 ∈ ω → (𝑏 ∈ ran 𝐸 ↔ ¬ suc 𝑏 ∈ ran 𝐸))
2221biimpd 232 . . . . . . . . . . 11 (𝑏 ∈ ω → (𝑏 ∈ ran 𝐸 → ¬ suc 𝑏 ∈ ran 𝐸))
2318, 22mpcom 38 . . . . . . . . . 10 (𝑏 ∈ ran 𝐸 → ¬ suc 𝑏 ∈ ran 𝐸)
2420, 23jca 515 . . . . . . . . 9 (𝑏 ∈ ran 𝐸 → (suc 𝑏 ∈ ω ∧ ¬ suc 𝑏 ∈ ran 𝐸))
25 eleq1 2839 . . . . . . . . . 10 (suc 𝑏 = 𝑎 → (suc 𝑏 ∈ ω ↔ 𝑎 ∈ ω))
26 eleq1 2839 . . . . . . . . . . 11 (suc 𝑏 = 𝑎 → (suc 𝑏 ∈ ran 𝐸𝑎 ∈ ran 𝐸))
2726notbid 321 . . . . . . . . . 10 (suc 𝑏 = 𝑎 → (¬ suc 𝑏 ∈ ran 𝐸 ↔ ¬ 𝑎 ∈ ran 𝐸))
2825, 27anbi12d 633 . . . . . . . . 9 (suc 𝑏 = 𝑎 → ((suc 𝑏 ∈ ω ∧ ¬ suc 𝑏 ∈ ran 𝐸) ↔ (𝑎 ∈ ω ∧ ¬ 𝑎 ∈ ran 𝐸)))
2924, 28syl5ibcom 248 . . . . . . . 8 (𝑏 ∈ ran 𝐸 → (suc 𝑏 = 𝑎 → (𝑎 ∈ ω ∧ ¬ 𝑎 ∈ ran 𝐸)))
3029rexlimiv 3204 . . . . . . 7 (∃𝑏 ∈ ran 𝐸 suc 𝑏 = 𝑎 → (𝑎 ∈ ω ∧ ¬ 𝑎 ∈ ran 𝐸))
31 peano1 7600 . . . . . . . . . . . . . 14 ∅ ∈ ω
323fin1a2lem3 9862 . . . . . . . . . . . . . 14 (∅ ∈ ω → (𝐸‘∅) = (2o ·o ∅))
3331, 32ax-mp 5 . . . . . . . . . . . . 13 (𝐸‘∅) = (2o ·o ∅)
34 2on 8121 . . . . . . . . . . . . . 14 2o ∈ On
35 om0 8152 . . . . . . . . . . . . . 14 (2o ∈ On → (2o ·o ∅) = ∅)
3634, 35ax-mp 5 . . . . . . . . . . . . 13 (2o ·o ∅) = ∅
3733, 36eqtri 2781 . . . . . . . . . . . 12 (𝐸‘∅) = ∅
38 f1fun 6562 . . . . . . . . . . . . . 14 (𝐸:ω–1-1→ω → Fun 𝐸)
394, 38ax-mp 5 . . . . . . . . . . . . 13 Fun 𝐸
40 f1dm 6564 . . . . . . . . . . . . . . 15 (𝐸:ω–1-1→ω → dom 𝐸 = ω)
414, 40ax-mp 5 . . . . . . . . . . . . . 14 dom 𝐸 = ω
4231, 41eleqtrri 2851 . . . . . . . . . . . . 13 ∅ ∈ dom 𝐸
43 fvelrn 6835 . . . . . . . . . . . . 13 ((Fun 𝐸 ∧ ∅ ∈ dom 𝐸) → (𝐸‘∅) ∈ ran 𝐸)
4439, 42, 43mp2an 691 . . . . . . . . . . . 12 (𝐸‘∅) ∈ ran 𝐸
4537, 44eqeltrri 2849 . . . . . . . . . . 11 ∅ ∈ ran 𝐸
46 eleq1 2839 . . . . . . . . . . 11 (𝑎 = ∅ → (𝑎 ∈ ran 𝐸 ↔ ∅ ∈ ran 𝐸))
4745, 46mpbiri 261 . . . . . . . . . 10 (𝑎 = ∅ → 𝑎 ∈ ran 𝐸)
4847necon3bi 2977 . . . . . . . . 9 𝑎 ∈ ran 𝐸𝑎 ≠ ∅)
49 nnsuc 7596 . . . . . . . . 9 ((𝑎 ∈ ω ∧ 𝑎 ≠ ∅) → ∃𝑏 ∈ ω 𝑎 = suc 𝑏)
5048, 49sylan2 595 . . . . . . . 8 ((𝑎 ∈ ω ∧ ¬ 𝑎 ∈ ran 𝐸) → ∃𝑏 ∈ ω 𝑎 = suc 𝑏)
51 eleq1 2839 . . . . . . . . . . . . 13 (𝑎 = suc 𝑏 → (𝑎 ∈ ω ↔ suc 𝑏 ∈ ω))
52 eleq1 2839 . . . . . . . . . . . . . 14 (𝑎 = suc 𝑏 → (𝑎 ∈ ran 𝐸 ↔ suc 𝑏 ∈ ran 𝐸))
5352notbid 321 . . . . . . . . . . . . 13 (𝑎 = suc 𝑏 → (¬ 𝑎 ∈ ran 𝐸 ↔ ¬ suc 𝑏 ∈ ran 𝐸))
5451, 53anbi12d 633 . . . . . . . . . . . 12 (𝑎 = suc 𝑏 → ((𝑎 ∈ ω ∧ ¬ 𝑎 ∈ ran 𝐸) ↔ (suc 𝑏 ∈ ω ∧ ¬ suc 𝑏 ∈ ran 𝐸)))
5554anbi1d 632 . . . . . . . . . . 11 (𝑎 = suc 𝑏 → (((𝑎 ∈ ω ∧ ¬ 𝑎 ∈ ran 𝐸) ∧ 𝑏 ∈ ω) ↔ ((suc 𝑏 ∈ ω ∧ ¬ suc 𝑏 ∈ ran 𝐸) ∧ 𝑏 ∈ ω)))
56 simplr 768 . . . . . . . . . . . 12 (((suc 𝑏 ∈ ω ∧ ¬ suc 𝑏 ∈ ran 𝐸) ∧ 𝑏 ∈ ω) → ¬ suc 𝑏 ∈ ran 𝐸)
5721adantl 485 . . . . . . . . . . . 12 (((suc 𝑏 ∈ ω ∧ ¬ suc 𝑏 ∈ ran 𝐸) ∧ 𝑏 ∈ ω) → (𝑏 ∈ ran 𝐸 ↔ ¬ suc 𝑏 ∈ ran 𝐸))
5856, 57mpbird 260 . . . . . . . . . . 11 (((suc 𝑏 ∈ ω ∧ ¬ suc 𝑏 ∈ ran 𝐸) ∧ 𝑏 ∈ ω) → 𝑏 ∈ ran 𝐸)
5955, 58syl6bi 256 . . . . . . . . . 10 (𝑎 = suc 𝑏 → (((𝑎 ∈ ω ∧ ¬ 𝑎 ∈ ran 𝐸) ∧ 𝑏 ∈ ω) → 𝑏 ∈ ran 𝐸))
6059com12 32 . . . . . . . . 9 (((𝑎 ∈ ω ∧ ¬ 𝑎 ∈ ran 𝐸) ∧ 𝑏 ∈ ω) → (𝑎 = suc 𝑏𝑏 ∈ ran 𝐸))
6160impr 458 . . . . . . . 8 (((𝑎 ∈ ω ∧ ¬ 𝑎 ∈ ran 𝐸) ∧ (𝑏 ∈ ω ∧ 𝑎 = suc 𝑏)) → 𝑏 ∈ ran 𝐸)
62 simprr 772 . . . . . . . . 9 (((𝑎 ∈ ω ∧ ¬ 𝑎 ∈ ran 𝐸) ∧ (𝑏 ∈ ω ∧ 𝑎 = suc 𝑏)) → 𝑎 = suc 𝑏)
6362eqcomd 2764 . . . . . . . 8 (((𝑎 ∈ ω ∧ ¬ 𝑎 ∈ ran 𝐸) ∧ (𝑏 ∈ ω ∧ 𝑎 = suc 𝑏)) → suc 𝑏 = 𝑎)
6450, 61, 63reximssdv 3200 . . . . . . 7 ((𝑎 ∈ ω ∧ ¬ 𝑎 ∈ ran 𝐸) → ∃𝑏 ∈ ran 𝐸 suc 𝑏 = 𝑎)
6530, 64impbii 212 . . . . . 6 (∃𝑏 ∈ ran 𝐸 suc 𝑏 = 𝑎 ↔ (𝑎 ∈ ω ∧ ¬ 𝑎 ∈ ran 𝐸))
6616, 65bitri 278 . . . . 5 (∃𝑏 ∈ ran 𝐸(𝑆𝑏) = 𝑎 ↔ (𝑎 ∈ ω ∧ ¬ 𝑎 ∈ ran 𝐸))
67 f1fn 6561 . . . . . . 7 (𝑆:On–1-1→On → 𝑆 Fn On)
682, 67ax-mp 5 . . . . . 6 𝑆 Fn On
69 fvelimab 6725 . . . . . 6 ((𝑆 Fn On ∧ ran 𝐸 ⊆ On) → (𝑎 ∈ (𝑆 “ ran 𝐸) ↔ ∃𝑏 ∈ ran 𝐸(𝑆𝑏) = 𝑎))
7068, 9, 69mp2an 691 . . . . 5 (𝑎 ∈ (𝑆 “ ran 𝐸) ↔ ∃𝑏 ∈ ran 𝐸(𝑆𝑏) = 𝑎)
71 eldif 3868 . . . . 5 (𝑎 ∈ (ω ∖ ran 𝐸) ↔ (𝑎 ∈ ω ∧ ¬ 𝑎 ∈ ran 𝐸))
7266, 70, 713bitr4i 306 . . . 4 (𝑎 ∈ (𝑆 “ ran 𝐸) ↔ 𝑎 ∈ (ω ∖ ran 𝐸))
7372eqriv 2755 . . 3 (𝑆 “ ran 𝐸) = (ω ∖ ran 𝐸)
74 f1oeq3 6592 . . 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 233 1 (𝑆 ↾ ran 𝐸):ran 𝐸1-1-onto→(ω ∖ ran 𝐸)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   ↔ wb 209   ∧ wa 399   = wceq 1538   ∈ wcel 2111   ≠ wne 2951  ∃wrex 3071   ∖ cdif 3855   ⊆ wss 3858  ∅c0 4225   ↦ cmpt 5112  dom cdm 5524  ran crn 5525   ↾ cres 5526   “ cima 5527  Oncon0 6169  suc csuc 6171  Fun wfun 6329   Fn wfn 6330  ⟶wf 6331  –1-1→wf1 6332  –1-1-onto→wf1o 6334  ‘cfv 6335  (class class class)co 7150  ωcom 7579  2oc2o 8106   ·o comu 8110 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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729  ax-rep 5156  ax-sep 5169  ax-nul 5176  ax-pr 5298  ax-un 7459 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2557  df-eu 2588  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-ne 2952  df-ral 3075  df-rex 3076  df-reu 3077  df-rab 3079  df-v 3411  df-sbc 3697  df-csb 3806  df-dif 3861  df-un 3863  df-in 3865  df-ss 3875  df-pss 3877  df-nul 4226  df-if 4421  df-pw 4496  df-sn 4523  df-pr 4525  df-tp 4527  df-op 4529  df-uni 4799  df-iun 4885  df-br 5033  df-opab 5095  df-mpt 5113  df-tr 5139  df-id 5430  df-eprel 5435  df-po 5443  df-so 5444  df-fr 5483  df-we 5485  df-xp 5530  df-rel 5531  df-cnv 5532  df-co 5533  df-dm 5534  df-rn 5535  df-res 5536  df-ima 5537  df-pred 6126  df-ord 6172  df-on 6173  df-lim 6174  df-suc 6175  df-iota 6294  df-fun 6337  df-fn 6338  df-f 6339  df-f1 6340  df-fo 6341  df-f1o 6342  df-fv 6343  df-ov 7153  df-oprab 7154  df-mpo 7155  df-om 7580  df-wrecs 7957  df-recs 8018  df-rdg 8056  df-1o 8112  df-2o 8113  df-oadd 8116  df-omul 8117 This theorem is referenced by:  fin1a2lem7  9866
 Copyright terms: Public domain W3C validator