Step |
Hyp |
Ref |
Expression |
1 |
|
onsstopbas |
⊢ On ⊆ TopBases |
2 |
|
indistop |
⊢ { ∅ , { { ∅ } } } ∈ Top |
3 |
|
topbas |
⊢ ( { ∅ , { { ∅ } } } ∈ Top → { ∅ , { { ∅ } } } ∈ TopBases ) |
4 |
2 3
|
ax-mp |
⊢ { ∅ , { { ∅ } } } ∈ TopBases |
5 |
|
snex |
⊢ { { ∅ } } ∈ V |
6 |
5
|
prid2 |
⊢ { { ∅ } } ∈ { ∅ , { { ∅ } } } |
7 |
|
snsn0non |
⊢ ¬ { { ∅ } } ∈ On |
8 |
|
jcn |
⊢ ( { { ∅ } } ∈ { ∅ , { { ∅ } } } → ( ¬ { { ∅ } } ∈ On → ¬ ( { { ∅ } } ∈ { ∅ , { { ∅ } } } → { { ∅ } } ∈ On ) ) ) |
9 |
6 7 8
|
mp2 |
⊢ ¬ ( { { ∅ } } ∈ { ∅ , { { ∅ } } } → { { ∅ } } ∈ On ) |
10 |
|
onelon |
⊢ ( ( { ∅ , { { ∅ } } } ∈ On ∧ { { ∅ } } ∈ { ∅ , { { ∅ } } } ) → { { ∅ } } ∈ On ) |
11 |
10
|
ex |
⊢ ( { ∅ , { { ∅ } } } ∈ On → ( { { ∅ } } ∈ { ∅ , { { ∅ } } } → { { ∅ } } ∈ On ) ) |
12 |
9 11
|
mto |
⊢ ¬ { ∅ , { { ∅ } } } ∈ On |
13 |
4 12
|
pm3.2i |
⊢ ( { ∅ , { { ∅ } } } ∈ TopBases ∧ ¬ { ∅ , { { ∅ } } } ∈ On ) |
14 |
|
ssnelpss |
⊢ ( On ⊆ TopBases → ( ( { ∅ , { { ∅ } } } ∈ TopBases ∧ ¬ { ∅ , { { ∅ } } } ∈ On ) → On ⊊ TopBases ) ) |
15 |
1 13 14
|
mp2 |
⊢ On ⊊ TopBases |