Step | Hyp | Ref
| Expression |
1 | | spacval 6282 |
. . 3
⊢ (M ∈ NC → ( Spac
‘M) = Clos1
({M}, {〈x, y〉 ∣ (x ∈ NC ∧ y ∈ NC ∧ y =
(2c ↑c x))})) |
2 | 1 | adantr 451 |
. 2
⊢ ((M ∈ NC ∧ ¬ (M ↑c 0c)
∈ NC ) → (
Spac ‘M) = Clos1 ({M}, {〈x, y〉 ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c
x))})) |
3 | | elimasn 5019 |
. . . . . . . 8
⊢ (p ∈ ({〈x, y〉 ∣ (x ∈ NC ∧ y ∈ NC ∧ y =
(2c ↑c x))} “ {M}) ↔ 〈M, p〉 ∈ {〈x, y〉 ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c
x))}) |
4 | | df-br 4640 |
. . . . . . . 8
⊢ (M{〈x, y〉 ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c
x))}p
↔ 〈M, p〉 ∈ {〈x, y〉 ∣ (x ∈ NC ∧ y ∈ NC ∧ y =
(2c ↑c x))}) |
5 | 3, 4 | bitr4i 243 |
. . . . . . 7
⊢ (p ∈ ({〈x, y〉 ∣ (x ∈ NC ∧ y ∈ NC ∧ y =
(2c ↑c x))} “ {M}) ↔ M{〈x, y〉 ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c
x))}p) |
6 | | vex 2862 |
. . . . . . . . 9
⊢ p ∈
V |
7 | | eleq1 2413 |
. . . . . . . . . . 11
⊢ (x = M →
(x ∈
NC ↔ M
∈ NC
)) |
8 | | oveq2 5531 |
. . . . . . . . . . . 12
⊢ (x = M →
(2c ↑c x) = (2c ↑c
M)) |
9 | 8 | eqeq2d 2364 |
. . . . . . . . . . 11
⊢ (x = M →
(y = (2c
↑c x) ↔
y = (2c
↑c M))) |
10 | 7, 9 | 3anbi13d 1254 |
. . . . . . . . . 10
⊢ (x = M →
((x ∈
NC ∧ y ∈ NC ∧ y = (2c ↑c
x)) ↔ (M ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c
M)))) |
11 | | eleq1 2413 |
. . . . . . . . . . 11
⊢ (y = p →
(y ∈
NC ↔ p
∈ NC
)) |
12 | | eqeq1 2359 |
. . . . . . . . . . 11
⊢ (y = p →
(y = (2c
↑c M) ↔
p = (2c
↑c M))) |
13 | 11, 12 | 3anbi23d 1255 |
. . . . . . . . . 10
⊢ (y = p →
((M ∈
NC ∧ y ∈ NC ∧ y = (2c ↑c
M)) ↔ (M ∈ NC ∧ p ∈ NC ∧ p = (2c ↑c
M)))) |
14 | | eqid 2353 |
. . . . . . . . . 10
⊢ {〈x, y〉 ∣ (x ∈ NC ∧ y ∈ NC ∧ y =
(2c ↑c x))} = {〈x, y〉 ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c
x))} |
15 | 10, 13, 14 | brabg 4706 |
. . . . . . . . 9
⊢ ((M ∈ NC ∧ p ∈ V) →
(M{〈x, y〉 ∣ (x ∈ NC ∧ y ∈ NC ∧ y =
(2c ↑c x))}p ↔
(M ∈
NC ∧ p ∈ NC ∧ p = (2c ↑c
M)))) |
16 | 6, 15 | mpan2 652 |
. . . . . . . 8
⊢ (M ∈ NC → (M{〈x, y〉 ∣ (x ∈ NC ∧ y ∈ NC ∧ y =
(2c ↑c x))}p ↔
(M ∈
NC ∧ p ∈ NC ∧ p = (2c ↑c
M)))) |
17 | | eleq1 2413 |
. . . . . . . . . . 11
⊢ (p = (2c ↑c
M) → (p ∈ NC ↔ (2c
↑c M) ∈ NC
)) |
18 | 17 | biimpac 472 |
. . . . . . . . . 10
⊢ ((p ∈ NC ∧ p = (2c ↑c
M)) → (2c
↑c M) ∈ NC
) |
19 | | 2nc 6168 |
. . . . . . . . . . 11
⊢
2c ∈ NC |
20 | | ceclr 6187 |
. . . . . . . . . . . 12
⊢
((2c ∈ NC ∧ M ∈ NC ∧
(2c ↑c M) ∈ NC ) → ((2c
↑c 0c) ∈ NC ∧ (M
↑c 0c) ∈ NC
)) |
21 | 20 | simprd 449 |
. . . . . . . . . . 11
⊢
((2c ∈ NC ∧ M ∈ NC ∧
(2c ↑c M) ∈ NC ) → (M
↑c 0c) ∈ NC
) |
22 | 19, 21 | mp3an1 1264 |
. . . . . . . . . 10
⊢ ((M ∈ NC ∧
(2c ↑c M) ∈ NC ) → (M
↑c 0c) ∈ NC
) |
23 | 18, 22 | sylan2 460 |
. . . . . . . . 9
⊢ ((M ∈ NC ∧ (p ∈ NC ∧ p = (2c ↑c
M))) → (M ↑c 0c)
∈ NC
) |
24 | 23 | 3impb 1147 |
. . . . . . . 8
⊢ ((M ∈ NC ∧ p ∈ NC ∧ p = (2c ↑c
M)) → (M ↑c 0c)
∈ NC
) |
25 | 16, 24 | syl6bi 219 |
. . . . . . 7
⊢ (M ∈ NC → (M{〈x, y〉 ∣ (x ∈ NC ∧ y ∈ NC ∧ y =
(2c ↑c x))}p →
(M ↑c
0c) ∈ NC )) |
26 | 5, 25 | syl5bi 208 |
. . . . . 6
⊢ (M ∈ NC → (p ∈ ({〈x, y〉 ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c
x))} “ {M}) → (M
↑c 0c) ∈ NC
)) |
27 | 26 | con3d 125 |
. . . . 5
⊢ (M ∈ NC → (¬ (M
↑c 0c) ∈ NC → ¬
p ∈
({〈x,
y〉 ∣ (x ∈ NC ∧ y ∈ NC ∧ y =
(2c ↑c x))} “ {M}))) |
28 | 27 | imp 418 |
. . . 4
⊢ ((M ∈ NC ∧ ¬ (M ↑c 0c)
∈ NC ) →
¬ p ∈
({〈x,
y〉 ∣ (x ∈ NC ∧ y ∈ NC ∧ y =
(2c ↑c x))} “ {M})) |
29 | 28 | eq0rdv 3585 |
. . 3
⊢ ((M ∈ NC ∧ ¬ (M ↑c 0c)
∈ NC ) →
({〈x,
y〉 ∣ (x ∈ NC ∧ y ∈ NC ∧ y =
(2c ↑c x))} “ {M}) = ∅) |
30 | | snex 4111 |
. . . 4
⊢ {M} ∈
V |
31 | | spacvallem1 6281 |
. . . 4
⊢ {〈x, y〉 ∣ (x ∈ NC ∧ y ∈ NC ∧ y =
(2c ↑c x))} ∈
V |
32 | | eqid 2353 |
. . . 4
⊢ Clos1 ({M}, {〈x, y〉 ∣ (x ∈ NC ∧ y ∈ NC ∧ y =
(2c ↑c x))}) = Clos1
({M}, {〈x, y〉 ∣ (x ∈ NC ∧ y ∈ NC ∧ y =
(2c ↑c x))}) |
33 | 30, 31, 32 | clos1nrel 5886 |
. . 3
⊢ (({〈x, y〉 ∣ (x ∈ NC ∧ y ∈ NC ∧ y =
(2c ↑c x))} “ {M}) = ∅ →
Clos1 ({M},
{〈x,
y〉 ∣ (x ∈ NC ∧ y ∈ NC ∧ y =
(2c ↑c x))}) = {M}) |
34 | 29, 33 | syl 15 |
. 2
⊢ ((M ∈ NC ∧ ¬ (M ↑c 0c)
∈ NC ) →
Clos1 ({M},
{〈x,
y〉 ∣ (x ∈ NC ∧ y ∈ NC ∧ y =
(2c ↑c x))}) = {M}) |
35 | 2, 34 | eqtrd 2385 |
1
⊢ ((M ∈ NC ∧ ¬ (M ↑c 0c)
∈ NC ) → (
Spac ‘M) = {M}) |