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	⊢ 𝑋 = ∪ 𝐽
	pibp19.19	⊢ 𝐶 = { 𝑥 ∈ Top ∣ ∀ 𝑦 ∈ 𝒫 𝑥 ( ( ∪ 𝑥 = ∪ 𝑦 ∧ 𝑦 ≼ ω ) → ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) ∪ 𝑥 = ∪ 𝑧 ) }
Assertion	pibp19	⊢ ( 𝐽 ∈ 𝐶 ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑦 ∈ 𝒫 𝐽 ( ( 𝑋 = ∪ 𝑦 ∧ 𝑦 ≼ ω ) → ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) 𝑋 = ∪ 𝑧 ) ) )

Proof

Step	Hyp	Ref	Expression
1		pibp19.x	⊢ 𝑋 = ∪ 𝐽
2		pibp19.19	⊢ 𝐶 = { 𝑥 ∈ Top ∣ ∀ 𝑦 ∈ 𝒫 𝑥 ( ( ∪ 𝑥 = ∪ 𝑦 ∧ 𝑦 ≼ ω ) → ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) ∪ 𝑥 = ∪ 𝑧 ) }
3		pweq	⊢ ( 𝑥 = 𝐽 → 𝒫 𝑥 = 𝒫 𝐽 )
4		unieq	⊢ ( 𝑥 = 𝐽 → ∪ 𝑥 = ∪ 𝐽 )
5	4 1	eqtr4di	⊢ ( 𝑥 = 𝐽 → ∪ 𝑥 = 𝑋 )
6	5	eqeq1d	⊢ ( 𝑥 = 𝐽 → ( ∪ 𝑥 = ∪ 𝑦 ↔ 𝑋 = ∪ 𝑦 ) )
7	6	anbi1d	⊢ ( 𝑥 = 𝐽 → ( ( ∪ 𝑥 = ∪ 𝑦 ∧ 𝑦 ≼ ω ) ↔ ( 𝑋 = ∪ 𝑦 ∧ 𝑦 ≼ ω ) ) )
8	5	eqeq1d	⊢ ( 𝑥 = 𝐽 → ( ∪ 𝑥 = ∪ 𝑧 ↔ 𝑋 = ∪ 𝑧 ) )
9	8	rexbidv	⊢ ( 𝑥 = 𝐽 → ( ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) ∪ 𝑥 = ∪ 𝑧 ↔ ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) 𝑋 = ∪ 𝑧 ) )
10	7 9	imbi12d	⊢ ( 𝑥 = 𝐽 → ( ( ( ∪ 𝑥 = ∪ 𝑦 ∧ 𝑦 ≼ ω ) → ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) ∪ 𝑥 = ∪ 𝑧 ) ↔ ( ( 𝑋 = ∪ 𝑦 ∧ 𝑦 ≼ ω ) → ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) 𝑋 = ∪ 𝑧 ) ) )
11	3 10	raleqbidv	⊢ ( 𝑥 = 𝐽 → ( ∀ 𝑦 ∈ 𝒫 𝑥 ( ( ∪ 𝑥 = ∪ 𝑦 ∧ 𝑦 ≼ ω ) → ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) ∪ 𝑥 = ∪ 𝑧 ) ↔ ∀ 𝑦 ∈ 𝒫 𝐽 ( ( 𝑋 = ∪ 𝑦 ∧ 𝑦 ≼ ω ) → ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) 𝑋 = ∪ 𝑧 ) ) )
12	11 2	elrab2	⊢ ( 𝐽 ∈ 𝐶 ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑦 ∈ 𝒫 𝐽 ( ( 𝑋 = ∪ 𝑦 ∧ 𝑦 ≼ ω ) → ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) 𝑋 = ∪ 𝑧 ) ) )