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

Theorem ackbij1lem5 9640
 Description: Lemma for ackbij2 9659. (Contributed by Stefan O'Rear, 19-Nov-2014.) (Proof shortened by AV, 18-Jul-2022.)
Assertion
Ref Expression
ackbij1lem5 (𝐴 ∈ ω → (card‘𝒫 suc 𝐴) = ((card‘𝒫 𝐴) +o (card‘𝒫 𝐴)))

Proof of Theorem ackbij1lem5
StepHypRef Expression
1 peano2 7596 . . . . . . 7 (𝐴 ∈ ω → suc 𝐴 ∈ ω)
2 pw2eng 8617 . . . . . . 7 (suc 𝐴 ∈ ω → 𝒫 suc 𝐴 ≈ (2om suc 𝐴))
31, 2syl 17 . . . . . 6 (𝐴 ∈ ω → 𝒫 suc 𝐴 ≈ (2om suc 𝐴))
4 df-suc 6191 . . . . . . . . . 10 suc 𝐴 = (𝐴 ∪ {𝐴})
54oveq2i 7161 . . . . . . . . 9 (2om suc 𝐴) = (2om (𝐴 ∪ {𝐴}))
6 elex 3512 . . . . . . . . . . 11 (𝐴 ∈ ω → 𝐴 ∈ V)
7 snex 5323 . . . . . . . . . . . 12 {𝐴} ∈ V
87a1i 11 . . . . . . . . . . 11 (𝐴 ∈ ω → {𝐴} ∈ V)
9 2onn 8260 . . . . . . . . . . . . 13 2o ∈ ω
109elexi 3513 . . . . . . . . . . . 12 2o ∈ V
1110a1i 11 . . . . . . . . . . 11 (𝐴 ∈ ω → 2o ∈ V)
12 nnord 7582 . . . . . . . . . . . 12 (𝐴 ∈ ω → Ord 𝐴)
13 orddisj 6223 . . . . . . . . . . . 12 (Ord 𝐴 → (𝐴 ∩ {𝐴}) = ∅)
1412, 13syl 17 . . . . . . . . . . 11 (𝐴 ∈ ω → (𝐴 ∩ {𝐴}) = ∅)
15 mapunen 8680 . . . . . . . . . . 11 (((𝐴 ∈ V ∧ {𝐴} ∈ V ∧ 2o ∈ V) ∧ (𝐴 ∩ {𝐴}) = ∅) → (2om (𝐴 ∪ {𝐴})) ≈ ((2om 𝐴) × (2om {𝐴})))
166, 8, 11, 14, 15syl31anc 1369 . . . . . . . . . 10 (𝐴 ∈ ω → (2om (𝐴 ∪ {𝐴})) ≈ ((2om 𝐴) × (2om {𝐴})))
17 ovex 7183 . . . . . . . . . . . 12 (2om 𝐴) ∈ V
1817enref 8536 . . . . . . . . . . 11 (2om 𝐴) ≈ (2om 𝐴)
19 2on 8105 . . . . . . . . . . . . 13 2o ∈ On
2019a1i 11 . . . . . . . . . . . 12 (𝐴 ∈ ω → 2o ∈ On)
21 id 22 . . . . . . . . . . . 12 (𝐴 ∈ ω → 𝐴 ∈ ω)
2220, 21mapsnend 8582 . . . . . . . . . . 11 (𝐴 ∈ ω → (2om {𝐴}) ≈ 2o)
23 xpen 8674 . . . . . . . . . . 11 (((2om 𝐴) ≈ (2om 𝐴) ∧ (2om {𝐴}) ≈ 2o) → ((2om 𝐴) × (2om {𝐴})) ≈ ((2om 𝐴) × 2o))
2418, 22, 23sylancr 589 . . . . . . . . . 10 (𝐴 ∈ ω → ((2om 𝐴) × (2om {𝐴})) ≈ ((2om 𝐴) × 2o))
25 entr 8555 . . . . . . . . . 10 (((2om (𝐴 ∪ {𝐴})) ≈ ((2om 𝐴) × (2om {𝐴})) ∧ ((2om 𝐴) × (2om {𝐴})) ≈ ((2om 𝐴) × 2o)) → (2om (𝐴 ∪ {𝐴})) ≈ ((2om 𝐴) × 2o))
2616, 24, 25syl2anc 586 . . . . . . . . 9 (𝐴 ∈ ω → (2om (𝐴 ∪ {𝐴})) ≈ ((2om 𝐴) × 2o))
275, 26eqbrtrid 5093 . . . . . . . 8 (𝐴 ∈ ω → (2om suc 𝐴) ≈ ((2om 𝐴) × 2o))
2817, 10xpcomen 8602 . . . . . . . 8 ((2om 𝐴) × 2o) ≈ (2o × (2om 𝐴))
29 entr 8555 . . . . . . . 8 (((2om suc 𝐴) ≈ ((2om 𝐴) × 2o) ∧ ((2om 𝐴) × 2o) ≈ (2o × (2om 𝐴))) → (2om suc 𝐴) ≈ (2o × (2om 𝐴)))
3027, 28, 29sylancl 588 . . . . . . 7 (𝐴 ∈ ω → (2om suc 𝐴) ≈ (2o × (2om 𝐴)))
3110enref 8536 . . . . . . . . 9 2o ≈ 2o
32 pw2eng 8617 . . . . . . . . 9 (𝐴 ∈ ω → 𝒫 𝐴 ≈ (2om 𝐴))
33 xpen 8674 . . . . . . . . 9 ((2o ≈ 2o ∧ 𝒫 𝐴 ≈ (2om 𝐴)) → (2o × 𝒫 𝐴) ≈ (2o × (2om 𝐴)))
3431, 32, 33sylancr 589 . . . . . . . 8 (𝐴 ∈ ω → (2o × 𝒫 𝐴) ≈ (2o × (2om 𝐴)))
3534ensymd 8554 . . . . . . 7 (𝐴 ∈ ω → (2o × (2om 𝐴)) ≈ (2o × 𝒫 𝐴))
36 entr 8555 . . . . . . 7 (((2om suc 𝐴) ≈ (2o × (2om 𝐴)) ∧ (2o × (2om 𝐴)) ≈ (2o × 𝒫 𝐴)) → (2om suc 𝐴) ≈ (2o × 𝒫 𝐴))
3730, 35, 36syl2anc 586 . . . . . 6 (𝐴 ∈ ω → (2om suc 𝐴) ≈ (2o × 𝒫 𝐴))
38 entr 8555 . . . . . 6 ((𝒫 suc 𝐴 ≈ (2om suc 𝐴) ∧ (2om suc 𝐴) ≈ (2o × 𝒫 𝐴)) → 𝒫 suc 𝐴 ≈ (2o × 𝒫 𝐴))
393, 37, 38syl2anc 586 . . . . 5 (𝐴 ∈ ω → 𝒫 suc 𝐴 ≈ (2o × 𝒫 𝐴))
40 xp2dju 9596 . . . . 5 (2o × 𝒫 𝐴) = (𝒫 𝐴 ⊔ 𝒫 𝐴)
4139, 40breqtrdi 5099 . . . 4 (𝐴 ∈ ω → 𝒫 suc 𝐴 ≈ (𝒫 𝐴 ⊔ 𝒫 𝐴))
42 nnfi 8705 . . . . . . . 8 (𝐴 ∈ ω → 𝐴 ∈ Fin)
43 pwfi 8813 . . . . . . . 8 (𝐴 ∈ Fin ↔ 𝒫 𝐴 ∈ Fin)
4442, 43sylib 220 . . . . . . 7 (𝐴 ∈ ω → 𝒫 𝐴 ∈ Fin)
45 ficardid 9385 . . . . . . 7 (𝒫 𝐴 ∈ Fin → (card‘𝒫 𝐴) ≈ 𝒫 𝐴)
4644, 45syl 17 . . . . . 6 (𝐴 ∈ ω → (card‘𝒫 𝐴) ≈ 𝒫 𝐴)
47 djuen 9589 . . . . . 6 (((card‘𝒫 𝐴) ≈ 𝒫 𝐴 ∧ (card‘𝒫 𝐴) ≈ 𝒫 𝐴) → ((card‘𝒫 𝐴) ⊔ (card‘𝒫 𝐴)) ≈ (𝒫 𝐴 ⊔ 𝒫 𝐴))
4846, 46, 47syl2anc 586 . . . . 5 (𝐴 ∈ ω → ((card‘𝒫 𝐴) ⊔ (card‘𝒫 𝐴)) ≈ (𝒫 𝐴 ⊔ 𝒫 𝐴))
4948ensymd 8554 . . . 4 (𝐴 ∈ ω → (𝒫 𝐴 ⊔ 𝒫 𝐴) ≈ ((card‘𝒫 𝐴) ⊔ (card‘𝒫 𝐴)))
50 entr 8555 . . . 4 ((𝒫 suc 𝐴 ≈ (𝒫 𝐴 ⊔ 𝒫 𝐴) ∧ (𝒫 𝐴 ⊔ 𝒫 𝐴) ≈ ((card‘𝒫 𝐴) ⊔ (card‘𝒫 𝐴))) → 𝒫 suc 𝐴 ≈ ((card‘𝒫 𝐴) ⊔ (card‘𝒫 𝐴)))
5141, 49, 50syl2anc 586 . . 3 (𝐴 ∈ ω → 𝒫 suc 𝐴 ≈ ((card‘𝒫 𝐴) ⊔ (card‘𝒫 𝐴)))
52 carden2b 9390 . . 3 (𝒫 suc 𝐴 ≈ ((card‘𝒫 𝐴) ⊔ (card‘𝒫 𝐴)) → (card‘𝒫 suc 𝐴) = (card‘((card‘𝒫 𝐴) ⊔ (card‘𝒫 𝐴))))
5351, 52syl 17 . 2 (𝐴 ∈ ω → (card‘𝒫 suc 𝐴) = (card‘((card‘𝒫 𝐴) ⊔ (card‘𝒫 𝐴))))
54 ficardom 9384 . . . 4 (𝒫 𝐴 ∈ Fin → (card‘𝒫 𝐴) ∈ ω)
5544, 54syl 17 . . 3 (𝐴 ∈ ω → (card‘𝒫 𝐴) ∈ ω)
56 nnadju 9617 . . 3 (((card‘𝒫 𝐴) ∈ ω ∧ (card‘𝒫 𝐴) ∈ ω) → (card‘((card‘𝒫 𝐴) ⊔ (card‘𝒫 𝐴))) = ((card‘𝒫 𝐴) +o (card‘𝒫 𝐴)))
5755, 55, 56syl2anc 586 . 2 (𝐴 ∈ ω → (card‘((card‘𝒫 𝐴) ⊔ (card‘𝒫 𝐴))) = ((card‘𝒫 𝐴) +o (card‘𝒫 𝐴)))
5853, 57eqtrd 2856 1 (𝐴 ∈ ω → (card‘𝒫 suc 𝐴) = ((card‘𝒫 𝐴) +o (card‘𝒫 𝐴)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   = wceq 1533   ∈ wcel 2110  Vcvv 3494   ∪ cun 3933   ∩ cin 3934  ∅c0 4290  𝒫 cpw 4538  {csn 4560   class class class wbr 5058   × cxp 5547  Ord word 6184  Oncon0 6185  suc csuc 6187  ‘cfv 6349  (class class class)co 7150  ωcom 7574  2oc2o 8090   +o coa 8093   ↑m cmap 8400   ≈ cen 8500  Fincfn 8503   ⊔ cdju 9321  cardccrd 9358 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-rep 5182  ax-sep 5195  ax-nul 5202  ax-pow 5258  ax-pr 5321  ax-un 7455 This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-reu 3145  df-rmo 3146  df-rab 3147  df-v 3496  df-sbc 3772  df-csb 3883  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-pss 3953  df-nul 4291  df-if 4467  df-pw 4540  df-sn 4561  df-pr 4563  df-tp 4565  df-op 4567  df-uni 4832  df-int 4869  df-iun 4913  df-br 5059  df-opab 5121  df-mpt 5139  df-tr 5165  df-id 5454  df-eprel 5459  df-po 5468  df-so 5469  df-fr 5508  df-we 5510  df-xp 5555  df-rel 5556  df-cnv 5557  df-co 5558  df-dm 5559  df-rn 5560  df-res 5561  df-ima 5562  df-pred 6142  df-ord 6188  df-on 6189  df-lim 6190  df-suc 6191  df-iota 6308  df-fun 6351  df-fn 6352  df-f 6353  df-f1 6354  df-fo 6355  df-f1o 6356  df-fv 6357  df-ov 7153  df-oprab 7154  df-mpo 7155  df-om 7575  df-1st 7683  df-2nd 7684  df-wrecs 7941  df-recs 8002  df-rdg 8040  df-1o 8096  df-2o 8097  df-oadd 8100  df-er 8283  df-map 8402  df-en 8504  df-dom 8505  df-sdom 8506  df-fin 8507  df-dju 9324  df-card 9362 This theorem is referenced by:  ackbij1lem14  9649
 Copyright terms: Public domain W3C validator