Step | Hyp | Ref
| Expression |
1 | | elin 3758 |
. . . . 5
⊢ (𝑗 ∈ (On ∩ Fre) ↔
(𝑗 ∈ On ∧ 𝑗 ∈ Fre)) |
2 | | eqid 2610 |
. . . . . . . . . . 11
⊢ ∪ 𝑗 =
∪ 𝑗 |
3 | 2 | ist1 20935 |
. . . . . . . . . 10
⊢ (𝑗 ∈ Fre ↔ (𝑗 ∈ Top ∧ ∀𝑎 ∈ ∪ 𝑗{𝑎} ∈ (Clsd‘𝑗))) |
4 | 3 | simprbi 479 |
. . . . . . . . 9
⊢ (𝑗 ∈ Fre → ∀𝑎 ∈ ∪ 𝑗{𝑎} ∈ (Clsd‘𝑗)) |
5 | | onelon 5665 |
. . . . . . . . . . . . . . 15
⊢ ((𝑗 ∈ On ∧ (∪ 𝑗
∖ {∅}) ∈ 𝑗) → (∪ 𝑗 ∖ {∅}) ∈
On) |
6 | 5 | ex 449 |
. . . . . . . . . . . . . 14
⊢ (𝑗 ∈ On → ((∪ 𝑗
∖ {∅}) ∈ 𝑗
→ (∪ 𝑗 ∖ {∅}) ∈
On)) |
7 | | neldifsnd 4263 |
. . . . . . . . . . . . . . . . 17
⊢
(2𝑜 ∈ 𝑗 → ¬ ∅ ∈ (∪ 𝑗
∖ {∅})) |
8 | | p0ex 4779 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ {∅}
∈ V |
9 | 8 | prid2 4242 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ {∅}
∈ {∅, {∅}} |
10 | | df2o2 7461 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
2𝑜 = {∅, {∅}} |
11 | 9, 10 | eleqtrri 2687 |
. . . . . . . . . . . . . . . . . . . 20
⊢ {∅}
∈ 2𝑜 |
12 | | elunii 4377 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(({∅} ∈ 2𝑜 ∧ 2𝑜
∈ 𝑗) → {∅}
∈ ∪ 𝑗) |
13 | 11, 12 | mpan 702 |
. . . . . . . . . . . . . . . . . . 19
⊢
(2𝑜 ∈ 𝑗 → {∅} ∈ ∪ 𝑗) |
14 | | df1o2 7459 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
1𝑜 = {∅} |
15 | | 1on 7454 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
1𝑜 ∈ On |
16 | 14, 15 | eqeltrri 2685 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ {∅}
∈ On |
17 | 16 | onirri 5751 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ¬
{∅} ∈ {∅} |
18 | 17 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢
(2𝑜 ∈ 𝑗 → ¬ {∅} ∈
{∅}) |
19 | 13, 18 | eldifd 3551 |
. . . . . . . . . . . . . . . . . 18
⊢
(2𝑜 ∈ 𝑗 → {∅} ∈ (∪ 𝑗
∖ {∅})) |
20 | | ne0i 3880 |
. . . . . . . . . . . . . . . . . 18
⊢
({∅} ∈ (∪ 𝑗 ∖ {∅}) → (∪ 𝑗
∖ {∅}) ≠ ∅) |
21 | 19, 20 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢
(2𝑜 ∈ 𝑗 → (∪ 𝑗 ∖ {∅}) ≠
∅) |
22 | 7, 21 | 2thd 254 |
. . . . . . . . . . . . . . . 16
⊢
(2𝑜 ∈ 𝑗 → (¬ ∅ ∈ (∪ 𝑗
∖ {∅}) ↔ (∪ 𝑗 ∖ {∅}) ≠
∅)) |
23 | | nbbn 372 |
. . . . . . . . . . . . . . . 16
⊢ ((¬
∅ ∈ (∪ 𝑗 ∖ {∅}) ↔ (∪ 𝑗
∖ {∅}) ≠ ∅) ↔ ¬ (∅ ∈ (∪ 𝑗
∖ {∅}) ↔ (∪ 𝑗 ∖ {∅}) ≠
∅)) |
24 | 22, 23 | sylib 207 |
. . . . . . . . . . . . . . 15
⊢
(2𝑜 ∈ 𝑗 → ¬ (∅ ∈ (∪ 𝑗
∖ {∅}) ↔ (∪ 𝑗 ∖ {∅}) ≠
∅)) |
25 | | on0eln0 5697 |
. . . . . . . . . . . . . . 15
⊢ ((∪ 𝑗
∖ {∅}) ∈ On → (∅ ∈ (∪ 𝑗
∖ {∅}) ↔ (∪ 𝑗 ∖ {∅}) ≠
∅)) |
26 | 24, 25 | nsyl 134 |
. . . . . . . . . . . . . 14
⊢
(2𝑜 ∈ 𝑗 → ¬ (∪
𝑗 ∖ {∅}) ∈
On) |
27 | 6, 26 | nsyli 154 |
. . . . . . . . . . . . 13
⊢ (𝑗 ∈ On →
(2𝑜 ∈ 𝑗 → ¬ (∪
𝑗 ∖ {∅}) ∈
𝑗)) |
28 | 27 | imp 444 |
. . . . . . . . . . . 12
⊢ ((𝑗 ∈ On ∧
2𝑜 ∈ 𝑗) → ¬ (∪
𝑗 ∖ {∅}) ∈
𝑗) |
29 | | 0ex 4718 |
. . . . . . . . . . . . . . . . . 18
⊢ ∅
∈ V |
30 | 29 | prid1 4241 |
. . . . . . . . . . . . . . . . 17
⊢ ∅
∈ {∅, {∅}} |
31 | 30, 10 | eleqtrri 2687 |
. . . . . . . . . . . . . . . 16
⊢ ∅
∈ 2𝑜 |
32 | | elunii 4377 |
. . . . . . . . . . . . . . . 16
⊢ ((∅
∈ 2𝑜 ∧ 2𝑜 ∈ 𝑗) → ∅ ∈ ∪ 𝑗) |
33 | 31, 32 | mpan 702 |
. . . . . . . . . . . . . . 15
⊢
(2𝑜 ∈ 𝑗 → ∅ ∈ ∪ 𝑗) |
34 | 33 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝑗 ∈ On ∧
2𝑜 ∈ 𝑗) → ∅ ∈ ∪ 𝑗) |
35 | | simpr 476 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑗 ∈ On ∧
2𝑜 ∈ 𝑗) ∧ 𝑎 = ∅) → 𝑎 = ∅) |
36 | 35 | sneqd 4137 |
. . . . . . . . . . . . . . 15
⊢ (((𝑗 ∈ On ∧
2𝑜 ∈ 𝑗) ∧ 𝑎 = ∅) → {𝑎} = {∅}) |
37 | 36 | eleq1d 2672 |
. . . . . . . . . . . . . 14
⊢ (((𝑗 ∈ On ∧
2𝑜 ∈ 𝑗) ∧ 𝑎 = ∅) → ({𝑎} ∈ (Clsd‘𝑗) ↔ {∅} ∈ (Clsd‘𝑗))) |
38 | 34, 37 | rspcdv 3285 |
. . . . . . . . . . . . 13
⊢ ((𝑗 ∈ On ∧
2𝑜 ∈ 𝑗) → (∀𝑎 ∈ ∪ 𝑗{𝑎} ∈ (Clsd‘𝑗) → {∅} ∈ (Clsd‘𝑗))) |
39 | 2 | cldopn 20645 |
. . . . . . . . . . . . 13
⊢
({∅} ∈ (Clsd‘𝑗) → (∪ 𝑗 ∖ {∅}) ∈ 𝑗) |
40 | 38, 39 | syl6 34 |
. . . . . . . . . . . 12
⊢ ((𝑗 ∈ On ∧
2𝑜 ∈ 𝑗) → (∀𝑎 ∈ ∪ 𝑗{𝑎} ∈ (Clsd‘𝑗) → (∪ 𝑗 ∖ {∅}) ∈ 𝑗)) |
41 | 28, 40 | mtod 188 |
. . . . . . . . . . 11
⊢ ((𝑗 ∈ On ∧
2𝑜 ∈ 𝑗) → ¬ ∀𝑎 ∈ ∪ 𝑗{𝑎} ∈ (Clsd‘𝑗)) |
42 | 41 | ex 449 |
. . . . . . . . . 10
⊢ (𝑗 ∈ On →
(2𝑜 ∈ 𝑗 → ¬ ∀𝑎 ∈ ∪ 𝑗{𝑎} ∈ (Clsd‘𝑗))) |
43 | 42 | con2d 128 |
. . . . . . . . 9
⊢ (𝑗 ∈ On → (∀𝑎 ∈ ∪ 𝑗{𝑎} ∈ (Clsd‘𝑗) → ¬ 2𝑜 ∈
𝑗)) |
44 | 4, 43 | syl5 33 |
. . . . . . . 8
⊢ (𝑗 ∈ On → (𝑗 ∈ Fre → ¬
2𝑜 ∈ 𝑗)) |
45 | | 2on 7455 |
. . . . . . . . 9
⊢
2𝑜 ∈ On |
46 | | ontri1 5674 |
. . . . . . . . . 10
⊢ ((𝑗 ∈ On ∧
2𝑜 ∈ On) → (𝑗 ⊆ 2𝑜 ↔ ¬
2𝑜 ∈ 𝑗)) |
47 | | onsssuc 5730 |
. . . . . . . . . 10
⊢ ((𝑗 ∈ On ∧
2𝑜 ∈ On) → (𝑗 ⊆ 2𝑜 ↔ 𝑗 ∈ suc
2𝑜)) |
48 | 46, 47 | bitr3d 269 |
. . . . . . . . 9
⊢ ((𝑗 ∈ On ∧
2𝑜 ∈ On) → (¬ 2𝑜 ∈
𝑗 ↔ 𝑗 ∈ suc
2𝑜)) |
49 | 45, 48 | mpan2 703 |
. . . . . . . 8
⊢ (𝑗 ∈ On → (¬
2𝑜 ∈ 𝑗 ↔ 𝑗 ∈ suc
2𝑜)) |
50 | 44, 49 | sylibd 228 |
. . . . . . 7
⊢ (𝑗 ∈ On → (𝑗 ∈ Fre → 𝑗 ∈ suc
2𝑜)) |
51 | 50 | imp 444 |
. . . . . 6
⊢ ((𝑗 ∈ On ∧ 𝑗 ∈ Fre) → 𝑗 ∈ suc
2𝑜) |
52 | | 0ntop 20535 |
. . . . . . . . . 10
⊢ ¬
∅ ∈ Top |
53 | | t1top 20944 |
. . . . . . . . . 10
⊢ (∅
∈ Fre → ∅ ∈ Top) |
54 | 52, 53 | mto 187 |
. . . . . . . . 9
⊢ ¬
∅ ∈ Fre |
55 | | nelneq 2712 |
. . . . . . . . 9
⊢ ((𝑗 ∈ Fre ∧ ¬ ∅
∈ Fre) → ¬ 𝑗
= ∅) |
56 | 54, 55 | mpan2 703 |
. . . . . . . 8
⊢ (𝑗 ∈ Fre → ¬ 𝑗 = ∅) |
57 | | elsni 4142 |
. . . . . . . 8
⊢ (𝑗 ∈ {∅} → 𝑗 = ∅) |
58 | 56, 57 | nsyl 134 |
. . . . . . 7
⊢ (𝑗 ∈ Fre → ¬ 𝑗 ∈
{∅}) |
59 | 58 | adantl 481 |
. . . . . 6
⊢ ((𝑗 ∈ On ∧ 𝑗 ∈ Fre) → ¬ 𝑗 ∈
{∅}) |
60 | 51, 59 | eldifd 3551 |
. . . . 5
⊢ ((𝑗 ∈ On ∧ 𝑗 ∈ Fre) → 𝑗 ∈ (suc
2𝑜 ∖ {∅})) |
61 | 1, 60 | sylbi 206 |
. . . 4
⊢ (𝑗 ∈ (On ∩ Fre) →
𝑗 ∈ (suc
2𝑜 ∖ {∅})) |
62 | 61 | ssriv 3572 |
. . 3
⊢ (On ∩
Fre) ⊆ (suc 2𝑜 ∖ {∅}) |
63 | | df-suc 5646 |
. . . . . 6
⊢ suc
2𝑜 = (2𝑜 ∪
{2𝑜}) |
64 | 63 | difeq1i 3686 |
. . . . 5
⊢ (suc
2𝑜 ∖ {∅}) = ((2𝑜 ∪
{2𝑜}) ∖ {∅}) |
65 | | difundir 3839 |
. . . . 5
⊢
((2𝑜 ∪ {2𝑜}) ∖
{∅}) = ((2𝑜 ∖ {∅}) ∪
({2𝑜} ∖ {∅})) |
66 | 64, 65 | eqtri 2632 |
. . . 4
⊢ (suc
2𝑜 ∖ {∅}) = ((2𝑜 ∖
{∅}) ∪ ({2𝑜} ∖ {∅})) |
67 | | df-pr 4128 |
. . . . 5
⊢
{1𝑜, 2𝑜} =
({1𝑜} ∪ {2𝑜}) |
68 | | df2o3 7460 |
. . . . . . . . 9
⊢
2𝑜 = {∅,
1𝑜} |
69 | | df-pr 4128 |
. . . . . . . . 9
⊢ {∅,
1𝑜} = ({∅} ∪
{1𝑜}) |
70 | 68, 69 | eqtri 2632 |
. . . . . . . 8
⊢
2𝑜 = ({∅} ∪
{1𝑜}) |
71 | 70 | difeq1i 3686 |
. . . . . . 7
⊢
(2𝑜 ∖ {∅}) = (({∅} ∪
{1𝑜}) ∖ {∅}) |
72 | | difundir 3839 |
. . . . . . 7
⊢
(({∅} ∪ {1𝑜}) ∖ {∅}) =
(({∅} ∖ {∅}) ∪ ({1𝑜} ∖
{∅})) |
73 | | difid 3902 |
. . . . . . . . 9
⊢
({∅} ∖ {∅}) = ∅ |
74 | | 1n0 7462 |
. . . . . . . . . . . 12
⊢
1𝑜 ≠ ∅ |
75 | | disjsn2 4193 |
. . . . . . . . . . . 12
⊢
(1𝑜 ≠ ∅ → ({1𝑜}
∩ {∅}) = ∅) |
76 | 74, 75 | ax-mp 5 |
. . . . . . . . . . 11
⊢
({1𝑜} ∩ {∅}) = ∅ |
77 | 76 | difeq2i 3687 |
. . . . . . . . . 10
⊢
({1𝑜} ∖ ({1𝑜} ∩
{∅})) = ({1𝑜} ∖ ∅) |
78 | | difin 3823 |
. . . . . . . . . 10
⊢
({1𝑜} ∖ ({1𝑜} ∩
{∅})) = ({1𝑜} ∖ {∅}) |
79 | | dif0 3904 |
. . . . . . . . . 10
⊢
({1𝑜} ∖ ∅) =
{1𝑜} |
80 | 77, 78, 79 | 3eqtr3i 2640 |
. . . . . . . . 9
⊢
({1𝑜} ∖ {∅}) =
{1𝑜} |
81 | 73, 80 | uneq12i 3727 |
. . . . . . . 8
⊢
(({∅} ∖ {∅}) ∪ ({1𝑜} ∖
{∅})) = (∅ ∪ {1𝑜}) |
82 | | uncom 3719 |
. . . . . . . 8
⊢ (∅
∪ {1𝑜}) = ({1𝑜} ∪
∅) |
83 | | un0 3919 |
. . . . . . . 8
⊢
({1𝑜} ∪ ∅) =
{1𝑜} |
84 | 81, 82, 83 | 3eqtri 2636 |
. . . . . . 7
⊢
(({∅} ∖ {∅}) ∪ ({1𝑜} ∖
{∅})) = {1𝑜} |
85 | 71, 72, 84 | 3eqtri 2636 |
. . . . . 6
⊢
(2𝑜 ∖ {∅}) =
{1𝑜} |
86 | | 2on0 7456 |
. . . . . . . . 9
⊢
2𝑜 ≠ ∅ |
87 | | disjsn2 4193 |
. . . . . . . . 9
⊢
(2𝑜 ≠ ∅ → ({2𝑜}
∩ {∅}) = ∅) |
88 | 86, 87 | ax-mp 5 |
. . . . . . . 8
⊢
({2𝑜} ∩ {∅}) = ∅ |
89 | 88 | difeq2i 3687 |
. . . . . . 7
⊢
({2𝑜} ∖ ({2𝑜} ∩
{∅})) = ({2𝑜} ∖ ∅) |
90 | | difin 3823 |
. . . . . . 7
⊢
({2𝑜} ∖ ({2𝑜} ∩
{∅})) = ({2𝑜} ∖ {∅}) |
91 | | dif0 3904 |
. . . . . . 7
⊢
({2𝑜} ∖ ∅) =
{2𝑜} |
92 | 89, 90, 91 | 3eqtr3i 2640 |
. . . . . 6
⊢
({2𝑜} ∖ {∅}) =
{2𝑜} |
93 | 85, 92 | uneq12i 3727 |
. . . . 5
⊢
((2𝑜 ∖ {∅}) ∪
({2𝑜} ∖ {∅})) = ({1𝑜} ∪
{2𝑜}) |
94 | 67, 93 | eqtr4i 2635 |
. . . 4
⊢
{1𝑜, 2𝑜} = ((2𝑜
∖ {∅}) ∪ ({2𝑜} ∖
{∅})) |
95 | 66, 94 | eqtr4i 2635 |
. . 3
⊢ (suc
2𝑜 ∖ {∅}) = {1𝑜,
2𝑜} |
96 | 62, 95 | sseqtri 3600 |
. 2
⊢ (On ∩
Fre) ⊆ {1𝑜, 2𝑜} |
97 | | ssoninhaus 31617 |
. . 3
⊢
{1𝑜, 2𝑜} ⊆ (On ∩
Haus) |
98 | | haust1 20966 |
. . . . 5
⊢ (𝑗 ∈ Haus → 𝑗 ∈ Fre) |
99 | 98 | ssriv 3572 |
. . . 4
⊢ Haus
⊆ Fre |
100 | | sslin 3801 |
. . . 4
⊢ (Haus
⊆ Fre → (On ∩ Haus) ⊆ (On ∩ Fre)) |
101 | 99, 100 | ax-mp 5 |
. . 3
⊢ (On ∩
Haus) ⊆ (On ∩ Fre) |
102 | 97, 101 | sstri 3577 |
. 2
⊢
{1𝑜, 2𝑜} ⊆ (On ∩
Fre) |
103 | 96, 102 | eqssi 3584 |
1
⊢ (On ∩
Fre) = {1𝑜, 2𝑜} |