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

Theorem phplem4on 6772
 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 6652 . . . . 5 (suc 𝐴 ≈ suc 𝐵 ↔ ∃𝑓 𝑓:suc 𝐴1-1-onto→suc 𝐵)
21biimpi 119 . . . 4 (suc 𝐴 ≈ suc 𝐵 → ∃𝑓 𝑓:suc 𝐴1-1-onto→suc 𝐵)
32adantl 275 . . 3 (((𝐴 ∈ On ∧ 𝐵 ∈ ω) ∧ suc 𝐴 ≈ suc 𝐵) → ∃𝑓 𝑓:suc 𝐴1-1-onto→suc 𝐵)
4 f1of1 5377 . . . . . . . 8 (𝑓:suc 𝐴1-1-onto→suc 𝐵𝑓:suc 𝐴1-1→suc 𝐵)
54adantl 275 . . . . . . 7 ((((𝐴 ∈ On ∧ 𝐵 ∈ ω) ∧ suc 𝐴 ≈ suc 𝐵) ∧ 𝑓:suc 𝐴1-1-onto→suc 𝐵) → 𝑓:suc 𝐴1-1→suc 𝐵)
6 peano2 4519 . . . . . . . . 9 (𝐵 ∈ ω → suc 𝐵 ∈ ω)
7 nnon 4534 . . . . . . . . 9 (suc 𝐵 ∈ ω → suc 𝐵 ∈ On)
86, 7syl 14 . . . . . . . 8 (𝐵 ∈ ω → suc 𝐵 ∈ On)
98ad3antlr 485 . . . . . . 7 ((((𝐴 ∈ On ∧ 𝐵 ∈ ω) ∧ suc 𝐴 ≈ suc 𝐵) ∧ 𝑓:suc 𝐴1-1-onto→suc 𝐵) → suc 𝐵 ∈ On)
10 sssucid 4347 . . . . . . . 8 𝐴 ⊆ suc 𝐴
1110a1i 9 . . . . . . 7 ((((𝐴 ∈ On ∧ 𝐵 ∈ ω) ∧ suc 𝐴 ≈ suc 𝐵) ∧ 𝑓:suc 𝐴1-1-onto→suc 𝐵) → 𝐴 ⊆ suc 𝐴)
12 simplll 523 . . . . . . 7 ((((𝐴 ∈ On ∧ 𝐵 ∈ ω) ∧ suc 𝐴 ≈ suc 𝐵) ∧ 𝑓:suc 𝐴1-1-onto→suc 𝐵) → 𝐴 ∈ On)
13 f1imaen2g 6698 . . . . . . 7 (((𝑓:suc 𝐴1-1→suc 𝐵 ∧ suc 𝐵 ∈ On) ∧ (𝐴 ⊆ suc 𝐴𝐴 ∈ On)) → (𝑓𝐴) ≈ 𝐴)
145, 9, 11, 12, 13syl22anc 1218 . . . . . 6 ((((𝐴 ∈ On ∧ 𝐵 ∈ ω) ∧ suc 𝐴 ≈ suc 𝐵) ∧ 𝑓:suc 𝐴1-1-onto→suc 𝐵) → (𝑓𝐴) ≈ 𝐴)
1514ensymd 6688 . . . . 5 ((((𝐴 ∈ On ∧ 𝐵 ∈ ω) ∧ suc 𝐴 ≈ suc 𝐵) ∧ 𝑓:suc 𝐴1-1-onto→suc 𝐵) → 𝐴 ≈ (𝑓𝐴))
16 eloni 4307 . . . . . . . . 9 (𝐴 ∈ On → Ord 𝐴)
17 orddif 4472 . . . . . . . . 9 (Ord 𝐴𝐴 = (suc 𝐴 ∖ {𝐴}))
1816, 17syl 14 . . . . . . . 8 (𝐴 ∈ On → 𝐴 = (suc 𝐴 ∖ {𝐴}))
1918imaeq2d 4892 . . . . . . 7 (𝐴 ∈ On → (𝑓𝐴) = (𝑓 “ (suc 𝐴 ∖ {𝐴})))
2019ad3antrrr 484 . . . . . 6 ((((𝐴 ∈ On ∧ 𝐵 ∈ ω) ∧ suc 𝐴 ≈ suc 𝐵) ∧ 𝑓:suc 𝐴1-1-onto→suc 𝐵) → (𝑓𝐴) = (𝑓 “ (suc 𝐴 ∖ {𝐴})))
21 f1ofn 5379 . . . . . . . . . 10 (𝑓:suc 𝐴1-1-onto→suc 𝐵𝑓 Fn suc 𝐴)
2221adantl 275 . . . . . . . . 9 ((((𝐴 ∈ On ∧ 𝐵 ∈ ω) ∧ suc 𝐴 ≈ suc 𝐵) ∧ 𝑓:suc 𝐴1-1-onto→suc 𝐵) → 𝑓 Fn suc 𝐴)
23 sucidg 4348 . . . . . . . . . 10 (𝐴 ∈ On → 𝐴 ∈ suc 𝐴)
2412, 23syl 14 . . . . . . . . 9 ((((𝐴 ∈ On ∧ 𝐵 ∈ ω) ∧ suc 𝐴 ≈ suc 𝐵) ∧ 𝑓:suc 𝐴1-1-onto→suc 𝐵) → 𝐴 ∈ suc 𝐴)
25 fnsnfv 5491 . . . . . . . . 9 ((𝑓 Fn suc 𝐴𝐴 ∈ suc 𝐴) → {(𝑓𝐴)} = (𝑓 “ {𝐴}))
2622, 24, 25syl2anc 409 . . . . . . . 8 ((((𝐴 ∈ On ∧ 𝐵 ∈ ω) ∧ suc 𝐴 ≈ suc 𝐵) ∧ 𝑓:suc 𝐴1-1-onto→suc 𝐵) → {(𝑓𝐴)} = (𝑓 “ {𝐴}))
2726difeq2d 3200 . . . . . . 7 ((((𝐴 ∈ On ∧ 𝐵 ∈ ω) ∧ suc 𝐴 ≈ suc 𝐵) ∧ 𝑓:suc 𝐴1-1-onto→suc 𝐵) → ((𝑓 “ suc 𝐴) ∖ {(𝑓𝐴)}) = ((𝑓 “ suc 𝐴) ∖ (𝑓 “ {𝐴})))
28 imadmrn 4902 . . . . . . . . . . 11 (𝑓 “ dom 𝑓) = ran 𝑓
2928eqcomi 2144 . . . . . . . . . 10 ran 𝑓 = (𝑓 “ dom 𝑓)
30 f1ofo 5385 . . . . . . . . . . 11 (𝑓:suc 𝐴1-1-onto→suc 𝐵𝑓:suc 𝐴onto→suc 𝐵)
31 forn 5359 . . . . . . . . . . 11 (𝑓:suc 𝐴onto→suc 𝐵 → ran 𝑓 = suc 𝐵)
3230, 31syl 14 . . . . . . . . . 10 (𝑓:suc 𝐴1-1-onto→suc 𝐵 → ran 𝑓 = suc 𝐵)
33 f1odm 5382 . . . . . . . . . . 11 (𝑓:suc 𝐴1-1-onto→suc 𝐵 → dom 𝑓 = suc 𝐴)
3433imaeq2d 4892 . . . . . . . . . 10 (𝑓:suc 𝐴1-1-onto→suc 𝐵 → (𝑓 “ dom 𝑓) = (𝑓 “ suc 𝐴))
3529, 32, 343eqtr3a 2197 . . . . . . . . 9 (𝑓:suc 𝐴1-1-onto→suc 𝐵 → suc 𝐵 = (𝑓 “ suc 𝐴))
3635difeq1d 3199 . . . . . . . 8 (𝑓:suc 𝐴1-1-onto→suc 𝐵 → (suc 𝐵 ∖ {(𝑓𝐴)}) = ((𝑓 “ suc 𝐴) ∖ {(𝑓𝐴)}))
3736adantl 275 . . . . . . 7 ((((𝐴 ∈ On ∧ 𝐵 ∈ ω) ∧ suc 𝐴 ≈ suc 𝐵) ∧ 𝑓:suc 𝐴1-1-onto→suc 𝐵) → (suc 𝐵 ∖ {(𝑓𝐴)}) = ((𝑓 “ suc 𝐴) ∖ {(𝑓𝐴)}))
38 dff1o3 5384 . . . . . . . . . 10 (𝑓:suc 𝐴1-1-onto→suc 𝐵 ↔ (𝑓:suc 𝐴onto→suc 𝐵 ∧ Fun 𝑓))
3938simprbi 273 . . . . . . . . 9 (𝑓:suc 𝐴1-1-onto→suc 𝐵 → Fun 𝑓)
40 imadif 5214 . . . . . . . . 9 (Fun 𝑓 → (𝑓 “ (suc 𝐴 ∖ {𝐴})) = ((𝑓 “ suc 𝐴) ∖ (𝑓 “ {𝐴})))
4139, 40syl 14 . . . . . . . 8 (𝑓:suc 𝐴1-1-onto→suc 𝐵 → (𝑓 “ (suc 𝐴 ∖ {𝐴})) = ((𝑓 “ suc 𝐴) ∖ (𝑓 “ {𝐴})))
4241adantl 275 . . . . . . 7 ((((𝐴 ∈ On ∧ 𝐵 ∈ ω) ∧ suc 𝐴 ≈ suc 𝐵) ∧ 𝑓:suc 𝐴1-1-onto→suc 𝐵) → (𝑓 “ (suc 𝐴 ∖ {𝐴})) = ((𝑓 “ suc 𝐴) ∖ (𝑓 “ {𝐴})))
4327, 37, 423eqtr4rd 2184 . . . . . 6 ((((𝐴 ∈ On ∧ 𝐵 ∈ ω) ∧ suc 𝐴 ≈ suc 𝐵) ∧ 𝑓:suc 𝐴1-1-onto→suc 𝐵) → (𝑓 “ (suc 𝐴 ∖ {𝐴})) = (suc 𝐵 ∖ {(𝑓𝐴)}))
4420, 43eqtrd 2173 . . . . 5 ((((𝐴 ∈ On ∧ 𝐵 ∈ ω) ∧ suc 𝐴 ≈ suc 𝐵) ∧ 𝑓:suc 𝐴1-1-onto→suc 𝐵) → (𝑓𝐴) = (suc 𝐵 ∖ {(𝑓𝐴)}))
4515, 44breqtrd 3963 . . . 4 ((((𝐴 ∈ On ∧ 𝐵 ∈ ω) ∧ suc 𝐴 ≈ suc 𝐵) ∧ 𝑓:suc 𝐴1-1-onto→suc 𝐵) → 𝐴 ≈ (suc 𝐵 ∖ {(𝑓𝐴)}))
46 simpllr 524 . . . . . 6 ((((𝐴 ∈ On ∧ 𝐵 ∈ ω) ∧ suc 𝐴 ≈ suc 𝐵) ∧ 𝑓:suc 𝐴1-1-onto→suc 𝐵) → 𝐵 ∈ ω)
47 fnfvelrn 5563 . . . . . . . 8 ((𝑓 Fn suc 𝐴𝐴 ∈ suc 𝐴) → (𝑓𝐴) ∈ ran 𝑓)
4822, 24, 47syl2anc 409 . . . . . . 7 ((((𝐴 ∈ On ∧ 𝐵 ∈ ω) ∧ suc 𝐴 ≈ suc 𝐵) ∧ 𝑓:suc 𝐴1-1-onto→suc 𝐵) → (𝑓𝐴) ∈ ran 𝑓)
4931eleq2d 2210 . . . . . . . . 9 (𝑓:suc 𝐴onto→suc 𝐵 → ((𝑓𝐴) ∈ ran 𝑓 ↔ (𝑓𝐴) ∈ suc 𝐵))
5030, 49syl 14 . . . . . . . 8 (𝑓:suc 𝐴1-1-onto→suc 𝐵 → ((𝑓𝐴) ∈ ran 𝑓 ↔ (𝑓𝐴) ∈ suc 𝐵))
5150adantl 275 . . . . . . 7 ((((𝐴 ∈ On ∧ 𝐵 ∈ ω) ∧ suc 𝐴 ≈ suc 𝐵) ∧ 𝑓:suc 𝐴1-1-onto→suc 𝐵) → ((𝑓𝐴) ∈ ran 𝑓 ↔ (𝑓𝐴) ∈ suc 𝐵))
5248, 51mpbid 146 . . . . . 6 ((((𝐴 ∈ On ∧ 𝐵 ∈ ω) ∧ suc 𝐴 ≈ suc 𝐵) ∧ 𝑓:suc 𝐴1-1-onto→suc 𝐵) → (𝑓𝐴) ∈ suc 𝐵)
53 phplem3g 6761 . . . . . 6 ((𝐵 ∈ ω ∧ (𝑓𝐴) ∈ suc 𝐵) → 𝐵 ≈ (suc 𝐵 ∖ {(𝑓𝐴)}))
5446, 52, 53syl2anc 409 . . . . 5 ((((𝐴 ∈ On ∧ 𝐵 ∈ ω) ∧ suc 𝐴 ≈ suc 𝐵) ∧ 𝑓:suc 𝐴1-1-onto→suc 𝐵) → 𝐵 ≈ (suc 𝐵 ∖ {(𝑓𝐴)}))
5554ensymd 6688 . . . 4 ((((𝐴 ∈ On ∧ 𝐵 ∈ ω) ∧ suc 𝐴 ≈ suc 𝐵) ∧ 𝑓:suc 𝐴1-1-onto→suc 𝐵) → (suc 𝐵 ∖ {(𝑓𝐴)}) ≈ 𝐵)
56 entr 6689 . . . 4 ((𝐴 ≈ (suc 𝐵 ∖ {(𝑓𝐴)}) ∧ (suc 𝐵 ∖ {(𝑓𝐴)}) ≈ 𝐵) → 𝐴𝐵)
5745, 55, 56syl2anc 409 . . 3 ((((𝐴 ∈ On ∧ 𝐵 ∈ ω) ∧ suc 𝐴 ≈ suc 𝐵) ∧ 𝑓:suc 𝐴1-1-onto→suc 𝐵) → 𝐴𝐵)
583, 57exlimddv 1871 . 2 (((𝐴 ∈ On ∧ 𝐵 ∈ ω) ∧ suc 𝐴 ≈ suc 𝐵) → 𝐴𝐵)
5958ex 114 1 ((𝐴 ∈ On ∧ 𝐵 ∈ ω) → (suc 𝐴 ≈ suc 𝐵𝐴𝐵))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104   = wceq 1332  ∃wex 1469   ∈ wcel 1481   ∖ cdif 3074   ⊆ wss 3077  {csn 3533   class class class wbr 3938  Ord word 4294  Oncon0 4295  suc csuc 4297  ωcom 4514  ◡ccnv 4549  dom cdm 4550  ran crn 4551   “ cima 4553  Fun wfun 5128   Fn wfn 5129  –1-1→wf1 5131  –onto→wfo 5132  –1-1-onto→wf1o 5133  ‘cfv 5134   ≈ cen 6643 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-13 1492  ax-14 1493  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122  ax-sep 4055  ax-nul 4063  ax-pow 4107  ax-pr 4141  ax-un 4365  ax-setind 4462  ax-iinf 4512 This theorem depends on definitions:  df-bi 116  df-dc 821  df-3or 964  df-3an 965  df-tru 1335  df-fal 1338  df-nf 1438  df-sb 1737  df-eu 2003  df-mo 2004  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-ne 2310  df-ral 2422  df-rex 2423  df-rab 2426  df-v 2692  df-sbc 2915  df-dif 3079  df-un 3081  df-in 3083  df-ss 3090  df-nul 3370  df-pw 3518  df-sn 3539  df-pr 3540  df-op 3542  df-uni 3746  df-int 3781  df-br 3939  df-opab 3999  df-tr 4036  df-id 4225  df-iord 4298  df-on 4300  df-suc 4303  df-iom 4515  df-xp 4556  df-rel 4557  df-cnv 4558  df-co 4559  df-dm 4560  df-rn 4561  df-res 4562  df-ima 4563  df-iota 5099  df-fun 5136  df-fn 5137  df-f 5138  df-f1 5139  df-fo 5140  df-f1o 5141  df-fv 5142  df-er 6440  df-en 6646 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator