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

Theorem phplem4on 6359
Description: Equinumerosity of successors of an ordinal and a natural number implies equinumerosity of the originals. (Contributed by Jim Kingdon, 5-Sep-2021.)
Assertion
Ref Expression
phplem4on ((𝐴 ∈ On ∧ 𝐵 ∈ ω) → (suc 𝐴 ≈ suc 𝐵𝐴𝐵))

Proof of Theorem phplem4on
Dummy variable 𝑓 is distinct from all other variables.
StepHypRef Expression
1 bren 6258 . . . . 5 (suc 𝐴 ≈ suc 𝐵 ↔ ∃𝑓 𝑓:suc 𝐴1-1-onto→suc 𝐵)
21biimpi 117 . . . 4 (suc 𝐴 ≈ suc 𝐵 → ∃𝑓 𝑓:suc 𝐴1-1-onto→suc 𝐵)
32adantl 266 . . 3 (((𝐴 ∈ On ∧ 𝐵 ∈ ω) ∧ suc 𝐴 ≈ suc 𝐵) → ∃𝑓 𝑓:suc 𝐴1-1-onto→suc 𝐵)
4 f1of1 5152 . . . . . . . 8 (𝑓:suc 𝐴1-1-onto→suc 𝐵𝑓:suc 𝐴1-1→suc 𝐵)
54adantl 266 . . . . . . 7 ((((𝐴 ∈ On ∧ 𝐵 ∈ ω) ∧ suc 𝐴 ≈ suc 𝐵) ∧ 𝑓:suc 𝐴1-1-onto→suc 𝐵) → 𝑓:suc 𝐴1-1→suc 𝐵)
6 peano2 4345 . . . . . . . . 9 (𝐵 ∈ ω → suc 𝐵 ∈ ω)
7 nnon 4359 . . . . . . . . 9 (suc 𝐵 ∈ ω → suc 𝐵 ∈ On)
86, 7syl 14 . . . . . . . 8 (𝐵 ∈ ω → suc 𝐵 ∈ On)
98ad3antlr 470 . . . . . . 7 ((((𝐴 ∈ On ∧ 𝐵 ∈ ω) ∧ suc 𝐴 ≈ suc 𝐵) ∧ 𝑓:suc 𝐴1-1-onto→suc 𝐵) → suc 𝐵 ∈ On)
10 sssucid 4179 . . . . . . . 8 𝐴 ⊆ suc 𝐴
1110a1i 9 . . . . . . 7 ((((𝐴 ∈ On ∧ 𝐵 ∈ ω) ∧ suc 𝐴 ≈ suc 𝐵) ∧ 𝑓:suc 𝐴1-1-onto→suc 𝐵) → 𝐴 ⊆ suc 𝐴)
12 simplll 493 . . . . . . 7 ((((𝐴 ∈ On ∧ 𝐵 ∈ ω) ∧ suc 𝐴 ≈ suc 𝐵) ∧ 𝑓:suc 𝐴1-1-onto→suc 𝐵) → 𝐴 ∈ On)
13 f1imaen2g 6303 . . . . . . 7 (((𝑓:suc 𝐴1-1→suc 𝐵 ∧ suc 𝐵 ∈ On) ∧ (𝐴 ⊆ suc 𝐴𝐴 ∈ On)) → (𝑓𝐴) ≈ 𝐴)
145, 9, 11, 12, 13syl22anc 1147 . . . . . 6 ((((𝐴 ∈ On ∧ 𝐵 ∈ ω) ∧ suc 𝐴 ≈ suc 𝐵) ∧ 𝑓:suc 𝐴1-1-onto→suc 𝐵) → (𝑓𝐴) ≈ 𝐴)
1514ensymd 6293 . . . . 5 ((((𝐴 ∈ On ∧ 𝐵 ∈ ω) ∧ suc 𝐴 ≈ suc 𝐵) ∧ 𝑓:suc 𝐴1-1-onto→suc 𝐵) → 𝐴 ≈ (𝑓𝐴))
16 eloni 4139 . . . . . . . . 9 (𝐴 ∈ On → Ord 𝐴)
17 orddif 4298 . . . . . . . . 9 (Ord 𝐴𝐴 = (suc 𝐴 ∖ {𝐴}))
1816, 17syl 14 . . . . . . . 8 (𝐴 ∈ On → 𝐴 = (suc 𝐴 ∖ {𝐴}))
1918imaeq2d 4695 . . . . . . 7 (𝐴 ∈ On → (𝑓𝐴) = (𝑓 “ (suc 𝐴 ∖ {𝐴})))
2019ad3antrrr 469 . . . . . 6 ((((𝐴 ∈ On ∧ 𝐵 ∈ ω) ∧ suc 𝐴 ≈ suc 𝐵) ∧ 𝑓:suc 𝐴1-1-onto→suc 𝐵) → (𝑓𝐴) = (𝑓 “ (suc 𝐴 ∖ {𝐴})))
21 f1ofn 5154 . . . . . . . . . 10 (𝑓:suc 𝐴1-1-onto→suc 𝐵𝑓 Fn suc 𝐴)
2221adantl 266 . . . . . . . . 9 ((((𝐴 ∈ On ∧ 𝐵 ∈ ω) ∧ suc 𝐴 ≈ suc 𝐵) ∧ 𝑓:suc 𝐴1-1-onto→suc 𝐵) → 𝑓 Fn suc 𝐴)
23 sucidg 4180 . . . . . . . . . 10 (𝐴 ∈ On → 𝐴 ∈ suc 𝐴)
2412, 23syl 14 . . . . . . . . 9 ((((𝐴 ∈ On ∧ 𝐵 ∈ ω) ∧ suc 𝐴 ≈ suc 𝐵) ∧ 𝑓:suc 𝐴1-1-onto→suc 𝐵) → 𝐴 ∈ suc 𝐴)
25 fnsnfv 5259 . . . . . . . . 9 ((𝑓 Fn suc 𝐴𝐴 ∈ suc 𝐴) → {(𝑓𝐴)} = (𝑓 “ {𝐴}))
2622, 24, 25syl2anc 397 . . . . . . . 8 ((((𝐴 ∈ On ∧ 𝐵 ∈ ω) ∧ suc 𝐴 ≈ suc 𝐵) ∧ 𝑓:suc 𝐴1-1-onto→suc 𝐵) → {(𝑓𝐴)} = (𝑓 “ {𝐴}))
2726difeq2d 3089 . . . . . . 7 ((((𝐴 ∈ On ∧ 𝐵 ∈ ω) ∧ suc 𝐴 ≈ suc 𝐵) ∧ 𝑓:suc 𝐴1-1-onto→suc 𝐵) → ((𝑓 “ suc 𝐴) ∖ {(𝑓𝐴)}) = ((𝑓 “ suc 𝐴) ∖ (𝑓 “ {𝐴})))
28 imadmrn 4705 . . . . . . . . . . 11 (𝑓 “ dom 𝑓) = ran 𝑓
2928eqcomi 2060 . . . . . . . . . 10 ran 𝑓 = (𝑓 “ dom 𝑓)
30 f1ofo 5160 . . . . . . . . . . 11 (𝑓:suc 𝐴1-1-onto→suc 𝐵𝑓:suc 𝐴onto→suc 𝐵)
31 forn 5136 . . . . . . . . . . 11 (𝑓:suc 𝐴onto→suc 𝐵 → ran 𝑓 = suc 𝐵)
3230, 31syl 14 . . . . . . . . . 10 (𝑓:suc 𝐴1-1-onto→suc 𝐵 → ran 𝑓 = suc 𝐵)
33 f1odm 5157 . . . . . . . . . . 11 (𝑓:suc 𝐴1-1-onto→suc 𝐵 → dom 𝑓 = suc 𝐴)
3433imaeq2d 4695 . . . . . . . . . 10 (𝑓:suc 𝐴1-1-onto→suc 𝐵 → (𝑓 “ dom 𝑓) = (𝑓 “ suc 𝐴))
3529, 32, 343eqtr3a 2112 . . . . . . . . 9 (𝑓:suc 𝐴1-1-onto→suc 𝐵 → suc 𝐵 = (𝑓 “ suc 𝐴))
3635difeq1d 3088 . . . . . . . 8 (𝑓:suc 𝐴1-1-onto→suc 𝐵 → (suc 𝐵 ∖ {(𝑓𝐴)}) = ((𝑓 “ suc 𝐴) ∖ {(𝑓𝐴)}))
3736adantl 266 . . . . . . 7 ((((𝐴 ∈ On ∧ 𝐵 ∈ ω) ∧ suc 𝐴 ≈ suc 𝐵) ∧ 𝑓:suc 𝐴1-1-onto→suc 𝐵) → (suc 𝐵 ∖ {(𝑓𝐴)}) = ((𝑓 “ suc 𝐴) ∖ {(𝑓𝐴)}))
38 dff1o3 5159 . . . . . . . . . 10 (𝑓:suc 𝐴1-1-onto→suc 𝐵 ↔ (𝑓:suc 𝐴onto→suc 𝐵 ∧ Fun 𝑓))
3938simprbi 264 . . . . . . . . 9 (𝑓:suc 𝐴1-1-onto→suc 𝐵 → Fun 𝑓)
40 imadif 5006 . . . . . . . . 9 (Fun 𝑓 → (𝑓 “ (suc 𝐴 ∖ {𝐴})) = ((𝑓 “ suc 𝐴) ∖ (𝑓 “ {𝐴})))
4139, 40syl 14 . . . . . . . 8 (𝑓:suc 𝐴1-1-onto→suc 𝐵 → (𝑓 “ (suc 𝐴 ∖ {𝐴})) = ((𝑓 “ suc 𝐴) ∖ (𝑓 “ {𝐴})))
4241adantl 266 . . . . . . 7 ((((𝐴 ∈ On ∧ 𝐵 ∈ ω) ∧ suc 𝐴 ≈ suc 𝐵) ∧ 𝑓:suc 𝐴1-1-onto→suc 𝐵) → (𝑓 “ (suc 𝐴 ∖ {𝐴})) = ((𝑓 “ suc 𝐴) ∖ (𝑓 “ {𝐴})))
4327, 37, 423eqtr4rd 2099 . . . . . 6 ((((𝐴 ∈ On ∧ 𝐵 ∈ ω) ∧ suc 𝐴 ≈ suc 𝐵) ∧ 𝑓:suc 𝐴1-1-onto→suc 𝐵) → (𝑓 “ (suc 𝐴 ∖ {𝐴})) = (suc 𝐵 ∖ {(𝑓𝐴)}))
4420, 43eqtrd 2088 . . . . 5 ((((𝐴 ∈ On ∧ 𝐵 ∈ ω) ∧ suc 𝐴 ≈ suc 𝐵) ∧ 𝑓:suc 𝐴1-1-onto→suc 𝐵) → (𝑓𝐴) = (suc 𝐵 ∖ {(𝑓𝐴)}))
4515, 44breqtrd 3815 . . . 4 ((((𝐴 ∈ On ∧ 𝐵 ∈ ω) ∧ suc 𝐴 ≈ suc 𝐵) ∧ 𝑓:suc 𝐴1-1-onto→suc 𝐵) → 𝐴 ≈ (suc 𝐵 ∖ {(𝑓𝐴)}))
46 simpllr 494 . . . . . 6 ((((𝐴 ∈ On ∧ 𝐵 ∈ ω) ∧ suc 𝐴 ≈ suc 𝐵) ∧ 𝑓:suc 𝐴1-1-onto→suc 𝐵) → 𝐵 ∈ ω)
47 fnfvelrn 5326 . . . . . . . 8 ((𝑓 Fn suc 𝐴𝐴 ∈ suc 𝐴) → (𝑓𝐴) ∈ ran 𝑓)
4822, 24, 47syl2anc 397 . . . . . . 7 ((((𝐴 ∈ On ∧ 𝐵 ∈ ω) ∧ suc 𝐴 ≈ suc 𝐵) ∧ 𝑓:suc 𝐴1-1-onto→suc 𝐵) → (𝑓𝐴) ∈ ran 𝑓)
4931eleq2d 2123 . . . . . . . . 9 (𝑓:suc 𝐴onto→suc 𝐵 → ((𝑓𝐴) ∈ ran 𝑓 ↔ (𝑓𝐴) ∈ suc 𝐵))
5030, 49syl 14 . . . . . . . 8 (𝑓:suc 𝐴1-1-onto→suc 𝐵 → ((𝑓𝐴) ∈ ran 𝑓 ↔ (𝑓𝐴) ∈ suc 𝐵))
5150adantl 266 . . . . . . 7 ((((𝐴 ∈ On ∧ 𝐵 ∈ ω) ∧ suc 𝐴 ≈ suc 𝐵) ∧ 𝑓:suc 𝐴1-1-onto→suc 𝐵) → ((𝑓𝐴) ∈ ran 𝑓 ↔ (𝑓𝐴) ∈ suc 𝐵))
5248, 51mpbid 139 . . . . . 6 ((((𝐴 ∈ On ∧ 𝐵 ∈ ω) ∧ suc 𝐴 ≈ suc 𝐵) ∧ 𝑓:suc 𝐴1-1-onto→suc 𝐵) → (𝑓𝐴) ∈ suc 𝐵)
53 phplem3g 6349 . . . . . 6 ((𝐵 ∈ ω ∧ (𝑓𝐴) ∈ suc 𝐵) → 𝐵 ≈ (suc 𝐵 ∖ {(𝑓𝐴)}))
5446, 52, 53syl2anc 397 . . . . 5 ((((𝐴 ∈ On ∧ 𝐵 ∈ ω) ∧ suc 𝐴 ≈ suc 𝐵) ∧ 𝑓:suc 𝐴1-1-onto→suc 𝐵) → 𝐵 ≈ (suc 𝐵 ∖ {(𝑓𝐴)}))
5554ensymd 6293 . . . 4 ((((𝐴 ∈ On ∧ 𝐵 ∈ ω) ∧ suc 𝐴 ≈ suc 𝐵) ∧ 𝑓:suc 𝐴1-1-onto→suc 𝐵) → (suc 𝐵 ∖ {(𝑓𝐴)}) ≈ 𝐵)
56 entr 6294 . . . 4 ((𝐴 ≈ (suc 𝐵 ∖ {(𝑓𝐴)}) ∧ (suc 𝐵 ∖ {(𝑓𝐴)}) ≈ 𝐵) → 𝐴𝐵)
5745, 55, 56syl2anc 397 . . 3 ((((𝐴 ∈ On ∧ 𝐵 ∈ ω) ∧ suc 𝐴 ≈ suc 𝐵) ∧ 𝑓:suc 𝐴1-1-onto→suc 𝐵) → 𝐴𝐵)
583, 57exlimddv 1794 . 2 (((𝐴 ∈ On ∧ 𝐵 ∈ ω) ∧ suc 𝐴 ≈ suc 𝐵) → 𝐴𝐵)
5958ex 112 1 ((𝐴 ∈ On ∧ 𝐵 ∈ ω) → (suc 𝐴 ≈ suc 𝐵𝐴𝐵))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 101  wb 102   = wceq 1259  wex 1397  wcel 1409  cdif 2941  wss 2944  {csn 3402   class class class wbr 3791  Ord word 4126  Oncon0 4127  suc csuc 4129  ωcom 4340  ccnv 4371  dom cdm 4372  ran crn 4373  cima 4375  Fun wfun 4923   Fn wfn 4924  1-1wf1 4926  ontowfo 4927  1-1-ontowf1o 4928  cfv 4929  cen 6249
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-in1 554  ax-in2 555  ax-io 640  ax-5 1352  ax-7 1353  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-8 1411  ax-10 1412  ax-11 1413  ax-i12 1414  ax-bndl 1415  ax-4 1416  ax-13 1420  ax-14 1421  ax-17 1435  ax-i9 1439  ax-ial 1443  ax-i5r 1444  ax-ext 2038  ax-sep 3902  ax-nul 3910  ax-pow 3954  ax-pr 3971  ax-un 4197  ax-setind 4289  ax-iinf 4338
This theorem depends on definitions:  df-bi 114  df-dc 754  df-3or 897  df-3an 898  df-tru 1262  df-fal 1265  df-nf 1366  df-sb 1662  df-eu 1919  df-mo 1920  df-clab 2043  df-cleq 2049  df-clel 2052  df-nfc 2183  df-ne 2221  df-ral 2328  df-rex 2329  df-rab 2332  df-v 2576  df-sbc 2787  df-dif 2947  df-un 2949  df-in 2951  df-ss 2958  df-nul 3252  df-pw 3388  df-sn 3408  df-pr 3409  df-op 3411  df-uni 3608  df-int 3643  df-br 3792  df-opab 3846  df-tr 3882  df-id 4057  df-iord 4130  df-on 4132  df-suc 4135  df-iom 4341  df-xp 4378  df-rel 4379  df-cnv 4380  df-co 4381  df-dm 4382  df-rn 4383  df-res 4384  df-ima 4385  df-iota 4894  df-fun 4931  df-fn 4932  df-f 4933  df-f1 4934  df-fo 4935  df-f1o 4936  df-fv 4937  df-er 6136  df-en 6252
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator