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 ) |