Theorem iscmp

Description: The predicate "is a compact topology". (Contributed by FL, 22-Dec-2008) (Revised by Mario Carneiro, 11-Feb-2015)

	Ref	Expression
Hypothesis	iscmp.1	⊢ 𝑋 = ∪ 𝐽
Assertion	iscmp	⊢ ( 𝐽 ∈ Comp ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑦 ∈ 𝒫 𝐽 ( 𝑋 = ∪ 𝑦 → ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) 𝑋 = ∪ 𝑧 ) ) )

Proof

Step	Hyp	Ref	Expression
1		iscmp.1	⊢ 𝑋 = ∪ 𝐽
2		pweq	⊢ ( 𝑥 = 𝐽 → 𝒫 𝑥 = 𝒫 𝐽 )
3		unieq	⊢ ( 𝑥 = 𝐽 → ∪ 𝑥 = ∪ 𝐽 )
4	3 1	eqtr4di	⊢ ( 𝑥 = 𝐽 → ∪ 𝑥 = 𝑋 )
5	4	eqeq1d	⊢ ( 𝑥 = 𝐽 → ( ∪ 𝑥 = ∪ 𝑦 ↔ 𝑋 = ∪ 𝑦 ) )
6	4	eqeq1d	⊢ ( 𝑥 = 𝐽 → ( ∪ 𝑥 = ∪ 𝑧 ↔ 𝑋 = ∪ 𝑧 ) )
7	6	rexbidv	⊢ ( 𝑥 = 𝐽 → ( ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) ∪ 𝑥 = ∪ 𝑧 ↔ ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) 𝑋 = ∪ 𝑧 ) )
8	5 7	imbi12d	⊢ ( 𝑥 = 𝐽 → ( ( ∪ 𝑥 = ∪ 𝑦 → ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) ∪ 𝑥 = ∪ 𝑧 ) ↔ ( 𝑋 = ∪ 𝑦 → ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) 𝑋 = ∪ 𝑧 ) ) )
9	2 8	raleqbidv	⊢ ( 𝑥 = 𝐽 → ( ∀ 𝑦 ∈ 𝒫 𝑥 ( ∪ 𝑥 = ∪ 𝑦 → ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) ∪ 𝑥 = ∪ 𝑧 ) ↔ ∀ 𝑦 ∈ 𝒫 𝐽 ( 𝑋 = ∪ 𝑦 → ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) 𝑋 = ∪ 𝑧 ) ) )
10		df-cmp	⊢ Comp = { 𝑥 ∈ Top ∣ ∀ 𝑦 ∈ 𝒫 𝑥 ( ∪ 𝑥 = ∪ 𝑦 → ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) ∪ 𝑥 = ∪ 𝑧 ) }
11	9 10	elrab2	⊢ ( 𝐽 ∈ Comp ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑦 ∈ 𝒫 𝐽 ( 𝑋 = ∪ 𝑦 → ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) 𝑋 = ∪ 𝑧 ) ) )