Theorem alexsubALTlem1

Description: Lemma for alexsubALT . A compact space has a subbase such that every cover taken from it has a finite subcover. (Contributed by Jeff Hankins, 27-Jan-2010)

	Ref	Expression
Hypothesis	alexsubALT.1	⊢ 𝑋 = ∪ 𝐽
Assertion	alexsubALTlem1	⊢ ( 𝐽 ∈ Comp → ∃ 𝑥 ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ) )

Proof

Step	Hyp	Ref	Expression
1		alexsubALT.1	⊢ 𝑋 = ∪ 𝐽
2		cmptop	⊢ ( 𝐽 ∈ Comp → 𝐽 ∈ Top )
3		fitop	⊢ ( 𝐽 ∈ Top → ( fi ‘ 𝐽 ) = 𝐽 )
4	3	fveq2d	⊢ ( 𝐽 ∈ Top → ( topGen ‘ ( fi ‘ 𝐽 ) ) = ( topGen ‘ 𝐽 ) )
5		tgtop	⊢ ( 𝐽 ∈ Top → ( topGen ‘ 𝐽 ) = 𝐽 )
6	4 5	eqtr2d	⊢ ( 𝐽 ∈ Top → 𝐽 = ( topGen ‘ ( fi ‘ 𝐽 ) ) )
7	2 6	syl	⊢ ( 𝐽 ∈ Comp → 𝐽 = ( topGen ‘ ( fi ‘ 𝐽 ) ) )
8		velpw	⊢ ( 𝑐 ∈ 𝒫 𝐽 ↔ 𝑐 ⊆ 𝐽 )
9	1	cmpcov	⊢ ( ( 𝐽 ∈ Comp ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐 ) → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 )
10	9	3exp	⊢ ( 𝐽 ∈ Comp → ( 𝑐 ⊆ 𝐽 → ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ) )
11	8 10	syl5bi	⊢ ( 𝐽 ∈ Comp → ( 𝑐 ∈ 𝒫 𝐽 → ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ) )
12	11	ralrimiv	⊢ ( 𝐽 ∈ Comp → ∀ 𝑐 ∈ 𝒫 𝐽 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) )
13		2fveq3	⊢ ( 𝑥 = 𝐽 → ( topGen ‘ ( fi ‘ 𝑥 ) ) = ( topGen ‘ ( fi ‘ 𝐽 ) ) )
14	13	eqeq2d	⊢ ( 𝑥 = 𝐽 → ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ↔ 𝐽 = ( topGen ‘ ( fi ‘ 𝐽 ) ) ) )
15		pweq	⊢ ( 𝑥 = 𝐽 → 𝒫 𝑥 = 𝒫 𝐽 )
16	15	raleqdv	⊢ ( 𝑥 = 𝐽 → ( ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ↔ ∀ 𝑐 ∈ 𝒫 𝐽 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ) )
17	14 16	anbi12d	⊢ ( 𝑥 = 𝐽 → ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ) ↔ ( 𝐽 = ( topGen ‘ ( fi ‘ 𝐽 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝐽 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ) ) )
18	17	spcegv	⊢ ( 𝐽 ∈ Comp → ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝐽 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝐽 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ) → ∃ 𝑥 ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ) ) )
19	7 12 18	mp2and	⊢ ( 𝐽 ∈ Comp → ∃ 𝑥 ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ) )