ackbij1lem14

		Ref	Expression
	Hypothesis	ackbij.f	$⊢ F = (x \in (𝒫 ω \cap Fin) ⟼ card (⋃_{y \in x} (\{y\} \times 𝒫 y)))$
	Assertion	ackbij1lem14	$⊢ A \in ω \to F (\{A\}) = suc F (A)$

Proof

Step	Hyp	Ref	Expression
1		ackbij.f	$⊢ F = (x \in (𝒫 ω \cap Fin) ⟼ card (⋃_{y \in x} (\{y\} \times 𝒫 y)))$
2	1	ackbij1lem8	$⊢ A \in ω \to F (\{A\}) = card (𝒫 A)$
3		pweq	$⊢ a = \emptyset \to 𝒫 a = 𝒫 \emptyset$
4	3	fveq2d	$⊢ a = \emptyset \to card (𝒫 a) = card (𝒫 \emptyset)$
5		fveq2	$⊢ a = \emptyset \to F (a) = F (\emptyset)$
6		suceq	$⊢ F (a) = F (\emptyset) \to suc F (a) = suc F (\emptyset)$
7	5 6	syl	$⊢ a = \emptyset \to suc F (a) = suc F (\emptyset)$
8	4 7	eqeq12d	$⊢ a = \emptyset \to (card (𝒫 a) = suc F (a) \leftrightarrow card (𝒫 \emptyset) = suc F (\emptyset))$
9		pweq	$⊢ a = b \to 𝒫 a = 𝒫 b$
10	9	fveq2d	$⊢ a = b \to card (𝒫 a) = card (𝒫 b)$
11		fveq2	$⊢ a = b \to F (a) = F (b)$
12		suceq	$⊢ F (a) = F (b) \to suc F (a) = suc F (b)$
13	11 12	syl	$⊢ a = b \to suc F (a) = suc F (b)$
14	10 13	eqeq12d	$⊢ a = b \to (card (𝒫 a) = suc F (a) \leftrightarrow card (𝒫 b) = suc F (b))$
15		pweq	$⊢ a = suc b \to 𝒫 a = 𝒫 suc b$
16	15	fveq2d	$⊢ a = suc b \to card (𝒫 a) = card (𝒫 suc b)$
17		fveq2	$⊢ a = suc b \to F (a) = F (suc b)$
18		suceq	$⊢ F (a) = F (suc b) \to suc F (a) = suc F (suc b)$
19	17 18	syl	$⊢ a = suc b \to suc F (a) = suc F (suc b)$
20	16 19	eqeq12d	$⊢ a = suc b \to (card (𝒫 a) = suc F (a) \leftrightarrow card (𝒫 suc b) = suc F (suc b))$
21		pweq	$⊢ a = A \to 𝒫 a = 𝒫 A$
22	21	fveq2d	$⊢ a = A \to card (𝒫 a) = card (𝒫 A)$
23		fveq2	$⊢ a = A \to F (a) = F (A)$
24		suceq	$⊢ F (a) = F (A) \to suc F (a) = suc F (A)$
25	23 24	syl	$⊢ a = A \to suc F (a) = suc F (A)$
26	22 25	eqeq12d	$⊢ a = A \to (card (𝒫 a) = suc F (a) \leftrightarrow card (𝒫 A) = suc F (A))$
27		df-1o	$⊢ 1_{𝑜} = suc \emptyset$
28		pw0	$⊢ 𝒫 \emptyset = \{\emptyset\}$
29	28	fveq2i	$⊢ card (𝒫 \emptyset) = card (\{\emptyset\})$
30		0ex	$⊢ \emptyset \in V$
31		cardsn	$⊢ \emptyset \in V \to card (\{\emptyset\}) = 1_{𝑜}$
32	30 31	ax-mp	$⊢ card (\{\emptyset\}) = 1_{𝑜}$
33	29 32	eqtri	$⊢ card (𝒫 \emptyset) = 1_{𝑜}$
34	1	ackbij1lem13	$⊢ F (\emptyset) = \emptyset$
35		suceq	$⊢ F (\emptyset) = \emptyset \to suc F (\emptyset) = suc \emptyset$
36	34 35	ax-mp	$⊢ suc F (\emptyset) = suc \emptyset$
37	27 33 36	3eqtr4i	$⊢ card (𝒫 \emptyset) = suc F (\emptyset)$
38		oveq2	$⊢ card (𝒫 b) = suc F (b) \to card (𝒫 b) +_{𝑜} card (𝒫 b) = card (𝒫 b) +_{𝑜} suc F (b)$
39	38	adantl	$⊢ (b \in ω \land card (𝒫 b) = suc F (b)) \to card (𝒫 b) +_{𝑜} card (𝒫 b) = card (𝒫 b) +_{𝑜} suc F (b)$
40		ackbij1lem5	$⊢ b \in ω \to card (𝒫 suc b) = card (𝒫 b) +_{𝑜} card (𝒫 b)$
41	40	adantr	$⊢ (b \in ω \land card (𝒫 b) = suc F (b)) \to card (𝒫 suc b) = card (𝒫 b) +_{𝑜} card (𝒫 b)$
42		df-suc	$⊢ suc b = b \cup \{b\}$
43	42	equncomi	$⊢ suc b = \{b\} \cup b$
44	43	fveq2i	$⊢ F (suc b) = F (\{b\} \cup b)$
45		ackbij1lem4	$⊢ b \in ω \to \{b\} \in (𝒫 ω \cap Fin)$
46	45	adantr	$⊢ (b \in ω \land card (𝒫 b) = suc F (b)) \to \{b\} \in (𝒫 ω \cap Fin)$
47		ackbij1lem3	$⊢ b \in ω \to b \in (𝒫 ω \cap Fin)$
48	47	adantr	$⊢ (b \in ω \land card (𝒫 b) = suc F (b)) \to b \in (𝒫 ω \cap Fin)$
49		incom	$⊢ \{b\} \cap b = b \cap \{b\}$
50		nnord	$⊢ b \in ω \to Ord b$
51		orddisj	$⊢ Ord b \to b \cap \{b\} = \emptyset$
52	50 51	syl	$⊢ b \in ω \to b \cap \{b\} = \emptyset$
53	49 52	syl5eq	$⊢ b \in ω \to \{b\} \cap b = \emptyset$
54	53	adantr	$⊢ (b \in ω \land card (𝒫 b) = suc F (b)) \to \{b\} \cap b = \emptyset$
55	1	ackbij1lem9	$⊢ (\{b\} \in (𝒫 ω \cap Fin) \land b \in (𝒫 ω \cap Fin) \land \{b\} \cap b = \emptyset) \to F (\{b\} \cup b) = F (\{b\}) +_{𝑜} F (b)$
56	46 48 54 55	syl3anc	$⊢ (b \in ω \land card (𝒫 b) = suc F (b)) \to F (\{b\} \cup b) = F (\{b\}) +_{𝑜} F (b)$
57	1	ackbij1lem8	$⊢ b \in ω \to F (\{b\}) = card (𝒫 b)$
58	57	adantr	$⊢ (b \in ω \land card (𝒫 b) = suc F (b)) \to F (\{b\}) = card (𝒫 b)$
59	58	oveq1d	$⊢ (b \in ω \land card (𝒫 b) = suc F (b)) \to F (\{b\}) +_{𝑜} F (b) = card (𝒫 b) +_{𝑜} F (b)$
60	56 59	eqtrd	$⊢ (b \in ω \land card (𝒫 b) = suc F (b)) \to F (\{b\} \cup b) = card (𝒫 b) +_{𝑜} F (b)$
61	44 60	syl5eq	$⊢ (b \in ω \land card (𝒫 b) = suc F (b)) \to F (suc b) = card (𝒫 b) +_{𝑜} F (b)$
62		suceq	$⊢ F (suc b) = card (𝒫 b) +_{𝑜} F (b) \to suc F (suc b) = suc (card (𝒫 b) +_{𝑜} F (b))$
63	61 62	syl	$⊢ (b \in ω \land card (𝒫 b) = suc F (b)) \to suc F (suc b) = suc (card (𝒫 b) +_{𝑜} F (b))$
64		nnfi	$⊢ b \in ω \to b \in Fin$
65		pwfi	$⊢ b \in Fin \leftrightarrow 𝒫 b \in Fin$
66	64 65	sylib	$⊢ b \in ω \to 𝒫 b \in Fin$
67	66	adantr	$⊢ (b \in ω \land card (𝒫 b) = suc F (b)) \to 𝒫 b \in Fin$
68		ficardom	$⊢ 𝒫 b \in Fin \to card (𝒫 b) \in ω$
69	67 68	syl	$⊢ (b \in ω \land card (𝒫 b) = suc F (b)) \to card (𝒫 b) \in ω$
70	1	ackbij1lem10	$⊢ F : 𝒫 ω \cap Fin ⟶ ω$
71	70	ffvelrni	$⊢ b \in (𝒫 ω \cap Fin) \to F (b) \in ω$
72	48 71	syl	$⊢ (b \in ω \land card (𝒫 b) = suc F (b)) \to F (b) \in ω$
73		nnasuc	$⊢ (card (𝒫 b) \in ω \land F (b) \in ω) \to card (𝒫 b) +_{𝑜} suc F (b) = suc (card (𝒫 b) +_{𝑜} F (b))$
74	69 72 73	syl2anc	$⊢ (b \in ω \land card (𝒫 b) = suc F (b)) \to card (𝒫 b) +_{𝑜} suc F (b) = suc (card (𝒫 b) +_{𝑜} F (b))$
75	63 74	eqtr4d	$⊢ (b \in ω \land card (𝒫 b) = suc F (b)) \to suc F (suc b) = card (𝒫 b) +_{𝑜} suc F (b)$
76	39 41 75	3eqtr4d	$⊢ (b \in ω \land card (𝒫 b) = suc F (b)) \to card (𝒫 suc b) = suc F (suc b)$
77	76	ex	$⊢ b \in ω \to (card (𝒫 b) = suc F (b) \to card (𝒫 suc b) = suc F (suc b))$
78	8 14 20 26 37 77	finds	$⊢ A \in ω \to card (𝒫 A) = suc F (A)$
79	2 78	eqtrd	$⊢ A \in ω \to F (\{A\}) = suc F (A)$

Metamath Proof Explorer

Theorem ackbij1lem14

Proof