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

Theorem ackbij1lem5 9006
Description: Lemma for ackbij2 9025. (Contributed by Stefan O'Rear, 19-Nov-2014.)
Assertion
Ref Expression
ackbij1lem5 (𝐴 ∈ ω → (card‘𝒫 suc 𝐴) = ((card‘𝒫 𝐴) +𝑜 (card‘𝒫 𝐴)))

Proof of Theorem ackbij1lem5
Dummy variable 𝑎 is distinct from all other variables.
StepHypRef Expression
1 suceq 5759 . . . . 5 (𝑎 = 𝐴 → suc 𝑎 = suc 𝐴)
21pweqd 4141 . . . 4 (𝑎 = 𝐴 → 𝒫 suc 𝑎 = 𝒫 suc 𝐴)
32fveq2d 6162 . . 3 (𝑎 = 𝐴 → (card‘𝒫 suc 𝑎) = (card‘𝒫 suc 𝐴))
4 pweq 4139 . . . . 5 (𝑎 = 𝐴 → 𝒫 𝑎 = 𝒫 𝐴)
54fveq2d 6162 . . . 4 (𝑎 = 𝐴 → (card‘𝒫 𝑎) = (card‘𝒫 𝐴))
65, 5oveq12d 6633 . . 3 (𝑎 = 𝐴 → ((card‘𝒫 𝑎) +𝑜 (card‘𝒫 𝑎)) = ((card‘𝒫 𝐴) +𝑜 (card‘𝒫 𝐴)))
73, 6eqeq12d 2636 . 2 (𝑎 = 𝐴 → ((card‘𝒫 suc 𝑎) = ((card‘𝒫 𝑎) +𝑜 (card‘𝒫 𝑎)) ↔ (card‘𝒫 suc 𝐴) = ((card‘𝒫 𝐴) +𝑜 (card‘𝒫 𝐴))))
8 vex 3193 . . . . . . . . 9 𝑎 ∈ V
98sucex 6973 . . . . . . . 8 suc 𝑎 ∈ V
109pw2en 8027 . . . . . . 7 𝒫 suc 𝑎 ≈ (2𝑜𝑚 suc 𝑎)
11 df-suc 5698 . . . . . . . . . 10 suc 𝑎 = (𝑎 ∪ {𝑎})
1211oveq2i 6626 . . . . . . . . 9 (2𝑜𝑚 suc 𝑎) = (2𝑜𝑚 (𝑎 ∪ {𝑎}))
13 nnord 7035 . . . . . . . . . . 11 (𝑎 ∈ ω → Ord 𝑎)
14 orddisj 5731 . . . . . . . . . . 11 (Ord 𝑎 → (𝑎 ∩ {𝑎}) = ∅)
15 snex 4879 . . . . . . . . . . . 12 {𝑎} ∈ V
16 2onn 7680 . . . . . . . . . . . . 13 2𝑜 ∈ ω
1716elexi 3203 . . . . . . . . . . . 12 2𝑜 ∈ V
18 mapunen 8089 . . . . . . . . . . . . 13 (((𝑎 ∈ V ∧ {𝑎} ∈ V ∧ 2𝑜 ∈ V) ∧ (𝑎 ∩ {𝑎}) = ∅) → (2𝑜𝑚 (𝑎 ∪ {𝑎})) ≈ ((2𝑜𝑚 𝑎) × (2𝑜𝑚 {𝑎})))
1918ex 450 . . . . . . . . . . . 12 ((𝑎 ∈ V ∧ {𝑎} ∈ V ∧ 2𝑜 ∈ V) → ((𝑎 ∩ {𝑎}) = ∅ → (2𝑜𝑚 (𝑎 ∪ {𝑎})) ≈ ((2𝑜𝑚 𝑎) × (2𝑜𝑚 {𝑎}))))
208, 15, 17, 19mp3an 1421 . . . . . . . . . . 11 ((𝑎 ∩ {𝑎}) = ∅ → (2𝑜𝑚 (𝑎 ∪ {𝑎})) ≈ ((2𝑜𝑚 𝑎) × (2𝑜𝑚 {𝑎})))
2113, 14, 203syl 18 . . . . . . . . . 10 (𝑎 ∈ ω → (2𝑜𝑚 (𝑎 ∪ {𝑎})) ≈ ((2𝑜𝑚 𝑎) × (2𝑜𝑚 {𝑎})))
22 ovex 6643 . . . . . . . . . . . 12 (2𝑜𝑚 𝑎) ∈ V
2322enref 7948 . . . . . . . . . . 11 (2𝑜𝑚 𝑎) ≈ (2𝑜𝑚 𝑎)
2417, 8mapsnen 7995 . . . . . . . . . . 11 (2𝑜𝑚 {𝑎}) ≈ 2𝑜
25 xpen 8083 . . . . . . . . . . 11 (((2𝑜𝑚 𝑎) ≈ (2𝑜𝑚 𝑎) ∧ (2𝑜𝑚 {𝑎}) ≈ 2𝑜) → ((2𝑜𝑚 𝑎) × (2𝑜𝑚 {𝑎})) ≈ ((2𝑜𝑚 𝑎) × 2𝑜))
2623, 24, 25mp2an 707 . . . . . . . . . 10 ((2𝑜𝑚 𝑎) × (2𝑜𝑚 {𝑎})) ≈ ((2𝑜𝑚 𝑎) × 2𝑜)
27 entr 7968 . . . . . . . . . 10 (((2𝑜𝑚 (𝑎 ∪ {𝑎})) ≈ ((2𝑜𝑚 𝑎) × (2𝑜𝑚 {𝑎})) ∧ ((2𝑜𝑚 𝑎) × (2𝑜𝑚 {𝑎})) ≈ ((2𝑜𝑚 𝑎) × 2𝑜)) → (2𝑜𝑚 (𝑎 ∪ {𝑎})) ≈ ((2𝑜𝑚 𝑎) × 2𝑜))
2821, 26, 27sylancl 693 . . . . . . . . 9 (𝑎 ∈ ω → (2𝑜𝑚 (𝑎 ∪ {𝑎})) ≈ ((2𝑜𝑚 𝑎) × 2𝑜))
2912, 28syl5eqbr 4658 . . . . . . . 8 (𝑎 ∈ ω → (2𝑜𝑚 suc 𝑎) ≈ ((2𝑜𝑚 𝑎) × 2𝑜))
308pw2en 8027 . . . . . . . . . 10 𝒫 𝑎 ≈ (2𝑜𝑚 𝑎)
3117enref 7948 . . . . . . . . . 10 2𝑜 ≈ 2𝑜
32 xpen 8083 . . . . . . . . . 10 ((𝒫 𝑎 ≈ (2𝑜𝑚 𝑎) ∧ 2𝑜 ≈ 2𝑜) → (𝒫 𝑎 × 2𝑜) ≈ ((2𝑜𝑚 𝑎) × 2𝑜))
3330, 31, 32mp2an 707 . . . . . . . . 9 (𝒫 𝑎 × 2𝑜) ≈ ((2𝑜𝑚 𝑎) × 2𝑜)
3433ensymi 7966 . . . . . . . 8 ((2𝑜𝑚 𝑎) × 2𝑜) ≈ (𝒫 𝑎 × 2𝑜)
35 entr 7968 . . . . . . . 8 (((2𝑜𝑚 suc 𝑎) ≈ ((2𝑜𝑚 𝑎) × 2𝑜) ∧ ((2𝑜𝑚 𝑎) × 2𝑜) ≈ (𝒫 𝑎 × 2𝑜)) → (2𝑜𝑚 suc 𝑎) ≈ (𝒫 𝑎 × 2𝑜))
3629, 34, 35sylancl 693 . . . . . . 7 (𝑎 ∈ ω → (2𝑜𝑚 suc 𝑎) ≈ (𝒫 𝑎 × 2𝑜))
37 entr 7968 . . . . . . 7 ((𝒫 suc 𝑎 ≈ (2𝑜𝑚 suc 𝑎) ∧ (2𝑜𝑚 suc 𝑎) ≈ (𝒫 𝑎 × 2𝑜)) → 𝒫 suc 𝑎 ≈ (𝒫 𝑎 × 2𝑜))
3810, 36, 37sylancr 694 . . . . . 6 (𝑎 ∈ ω → 𝒫 suc 𝑎 ≈ (𝒫 𝑎 × 2𝑜))
39 vpwex 4819 . . . . . . 7 𝒫 𝑎 ∈ V
40 xp2cda 8962 . . . . . . 7 (𝒫 𝑎 ∈ V → (𝒫 𝑎 × 2𝑜) = (𝒫 𝑎 +𝑐 𝒫 𝑎))
4139, 40ax-mp 5 . . . . . 6 (𝒫 𝑎 × 2𝑜) = (𝒫 𝑎 +𝑐 𝒫 𝑎)
4238, 41syl6breq 4664 . . . . 5 (𝑎 ∈ ω → 𝒫 suc 𝑎 ≈ (𝒫 𝑎 +𝑐 𝒫 𝑎))
43 nnfi 8113 . . . . . . . . 9 (𝑎 ∈ ω → 𝑎 ∈ Fin)
44 pwfi 8221 . . . . . . . . 9 (𝑎 ∈ Fin ↔ 𝒫 𝑎 ∈ Fin)
4543, 44sylib 208 . . . . . . . 8 (𝑎 ∈ ω → 𝒫 𝑎 ∈ Fin)
46 ficardid 8748 . . . . . . . 8 (𝒫 𝑎 ∈ Fin → (card‘𝒫 𝑎) ≈ 𝒫 𝑎)
4745, 46syl 17 . . . . . . 7 (𝑎 ∈ ω → (card‘𝒫 𝑎) ≈ 𝒫 𝑎)
48 cdaen 8955 . . . . . . 7 (((card‘𝒫 𝑎) ≈ 𝒫 𝑎 ∧ (card‘𝒫 𝑎) ≈ 𝒫 𝑎) → ((card‘𝒫 𝑎) +𝑐 (card‘𝒫 𝑎)) ≈ (𝒫 𝑎 +𝑐 𝒫 𝑎))
4947, 47, 48syl2anc 692 . . . . . 6 (𝑎 ∈ ω → ((card‘𝒫 𝑎) +𝑐 (card‘𝒫 𝑎)) ≈ (𝒫 𝑎 +𝑐 𝒫 𝑎))
5049ensymd 7967 . . . . 5 (𝑎 ∈ ω → (𝒫 𝑎 +𝑐 𝒫 𝑎) ≈ ((card‘𝒫 𝑎) +𝑐 (card‘𝒫 𝑎)))
51 entr 7968 . . . . 5 ((𝒫 suc 𝑎 ≈ (𝒫 𝑎 +𝑐 𝒫 𝑎) ∧ (𝒫 𝑎 +𝑐 𝒫 𝑎) ≈ ((card‘𝒫 𝑎) +𝑐 (card‘𝒫 𝑎))) → 𝒫 suc 𝑎 ≈ ((card‘𝒫 𝑎) +𝑐 (card‘𝒫 𝑎)))
5242, 50, 51syl2anc 692 . . . 4 (𝑎 ∈ ω → 𝒫 suc 𝑎 ≈ ((card‘𝒫 𝑎) +𝑐 (card‘𝒫 𝑎)))
53 carden2b 8753 . . . 4 (𝒫 suc 𝑎 ≈ ((card‘𝒫 𝑎) +𝑐 (card‘𝒫 𝑎)) → (card‘𝒫 suc 𝑎) = (card‘((card‘𝒫 𝑎) +𝑐 (card‘𝒫 𝑎))))
5452, 53syl 17 . . 3 (𝑎 ∈ ω → (card‘𝒫 suc 𝑎) = (card‘((card‘𝒫 𝑎) +𝑐 (card‘𝒫 𝑎))))
55 ficardom 8747 . . . . 5 (𝒫 𝑎 ∈ Fin → (card‘𝒫 𝑎) ∈ ω)
5645, 55syl 17 . . . 4 (𝑎 ∈ ω → (card‘𝒫 𝑎) ∈ ω)
57 nnacda 8983 . . . 4 (((card‘𝒫 𝑎) ∈ ω ∧ (card‘𝒫 𝑎) ∈ ω) → (card‘((card‘𝒫 𝑎) +𝑐 (card‘𝒫 𝑎))) = ((card‘𝒫 𝑎) +𝑜 (card‘𝒫 𝑎)))
5856, 56, 57syl2anc 692 . . 3 (𝑎 ∈ ω → (card‘((card‘𝒫 𝑎) +𝑐 (card‘𝒫 𝑎))) = ((card‘𝒫 𝑎) +𝑜 (card‘𝒫 𝑎)))
5954, 58eqtrd 2655 . 2 (𝑎 ∈ ω → (card‘𝒫 suc 𝑎) = ((card‘𝒫 𝑎) +𝑜 (card‘𝒫 𝑎)))
607, 59vtoclga 3262 1 (𝐴 ∈ ω → (card‘𝒫 suc 𝐴) = ((card‘𝒫 𝐴) +𝑜 (card‘𝒫 𝐴)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1036   = wceq 1480  wcel 1987  Vcvv 3190  cun 3558  cin 3559  c0 3897  𝒫 cpw 4136  {csn 4155   class class class wbr 4623   × cxp 5082  Ord word 5691  suc csuc 5694  cfv 5857  (class class class)co 6615  ωcom 7027  2𝑜c2o 7514   +𝑜 coa 7517  𝑚 cmap 7817  cen 7912  Fincfn 7915  cardccrd 8721   +𝑐 ccda 8949
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4741  ax-sep 4751  ax-nul 4759  ax-pow 4813  ax-pr 4877  ax-un 6914
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2913  df-rex 2914  df-reu 2915  df-rmo 2916  df-rab 2917  df-v 3192  df-sbc 3423  df-csb 3520  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-pss 3576  df-nul 3898  df-if 4065  df-pw 4138  df-sn 4156  df-pr 4158  df-tp 4160  df-op 4162  df-uni 4410  df-int 4448  df-iun 4494  df-br 4624  df-opab 4684  df-mpt 4685  df-tr 4723  df-eprel 4995  df-id 4999  df-po 5005  df-so 5006  df-fr 5043  df-we 5045  df-xp 5090  df-rel 5091  df-cnv 5092  df-co 5093  df-dm 5094  df-rn 5095  df-res 5096  df-ima 5097  df-pred 5649  df-ord 5695  df-on 5696  df-lim 5697  df-suc 5698  df-iota 5820  df-fun 5859  df-fn 5860  df-f 5861  df-f1 5862  df-fo 5863  df-f1o 5864  df-fv 5865  df-ov 6618  df-oprab 6619  df-mpt2 6620  df-om 7028  df-1st 7128  df-2nd 7129  df-wrecs 7367  df-recs 7428  df-rdg 7466  df-1o 7520  df-2o 7521  df-oadd 7524  df-er 7702  df-map 7819  df-en 7916  df-dom 7917  df-sdom 7918  df-fin 7919  df-card 8725  df-cda 8950
This theorem is referenced by:  ackbij1lem14  9015
  Copyright terms: Public domain W3C validator