Theorem cmpcov

Description: An open cover of a compact topology has a finite subcover. (Contributed by Jeff Hankins, 29-Jun-2009)

	Ref	Expression
Hypothesis	iscmp.1	⊢ 𝑋 = ∪ 𝐽
Assertion	cmpcov	⊢ ( ( 𝐽 ∈ Comp ∧ 𝑆 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑆 ) → ∃ 𝑠 ∈ ( 𝒫 𝑆 ∩ Fin ) 𝑋 = ∪ 𝑠 )

Proof

Step	Hyp	Ref	Expression
1		iscmp.1	⊢ 𝑋 = ∪ 𝐽
2		unieq	⊢ ( 𝑟 = 𝑆 → ∪ 𝑟 = ∪ 𝑆 )
3	2	eqeq2d	⊢ ( 𝑟 = 𝑆 → ( 𝑋 = ∪ 𝑟 ↔ 𝑋 = ∪ 𝑆 ) )
4		pweq	⊢ ( 𝑟 = 𝑆 → 𝒫 𝑟 = 𝒫 𝑆 )
5	4	ineq1d	⊢ ( 𝑟 = 𝑆 → ( 𝒫 𝑟 ∩ Fin ) = ( 𝒫 𝑆 ∩ Fin ) )
6	5	rexeqdv	⊢ ( 𝑟 = 𝑆 → ( ∃ 𝑠 ∈ ( 𝒫 𝑟 ∩ Fin ) 𝑋 = ∪ 𝑠 ↔ ∃ 𝑠 ∈ ( 𝒫 𝑆 ∩ Fin ) 𝑋 = ∪ 𝑠 ) )
7	3 6	imbi12d	⊢ ( 𝑟 = 𝑆 → ( ( 𝑋 = ∪ 𝑟 → ∃ 𝑠 ∈ ( 𝒫 𝑟 ∩ Fin ) 𝑋 = ∪ 𝑠 ) ↔ ( 𝑋 = ∪ 𝑆 → ∃ 𝑠 ∈ ( 𝒫 𝑆 ∩ Fin ) 𝑋 = ∪ 𝑠 ) ) )
8	1	iscmp	⊢ ( 𝐽 ∈ Comp ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑟 ∈ 𝒫 𝐽 ( 𝑋 = ∪ 𝑟 → ∃ 𝑠 ∈ ( 𝒫 𝑟 ∩ Fin ) 𝑋 = ∪ 𝑠 ) ) )
9	8	simprbi	⊢ ( 𝐽 ∈ Comp → ∀ 𝑟 ∈ 𝒫 𝐽 ( 𝑋 = ∪ 𝑟 → ∃ 𝑠 ∈ ( 𝒫 𝑟 ∩ Fin ) 𝑋 = ∪ 𝑠 ) )
10	9	adantr	⊢ ( ( 𝐽 ∈ Comp ∧ 𝑆 ⊆ 𝐽 ) → ∀ 𝑟 ∈ 𝒫 𝐽 ( 𝑋 = ∪ 𝑟 → ∃ 𝑠 ∈ ( 𝒫 𝑟 ∩ Fin ) 𝑋 = ∪ 𝑠 ) )
11		ssexg	⊢ ( ( 𝑆 ⊆ 𝐽 ∧ 𝐽 ∈ Comp ) → 𝑆 ∈ V )
12	11	ancoms	⊢ ( ( 𝐽 ∈ Comp ∧ 𝑆 ⊆ 𝐽 ) → 𝑆 ∈ V )
13		simpr	⊢ ( ( 𝐽 ∈ Comp ∧ 𝑆 ⊆ 𝐽 ) → 𝑆 ⊆ 𝐽 )
14	12 13	elpwd	⊢ ( ( 𝐽 ∈ Comp ∧ 𝑆 ⊆ 𝐽 ) → 𝑆 ∈ 𝒫 𝐽 )
15	7 10 14	rspcdva	⊢ ( ( 𝐽 ∈ Comp ∧ 𝑆 ⊆ 𝐽 ) → ( 𝑋 = ∪ 𝑆 → ∃ 𝑠 ∈ ( 𝒫 𝑆 ∩ Fin ) 𝑋 = ∪ 𝑠 ) )
16	15	3impia	⊢ ( ( 𝐽 ∈ Comp ∧ 𝑆 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑆 ) → ∃ 𝑠 ∈ ( 𝒫 𝑆 ∩ Fin ) 𝑋 = ∪ 𝑠 )