ackbij1lem9

		Ref	Expression
	Hypothesis	ackbij.f	$⊢ F = (x \in (𝒫 ω \cap Fin) ⟼ card (⋃_{y \in x} (\{y\} \times 𝒫 y)))$
	Assertion	ackbij1lem9	$⊢ (A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin) \land A \cap B = \emptyset) \to F (A \cup B) = F (A) +_{𝑜} F (B)$

Proof

Step	Hyp	Ref	Expression
1		ackbij.f	$⊢ F = (x \in (𝒫 ω \cap Fin) ⟼ card (⋃_{y \in x} (\{y\} \times 𝒫 y)))$
2		elinel2	$⊢ A \in (𝒫 ω \cap Fin) \to A \in Fin$
3	2	3ad2ant1	$⊢ (A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin) \land A \cap B = \emptyset) \to A \in Fin$
4		snfi	$⊢ \{y\} \in Fin$
5		elinel1	$⊢ A \in (𝒫 ω \cap Fin) \to A \in 𝒫 ω$
6	5	elpwid	$⊢ A \in (𝒫 ω \cap Fin) \to A \subseteq ω$
7	6	3ad2ant1	$⊢ (A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin) \land A \cap B = \emptyset) \to A \subseteq ω$
8		onfin2	$⊢ ω = On \cap Fin$
9		inss2	$⊢ On \cap Fin \subseteq Fin$
10	8 9	eqsstri	$⊢ ω \subseteq Fin$
11	7 10	sstrdi	$⊢ (A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin) \land A \cap B = \emptyset) \to A \subseteq Fin$
12	11	sselda	$⊢ ((A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin) \land A \cap B = \emptyset) \land y \in A) \to y \in Fin$
13		pwfi	$⊢ y \in Fin \leftrightarrow 𝒫 y \in Fin$
14	12 13	sylib	$⊢ ((A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin) \land A \cap B = \emptyset) \land y \in A) \to 𝒫 y \in Fin$
15		xpfi	$⊢ (\{y\} \in Fin \land 𝒫 y \in Fin) \to \{y\} \times 𝒫 y \in Fin$
16	4 14 15	sylancr	$⊢ ((A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin) \land A \cap B = \emptyset) \land y \in A) \to \{y\} \times 𝒫 y \in Fin$
17	16	ralrimiva	$⊢ (A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin) \land A \cap B = \emptyset) \to \forall y \in A \{y\} \times 𝒫 y \in Fin$
18		iunfi	$⊢ (A \in Fin \land \forall y \in A \{y\} \times 𝒫 y \in Fin) \to ⋃_{y \in A} (\{y\} \times 𝒫 y) \in Fin$
19	3 17 18	syl2anc	$⊢ (A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin) \land A \cap B = \emptyset) \to ⋃_{y \in A} (\{y\} \times 𝒫 y) \in Fin$
20		ficardid	$⊢ ⋃_{y \in A} (\{y\} \times 𝒫 y) \in Fin \to card (⋃_{y \in A} (\{y\} \times 𝒫 y)) \approx ⋃_{y \in A} (\{y\} \times 𝒫 y)$
21	19 20	syl	$⊢ (A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin) \land A \cap B = \emptyset) \to card (⋃_{y \in A} (\{y\} \times 𝒫 y)) \approx ⋃_{y \in A} (\{y\} \times 𝒫 y)$
22		elinel2	$⊢ B \in (𝒫 ω \cap Fin) \to B \in Fin$
23	22	3ad2ant2	$⊢ (A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin) \land A \cap B = \emptyset) \to B \in Fin$
24		elinel1	$⊢ B \in (𝒫 ω \cap Fin) \to B \in 𝒫 ω$
25	24	elpwid	$⊢ B \in (𝒫 ω \cap Fin) \to B \subseteq ω$
26	25	3ad2ant2	$⊢ (A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin) \land A \cap B = \emptyset) \to B \subseteq ω$
27	26 10	sstrdi	$⊢ (A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin) \land A \cap B = \emptyset) \to B \subseteq Fin$
28	27	sselda	$⊢ ((A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin) \land A \cap B = \emptyset) \land y \in B) \to y \in Fin$
29	28 13	sylib	$⊢ ((A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin) \land A \cap B = \emptyset) \land y \in B) \to 𝒫 y \in Fin$
30	4 29 15	sylancr	$⊢ ((A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin) \land A \cap B = \emptyset) \land y \in B) \to \{y\} \times 𝒫 y \in Fin$
31	30	ralrimiva	$⊢ (A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin) \land A \cap B = \emptyset) \to \forall y \in B \{y\} \times 𝒫 y \in Fin$
32		iunfi	$⊢ (B \in Fin \land \forall y \in B \{y\} \times 𝒫 y \in Fin) \to ⋃_{y \in B} (\{y\} \times 𝒫 y) \in Fin$
33	23 31 32	syl2anc	$⊢ (A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin) \land A \cap B = \emptyset) \to ⋃_{y \in B} (\{y\} \times 𝒫 y) \in Fin$
34		ficardid	$⊢ ⋃_{y \in B} (\{y\} \times 𝒫 y) \in Fin \to card (⋃_{y \in B} (\{y\} \times 𝒫 y)) \approx ⋃_{y \in B} (\{y\} \times 𝒫 y)$
35	33 34	syl	$⊢ (A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin) \land A \cap B = \emptyset) \to card (⋃_{y \in B} (\{y\} \times 𝒫 y)) \approx ⋃_{y \in B} (\{y\} \times 𝒫 y)$
36		djuen	$⊢ (card (⋃_{y \in A} (\{y\} \times 𝒫 y)) \approx ⋃_{y \in A} (\{y\} \times 𝒫 y) \land card (⋃_{y \in B} (\{y\} \times 𝒫 y)) \approx ⋃_{y \in B} (\{y\} \times 𝒫 y)) \to (card (⋃_{y \in A} (\{y\} \times 𝒫 y)) ⊔︀ card (⋃_{y \in B} (\{y\} \times 𝒫 y))) \approx (⋃_{y \in A} (\{y\} \times 𝒫 y) ⊔︀ ⋃_{y \in B} (\{y\} \times 𝒫 y))$
37	21 35 36	syl2anc	$⊢ (A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin) \land A \cap B = \emptyset) \to (card (⋃_{y \in A} (\{y\} \times 𝒫 y)) ⊔︀ card (⋃_{y \in B} (\{y\} \times 𝒫 y))) \approx (⋃_{y \in A} (\{y\} \times 𝒫 y) ⊔︀ ⋃_{y \in B} (\{y\} \times 𝒫 y))$
38		djudisj	$⊢ A \cap B = \emptyset \to ⋃_{y \in A} (\{y\} \times 𝒫 y) \cap ⋃_{y \in B} (\{y\} \times 𝒫 y) = \emptyset$
39	38	3ad2ant3	$⊢ (A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin) \land A \cap B = \emptyset) \to ⋃_{y \in A} (\{y\} \times 𝒫 y) \cap ⋃_{y \in B} (\{y\} \times 𝒫 y) = \emptyset$
40		endjudisj	$⊢ (⋃_{y \in A} (\{y\} \times 𝒫 y) \in Fin \land ⋃_{y \in B} (\{y\} \times 𝒫 y) \in Fin \land ⋃_{y \in A} (\{y\} \times 𝒫 y) \cap ⋃_{y \in B} (\{y\} \times 𝒫 y) = \emptyset) \to (⋃_{y \in A} (\{y\} \times 𝒫 y) ⊔︀ ⋃_{y \in B} (\{y\} \times 𝒫 y)) \approx (⋃_{y \in A} (\{y\} \times 𝒫 y) \cup ⋃_{y \in B} (\{y\} \times 𝒫 y))$
41	19 33 39 40	syl3anc	$⊢ (A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin) \land A \cap B = \emptyset) \to (⋃_{y \in A} (\{y\} \times 𝒫 y) ⊔︀ ⋃_{y \in B} (\{y\} \times 𝒫 y)) \approx (⋃_{y \in A} (\{y\} \times 𝒫 y) \cup ⋃_{y \in B} (\{y\} \times 𝒫 y))$
42		iunxun	$⊢ ⋃_{y \in A \cup B} (\{y\} \times 𝒫 y) = ⋃_{y \in A} (\{y\} \times 𝒫 y) \cup ⋃_{y \in B} (\{y\} \times 𝒫 y)$
43	41 42	breqtrrdi	$⊢ (A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin) \land A \cap B = \emptyset) \to (⋃_{y \in A} (\{y\} \times 𝒫 y) ⊔︀ ⋃_{y \in B} (\{y\} \times 𝒫 y)) \approx ⋃_{y \in A \cup B} (\{y\} \times 𝒫 y)$
44		entr	$⊢ ((card (⋃_{y \in A} (\{y\} \times 𝒫 y)) ⊔︀ card (⋃_{y \in B} (\{y\} \times 𝒫 y))) \approx (⋃_{y \in A} (\{y\} \times 𝒫 y) ⊔︀ ⋃_{y \in B} (\{y\} \times 𝒫 y)) \land (⋃_{y \in A} (\{y\} \times 𝒫 y) ⊔︀ ⋃_{y \in B} (\{y\} \times 𝒫 y)) \approx ⋃_{y \in A \cup B} (\{y\} \times 𝒫 y)) \to (card (⋃_{y \in A} (\{y\} \times 𝒫 y)) ⊔︀ card (⋃_{y \in B} (\{y\} \times 𝒫 y))) \approx ⋃_{y \in A \cup B} (\{y\} \times 𝒫 y)$
45	37 43 44	syl2anc	$⊢ (A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin) \land A \cap B = \emptyset) \to (card (⋃_{y \in A} (\{y\} \times 𝒫 y)) ⊔︀ card (⋃_{y \in B} (\{y\} \times 𝒫 y))) \approx ⋃_{y \in A \cup B} (\{y\} \times 𝒫 y)$
46		carden2b	$⊢ (card (⋃_{y \in A} (\{y\} \times 𝒫 y)) ⊔︀ card (⋃_{y \in B} (\{y\} \times 𝒫 y))) \approx ⋃_{y \in A \cup B} (\{y\} \times 𝒫 y) \to card ((card (⋃_{y \in A} (\{y\} \times 𝒫 y)) ⊔︀ card (⋃_{y \in B} (\{y\} \times 𝒫 y)))) = card (⋃_{y \in A \cup B} (\{y\} \times 𝒫 y))$
47	45 46	syl	$⊢ (A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin) \land A \cap B = \emptyset) \to card ((card (⋃_{y \in A} (\{y\} \times 𝒫 y)) ⊔︀ card (⋃_{y \in B} (\{y\} \times 𝒫 y)))) = card (⋃_{y \in A \cup B} (\{y\} \times 𝒫 y))$
48		ficardom	$⊢ ⋃_{y \in A} (\{y\} \times 𝒫 y) \in Fin \to card (⋃_{y \in A} (\{y\} \times 𝒫 y)) \in ω$
49	19 48	syl	$⊢ (A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin) \land A \cap B = \emptyset) \to card (⋃_{y \in A} (\{y\} \times 𝒫 y)) \in ω$
50		ficardom	$⊢ ⋃_{y \in B} (\{y\} \times 𝒫 y) \in Fin \to card (⋃_{y \in B} (\{y\} \times 𝒫 y)) \in ω$
51	33 50	syl	$⊢ (A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin) \land A \cap B = \emptyset) \to card (⋃_{y \in B} (\{y\} \times 𝒫 y)) \in ω$
52		nnadju	$⊢ (card (⋃_{y \in A} (\{y\} \times 𝒫 y)) \in ω \land card (⋃_{y \in B} (\{y\} \times 𝒫 y)) \in ω) \to card ((card (⋃_{y \in A} (\{y\} \times 𝒫 y)) ⊔︀ card (⋃_{y \in B} (\{y\} \times 𝒫 y)))) = card (⋃_{y \in A} (\{y\} \times 𝒫 y)) +_{𝑜} card (⋃_{y \in B} (\{y\} \times 𝒫 y))$
53	49 51 52	syl2anc	$⊢ (A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin) \land A \cap B = \emptyset) \to card ((card (⋃_{y \in A} (\{y\} \times 𝒫 y)) ⊔︀ card (⋃_{y \in B} (\{y\} \times 𝒫 y)))) = card (⋃_{y \in A} (\{y\} \times 𝒫 y)) +_{𝑜} card (⋃_{y \in B} (\{y\} \times 𝒫 y))$
54	47 53	eqtr3d	$⊢ (A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin) \land A \cap B = \emptyset) \to card (⋃_{y \in A \cup B} (\{y\} \times 𝒫 y)) = card (⋃_{y \in A} (\{y\} \times 𝒫 y)) +_{𝑜} card (⋃_{y \in B} (\{y\} \times 𝒫 y))$
55		ackbij1lem6	$⊢ (A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin)) \to A \cup B \in (𝒫 ω \cap Fin)$
56	55	3adant3	$⊢ (A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin) \land A \cap B = \emptyset) \to A \cup B \in (𝒫 ω \cap Fin)$
57	1	ackbij1lem7	$⊢ A \cup B \in (𝒫 ω \cap Fin) \to F (A \cup B) = card (⋃_{y \in A \cup B} (\{y\} \times 𝒫 y))$
58	56 57	syl	$⊢ (A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin) \land A \cap B = \emptyset) \to F (A \cup B) = card (⋃_{y \in A \cup B} (\{y\} \times 𝒫 y))$
59	1	ackbij1lem7	$⊢ A \in (𝒫 ω \cap Fin) \to F (A) = card (⋃_{y \in A} (\{y\} \times 𝒫 y))$
60	1	ackbij1lem7	$⊢ B \in (𝒫 ω \cap Fin) \to F (B) = card (⋃_{y \in B} (\{y\} \times 𝒫 y))$
61	59 60	oveqan12d	$⊢ (A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin)) \to F (A) +_{𝑜} F (B) = card (⋃_{y \in A} (\{y\} \times 𝒫 y)) +_{𝑜} card (⋃_{y \in B} (\{y\} \times 𝒫 y))$
62	61	3adant3	$⊢ (A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin) \land A \cap B = \emptyset) \to F (A) +_{𝑜} F (B) = card (⋃_{y \in A} (\{y\} \times 𝒫 y)) +_{𝑜} card (⋃_{y \in B} (\{y\} \times 𝒫 y))$
63	54 58 62	3eqtr4d	$⊢ (A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin) \land A \cap B = \emptyset) \to F (A \cup B) = F (A) +_{𝑜} F (B)$

Metamath Proof Explorer

Theorem ackbij1lem9

Proof