| Step | Hyp | Ref
| Expression |
| 1 | | elin 3967 |
. . . . 5
⊢ (𝑗 ∈ (On ∩ Fre) ↔
(𝑗 ∈ On ∧ 𝑗 ∈ Fre)) |
| 2 | | eqid 2737 |
. . . . . . . . . . 11
⊢ ∪ 𝑗 =
∪ 𝑗 |
| 3 | 2 | ist1 23329 |
. . . . . . . . . 10
⊢ (𝑗 ∈ Fre ↔ (𝑗 ∈ Top ∧ ∀𝑎 ∈ ∪ 𝑗{𝑎} ∈ (Clsd‘𝑗))) |
| 4 | 3 | simprbi 496 |
. . . . . . . . 9
⊢ (𝑗 ∈ Fre → ∀𝑎 ∈ ∪ 𝑗{𝑎} ∈ (Clsd‘𝑗)) |
| 5 | | onelon 6409 |
. . . . . . . . . . . . . . 15
⊢ ((𝑗 ∈ On ∧ (∪ 𝑗
∖ {∅}) ∈ 𝑗) → (∪ 𝑗 ∖ {∅}) ∈
On) |
| 6 | 5 | ex 412 |
. . . . . . . . . . . . . 14
⊢ (𝑗 ∈ On → ((∪ 𝑗
∖ {∅}) ∈ 𝑗
→ (∪ 𝑗 ∖ {∅}) ∈
On)) |
| 7 | | neldifsnd 4793 |
. . . . . . . . . . . . . . . . 17
⊢
(2o ∈ 𝑗 → ¬ ∅ ∈ (∪ 𝑗
∖ {∅})) |
| 8 | | p0ex 5384 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ {∅}
∈ V |
| 9 | 8 | prid2 4763 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ {∅}
∈ {∅, {∅}} |
| 10 | | df2o2 8515 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
2o = {∅, {∅}} |
| 11 | 9, 10 | eleqtrri 2840 |
. . . . . . . . . . . . . . . . . . . 20
⊢ {∅}
∈ 2o |
| 12 | | elunii 4912 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(({∅} ∈ 2o ∧ 2o ∈ 𝑗) → {∅} ∈ ∪ 𝑗) |
| 13 | 11, 12 | mpan 690 |
. . . . . . . . . . . . . . . . . . 19
⊢
(2o ∈ 𝑗 → {∅} ∈ ∪ 𝑗) |
| 14 | | df1o2 8513 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
1o = {∅} |
| 15 | | 1on 8518 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
1o ∈ On |
| 16 | 14, 15 | eqeltrri 2838 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ {∅}
∈ On |
| 17 | 16 | onirri 6497 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ¬
{∅} ∈ {∅} |
| 18 | 17 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢
(2o ∈ 𝑗 → ¬ {∅} ∈
{∅}) |
| 19 | 13, 18 | eldifd 3962 |
. . . . . . . . . . . . . . . . . 18
⊢
(2o ∈ 𝑗 → {∅} ∈ (∪ 𝑗
∖ {∅})) |
| 20 | 19 | ne0d 4342 |
. . . . . . . . . . . . . . . . 17
⊢
(2o ∈ 𝑗 → (∪ 𝑗 ∖ {∅}) ≠
∅) |
| 21 | 7, 20 | 2thd 265 |
. . . . . . . . . . . . . . . 16
⊢
(2o ∈ 𝑗 → (¬ ∅ ∈ (∪ 𝑗
∖ {∅}) ↔ (∪ 𝑗 ∖ {∅}) ≠
∅)) |
| 22 | | nbbn 383 |
. . . . . . . . . . . . . . . 16
⊢ ((¬
∅ ∈ (∪ 𝑗 ∖ {∅}) ↔ (∪ 𝑗
∖ {∅}) ≠ ∅) ↔ ¬ (∅ ∈ (∪ 𝑗
∖ {∅}) ↔ (∪ 𝑗 ∖ {∅}) ≠
∅)) |
| 23 | 21, 22 | sylib 218 |
. . . . . . . . . . . . . . 15
⊢
(2o ∈ 𝑗 → ¬ (∅ ∈ (∪ 𝑗
∖ {∅}) ↔ (∪ 𝑗 ∖ {∅}) ≠
∅)) |
| 24 | | on0eln0 6440 |
. . . . . . . . . . . . . . 15
⊢ ((∪ 𝑗
∖ {∅}) ∈ On → (∅ ∈ (∪ 𝑗
∖ {∅}) ↔ (∪ 𝑗 ∖ {∅}) ≠
∅)) |
| 25 | 23, 24 | nsyl 140 |
. . . . . . . . . . . . . 14
⊢
(2o ∈ 𝑗 → ¬ (∪
𝑗 ∖ {∅}) ∈
On) |
| 26 | 6, 25 | nsyli 157 |
. . . . . . . . . . . . 13
⊢ (𝑗 ∈ On → (2o
∈ 𝑗 → ¬
(∪ 𝑗 ∖ {∅}) ∈ 𝑗)) |
| 27 | 26 | imp 406 |
. . . . . . . . . . . 12
⊢ ((𝑗 ∈ On ∧ 2o
∈ 𝑗) → ¬
(∪ 𝑗 ∖ {∅}) ∈ 𝑗) |
| 28 | | 0ex 5307 |
. . . . . . . . . . . . . . . . . 18
⊢ ∅
∈ V |
| 29 | 28 | prid1 4762 |
. . . . . . . . . . . . . . . . 17
⊢ ∅
∈ {∅, {∅}} |
| 30 | 29, 10 | eleqtrri 2840 |
. . . . . . . . . . . . . . . 16
⊢ ∅
∈ 2o |
| 31 | | elunii 4912 |
. . . . . . . . . . . . . . . 16
⊢ ((∅
∈ 2o ∧ 2o ∈ 𝑗) → ∅ ∈ ∪ 𝑗) |
| 32 | 30, 31 | mpan 690 |
. . . . . . . . . . . . . . 15
⊢
(2o ∈ 𝑗 → ∅ ∈ ∪ 𝑗) |
| 33 | 32 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝑗 ∈ On ∧ 2o
∈ 𝑗) → ∅
∈ ∪ 𝑗) |
| 34 | | simpr 484 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑗 ∈ On ∧ 2o
∈ 𝑗) ∧ 𝑎 = ∅) → 𝑎 = ∅) |
| 35 | 34 | sneqd 4638 |
. . . . . . . . . . . . . . 15
⊢ (((𝑗 ∈ On ∧ 2o
∈ 𝑗) ∧ 𝑎 = ∅) → {𝑎} = {∅}) |
| 36 | 35 | eleq1d 2826 |
. . . . . . . . . . . . . 14
⊢ (((𝑗 ∈ On ∧ 2o
∈ 𝑗) ∧ 𝑎 = ∅) → ({𝑎} ∈ (Clsd‘𝑗) ↔ {∅} ∈
(Clsd‘𝑗))) |
| 37 | 33, 36 | rspcdv 3614 |
. . . . . . . . . . . . 13
⊢ ((𝑗 ∈ On ∧ 2o
∈ 𝑗) →
(∀𝑎 ∈ ∪ 𝑗{𝑎} ∈ (Clsd‘𝑗) → {∅} ∈ (Clsd‘𝑗))) |
| 38 | 2 | cldopn 23039 |
. . . . . . . . . . . . 13
⊢
({∅} ∈ (Clsd‘𝑗) → (∪ 𝑗 ∖ {∅}) ∈ 𝑗) |
| 39 | 37, 38 | syl6 35 |
. . . . . . . . . . . 12
⊢ ((𝑗 ∈ On ∧ 2o
∈ 𝑗) →
(∀𝑎 ∈ ∪ 𝑗{𝑎} ∈ (Clsd‘𝑗) → (∪ 𝑗 ∖ {∅}) ∈ 𝑗)) |
| 40 | 27, 39 | mtod 198 |
. . . . . . . . . . 11
⊢ ((𝑗 ∈ On ∧ 2o
∈ 𝑗) → ¬
∀𝑎 ∈ ∪ 𝑗{𝑎} ∈ (Clsd‘𝑗)) |
| 41 | 40 | ex 412 |
. . . . . . . . . 10
⊢ (𝑗 ∈ On → (2o
∈ 𝑗 → ¬
∀𝑎 ∈ ∪ 𝑗{𝑎} ∈ (Clsd‘𝑗))) |
| 42 | 41 | con2d 134 |
. . . . . . . . 9
⊢ (𝑗 ∈ On → (∀𝑎 ∈ ∪ 𝑗{𝑎} ∈ (Clsd‘𝑗) → ¬ 2o ∈ 𝑗)) |
| 43 | 4, 42 | syl5 34 |
. . . . . . . 8
⊢ (𝑗 ∈ On → (𝑗 ∈ Fre → ¬
2o ∈ 𝑗)) |
| 44 | | 2on 8520 |
. . . . . . . . 9
⊢
2o ∈ On |
| 45 | | ontri1 6418 |
. . . . . . . . . 10
⊢ ((𝑗 ∈ On ∧ 2o
∈ On) → (𝑗
⊆ 2o ↔ ¬ 2o ∈ 𝑗)) |
| 46 | | onsssuc 6474 |
. . . . . . . . . 10
⊢ ((𝑗 ∈ On ∧ 2o
∈ On) → (𝑗
⊆ 2o ↔ 𝑗 ∈ suc 2o)) |
| 47 | 45, 46 | bitr3d 281 |
. . . . . . . . 9
⊢ ((𝑗 ∈ On ∧ 2o
∈ On) → (¬ 2o ∈ 𝑗 ↔ 𝑗 ∈ suc 2o)) |
| 48 | 44, 47 | mpan2 691 |
. . . . . . . 8
⊢ (𝑗 ∈ On → (¬
2o ∈ 𝑗
↔ 𝑗 ∈ suc
2o)) |
| 49 | 43, 48 | sylibd 239 |
. . . . . . 7
⊢ (𝑗 ∈ On → (𝑗 ∈ Fre → 𝑗 ∈ suc
2o)) |
| 50 | 49 | imp 406 |
. . . . . 6
⊢ ((𝑗 ∈ On ∧ 𝑗 ∈ Fre) → 𝑗 ∈ suc
2o) |
| 51 | | 0ntop 22911 |
. . . . . . . . . 10
⊢ ¬
∅ ∈ Top |
| 52 | | t1top 23338 |
. . . . . . . . . 10
⊢ (∅
∈ Fre → ∅ ∈ Top) |
| 53 | 51, 52 | mto 197 |
. . . . . . . . 9
⊢ ¬
∅ ∈ Fre |
| 54 | | nelneq 2865 |
. . . . . . . . 9
⊢ ((𝑗 ∈ Fre ∧ ¬ ∅
∈ Fre) → ¬ 𝑗
= ∅) |
| 55 | 53, 54 | mpan2 691 |
. . . . . . . 8
⊢ (𝑗 ∈ Fre → ¬ 𝑗 = ∅) |
| 56 | | elsni 4643 |
. . . . . . . 8
⊢ (𝑗 ∈ {∅} → 𝑗 = ∅) |
| 57 | 55, 56 | nsyl 140 |
. . . . . . 7
⊢ (𝑗 ∈ Fre → ¬ 𝑗 ∈
{∅}) |
| 58 | 57 | adantl 481 |
. . . . . 6
⊢ ((𝑗 ∈ On ∧ 𝑗 ∈ Fre) → ¬ 𝑗 ∈
{∅}) |
| 59 | 50, 58 | eldifd 3962 |
. . . . 5
⊢ ((𝑗 ∈ On ∧ 𝑗 ∈ Fre) → 𝑗 ∈ (suc 2o
∖ {∅})) |
| 60 | 1, 59 | sylbi 217 |
. . . 4
⊢ (𝑗 ∈ (On ∩ Fre) →
𝑗 ∈ (suc 2o
∖ {∅})) |
| 61 | 60 | ssriv 3987 |
. . 3
⊢ (On ∩
Fre) ⊆ (suc 2o ∖ {∅}) |
| 62 | | df-suc 6390 |
. . . . . 6
⊢ suc
2o = (2o ∪ {2o}) |
| 63 | 62 | difeq1i 4122 |
. . . . 5
⊢ (suc
2o ∖ {∅}) = ((2o ∪ {2o})
∖ {∅}) |
| 64 | | difundir 4291 |
. . . . 5
⊢
((2o ∪ {2o}) ∖ {∅}) =
((2o ∖ {∅}) ∪ ({2o} ∖
{∅})) |
| 65 | 63, 64 | eqtri 2765 |
. . . 4
⊢ (suc
2o ∖ {∅}) = ((2o ∖ {∅}) ∪
({2o} ∖ {∅})) |
| 66 | | df-pr 4629 |
. . . . 5
⊢
{1o, 2o} = ({1o} ∪
{2o}) |
| 67 | | df2o3 8514 |
. . . . . . . . 9
⊢
2o = {∅, 1o} |
| 68 | | df-pr 4629 |
. . . . . . . . 9
⊢ {∅,
1o} = ({∅} ∪ {1o}) |
| 69 | 67, 68 | eqtri 2765 |
. . . . . . . 8
⊢
2o = ({∅} ∪ {1o}) |
| 70 | 69 | difeq1i 4122 |
. . . . . . 7
⊢
(2o ∖ {∅}) = (({∅} ∪ {1o})
∖ {∅}) |
| 71 | | difundir 4291 |
. . . . . . 7
⊢
(({∅} ∪ {1o}) ∖ {∅}) = (({∅}
∖ {∅}) ∪ ({1o} ∖ {∅})) |
| 72 | | difid 4376 |
. . . . . . . . 9
⊢
({∅} ∖ {∅}) = ∅ |
| 73 | | 1n0 8526 |
. . . . . . . . . . . 12
⊢
1o ≠ ∅ |
| 74 | | disjsn2 4712 |
. . . . . . . . . . . 12
⊢
(1o ≠ ∅ → ({1o} ∩ {∅}) =
∅) |
| 75 | 73, 74 | ax-mp 5 |
. . . . . . . . . . 11
⊢
({1o} ∩ {∅}) = ∅ |
| 76 | 75 | difeq2i 4123 |
. . . . . . . . . 10
⊢
({1o} ∖ ({1o} ∩ {∅})) =
({1o} ∖ ∅) |
| 77 | | difin 4272 |
. . . . . . . . . 10
⊢
({1o} ∖ ({1o} ∩ {∅})) =
({1o} ∖ {∅}) |
| 78 | | dif0 4378 |
. . . . . . . . . 10
⊢
({1o} ∖ ∅) = {1o} |
| 79 | 76, 77, 78 | 3eqtr3i 2773 |
. . . . . . . . 9
⊢
({1o} ∖ {∅}) = {1o} |
| 80 | 72, 79 | uneq12i 4166 |
. . . . . . . 8
⊢
(({∅} ∖ {∅}) ∪ ({1o} ∖
{∅})) = (∅ ∪ {1o}) |
| 81 | | uncom 4158 |
. . . . . . . 8
⊢ (∅
∪ {1o}) = ({1o} ∪ ∅) |
| 82 | | un0 4394 |
. . . . . . . 8
⊢
({1o} ∪ ∅) = {1o} |
| 83 | 80, 81, 82 | 3eqtri 2769 |
. . . . . . 7
⊢
(({∅} ∖ {∅}) ∪ ({1o} ∖
{∅})) = {1o} |
| 84 | 70, 71, 83 | 3eqtri 2769 |
. . . . . 6
⊢
(2o ∖ {∅}) = {1o} |
| 85 | | 2on0 8522 |
. . . . . . . . 9
⊢
2o ≠ ∅ |
| 86 | | disjsn2 4712 |
. . . . . . . . 9
⊢
(2o ≠ ∅ → ({2o} ∩ {∅}) =
∅) |
| 87 | 85, 86 | ax-mp 5 |
. . . . . . . 8
⊢
({2o} ∩ {∅}) = ∅ |
| 88 | 87 | difeq2i 4123 |
. . . . . . 7
⊢
({2o} ∖ ({2o} ∩ {∅})) =
({2o} ∖ ∅) |
| 89 | | difin 4272 |
. . . . . . 7
⊢
({2o} ∖ ({2o} ∩ {∅})) =
({2o} ∖ {∅}) |
| 90 | | dif0 4378 |
. . . . . . 7
⊢
({2o} ∖ ∅) = {2o} |
| 91 | 88, 89, 90 | 3eqtr3i 2773 |
. . . . . 6
⊢
({2o} ∖ {∅}) = {2o} |
| 92 | 84, 91 | uneq12i 4166 |
. . . . 5
⊢
((2o ∖ {∅}) ∪ ({2o} ∖
{∅})) = ({1o} ∪ {2o}) |
| 93 | 66, 92 | eqtr4i 2768 |
. . . 4
⊢
{1o, 2o} = ((2o ∖ {∅})
∪ ({2o} ∖ {∅})) |
| 94 | 65, 93 | eqtr4i 2768 |
. . 3
⊢ (suc
2o ∖ {∅}) = {1o,
2o} |
| 95 | 61, 94 | sseqtri 4032 |
. 2
⊢ (On ∩
Fre) ⊆ {1o, 2o} |
| 96 | | ssoninhaus 36449 |
. . 3
⊢
{1o, 2o} ⊆ (On ∩ Haus) |
| 97 | | haust1 23360 |
. . . . 5
⊢ (𝑗 ∈ Haus → 𝑗 ∈ Fre) |
| 98 | 97 | ssriv 3987 |
. . . 4
⊢ Haus
⊆ Fre |
| 99 | | sslin 4243 |
. . . 4
⊢ (Haus
⊆ Fre → (On ∩ Haus) ⊆ (On ∩ Fre)) |
| 100 | 98, 99 | ax-mp 5 |
. . 3
⊢ (On ∩
Haus) ⊆ (On ∩ Fre) |
| 101 | 96, 100 | sstri 3993 |
. 2
⊢
{1o, 2o} ⊆ (On ∩ Fre) |
| 102 | 95, 101 | eqssi 4000 |
1
⊢ (On ∩
Fre) = {1o, 2o} |