fincmp

		Ref	Expression
	Assertion	fincmp	$⊢ J \in (Top \cap Fin) \to J \in Comp$

Step	Hyp	Ref	Expression
1		elinel1	$⊢ J \in (Top \cap Fin) \to J \in Top$
2		elinel2	$⊢ J \in (Top \cap Fin) \to J \in Fin$
3		vex	$⊢ y \in V$
4	3	pwid	$⊢ y \in 𝒫 y$
5		velpw	$⊢ y \in 𝒫 J \leftrightarrow y \subseteq J$
6		ssfi	$⊢ (J \in Fin \land y \subseteq J) \to y \in Fin$
7	5 6	sylan2b	$⊢ (J \in Fin \land y \in 𝒫 J) \to y \in Fin$
8		elin	$⊢ y \in (𝒫 y \cap Fin) \leftrightarrow (y \in 𝒫 y \land y \in Fin)$
9		unieq	$⊢ z = y \to ⋃ z = ⋃ y$
10	9	rspceeqv	$⊢ (y \in (𝒫 y \cap Fin) \land ⋃ J = ⋃ y) \to \exists z \in (𝒫 y \cap Fin) ⋃ J = ⋃ z$
11	10	ex	$⊢ y \in (𝒫 y \cap Fin) \to (⋃ J = ⋃ y \to \exists z \in (𝒫 y \cap Fin) ⋃ J = ⋃ z)$
12	8 11	sylbir	$⊢ (y \in 𝒫 y \land y \in Fin) \to (⋃ J = ⋃ y \to \exists z \in (𝒫 y \cap Fin) ⋃ J = ⋃ z)$
13	4 7 12	sylancr	$⊢ (J \in Fin \land y \in 𝒫 J) \to (⋃ J = ⋃ y \to \exists z \in (𝒫 y \cap Fin) ⋃ J = ⋃ z)$
14	13	ralrimiva	$⊢ J \in Fin \to \forall y \in 𝒫 J (⋃ J = ⋃ y \to \exists z \in (𝒫 y \cap Fin) ⋃ J = ⋃ z)$
15	2 14	syl	$⊢ J \in (Top \cap Fin) \to \forall y \in 𝒫 J (⋃ J = ⋃ y \to \exists z \in (𝒫 y \cap Fin) ⋃ J = ⋃ z)$
16		eqid	$⊢ ⋃ J = ⋃ J$
17	16	iscmp	$⊢ J \in Comp \leftrightarrow (J \in Top \land \forall y \in 𝒫 J (⋃ J = ⋃ y \to \exists z \in (𝒫 y \cap Fin) ⋃ J = ⋃ z))$
18	1 15 17	sylanbrc	$⊢ J \in (Top \cap Fin) \to J \in Comp$

Metamath Proof Explorer