ackbij1lem10

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

Step	Hyp	Ref	Expression
1		ackbij.f	$⊢ F = (x \in (𝒫 ω \cap Fin) ⟼ card (⋃_{y \in x} (\{y\} \times 𝒫 y)))$
2		elinel2	$⊢ x \in (𝒫 ω \cap Fin) \to x \in Fin$
3		snfi	$⊢ \{y\} \in Fin$
4		elinel1	$⊢ x \in (𝒫 ω \cap Fin) \to x \in 𝒫 ω$
5	4	elpwid	$⊢ x \in (𝒫 ω \cap Fin) \to x \subseteq ω$
6		onfin2	$⊢ ω = On \cap Fin$
7		inss2	$⊢ On \cap Fin \subseteq Fin$
8	6 7	eqsstri	$⊢ ω \subseteq Fin$
9	5 8	sstrdi	$⊢ x \in (𝒫 ω \cap Fin) \to x \subseteq Fin$
10	9	sselda	$⊢ (x \in (𝒫 ω \cap Fin) \land y \in x) \to y \in Fin$
11		pwfi	$⊢ y \in Fin \leftrightarrow 𝒫 y \in Fin$
12	10 11	sylib	$⊢ (x \in (𝒫 ω \cap Fin) \land y \in x) \to 𝒫 y \in Fin$
13		xpfi	$⊢ (\{y\} \in Fin \land 𝒫 y \in Fin) \to \{y\} \times 𝒫 y \in Fin$
14	3 12 13	sylancr	$⊢ (x \in (𝒫 ω \cap Fin) \land y \in x) \to \{y\} \times 𝒫 y \in Fin$
15	14	ralrimiva	$⊢ x \in (𝒫 ω \cap Fin) \to \forall y \in x \{y\} \times 𝒫 y \in Fin$
16		iunfi	$⊢ (x \in Fin \land \forall y \in x \{y\} \times 𝒫 y \in Fin) \to ⋃_{y \in x} (\{y\} \times 𝒫 y) \in Fin$
17	2 15 16	syl2anc	$⊢ x \in (𝒫 ω \cap Fin) \to ⋃_{y \in x} (\{y\} \times 𝒫 y) \in Fin$
18		ficardom	$⊢ ⋃_{y \in x} (\{y\} \times 𝒫 y) \in Fin \to card (⋃_{y \in x} (\{y\} \times 𝒫 y)) \in ω$
19	17 18	syl	$⊢ x \in (𝒫 ω \cap Fin) \to card (⋃_{y \in x} (\{y\} \times 𝒫 y)) \in ω$
20	1 19	fmpti	$⊢ F : 𝒫 ω \cap Fin ⟶ ω$

Metamath Proof Explorer