Metamath Proof Explorer

Theorem pibp19

Description: Property P000019 of pi-base. The class of countably compact topologies. A space X is countably compact if every countable open cover of X has a finite subcover. (Contributed by ML, 8-Dec-2020)

		Ref	Expression
	Hypotheses	pibp19.x	$⊢ X = ⋃ J$
		pibp19.19	$⊢ C = \{x \in Top \| \forall y \in 𝒫 x ((⋃ x = ⋃ y \land y ≼ ω) \to \exists z \in (𝒫 y \cap Fin) ⋃ x = ⋃ z)\}$
	Assertion	pibp19	$⊢ J \in C \leftrightarrow (J \in Top \land \forall y \in 𝒫 J ((X = ⋃ y \land y ≼ ω) \to \exists z \in (𝒫 y \cap Fin) X = ⋃ z))$

Proof

Step	Hyp	Ref	Expression
1		pibp19.x	$⊢ X = ⋃ J$
2		pibp19.19	$⊢ C = \{x \in Top \| \forall y \in 𝒫 x ((⋃ x = ⋃ y \land y ≼ ω) \to \exists z \in (𝒫 y \cap Fin) ⋃ x = ⋃ z)\}$
3		pweq	$⊢ x = J \to 𝒫 x = 𝒫 J$
4		unieq	$⊢ x = J \to ⋃ x = ⋃ J$
5	4 1	syl6eqr	$⊢ x = J \to ⋃ x = X$
6	5	eqeq1d	$⊢ x = J \to (⋃ x = ⋃ y \leftrightarrow X = ⋃ y)$
7	6	anbi1d	$⊢ x = J \to ((⋃ x = ⋃ y \land y ≼ ω) \leftrightarrow (X = ⋃ y \land y ≼ ω))$
8	5	eqeq1d	$⊢ x = J \to (⋃ x = ⋃ z \leftrightarrow X = ⋃ z)$
9	8	rexbidv	$⊢ x = J \to (\exists z \in (𝒫 y \cap Fin) ⋃ x = ⋃ z \leftrightarrow \exists z \in (𝒫 y \cap Fin) X = ⋃ z)$
10	7 9	imbi12d	$⊢ x = J \to (((⋃ x = ⋃ y \land y ≼ ω) \to \exists z \in (𝒫 y \cap Fin) ⋃ x = ⋃ z) \leftrightarrow ((X = ⋃ y \land y ≼ ω) \to \exists z \in (𝒫 y \cap Fin) X = ⋃ z))$
11	3 10	raleqbidv	$⊢ x = J \to (\forall y \in 𝒫 x ((⋃ x = ⋃ y \land y ≼ ω) \to \exists z \in (𝒫 y \cap Fin) ⋃ x = ⋃ z) \leftrightarrow \forall y \in 𝒫 J ((X = ⋃ y \land y ≼ ω) \to \exists z \in (𝒫 y \cap Fin) X = ⋃ z))$
12	11 2	elrab2	$⊢ J \in C \leftrightarrow (J \in Top \land \forall y \in 𝒫 J ((X = ⋃ y \land y ≼ ω) \to \exists z \in (𝒫 y \cap Fin) X = ⋃ z))$