Theorem ackbij1lem5 10117

Description: Lemma for ackbij2 10136. (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

Step	Hyp	Ref	Expression
1		peano2 7823	. . . . . . 7 ⊢ (𝐴 ∈ ω → suc 𝐴 ∈ ω)
2		pw2eng 9000	. . . . . . 7 ⊢ (suc 𝐴 ∈ ω → 𝒫 suc 𝐴 ≈ (2o ↑m suc 𝐴))
3	1, 2	syl 17	. . . . . 6 ⊢ (𝐴 ∈ ω → 𝒫 suc 𝐴 ≈ (2o ↑m suc 𝐴))
4		df-suc 6313	. . . . . . . . . 10 ⊢ suc 𝐴 = (𝐴 ∪ {𝐴})
5	4	oveq2i 7360	. . . . . . . . 9 ⊢ (2o ↑m suc 𝐴) = (2o ↑m (𝐴 ∪ {𝐴}))
6		elex 3457	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ω → 𝐴 ∈ V)
7		snex 5375	. . . . . . . . . . . 12 ⊢ {𝐴} ∈ V
8	7	a1i 11	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ω → {𝐴} ∈ V)
9		2onn 8560	. . . . . . . . . . . . 13 ⊢ 2o ∈ ω
10	9	elexi 3459	. . . . . . . . . . . 12 ⊢ 2o ∈ V
11	10	a1i 11	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ω → 2o ∈ V)
12		nnord 7807	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ω → Ord 𝐴)
13		orddisj 6345	. . . . . . . . . . . 12 ⊢ (Ord 𝐴 → (𝐴 ∩ {𝐴}) = ∅)
14	12, 13	syl 17	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ω → (𝐴 ∩ {𝐴}) = ∅)
15		mapunen 9063	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ V ∧ {𝐴} ∈ V ∧ 2o ∈ V) ∧ (𝐴 ∩ {𝐴}) = ∅) → (2o ↑m (𝐴 ∪ {𝐴})) ≈ ((2o ↑m 𝐴) × (2o ↑m {𝐴})))
16	6, 8, 11, 14, 15	syl31anc 1375	. . . . . . . . . 10 ⊢ (𝐴 ∈ ω → (2o ↑m (𝐴 ∪ {𝐴})) ≈ ((2o ↑m 𝐴) × (2o ↑m {𝐴})))
17		ovex 7382	. . . . . . . . . . . 12 ⊢ (2o ↑m 𝐴) ∈ V
18	17	enref 8910	. . . . . . . . . . 11 ⊢ (2o ↑m 𝐴) ≈ (2o ↑m 𝐴)
19		2on 8401	. . . . . . . . . . . . 13 ⊢ 2o ∈ On
20	19	a1i 11	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ω → 2o ∈ On)
21		id 22	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ω → 𝐴 ∈ ω)
22	20, 21	mapsnend 8961	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ω → (2o ↑m {𝐴}) ≈ 2o)
23		xpen 9057	. . . . . . . . . . 11 ⊢ (((2o ↑m 𝐴) ≈ (2o ↑m 𝐴) ∧ (2o ↑m {𝐴}) ≈ 2o) → ((2o ↑m 𝐴) × (2o ↑m {𝐴})) ≈ ((2o ↑m 𝐴) × 2o))
24	18, 22, 23	sylancr 587	. . . . . . . . . 10 ⊢ (𝐴 ∈ ω → ((2o ↑m 𝐴) × (2o ↑m {𝐴})) ≈ ((2o ↑m 𝐴) × 2o))
25		entr 8931	. . . . . . . . . 10 ⊢ (((2o ↑m (𝐴 ∪ {𝐴})) ≈ ((2o ↑m 𝐴) × (2o ↑m {𝐴})) ∧ ((2o ↑m 𝐴) × (2o ↑m {𝐴})) ≈ ((2o ↑m 𝐴) × 2o)) → (2o ↑m (𝐴 ∪ {𝐴})) ≈ ((2o ↑m 𝐴) × 2o))
26	16, 24, 25	syl2anc 584	. . . . . . . . 9 ⊢ (𝐴 ∈ ω → (2o ↑m (𝐴 ∪ {𝐴})) ≈ ((2o ↑m 𝐴) × 2o))
27	5, 26	eqbrtrid 5127	. . . . . . . 8 ⊢ (𝐴 ∈ ω → (2o ↑m suc 𝐴) ≈ ((2o ↑m 𝐴) × 2o))
28	17, 10	xpcomen 8985	. . . . . . . 8 ⊢ ((2o ↑m 𝐴) × 2o) ≈ (2o × (2o ↑m 𝐴))
29		entr 8931	. . . . . . . 8 ⊢ (((2o ↑m suc 𝐴) ≈ ((2o ↑m 𝐴) × 2o) ∧ ((2o ↑m 𝐴) × 2o) ≈ (2o × (2o ↑m 𝐴))) → (2o ↑m suc 𝐴) ≈ (2o × (2o ↑m 𝐴)))
30	27, 28, 29	sylancl 586	. . . . . . 7 ⊢ (𝐴 ∈ ω → (2o ↑m suc 𝐴) ≈ (2o × (2o ↑m 𝐴)))
31	10	enref 8910	. . . . . . . . 9 ⊢ 2o ≈ 2o
32		pw2eng 9000	. . . . . . . . 9 ⊢ (𝐴 ∈ ω → 𝒫 𝐴 ≈ (2o ↑m 𝐴))
33		xpen 9057	. . . . . . . . 9 ⊢ ((2o ≈ 2o ∧ 𝒫 𝐴 ≈ (2o ↑m 𝐴)) → (2o × 𝒫 𝐴) ≈ (2o × (2o ↑m 𝐴)))
34	31, 32, 33	sylancr 587	. . . . . . . 8 ⊢ (𝐴 ∈ ω → (2o × 𝒫 𝐴) ≈ (2o × (2o ↑m 𝐴)))
35	34	ensymd 8930	. . . . . . 7 ⊢ (𝐴 ∈ ω → (2o × (2o ↑m 𝐴)) ≈ (2o × 𝒫 𝐴))
36		entr 8931	. . . . . . 7 ⊢ (((2o ↑m suc 𝐴) ≈ (2o × (2o ↑m 𝐴)) ∧ (2o × (2o ↑m 𝐴)) ≈ (2o × 𝒫 𝐴)) → (2o ↑m suc 𝐴) ≈ (2o × 𝒫 𝐴))
37	30, 35, 36	syl2anc 584	. . . . . 6 ⊢ (𝐴 ∈ ω → (2o ↑m suc 𝐴) ≈ (2o × 𝒫 𝐴))
38		entr 8931	. . . . . 6 ⊢ ((𝒫 suc 𝐴 ≈ (2o ↑m suc 𝐴) ∧ (2o ↑m suc 𝐴) ≈ (2o × 𝒫 𝐴)) → 𝒫 suc 𝐴 ≈ (2o × 𝒫 𝐴))
39	3, 37, 38	syl2anc 584	. . . . 5 ⊢ (𝐴 ∈ ω → 𝒫 suc 𝐴 ≈ (2o × 𝒫 𝐴))
40		xp2dju 10071	. . . . 5 ⊢ (2o × 𝒫 𝐴) = (𝒫 𝐴 ⊔ 𝒫 𝐴)
41	39, 40	breqtrdi 5133	. . . 4 ⊢ (𝐴 ∈ ω → 𝒫 suc 𝐴 ≈ (𝒫 𝐴 ⊔ 𝒫 𝐴))
42		nnfi 9081	. . . . . . . 8 ⊢ (𝐴 ∈ ω → 𝐴 ∈ Fin)
43		pwfi 9208	. . . . . . . 8 ⊢ (𝐴 ∈ Fin ↔ 𝒫 𝐴 ∈ Fin)
44	42, 43	sylib 218	. . . . . . 7 ⊢ (𝐴 ∈ ω → 𝒫 𝐴 ∈ Fin)
45		ficardid 9858	. . . . . . 7 ⊢ (𝒫 𝐴 ∈ Fin → (card‘𝒫 𝐴) ≈ 𝒫 𝐴)
46	44, 45	syl 17	. . . . . 6 ⊢ (𝐴 ∈ ω → (card‘𝒫 𝐴) ≈ 𝒫 𝐴)
47		djuen 10064	. . . . . 6 ⊢ (((card‘𝒫 𝐴) ≈ 𝒫 𝐴 ∧ (card‘𝒫 𝐴) ≈ 𝒫 𝐴) → ((card‘𝒫 𝐴) ⊔ (card‘𝒫 𝐴)) ≈ (𝒫 𝐴 ⊔ 𝒫 𝐴))
48	46, 46, 47	syl2anc 584	. . . . 5 ⊢ (𝐴 ∈ ω → ((card‘𝒫 𝐴) ⊔ (card‘𝒫 𝐴)) ≈ (𝒫 𝐴 ⊔ 𝒫 𝐴))
49	48	ensymd 8930	. . . 4 ⊢ (𝐴 ∈ ω → (𝒫 𝐴 ⊔ 𝒫 𝐴) ≈ ((card‘𝒫 𝐴) ⊔ (card‘𝒫 𝐴)))
50		entr 8931	. . . 4 ⊢ ((𝒫 suc 𝐴 ≈ (𝒫 𝐴 ⊔ 𝒫 𝐴) ∧ (𝒫 𝐴 ⊔ 𝒫 𝐴) ≈ ((card‘𝒫 𝐴) ⊔ (card‘𝒫 𝐴))) → 𝒫 suc 𝐴 ≈ ((card‘𝒫 𝐴) ⊔ (card‘𝒫 𝐴)))
51	41, 49, 50	syl2anc 584	. . 3 ⊢ (𝐴 ∈ ω → 𝒫 suc 𝐴 ≈ ((card‘𝒫 𝐴) ⊔ (card‘𝒫 𝐴)))
52		carden2b 9863	. . 3 ⊢ (𝒫 suc 𝐴 ≈ ((card‘𝒫 𝐴) ⊔ (card‘𝒫 𝐴)) → (card‘𝒫 suc 𝐴) = (card‘((card‘𝒫 𝐴) ⊔ (card‘𝒫 𝐴))))
53	51, 52	syl 17	. 2 ⊢ (𝐴 ∈ ω → (card‘𝒫 suc 𝐴) = (card‘((card‘𝒫 𝐴) ⊔ (card‘𝒫 𝐴))))
54		ficardom 9857	. . . 4 ⊢ (𝒫 𝐴 ∈ Fin → (card‘𝒫 𝐴) ∈ ω)
55	44, 54	syl 17	. . 3 ⊢ (𝐴 ∈ ω → (card‘𝒫 𝐴) ∈ ω)
56		nnadju 10092	. . 3 ⊢ (((card‘𝒫 𝐴) ∈ ω ∧ (card‘𝒫 𝐴) ∈ ω) → (card‘((card‘𝒫 𝐴) ⊔ (card‘𝒫 𝐴))) = ((card‘𝒫 𝐴) +o (card‘𝒫 𝐴)))
57	55, 55, 56	syl2anc 584	. 2 ⊢ (𝐴 ∈ ω → (card‘((card‘𝒫 𝐴) ⊔ (card‘𝒫 𝐴))) = ((card‘𝒫 𝐴) +o (card‘𝒫 𝐴)))
58	53, 57	eqtrd 2764	1 ⊢ (𝐴 ∈ ω → (card‘𝒫 suc 𝐴) = ((card‘𝒫 𝐴) +o (card‘𝒫 𝐴)))

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  Vcvv 3436   ∪ cun 3901   ∩ cin 3902  ∅c0 4284  𝒫 cpw 4551  {csn 4577   class class class wbr 5092   × cxp 5617  Ord word 6306  Oncon0 6307  suc csuc 6309  ‘cfv 6482  (class class class)co 7349  ωcom 7799  2_oc2o 8382   +_o coa 8385   ↑_m cmap 8753   ≈ cen 8869  Fincfn 8872   ⊔ cdju 9794  cardccrd 9831

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5235  ax-nul 5245  ax-pow 5304  ax-pr 5371  ax-un 7671

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-reu 3344  df-rab 3395  df-v 3438  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4285  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-int 4897  df-iun 4943  df-br 5093  df-opab 5155  df-mpt 5174  df-tr 5200  df-id 5514  df-eprel 5519  df-po 5527  df-so 5528  df-fr 5572  df-we 5574  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-pred 6249  df-ord 6310  df-on 6311  df-lim 6312  df-suc 6313  df-iota 6438  df-fun 6484  df-fn 6485  df-f 6486  df-f1 6487  df-fo 6488  df-f1o 6489  df-fv 6490  df-ov 7352  df-oprab 7353  df-mpo 7354  df-om 7800  df-1st 7924  df-2nd 7925  df-frecs 8214  df-wrecs 8245  df-recs 8294  df-rdg 8332  df-1o 8388  df-2o 8389  df-oadd 8392  df-er 8625  df-map 8755  df-en 8873  df-dom 8874  df-sdom 8875  df-fin 8876  df-dju 9797  df-card 9835

This theorem is referenced by:  ackbij1lem14  10126