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 )