Theorem pibt1

Description: Theorem T000001 of pi-base. A compact topology is also countably compact. See pibp16 and pibp19 for the definitions of the relevant properties. (Contributed by ML, 8-Dec-2020)

	Ref	Expression
Hypothesis	pibt1.19	⊢ 𝐶 = { 𝑥 ∈ Top ∣ ∀ 𝑦 ∈ 𝒫 𝑥 ( ( ∪ 𝑥 = ∪ 𝑦 ∧ 𝑦 ≼ ω ) → ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) ∪ 𝑥 = ∪ 𝑧 ) }
Assertion	pibt1	⊢ ( 𝐽 ∈ Comp → 𝐽 ∈ 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		pibt1.19	⊢ 𝐶 = { 𝑥 ∈ Top ∣ ∀ 𝑦 ∈ 𝒫 𝑥 ( ( ∪ 𝑥 = ∪ 𝑦 ∧ 𝑦 ≼ ω ) → ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) ∪ 𝑥 = ∪ 𝑧 ) }
2		pm3.41	⊢ ( ( ∪ 𝐽 = ∪ 𝑦 → ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) ∪ 𝐽 = ∪ 𝑧 ) → ( ( ∪ 𝐽 = ∪ 𝑦 ∧ 𝑦 ≼ ω ) → ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) ∪ 𝐽 = ∪ 𝑧 ) )
3	2	ralimi	⊢ ( ∀ 𝑦 ∈ 𝒫 𝐽 ( ∪ 𝐽 = ∪ 𝑦 → ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) ∪ 𝐽 = ∪ 𝑧 ) → ∀ 𝑦 ∈ 𝒫 𝐽 ( ( ∪ 𝐽 = ∪ 𝑦 ∧ 𝑦 ≼ ω ) → ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) ∪ 𝐽 = ∪ 𝑧 ) )
4	3	anim2i	⊢ ( ( 𝐽 ∈ Top ∧ ∀ 𝑦 ∈ 𝒫 𝐽 ( ∪ 𝐽 = ∪ 𝑦 → ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) ∪ 𝐽 = ∪ 𝑧 ) ) → ( 𝐽 ∈ Top ∧ ∀ 𝑦 ∈ 𝒫 𝐽 ( ( ∪ 𝐽 = ∪ 𝑦 ∧ 𝑦 ≼ ω ) → ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) ∪ 𝐽 = ∪ 𝑧 ) ) )
5		eqid	⊢ ∪ 𝐽 = ∪ 𝐽
6	5	pibp16	⊢ ( 𝐽 ∈ Comp ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑦 ∈ 𝒫 𝐽 ( ∪ 𝐽 = ∪ 𝑦 → ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) ∪ 𝐽 = ∪ 𝑧 ) ) )
7	5 1	pibp19	⊢ ( 𝐽 ∈ 𝐶 ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑦 ∈ 𝒫 𝐽 ( ( ∪ 𝐽 = ∪ 𝑦 ∧ 𝑦 ≼ ω ) → ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) ∪ 𝐽 = ∪ 𝑧 ) ) )
8	4 6 7	3imtr4i	⊢ ( 𝐽 ∈ Comp → 𝐽 ∈ 𝐶 )