This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem kelac2lem

Description: Lemma for kelac2 and dfac21 : knob topologies are compact. (Contributed by Stefan O'Rear, 22-Feb-2015)

Ref Expression
Assertion kelac2lem ( 𝑆 ∈ 𝑉 → ( topGen ‘ { 𝑆 , { 𝒫 ∪ 𝑆 } } ) ∈ Comp )

Proof

Step Hyp Ref Expression
1 prex ⊢ { 𝑆 , { 𝒫 ∪ 𝑆 } } ∈ V
2 vex ⊢ 𝑥 ∈ V
3 2 elpr ⊢ ( 𝑥 ∈ { 𝑆 , { 𝒫 ∪ 𝑆 } } ↔ ( 𝑥 = 𝑆 ∨ 𝑥 = { 𝒫 ∪ 𝑆 } ) )
4 vex ⊢ 𝑦 ∈ V
5 4 elpr ⊢ ( 𝑦 ∈ { 𝑆 , { 𝒫 ∪ 𝑆 } } ↔ ( 𝑦 = 𝑆 ∨ 𝑦 = { 𝒫 ∪ 𝑆 } ) )
6 eqtr3 ⊢ ( ( 𝑥 = 𝑆 ∧ 𝑦 = 𝑆 ) → 𝑥 = 𝑦 )
7 6 orcd ⊢ ( ( 𝑥 = 𝑆 ∧ 𝑦 = 𝑆 ) → ( 𝑥 = 𝑦 ∨ ( 𝑥 ∩ 𝑦 ) = ∅ ) )
8 ineq12 ⊢ ( ( 𝑥 = { 𝒫 ∪ 𝑆 } ∧ 𝑦 = 𝑆 ) → ( 𝑥 ∩ 𝑦 ) = ( { 𝒫 ∪ 𝑆 } ∩ 𝑆 ) )
9 incom ⊢ ( { 𝒫 ∪ 𝑆 } ∩ 𝑆 ) = ( 𝑆 ∩ { 𝒫 ∪ 𝑆 } )
10 pwuninel ⊢ ¬ 𝒫 ∪ 𝑆 ∈ 𝑆
11 disjsn ⊢ ( ( 𝑆 ∩ { 𝒫 ∪ 𝑆 } ) = ∅ ↔ ¬ 𝒫 ∪ 𝑆 ∈ 𝑆 )
12 10 11 mpbir ⊢ ( 𝑆 ∩ { 𝒫 ∪ 𝑆 } ) = ∅
13 9 12 eqtri ⊢ ( { 𝒫 ∪ 𝑆 } ∩ 𝑆 ) = ∅
14 8 13 eqtrdi ⊢ ( ( 𝑥 = { 𝒫 ∪ 𝑆 } ∧ 𝑦 = 𝑆 ) → ( 𝑥 ∩ 𝑦 ) = ∅ )
15 14 olcd ⊢ ( ( 𝑥 = { 𝒫 ∪ 𝑆 } ∧ 𝑦 = 𝑆 ) → ( 𝑥 = 𝑦 ∨ ( 𝑥 ∩ 𝑦 ) = ∅ ) )
16 ineq12 ⊢ ( ( 𝑥 = 𝑆 ∧ 𝑦 = { 𝒫 ∪ 𝑆 } ) → ( 𝑥 ∩ 𝑦 ) = ( 𝑆 ∩ { 𝒫 ∪ 𝑆 } ) )
17 16 12 eqtrdi ⊢ ( ( 𝑥 = 𝑆 ∧ 𝑦 = { 𝒫 ∪ 𝑆 } ) → ( 𝑥 ∩ 𝑦 ) = ∅ )
18 17 olcd ⊢ ( ( 𝑥 = 𝑆 ∧ 𝑦 = { 𝒫 ∪ 𝑆 } ) → ( 𝑥 = 𝑦 ∨ ( 𝑥 ∩ 𝑦 ) = ∅ ) )
19 eqtr3 ⊢ ( ( 𝑥 = { 𝒫 ∪ 𝑆 } ∧ 𝑦 = { 𝒫 ∪ 𝑆 } ) → 𝑥 = 𝑦 )
20 19 orcd ⊢ ( ( 𝑥 = { 𝒫 ∪ 𝑆 } ∧ 𝑦 = { 𝒫 ∪ 𝑆 } ) → ( 𝑥 = 𝑦 ∨ ( 𝑥 ∩ 𝑦 ) = ∅ ) )
21 7 15 18 20 ccase ⊢ ( ( ( 𝑥 = 𝑆 ∨ 𝑥 = { 𝒫 ∪ 𝑆 } ) ∧ ( 𝑦 = 𝑆 ∨ 𝑦 = { 𝒫 ∪ 𝑆 } ) ) → ( 𝑥 = 𝑦 ∨ ( 𝑥 ∩ 𝑦 ) = ∅ ) )
22 3 5 21 syl2anb ⊢ ( ( 𝑥 ∈ { 𝑆 , { 𝒫 ∪ 𝑆 } } ∧ 𝑦 ∈ { 𝑆 , { 𝒫 ∪ 𝑆 } } ) → ( 𝑥 = 𝑦 ∨ ( 𝑥 ∩ 𝑦 ) = ∅ ) )
23 22 rgen2 ⊢ ∀ 𝑥 ∈ { 𝑆 , { 𝒫 ∪ 𝑆 } } ∀ 𝑦 ∈ { 𝑆 , { 𝒫 ∪ 𝑆 } } ( 𝑥 = 𝑦 ∨ ( 𝑥 ∩ 𝑦 ) = ∅ )
24 baspartn ⊢ ( ( { 𝑆 , { 𝒫 ∪ 𝑆 } } ∈ V ∧ ∀ 𝑥 ∈ { 𝑆 , { 𝒫 ∪ 𝑆 } } ∀ 𝑦 ∈ { 𝑆 , { 𝒫 ∪ 𝑆 } } ( 𝑥 = 𝑦 ∨ ( 𝑥 ∩ 𝑦 ) = ∅ ) ) → { 𝑆 , { 𝒫 ∪ 𝑆 } } ∈ TopBases )
25 1 23 24 mp2an ⊢ { 𝑆 , { 𝒫 ∪ 𝑆 } } ∈ TopBases
26 tgcl ⊢ ( { 𝑆 , { 𝒫 ∪ 𝑆 } } ∈ TopBases → ( topGen ‘ { 𝑆 , { 𝒫 ∪ 𝑆 } } ) ∈ Top )
27 25 26 mp1i ⊢ ( 𝑆 ∈ 𝑉 → ( topGen ‘ { 𝑆 , { 𝒫 ∪ 𝑆 } } ) ∈ Top )
28 prfi ⊢ { 𝑆 , { 𝒫 ∪ 𝑆 } } ∈ Fin
29 pwfi ⊢ ( { 𝑆 , { 𝒫 ∪ 𝑆 } } ∈ Fin ↔ 𝒫 { 𝑆 , { 𝒫 ∪ 𝑆 } } ∈ Fin )
30 28 29 mpbi ⊢ 𝒫 { 𝑆 , { 𝒫 ∪ 𝑆 } } ∈ Fin
31 tgdom ⊢ ( { 𝑆 , { 𝒫 ∪ 𝑆 } } ∈ V → ( topGen ‘ { 𝑆 , { 𝒫 ∪ 𝑆 } } ) ≼ 𝒫 { 𝑆 , { 𝒫 ∪ 𝑆 } } )
32 1 31 ax-mp ⊢ ( topGen ‘ { 𝑆 , { 𝒫 ∪ 𝑆 } } ) ≼ 𝒫 { 𝑆 , { 𝒫 ∪ 𝑆 } }
33 domfi ⊢ ( ( 𝒫 { 𝑆 , { 𝒫 ∪ 𝑆 } } ∈ Fin ∧ ( topGen ‘ { 𝑆 , { 𝒫 ∪ 𝑆 } } ) ≼ 𝒫 { 𝑆 , { 𝒫 ∪ 𝑆 } } ) → ( topGen ‘ { 𝑆 , { 𝒫 ∪ 𝑆 } } ) ∈ Fin )
34 30 32 33 mp2an ⊢ ( topGen ‘ { 𝑆 , { 𝒫 ∪ 𝑆 } } ) ∈ Fin
35 34 a1i ⊢ ( 𝑆 ∈ 𝑉 → ( topGen ‘ { 𝑆 , { 𝒫 ∪ 𝑆 } } ) ∈ Fin )
36 27 35 elind ⊢ ( 𝑆 ∈ 𝑉 → ( topGen ‘ { 𝑆 , { 𝒫 ∪ 𝑆 } } ) ∈ ( Top ∩ Fin ) )
37 fincmp ⊢ ( ( topGen ‘ { 𝑆 , { 𝒫 ∪ 𝑆 } } ) ∈ ( Top ∩ Fin ) → ( topGen ‘ { 𝑆 , { 𝒫 ∪ 𝑆 } } ) ∈ Comp )
38 36 37 syl ⊢ ( 𝑆 ∈ 𝑉 → ( topGen ‘ { 𝑆 , { 𝒫 ∪ 𝑆 } } ) ∈ Comp )