Theorem ackbij1lem5

Description: Lemma for ackbij2 . (Contributed by Stefan O'Rear, 19-Nov-2014) (Proof shortened by AV, 18-Jul-2022)

	Ref	Expression
Assertion	ackbij1lem5	⊢ ( 𝐴 ∈ ω → ( card ‘ 𝒫 suc 𝐴 ) = ( ( card ‘ 𝒫 𝐴 ) +o ( card ‘ 𝒫 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		peano2	⊢ ( 𝐴 ∈ ω → suc 𝐴 ∈ ω )
2		pw2eng	⊢ ( suc 𝐴 ∈ ω → 𝒫 suc 𝐴 ≈ ( 2o ↑m suc 𝐴 ) )
3	1 2	syl	⊢ ( 𝐴 ∈ ω → 𝒫 suc 𝐴 ≈ ( 2o ↑m suc 𝐴 ) )
4		df-suc	⊢ suc 𝐴 = ( 𝐴 ∪ { 𝐴 } )
5	4	oveq2i	⊢ ( 2o ↑m suc 𝐴 ) = ( 2o ↑m ( 𝐴 ∪ { 𝐴 } ) )
6		elex	⊢ ( 𝐴 ∈ ω → 𝐴 ∈ V )
7		snex	⊢ { 𝐴 } ∈ V
8	7	a1i	⊢ ( 𝐴 ∈ ω → { 𝐴 } ∈ V )
9		2onn	⊢ 2o ∈ ω
10	9	elexi	⊢ 2o ∈ V
11	10	a1i	⊢ ( 𝐴 ∈ ω → 2o ∈ V )
12		nnord	⊢ ( 𝐴 ∈ ω → Ord 𝐴 )
13		orddisj	⊢ ( Ord 𝐴 → ( 𝐴 ∩ { 𝐴 } ) = ∅ )
14	12 13	syl	⊢ ( 𝐴 ∈ ω → ( 𝐴 ∩ { 𝐴 } ) = ∅ )
15		mapunen	⊢ ( ( ( 𝐴 ∈ V ∧ { 𝐴 } ∈ V ∧ 2o ∈ V ) ∧ ( 𝐴 ∩ { 𝐴 } ) = ∅ ) → ( 2o ↑m ( 𝐴 ∪ { 𝐴 } ) ) ≈ ( ( 2o ↑m 𝐴 ) × ( 2o ↑m { 𝐴 } ) ) )
16	6 8 11 14 15	syl31anc	⊢ ( 𝐴 ∈ ω → ( 2o ↑m ( 𝐴 ∪ { 𝐴 } ) ) ≈ ( ( 2o ↑m 𝐴 ) × ( 2o ↑m { 𝐴 } ) ) )
17		ovex	⊢ ( 2o ↑m 𝐴 ) ∈ V
18	17	enref	⊢ ( 2o ↑m 𝐴 ) ≈ ( 2o ↑m 𝐴 )
19		2on	⊢ 2o ∈ On
20	19	a1i	⊢ ( 𝐴 ∈ ω → 2o ∈ On )
21		id	⊢ ( 𝐴 ∈ ω → 𝐴 ∈ ω )
22	20 21	mapsnend	⊢ ( 𝐴 ∈ ω → ( 2o ↑m { 𝐴 } ) ≈ 2o )
23		xpen	⊢ ( ( ( 2o ↑m 𝐴 ) ≈ ( 2o ↑m 𝐴 ) ∧ ( 2o ↑m { 𝐴 } ) ≈ 2o ) → ( ( 2o ↑m 𝐴 ) × ( 2o ↑m { 𝐴 } ) ) ≈ ( ( 2o ↑m 𝐴 ) × 2o ) )
24	18 22 23	sylancr	⊢ ( 𝐴 ∈ ω → ( ( 2o ↑m 𝐴 ) × ( 2o ↑m { 𝐴 } ) ) ≈ ( ( 2o ↑m 𝐴 ) × 2o ) )
25		entr	⊢ ( ( ( 2o ↑m ( 𝐴 ∪ { 𝐴 } ) ) ≈ ( ( 2o ↑m 𝐴 ) × ( 2o ↑m { 𝐴 } ) ) ∧ ( ( 2o ↑m 𝐴 ) × ( 2o ↑m { 𝐴 } ) ) ≈ ( ( 2o ↑m 𝐴 ) × 2o ) ) → ( 2o ↑m ( 𝐴 ∪ { 𝐴 } ) ) ≈ ( ( 2o ↑m 𝐴 ) × 2o ) )
26	16 24 25	syl2anc	⊢ ( 𝐴 ∈ ω → ( 2o ↑m ( 𝐴 ∪ { 𝐴 } ) ) ≈ ( ( 2o ↑m 𝐴 ) × 2o ) )
27	5 26	eqbrtrid	⊢ ( 𝐴 ∈ ω → ( 2o ↑m suc 𝐴 ) ≈ ( ( 2o ↑m 𝐴 ) × 2o ) )
28	17 10	xpcomen	⊢ ( ( 2o ↑m 𝐴 ) × 2o ) ≈ ( 2o × ( 2o ↑m 𝐴 ) )
29		entr	⊢ ( ( ( 2o ↑m suc 𝐴 ) ≈ ( ( 2o ↑m 𝐴 ) × 2o ) ∧ ( ( 2o ↑m 𝐴 ) × 2o ) ≈ ( 2o × ( 2o ↑m 𝐴 ) ) ) → ( 2o ↑m suc 𝐴 ) ≈ ( 2o × ( 2o ↑m 𝐴 ) ) )
30	27 28 29	sylancl	⊢ ( 𝐴 ∈ ω → ( 2o ↑m suc 𝐴 ) ≈ ( 2o × ( 2o ↑m 𝐴 ) ) )
31	10	enref	⊢ 2o ≈ 2o
32		pw2eng	⊢ ( 𝐴 ∈ ω → 𝒫 𝐴 ≈ ( 2o ↑m 𝐴 ) )
33		xpen	⊢ ( ( 2o ≈ 2o ∧ 𝒫 𝐴 ≈ ( 2o ↑m 𝐴 ) ) → ( 2o × 𝒫 𝐴 ) ≈ ( 2o × ( 2o ↑m 𝐴 ) ) )
34	31 32 33	sylancr	⊢ ( 𝐴 ∈ ω → ( 2o × 𝒫 𝐴 ) ≈ ( 2o × ( 2o ↑m 𝐴 ) ) )
35	34	ensymd	⊢ ( 𝐴 ∈ ω → ( 2o × ( 2o ↑m 𝐴 ) ) ≈ ( 2o × 𝒫 𝐴 ) )
36		entr	⊢ ( ( ( 2o ↑m suc 𝐴 ) ≈ ( 2o × ( 2o ↑m 𝐴 ) ) ∧ ( 2o × ( 2o ↑m 𝐴 ) ) ≈ ( 2o × 𝒫 𝐴 ) ) → ( 2o ↑m suc 𝐴 ) ≈ ( 2o × 𝒫 𝐴 ) )
37	30 35 36	syl2anc	⊢ ( 𝐴 ∈ ω → ( 2o ↑m suc 𝐴 ) ≈ ( 2o × 𝒫 𝐴 ) )
38		entr	⊢ ( ( 𝒫 suc 𝐴 ≈ ( 2o ↑m suc 𝐴 ) ∧ ( 2o ↑m suc 𝐴 ) ≈ ( 2o × 𝒫 𝐴 ) ) → 𝒫 suc 𝐴 ≈ ( 2o × 𝒫 𝐴 ) )
39	3 37 38	syl2anc	⊢ ( 𝐴 ∈ ω → 𝒫 suc 𝐴 ≈ ( 2o × 𝒫 𝐴 ) )
40		xp2dju	⊢ ( 2o × 𝒫 𝐴 ) = ( 𝒫 𝐴 ⊔ 𝒫 𝐴 )
41	39 40	breqtrdi	⊢ ( 𝐴 ∈ ω → 𝒫 suc 𝐴 ≈ ( 𝒫 𝐴 ⊔ 𝒫 𝐴 ) )
42		nnfi	⊢ ( 𝐴 ∈ ω → 𝐴 ∈ Fin )
43		pwfi	⊢ ( 𝐴 ∈ Fin ↔ 𝒫 𝐴 ∈ Fin )
44	42 43	sylib	⊢ ( 𝐴 ∈ ω → 𝒫 𝐴 ∈ Fin )
45		ficardid	⊢ ( 𝒫 𝐴 ∈ Fin → ( card ‘ 𝒫 𝐴 ) ≈ 𝒫 𝐴 )
46	44 45	syl	⊢ ( 𝐴 ∈ ω → ( card ‘ 𝒫 𝐴 ) ≈ 𝒫 𝐴 )
47		djuen	⊢ ( ( ( card ‘ 𝒫 𝐴 ) ≈ 𝒫 𝐴 ∧ ( card ‘ 𝒫 𝐴 ) ≈ 𝒫 𝐴 ) → ( ( card ‘ 𝒫 𝐴 ) ⊔ ( card ‘ 𝒫 𝐴 ) ) ≈ ( 𝒫 𝐴 ⊔ 𝒫 𝐴 ) )
48	46 46 47	syl2anc	⊢ ( 𝐴 ∈ ω → ( ( card ‘ 𝒫 𝐴 ) ⊔ ( card ‘ 𝒫 𝐴 ) ) ≈ ( 𝒫 𝐴 ⊔ 𝒫 𝐴 ) )
49	48	ensymd	⊢ ( 𝐴 ∈ ω → ( 𝒫 𝐴 ⊔ 𝒫 𝐴 ) ≈ ( ( card ‘ 𝒫 𝐴 ) ⊔ ( card ‘ 𝒫 𝐴 ) ) )
50		entr	⊢ ( ( 𝒫 suc 𝐴 ≈ ( 𝒫 𝐴 ⊔ 𝒫 𝐴 ) ∧ ( 𝒫 𝐴 ⊔ 𝒫 𝐴 ) ≈ ( ( card ‘ 𝒫 𝐴 ) ⊔ ( card ‘ 𝒫 𝐴 ) ) ) → 𝒫 suc 𝐴 ≈ ( ( card ‘ 𝒫 𝐴 ) ⊔ ( card ‘ 𝒫 𝐴 ) ) )
51	41 49 50	syl2anc	⊢ ( 𝐴 ∈ ω → 𝒫 suc 𝐴 ≈ ( ( card ‘ 𝒫 𝐴 ) ⊔ ( card ‘ 𝒫 𝐴 ) ) )
52		carden2b	⊢ ( 𝒫 suc 𝐴 ≈ ( ( card ‘ 𝒫 𝐴 ) ⊔ ( card ‘ 𝒫 𝐴 ) ) → ( card ‘ 𝒫 suc 𝐴 ) = ( card ‘ ( ( card ‘ 𝒫 𝐴 ) ⊔ ( card ‘ 𝒫 𝐴 ) ) ) )
53	51 52	syl	⊢ ( 𝐴 ∈ ω → ( card ‘ 𝒫 suc 𝐴 ) = ( card ‘ ( ( card ‘ 𝒫 𝐴 ) ⊔ ( card ‘ 𝒫 𝐴 ) ) ) )
54		ficardom	⊢ ( 𝒫 𝐴 ∈ Fin → ( card ‘ 𝒫 𝐴 ) ∈ ω )
55	44 54	syl	⊢ ( 𝐴 ∈ ω → ( card ‘ 𝒫 𝐴 ) ∈ ω )
56		nnadju	⊢ ( ( ( card ‘ 𝒫 𝐴 ) ∈ ω ∧ ( card ‘ 𝒫 𝐴 ) ∈ ω ) → ( card ‘ ( ( card ‘ 𝒫 𝐴 ) ⊔ ( card ‘ 𝒫 𝐴 ) ) ) = ( ( card ‘ 𝒫 𝐴 ) +o ( card ‘ 𝒫 𝐴 ) ) )
57	55 55 56	syl2anc	⊢ ( 𝐴 ∈ ω → ( card ‘ ( ( card ‘ 𝒫 𝐴 ) ⊔ ( card ‘ 𝒫 𝐴 ) ) ) = ( ( card ‘ 𝒫 𝐴 ) +o ( card ‘ 𝒫 𝐴 ) ) )
58	53 57	eqtrd	⊢ ( 𝐴 ∈ ω → ( card ‘ 𝒫 suc 𝐴 ) = ( ( card ‘ 𝒫 𝐴 ) +o ( card ‘ 𝒫 𝐴 ) ) )