Metamath Proof Explorer

Theorem topmeet

Description: Two equivalent formulations of the meet of a collection of topologies. (Contributed by Jeff Hankins, 4-Oct-2009) (Proof shortened by Mario Carneiro, 12-Sep-2015)

Ref Expression
Assertion topmeet ( ( 𝑋 ∈ 𝑉 ∧ 𝑆 ⊆ ( TopOn ‘ 𝑋 ) ) → ( 𝒫 𝑋 ∩ ∩ 𝑆 ) = ∪ { 𝑘 ∈ ( TopOn ‘ 𝑋 ) ∣ ∀ 𝑗 ∈ 𝑆 𝑘 ⊆ 𝑗 } )

Proof

Step Hyp Ref Expression
1 topmtcl ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑆 ⊆ ( TopOn ‘ 𝑋 ) ) → ( 𝒫 𝑋 ∩ ∩ 𝑆 ) ∈ ( TopOn ‘ 𝑋 ) )
2 inss2 ⊢ ( 𝒫 𝑋 ∩ ∩ 𝑆 ) ⊆ ∩ 𝑆
3 intss1 ⊢ ( 𝑗 ∈ 𝑆 → ∩ 𝑆 ⊆ 𝑗 )
4 2 3 sstrid ⊢ ( 𝑗 ∈ 𝑆 → ( 𝒫 𝑋 ∩ ∩ 𝑆 ) ⊆ 𝑗 )
5 4 rgen ⊢ ∀ 𝑗 ∈ 𝑆 ( 𝒫 𝑋 ∩ ∩ 𝑆 ) ⊆ 𝑗
6 sseq1 ⊢ ( 𝑘 = ( 𝒫 𝑋 ∩ ∩ 𝑆 ) → ( 𝑘 ⊆ 𝑗 ↔ ( 𝒫 𝑋 ∩ ∩ 𝑆 ) ⊆ 𝑗 ) )
7 6 ralbidv ⊢ ( 𝑘 = ( 𝒫 𝑋 ∩ ∩ 𝑆 ) → ( ∀ 𝑗 ∈ 𝑆 𝑘 ⊆ 𝑗 ↔ ∀ 𝑗 ∈ 𝑆 ( 𝒫 𝑋 ∩ ∩ 𝑆 ) ⊆ 𝑗 ) )
8 7 elrab ⊢ ( ( 𝒫 𝑋 ∩ ∩ 𝑆 ) ∈ { 𝑘 ∈ ( TopOn ‘ 𝑋 ) ∣ ∀ 𝑗 ∈ 𝑆 𝑘 ⊆ 𝑗 } ↔ ( ( 𝒫 𝑋 ∩ ∩ 𝑆 ) ∈ ( TopOn ‘ 𝑋 ) ∧ ∀ 𝑗 ∈ 𝑆 ( 𝒫 𝑋 ∩ ∩ 𝑆 ) ⊆ 𝑗 ) )
9 5 8 mpbiran2 ⊢ ( ( 𝒫 𝑋 ∩ ∩ 𝑆 ) ∈ { 𝑘 ∈ ( TopOn ‘ 𝑋 ) ∣ ∀ 𝑗 ∈ 𝑆 𝑘 ⊆ 𝑗 } ↔ ( 𝒫 𝑋 ∩ ∩ 𝑆 ) ∈ ( TopOn ‘ 𝑋 ) )
10 1 9 sylibr ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑆 ⊆ ( TopOn ‘ 𝑋 ) ) → ( 𝒫 𝑋 ∩ ∩ 𝑆 ) ∈ { 𝑘 ∈ ( TopOn ‘ 𝑋 ) ∣ ∀ 𝑗 ∈ 𝑆 𝑘 ⊆ 𝑗 } )
11 elssuni ⊢ ( ( 𝒫 𝑋 ∩ ∩ 𝑆 ) ∈ { 𝑘 ∈ ( TopOn ‘ 𝑋 ) ∣ ∀ 𝑗 ∈ 𝑆 𝑘 ⊆ 𝑗 } → ( 𝒫 𝑋 ∩ ∩ 𝑆 ) ⊆ ∪ { 𝑘 ∈ ( TopOn ‘ 𝑋 ) ∣ ∀ 𝑗 ∈ 𝑆 𝑘 ⊆ 𝑗 } )
12 10 11 syl ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑆 ⊆ ( TopOn ‘ 𝑋 ) ) → ( 𝒫 𝑋 ∩ ∩ 𝑆 ) ⊆ ∪ { 𝑘 ∈ ( TopOn ‘ 𝑋 ) ∣ ∀ 𝑗 ∈ 𝑆 𝑘 ⊆ 𝑗 } )
13 toponuni ⊢ ( 𝑘 ∈ ( TopOn ‘ 𝑋 ) → 𝑋 = ∪ 𝑘 )
14 eqimss2 ⊢ ( 𝑋 = ∪ 𝑘 → ∪ 𝑘 ⊆ 𝑋 )
15 13 14 syl ⊢ ( 𝑘 ∈ ( TopOn ‘ 𝑋 ) → ∪ 𝑘 ⊆ 𝑋 )
16 sspwuni ⊢ ( 𝑘 ⊆ 𝒫 𝑋 ↔ ∪ 𝑘 ⊆ 𝑋 )
17 15 16 sylibr ⊢ ( 𝑘 ∈ ( TopOn ‘ 𝑋 ) → 𝑘 ⊆ 𝒫 𝑋 )
18 17 3ad2ant2 ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑆 ⊆ ( TopOn ‘ 𝑋 ) ) ∧ 𝑘 ∈ ( TopOn ‘ 𝑋 ) ∧ ∀ 𝑗 ∈ 𝑆 𝑘 ⊆ 𝑗 ) → 𝑘 ⊆ 𝒫 𝑋 )
19 simp3 ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑆 ⊆ ( TopOn ‘ 𝑋 ) ) ∧ 𝑘 ∈ ( TopOn ‘ 𝑋 ) ∧ ∀ 𝑗 ∈ 𝑆 𝑘 ⊆ 𝑗 ) → ∀ 𝑗 ∈ 𝑆 𝑘 ⊆ 𝑗 )
20 ssint ⊢ ( 𝑘 ⊆ ∩ 𝑆 ↔ ∀ 𝑗 ∈ 𝑆 𝑘 ⊆ 𝑗 )
21 19 20 sylibr ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑆 ⊆ ( TopOn ‘ 𝑋 ) ) ∧ 𝑘 ∈ ( TopOn ‘ 𝑋 ) ∧ ∀ 𝑗 ∈ 𝑆 𝑘 ⊆ 𝑗 ) → 𝑘 ⊆ ∩ 𝑆 )
22 18 21 ssind ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑆 ⊆ ( TopOn ‘ 𝑋 ) ) ∧ 𝑘 ∈ ( TopOn ‘ 𝑋 ) ∧ ∀ 𝑗 ∈ 𝑆 𝑘 ⊆ 𝑗 ) → 𝑘 ⊆ ( 𝒫 𝑋 ∩ ∩ 𝑆 ) )
23 velpw ⊢ ( 𝑘 ∈ 𝒫 ( 𝒫 𝑋 ∩ ∩ 𝑆 ) ↔ 𝑘 ⊆ ( 𝒫 𝑋 ∩ ∩ 𝑆 ) )
24 22 23 sylibr ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑆 ⊆ ( TopOn ‘ 𝑋 ) ) ∧ 𝑘 ∈ ( TopOn ‘ 𝑋 ) ∧ ∀ 𝑗 ∈ 𝑆 𝑘 ⊆ 𝑗 ) → 𝑘 ∈ 𝒫 ( 𝒫 𝑋 ∩ ∩ 𝑆 ) )
25 24 rabssdv ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑆 ⊆ ( TopOn ‘ 𝑋 ) ) → { 𝑘 ∈ ( TopOn ‘ 𝑋 ) ∣ ∀ 𝑗 ∈ 𝑆 𝑘 ⊆ 𝑗 } ⊆ 𝒫 ( 𝒫 𝑋 ∩ ∩ 𝑆 ) )
26 sspwuni ⊢ ( { 𝑘 ∈ ( TopOn ‘ 𝑋 ) ∣ ∀ 𝑗 ∈ 𝑆 𝑘 ⊆ 𝑗 } ⊆ 𝒫 ( 𝒫 𝑋 ∩ ∩ 𝑆 ) ↔ ∪ { 𝑘 ∈ ( TopOn ‘ 𝑋 ) ∣ ∀ 𝑗 ∈ 𝑆 𝑘 ⊆ 𝑗 } ⊆ ( 𝒫 𝑋 ∩ ∩ 𝑆 ) )
27 25 26 sylib ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑆 ⊆ ( TopOn ‘ 𝑋 ) ) → ∪ { 𝑘 ∈ ( TopOn ‘ 𝑋 ) ∣ ∀ 𝑗 ∈ 𝑆 𝑘 ⊆ 𝑗 } ⊆ ( 𝒫 𝑋 ∩ ∩ 𝑆 ) )
28 12 27 eqssd ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑆 ⊆ ( TopOn ‘ 𝑋 ) ) → ( 𝒫 𝑋 ∩ ∩ 𝑆 ) = ∪ { 𝑘 ∈ ( TopOn ‘ 𝑋 ) ∣ ∀ 𝑗 ∈ 𝑆 𝑘 ⊆ 𝑗 } )