ackbij1lem5

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

		Ref	Expression
	Assertion	ackbij1lem5	$⊢ A \in ω \to card (𝒫 suc A) = card (𝒫 A) +_{𝑜} card (𝒫 A)$

Proof

Step	Hyp	Ref	Expression
1		peano2	$⊢ A \in ω \to suc A \in ω$
2		pw2eng	$⊢ suc A \in ω \to 𝒫 suc A \approx ({2_{𝑜}}^{suc A})$
3	1 2	syl	$⊢ A \in ω \to 𝒫 suc A \approx ({2_{𝑜}}^{suc A})$
4		df-suc	$⊢ suc A = A \cup \{A\}$
5	4	oveq2i	$⊢ {2_{𝑜}}^{suc A} = {2_{𝑜}}^{(A \cup \{A\})}$
6		elex	$⊢ A \in ω \to A \in V$
7		snex	$⊢ \{A\} \in V$
8	7	a1i	$⊢ A \in ω \to \{A\} \in V$
9		2onn	$⊢ 2_{𝑜} \in ω$
10	9	elexi	$⊢ 2_{𝑜} \in V$
11	10	a1i	$⊢ A \in ω \to 2_{𝑜} \in V$
12		nnord	$⊢ A \in ω \to Ord A$
13		orddisj	$⊢ Ord A \to A \cap \{A\} = \emptyset$
14	12 13	syl	$⊢ A \in ω \to A \cap \{A\} = \emptyset$
15		mapunen	$⊢ ((A \in V \land \{A\} \in V \land 2_{𝑜} \in V) \land A \cap \{A\} = \emptyset) \to ({2_{𝑜}}^{(A \cup \{A\})}) \approx (({2_{𝑜}}^{A}) \times ({2_{𝑜}}^{\{A\}}))$
16	6 8 11 14 15	syl31anc	$⊢ A \in ω \to ({2_{𝑜}}^{(A \cup \{A\})}) \approx (({2_{𝑜}}^{A}) \times ({2_{𝑜}}^{\{A\}}))$
17		ovex	$⊢ {2_{𝑜}}^{A} \in V$
18	17	enref	$⊢ ({2_{𝑜}}^{A}) \approx ({2_{𝑜}}^{A})$
19		2on	$⊢ 2_{𝑜} \in On$
20	19	a1i	$⊢ A \in ω \to 2_{𝑜} \in On$
21		id	$⊢ A \in ω \to A \in ω$
22	20 21	mapsnend	$⊢ A \in ω \to ({2_{𝑜}}^{\{A\}}) \approx 2_{𝑜}$
23		xpen	$⊢ (({2_{𝑜}}^{A}) \approx ({2_{𝑜}}^{A}) \land ({2_{𝑜}}^{\{A\}}) \approx 2_{𝑜}) \to (({2_{𝑜}}^{A}) \times ({2_{𝑜}}^{\{A\}})) \approx (({2_{𝑜}}^{A}) \times 2_{𝑜})$
24	18 22 23	sylancr	$⊢ A \in ω \to (({2_{𝑜}}^{A}) \times ({2_{𝑜}}^{\{A\}})) \approx (({2_{𝑜}}^{A}) \times 2_{𝑜})$
25		entr	$⊢ (({2_{𝑜}}^{(A \cup \{A\})}) \approx (({2_{𝑜}}^{A}) \times ({2_{𝑜}}^{\{A\}})) \land (({2_{𝑜}}^{A}) \times ({2_{𝑜}}^{\{A\}})) \approx (({2_{𝑜}}^{A}) \times 2_{𝑜})) \to ({2_{𝑜}}^{(A \cup \{A\})}) \approx (({2_{𝑜}}^{A}) \times 2_{𝑜})$
26	16 24 25	syl2anc	$⊢ A \in ω \to ({2_{𝑜}}^{(A \cup \{A\})}) \approx (({2_{𝑜}}^{A}) \times 2_{𝑜})$
27	5 26	eqbrtrid	$⊢ A \in ω \to ({2_{𝑜}}^{suc A}) \approx (({2_{𝑜}}^{A}) \times 2_{𝑜})$
28	17 10	xpcomen	$⊢ (({2_{𝑜}}^{A}) \times 2_{𝑜}) \approx (2_{𝑜} \times ({2_{𝑜}}^{A}))$
29		entr	$⊢ (({2_{𝑜}}^{suc A}) \approx (({2_{𝑜}}^{A}) \times 2_{𝑜}) \land (({2_{𝑜}}^{A}) \times 2_{𝑜}) \approx (2_{𝑜} \times ({2_{𝑜}}^{A}))) \to ({2_{𝑜}}^{suc A}) \approx (2_{𝑜} \times ({2_{𝑜}}^{A}))$
30	27 28 29	sylancl	$⊢ A \in ω \to ({2_{𝑜}}^{suc A}) \approx (2_{𝑜} \times ({2_{𝑜}}^{A}))$
31	10	enref	$⊢ 2_{𝑜} \approx 2_{𝑜}$
32		pw2eng	$⊢ A \in ω \to 𝒫 A \approx ({2_{𝑜}}^{A})$
33		xpen	$⊢ (2_{𝑜} \approx 2_{𝑜} \land 𝒫 A \approx ({2_{𝑜}}^{A})) \to (2_{𝑜} \times 𝒫 A) \approx (2_{𝑜} \times ({2_{𝑜}}^{A}))$
34	31 32 33	sylancr	$⊢ A \in ω \to (2_{𝑜} \times 𝒫 A) \approx (2_{𝑜} \times ({2_{𝑜}}^{A}))$
35	34	ensymd	$⊢ A \in ω \to (2_{𝑜} \times ({2_{𝑜}}^{A})) \approx (2_{𝑜} \times 𝒫 A)$
36		entr	$⊢ (({2_{𝑜}}^{suc A}) \approx (2_{𝑜} \times ({2_{𝑜}}^{A})) \land (2_{𝑜} \times ({2_{𝑜}}^{A})) \approx (2_{𝑜} \times 𝒫 A)) \to ({2_{𝑜}}^{suc A}) \approx (2_{𝑜} \times 𝒫 A)$
37	30 35 36	syl2anc	$⊢ A \in ω \to ({2_{𝑜}}^{suc A}) \approx (2_{𝑜} \times 𝒫 A)$
38		entr	$⊢ (𝒫 suc A \approx ({2_{𝑜}}^{suc A}) \land ({2_{𝑜}}^{suc A}) \approx (2_{𝑜} \times 𝒫 A)) \to 𝒫 suc A \approx (2_{𝑜} \times 𝒫 A)$
39	3 37 38	syl2anc	$⊢ A \in ω \to 𝒫 suc A \approx (2_{𝑜} \times 𝒫 A)$
40		xp2dju	$⊢ 2_{𝑜} \times 𝒫 A = (𝒫 A ⊔︀ 𝒫 A)$
41	39 40	breqtrdi	$⊢ A \in ω \to 𝒫 suc A \approx (𝒫 A ⊔︀ 𝒫 A)$
42		nnfi	$⊢ A \in ω \to A \in Fin$
43		pwfi	$⊢ A \in Fin \leftrightarrow 𝒫 A \in Fin$
44	42 43	sylib	$⊢ A \in ω \to 𝒫 A \in Fin$
45		ficardid	$⊢ 𝒫 A \in Fin \to card (𝒫 A) \approx 𝒫 A$
46	44 45	syl	$⊢ A \in ω \to card (𝒫 A) \approx 𝒫 A$
47		djuen	$⊢ (card (𝒫 A) \approx 𝒫 A \land card (𝒫 A) \approx 𝒫 A) \to (card (𝒫 A) ⊔︀ card (𝒫 A)) \approx (𝒫 A ⊔︀ 𝒫 A)$
48	46 46 47	syl2anc	$⊢ A \in ω \to (card (𝒫 A) ⊔︀ card (𝒫 A)) \approx (𝒫 A ⊔︀ 𝒫 A)$
49	48	ensymd	$⊢ A \in ω \to (𝒫 A ⊔︀ 𝒫 A) \approx (card (𝒫 A) ⊔︀ card (𝒫 A))$
50		entr	$⊢ (𝒫 suc A \approx (𝒫 A ⊔︀ 𝒫 A) \land (𝒫 A ⊔︀ 𝒫 A) \approx (card (𝒫 A) ⊔︀ card (𝒫 A))) \to 𝒫 suc A \approx (card (𝒫 A) ⊔︀ card (𝒫 A))$
51	41 49 50	syl2anc	$⊢ A \in ω \to 𝒫 suc A \approx (card (𝒫 A) ⊔︀ card (𝒫 A))$
52		carden2b	$⊢ 𝒫 suc A \approx (card (𝒫 A) ⊔︀ card (𝒫 A)) \to card (𝒫 suc A) = card ((card (𝒫 A) ⊔︀ card (𝒫 A)))$
53	51 52	syl	$⊢ A \in ω \to card (𝒫 suc A) = card ((card (𝒫 A) ⊔︀ card (𝒫 A)))$
54		ficardom	$⊢ 𝒫 A \in Fin \to card (𝒫 A) \in ω$
55	44 54	syl	$⊢ A \in ω \to card (𝒫 A) \in ω$
56		nnadju	$⊢ (card (𝒫 A) \in ω \land card (𝒫 A) \in ω) \to card ((card (𝒫 A) ⊔︀ card (𝒫 A))) = card (𝒫 A) +_{𝑜} card (𝒫 A)$
57	55 55 56	syl2anc	$⊢ A \in ω \to card ((card (𝒫 A) ⊔︀ card (𝒫 A))) = card (𝒫 A) +_{𝑜} card (𝒫 A)$
58	53 57	eqtrd	$⊢ A \in ω \to card (𝒫 suc A) = card (𝒫 A) +_{𝑜} card (𝒫 A)$

Metamath Proof Explorer

Theorem ackbij1lem5

Proof