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

Theorem ackbij1lem5 9159
Description: Lemma for ackbij2 9178. (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 5903 . . . . 5 (𝑎 = 𝐴 → suc 𝑎 = suc 𝐴)
21pweqd 4271 . . . 4 (𝑎 = 𝐴 → 𝒫 suc 𝑎 = 𝒫 suc 𝐴)
32fveq2d 6308 . . 3 (𝑎 = 𝐴 → (card‘𝒫 suc 𝑎) = (card‘𝒫 suc 𝐴))
4 pweq 4269 . . . . 5 (𝑎 = 𝐴 → 𝒫 𝑎 = 𝒫 𝐴)
54fveq2d 6308 . . . 4 (𝑎 = 𝐴 → (card‘𝒫 𝑎) = (card‘𝒫 𝐴))
65, 5oveq12d 6783 . . 3 (𝑎 = 𝐴 → ((card‘𝒫 𝑎) +𝑜 (card‘𝒫 𝑎)) = ((card‘𝒫 𝐴) +𝑜 (card‘𝒫 𝐴)))
73, 6eqeq12d 2739 . 2 (𝑎 = 𝐴 → ((card‘𝒫 suc 𝑎) = ((card‘𝒫 𝑎) +𝑜 (card‘𝒫 𝑎)) ↔ (card‘𝒫 suc 𝐴) = ((card‘𝒫 𝐴) +𝑜 (card‘𝒫 𝐴))))
8 vex 3307 . . . . . . . . 9 𝑎 ∈ V
98sucex 7128 . . . . . . . 8 suc 𝑎 ∈ V
109pw2en 8183 . . . . . . 7 𝒫 suc 𝑎 ≈ (2𝑜𝑚 suc 𝑎)
11 df-suc 5842 . . . . . . . . . 10 suc 𝑎 = (𝑎 ∪ {𝑎})
1211oveq2i 6776 . . . . . . . . 9 (2𝑜𝑚 suc 𝑎) = (2𝑜𝑚 (𝑎 ∪ {𝑎}))
13 nnord 7190 . . . . . . . . . . 11 (𝑎 ∈ ω → Ord 𝑎)
14 orddisj 5875 . . . . . . . . . . 11 (Ord 𝑎 → (𝑎 ∩ {𝑎}) = ∅)
15 snex 5013 . . . . . . . . . . . 12 {𝑎} ∈ V
16 2onn 7840 . . . . . . . . . . . . 13 2𝑜 ∈ ω
1716elexi 3317 . . . . . . . . . . . 12 2𝑜 ∈ V
18 mapunen 8245 . . . . . . . . . . . . 13 (((𝑎 ∈ V ∧ {𝑎} ∈ V ∧ 2𝑜 ∈ V) ∧ (𝑎 ∩ {𝑎}) = ∅) → (2𝑜𝑚 (𝑎 ∪ {𝑎})) ≈ ((2𝑜𝑚 𝑎) × (2𝑜𝑚 {𝑎})))
1918ex 449 . . . . . . . . . . . 12 ((𝑎 ∈ V ∧ {𝑎} ∈ V ∧ 2𝑜 ∈ V) → ((𝑎 ∩ {𝑎}) = ∅ → (2𝑜𝑚 (𝑎 ∪ {𝑎})) ≈ ((2𝑜𝑚 𝑎) × (2𝑜𝑚 {𝑎}))))
208, 15, 17, 19mp3an 1537 . . . . . . . . . . 11 ((𝑎 ∩ {𝑎}) = ∅ → (2𝑜𝑚 (𝑎 ∪ {𝑎})) ≈ ((2𝑜𝑚 𝑎) × (2𝑜𝑚 {𝑎})))
2113, 14, 203syl 18 . . . . . . . . . 10 (𝑎 ∈ ω → (2𝑜𝑚 (𝑎 ∪ {𝑎})) ≈ ((2𝑜𝑚 𝑎) × (2𝑜𝑚 {𝑎})))
22 ovex 6793 . . . . . . . . . . . 12 (2𝑜𝑚 𝑎) ∈ V
2322enref 8105 . . . . . . . . . . 11 (2𝑜𝑚 𝑎) ≈ (2𝑜𝑚 𝑎)
2417, 8mapsnen 8151 . . . . . . . . . . 11 (2𝑜𝑚 {𝑎}) ≈ 2𝑜
25 xpen 8239 . . . . . . . . . . 11 (((2𝑜𝑚 𝑎) ≈ (2𝑜𝑚 𝑎) ∧ (2𝑜𝑚 {𝑎}) ≈ 2𝑜) → ((2𝑜𝑚 𝑎) × (2𝑜𝑚 {𝑎})) ≈ ((2𝑜𝑚 𝑎) × 2𝑜))
2623, 24, 25mp2an 710 . . . . . . . . . 10 ((2𝑜𝑚 𝑎) × (2𝑜𝑚 {𝑎})) ≈ ((2𝑜𝑚 𝑎) × 2𝑜)
27 entr 8124 . . . . . . . . . 10 (((2𝑜𝑚 (𝑎 ∪ {𝑎})) ≈ ((2𝑜𝑚 𝑎) × (2𝑜𝑚 {𝑎})) ∧ ((2𝑜𝑚 𝑎) × (2𝑜𝑚 {𝑎})) ≈ ((2𝑜𝑚 𝑎) × 2𝑜)) → (2𝑜𝑚 (𝑎 ∪ {𝑎})) ≈ ((2𝑜𝑚 𝑎) × 2𝑜))
2821, 26, 27sylancl 697 . . . . . . . . 9 (𝑎 ∈ ω → (2𝑜𝑚 (𝑎 ∪ {𝑎})) ≈ ((2𝑜𝑚 𝑎) × 2𝑜))
2912, 28syl5eqbr 4795 . . . . . . . 8 (𝑎 ∈ ω → (2𝑜𝑚 suc 𝑎) ≈ ((2𝑜𝑚 𝑎) × 2𝑜))
308pw2en 8183 . . . . . . . . . 10 𝒫 𝑎 ≈ (2𝑜𝑚 𝑎)
3117enref 8105 . . . . . . . . . 10 2𝑜 ≈ 2𝑜
32 xpen 8239 . . . . . . . . . 10 ((𝒫 𝑎 ≈ (2𝑜𝑚 𝑎) ∧ 2𝑜 ≈ 2𝑜) → (𝒫 𝑎 × 2𝑜) ≈ ((2𝑜𝑚 𝑎) × 2𝑜))
3330, 31, 32mp2an 710 . . . . . . . . 9 (𝒫 𝑎 × 2𝑜) ≈ ((2𝑜𝑚 𝑎) × 2𝑜)
3433ensymi 8122 . . . . . . . 8 ((2𝑜𝑚 𝑎) × 2𝑜) ≈ (𝒫 𝑎 × 2𝑜)
35 entr 8124 . . . . . . . 8 (((2𝑜𝑚 suc 𝑎) ≈ ((2𝑜𝑚 𝑎) × 2𝑜) ∧ ((2𝑜𝑚 𝑎) × 2𝑜) ≈ (𝒫 𝑎 × 2𝑜)) → (2𝑜𝑚 suc 𝑎) ≈ (𝒫 𝑎 × 2𝑜))
3629, 34, 35sylancl 697 . . . . . . 7 (𝑎 ∈ ω → (2𝑜𝑚 suc 𝑎) ≈ (𝒫 𝑎 × 2𝑜))
37 entr 8124 . . . . . . 7 ((𝒫 suc 𝑎 ≈ (2𝑜𝑚 suc 𝑎) ∧ (2𝑜𝑚 suc 𝑎) ≈ (𝒫 𝑎 × 2𝑜)) → 𝒫 suc 𝑎 ≈ (𝒫 𝑎 × 2𝑜))
3810, 36, 37sylancr 698 . . . . . 6 (𝑎 ∈ ω → 𝒫 suc 𝑎 ≈ (𝒫 𝑎 × 2𝑜))
39 vpwex 4954 . . . . . . 7 𝒫 𝑎 ∈ V
40 xp2cda 9115 . . . . . . 7 (𝒫 𝑎 ∈ V → (𝒫 𝑎 × 2𝑜) = (𝒫 𝑎 +𝑐 𝒫 𝑎))
4139, 40ax-mp 5 . . . . . 6 (𝒫 𝑎 × 2𝑜) = (𝒫 𝑎 +𝑐 𝒫 𝑎)
4238, 41syl6breq 4801 . . . . 5 (𝑎 ∈ ω → 𝒫 suc 𝑎 ≈ (𝒫 𝑎 +𝑐 𝒫 𝑎))
43 nnfi 8269 . . . . . . . . 9 (𝑎 ∈ ω → 𝑎 ∈ Fin)
44 pwfi 8377 . . . . . . . . 9 (𝑎 ∈ Fin ↔ 𝒫 𝑎 ∈ Fin)
4543, 44sylib 208 . . . . . . . 8 (𝑎 ∈ ω → 𝒫 𝑎 ∈ Fin)
46 ficardid 8901 . . . . . . . 8 (𝒫 𝑎 ∈ Fin → (card‘𝒫 𝑎) ≈ 𝒫 𝑎)
4745, 46syl 17 . . . . . . 7 (𝑎 ∈ ω → (card‘𝒫 𝑎) ≈ 𝒫 𝑎)
48 cdaen 9108 . . . . . . 7 (((card‘𝒫 𝑎) ≈ 𝒫 𝑎 ∧ (card‘𝒫 𝑎) ≈ 𝒫 𝑎) → ((card‘𝒫 𝑎) +𝑐 (card‘𝒫 𝑎)) ≈ (𝒫 𝑎 +𝑐 𝒫 𝑎))
4947, 47, 48syl2anc 696 . . . . . 6 (𝑎 ∈ ω → ((card‘𝒫 𝑎) +𝑐 (card‘𝒫 𝑎)) ≈ (𝒫 𝑎 +𝑐 𝒫 𝑎))
5049ensymd 8123 . . . . 5 (𝑎 ∈ ω → (𝒫 𝑎 +𝑐 𝒫 𝑎) ≈ ((card‘𝒫 𝑎) +𝑐 (card‘𝒫 𝑎)))
51 entr 8124 . . . . 5 ((𝒫 suc 𝑎 ≈ (𝒫 𝑎 +𝑐 𝒫 𝑎) ∧ (𝒫 𝑎 +𝑐 𝒫 𝑎) ≈ ((card‘𝒫 𝑎) +𝑐 (card‘𝒫 𝑎))) → 𝒫 suc 𝑎 ≈ ((card‘𝒫 𝑎) +𝑐 (card‘𝒫 𝑎)))
5242, 50, 51syl2anc 696 . . . 4 (𝑎 ∈ ω → 𝒫 suc 𝑎 ≈ ((card‘𝒫 𝑎) +𝑐 (card‘𝒫 𝑎)))
53 carden2b 8906 . . . 4 (𝒫 suc 𝑎 ≈ ((card‘𝒫 𝑎) +𝑐 (card‘𝒫 𝑎)) → (card‘𝒫 suc 𝑎) = (card‘((card‘𝒫 𝑎) +𝑐 (card‘𝒫 𝑎))))
5452, 53syl 17 . . 3 (𝑎 ∈ ω → (card‘𝒫 suc 𝑎) = (card‘((card‘𝒫 𝑎) +𝑐 (card‘𝒫 𝑎))))
55 ficardom 8900 . . . . 5 (𝒫 𝑎 ∈ Fin → (card‘𝒫 𝑎) ∈ ω)
5645, 55syl 17 . . . 4 (𝑎 ∈ ω → (card‘𝒫 𝑎) ∈ ω)
57 nnacda 9136 . . . 4 (((card‘𝒫 𝑎) ∈ ω ∧ (card‘𝒫 𝑎) ∈ ω) → (card‘((card‘𝒫 𝑎) +𝑐 (card‘𝒫 𝑎))) = ((card‘𝒫 𝑎) +𝑜 (card‘𝒫 𝑎)))
5856, 56, 57syl2anc 696 . . 3 (𝑎 ∈ ω → (card‘((card‘𝒫 𝑎) +𝑐 (card‘𝒫 𝑎))) = ((card‘𝒫 𝑎) +𝑜 (card‘𝒫 𝑎)))
5954, 58eqtrd 2758 . 2 (𝑎 ∈ ω → (card‘𝒫 suc 𝑎) = ((card‘𝒫 𝑎) +𝑜 (card‘𝒫 𝑎)))
607, 59vtoclga 3376 1 (𝐴 ∈ ω → (card‘𝒫 suc 𝐴) = ((card‘𝒫 𝐴) +𝑜 (card‘𝒫 𝐴)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1072   = wceq 1596  wcel 2103  Vcvv 3304  cun 3678  cin 3679  c0 4023  𝒫 cpw 4266  {csn 4285   class class class wbr 4760   × cxp 5216  Ord word 5835  suc csuc 5838  cfv 6001  (class class class)co 6765  ωcom 7182  2𝑜c2o 7674   +𝑜 coa 7677  𝑚 cmap 7974  cen 8069  Fincfn 8072  cardccrd 8874   +𝑐 ccda 9102
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1835  ax-4 1850  ax-5 1952  ax-6 2018  ax-7 2054  ax-8 2105  ax-9 2112  ax-10 2132  ax-11 2147  ax-12 2160  ax-13 2355  ax-ext 2704  ax-rep 4879  ax-sep 4889  ax-nul 4897  ax-pow 4948  ax-pr 5011  ax-un 7066
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1599  df-ex 1818  df-nf 1823  df-sb 2011  df-eu 2575  df-mo 2576  df-clab 2711  df-cleq 2717  df-clel 2720  df-nfc 2855  df-ne 2897  df-ral 3019  df-rex 3020  df-reu 3021  df-rmo 3022  df-rab 3023  df-v 3306  df-sbc 3542  df-csb 3640  df-dif 3683  df-un 3685  df-in 3687  df-ss 3694  df-pss 3696  df-nul 4024  df-if 4195  df-pw 4268  df-sn 4286  df-pr 4288  df-tp 4290  df-op 4292  df-uni 4545  df-int 4584  df-iun 4630  df-br 4761  df-opab 4821  df-mpt 4838  df-tr 4861  df-id 5128  df-eprel 5133  df-po 5139  df-so 5140  df-fr 5177  df-we 5179  df-xp 5224  df-rel 5225  df-cnv 5226  df-co 5227  df-dm 5228  df-rn 5229  df-res 5230  df-ima 5231  df-pred 5793  df-ord 5839  df-on 5840  df-lim 5841  df-suc 5842  df-iota 5964  df-fun 6003  df-fn 6004  df-f 6005  df-f1 6006  df-fo 6007  df-f1o 6008  df-fv 6009  df-ov 6768  df-oprab 6769  df-mpt2 6770  df-om 7183  df-1st 7285  df-2nd 7286  df-wrecs 7527  df-recs 7588  df-rdg 7626  df-1o 7680  df-2o 7681  df-oadd 7684  df-er 7862  df-map 7976  df-en 8073  df-dom 8074  df-sdom 8075  df-fin 8076  df-card 8878  df-cda 9103
This theorem is referenced by:  ackbij1lem14  9168
  Copyright terms: Public domain W3C validator