Step | Hyp | Ref
| Expression |
1 | | simp2 956 |
. . . 4
⊢ ((M ∈ NC ∧ N ∈ ( Spac ‘M) ∧ (N ↑c 0c)
∈ NC ) →
N ∈ (
Spac ‘M)) |
2 | | spacval 6282 |
. . . . 5
⊢ (M ∈ NC → ( Spac
‘M) = Clos1
({M}, {〈x, y〉 ∣ (x ∈ NC ∧ y ∈ NC ∧ y =
(2c ↑c x))})) |
3 | 2 | 3ad2ant1 976 |
. . . 4
⊢ ((M ∈ NC ∧ N ∈ ( Spac ‘M) ∧ (N ↑c 0c)
∈ NC ) → (
Spac ‘M) = Clos1 ({M}, {〈x, y〉 ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c
x))})) |
4 | 1, 3 | eleqtrd 2429 |
. . 3
⊢ ((M ∈ NC ∧ N ∈ ( Spac ‘M) ∧ (N ↑c 0c)
∈ NC ) →
N ∈ Clos1 ({M}, {〈x, y〉 ∣ (x ∈ NC ∧ y ∈ NC ∧ y =
(2c ↑c x))})) |
5 | | spacssnc 6284 |
. . . . . 6
⊢ (M ∈ NC → ( Spac
‘M) ⊆ NC
) |
6 | 5 | sselda 3273 |
. . . . 5
⊢ ((M ∈ NC ∧ N ∈ ( Spac ‘M)) → N
∈ NC
) |
7 | 6 | 3adant3 975 |
. . . 4
⊢ ((M ∈ NC ∧ N ∈ ( Spac ‘M) ∧ (N ↑c 0c)
∈ NC ) →
N ∈ NC ) |
8 | | simp3 957 |
. . . . 5
⊢ ((M ∈ NC ∧ N ∈ ( Spac ‘M) ∧ (N ↑c 0c)
∈ NC ) →
(N ↑c
0c) ∈ NC ) |
9 | | 2nnc 6167 |
. . . . . 6
⊢
2c ∈ Nn |
10 | | ceclnn1 6189 |
. . . . . 6
⊢
((2c ∈ Nn ∧ N ∈ NC ∧ (N ↑c 0c)
∈ NC ) →
(2c ↑c N) ∈ NC ) |
11 | 9, 10 | mp3an1 1264 |
. . . . 5
⊢ ((N ∈ NC ∧ (N ↑c 0c)
∈ NC ) →
(2c ↑c N) ∈ NC ) |
12 | 7, 8, 11 | syl2anc 642 |
. . . 4
⊢ ((M ∈ NC ∧ N ∈ ( Spac ‘M) ∧ (N ↑c 0c)
∈ NC ) →
(2c ↑c N) ∈ NC ) |
13 | | eqidd 2354 |
. . . 4
⊢ ((M ∈ NC ∧ N ∈ ( Spac ‘M) ∧ (N ↑c 0c)
∈ NC ) →
(2c ↑c N) = (2c ↑c
N)) |
14 | | ovex 5551 |
. . . . . 6
⊢
(2c ↑c N) ∈
V |
15 | | eleq1 2413 |
. . . . . . . 8
⊢ (x = N →
(x ∈
NC ↔ N
∈ NC
)) |
16 | | oveq2 5531 |
. . . . . . . . 9
⊢ (x = N →
(2c ↑c x) = (2c ↑c
N)) |
17 | 16 | eqeq2d 2364 |
. . . . . . . 8
⊢ (x = N →
(y = (2c
↑c x) ↔
y = (2c
↑c N))) |
18 | 15, 17 | 3anbi13d 1254 |
. . . . . . 7
⊢ (x = N →
((x ∈
NC ∧ y ∈ NC ∧ y = (2c ↑c
x)) ↔ (N ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c
N)))) |
19 | | eleq1 2413 |
. . . . . . . 8
⊢ (y = (2c ↑c
N) → (y ∈ NC ↔ (2c
↑c N) ∈ NC
)) |
20 | | eqeq1 2359 |
. . . . . . . 8
⊢ (y = (2c ↑c
N) → (y = (2c ↑c
N) ↔ (2c
↑c N) =
(2c ↑c N))) |
21 | 19, 20 | 3anbi23d 1255 |
. . . . . . 7
⊢ (y = (2c ↑c
N) → ((N ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c
N)) ↔ (N ∈ NC ∧
(2c ↑c N) ∈ NC ∧
(2c ↑c N) = (2c ↑c
N)))) |
22 | | eqid 2353 |
. . . . . . 7
⊢ {〈x, y〉 ∣ (x ∈ NC ∧ y ∈ NC ∧ y =
(2c ↑c x))} = {〈x, y〉 ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c
x))} |
23 | 18, 21, 22 | brabg 4706 |
. . . . . 6
⊢ ((N ∈ ( Spac ‘M) ∧
(2c ↑c N) ∈ V) →
(N{〈x, y〉 ∣ (x ∈ NC ∧ y ∈ NC ∧ y =
(2c ↑c x))} (2c ↑c
N) ↔ (N ∈ NC ∧
(2c ↑c N) ∈ NC ∧
(2c ↑c N) = (2c ↑c
N)))) |
24 | 14, 23 | mpan2 652 |
. . . . 5
⊢ (N ∈ ( Spac ‘M) → (N{〈x, y〉 ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c
x))} (2c
↑c N) ↔
(N ∈
NC ∧
(2c ↑c N) ∈ NC ∧
(2c ↑c N) = (2c ↑c
N)))) |
25 | 24 | 3ad2ant2 977 |
. . . 4
⊢ ((M ∈ NC ∧ N ∈ ( Spac ‘M) ∧ (N ↑c 0c)
∈ NC ) →
(N{〈x, y〉 ∣ (x ∈ NC ∧ y ∈ NC ∧ y =
(2c ↑c x))} (2c ↑c
N) ↔ (N ∈ NC ∧
(2c ↑c N) ∈ NC ∧
(2c ↑c N) = (2c ↑c
N)))) |
26 | 7, 12, 13, 25 | mpbir3and 1135 |
. . 3
⊢ ((M ∈ NC ∧ N ∈ ( Spac ‘M) ∧ (N ↑c 0c)
∈ NC ) →
N{〈x, y〉 ∣ (x ∈ NC ∧ y ∈ NC ∧ y =
(2c ↑c x))} (2c ↑c
N)) |
27 | | 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))}) |
28 | 27 | clos1conn 5879 |
. . 3
⊢ ((N ∈ Clos1 ({M}, {〈x, y〉 ∣ (x ∈ NC ∧ y ∈ NC ∧ y =
(2c ↑c x))}) ∧ N{〈x, y〉 ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c
x))} (2c
↑c N)) →
(2c ↑c N) ∈ Clos1 ({M}, {〈x, y〉 ∣ (x ∈ NC ∧ y ∈ NC ∧ y =
(2c ↑c x))})) |
29 | 4, 26, 28 | syl2anc 642 |
. 2
⊢ ((M ∈ NC ∧ N ∈ ( Spac ‘M) ∧ (N ↑c 0c)
∈ NC ) →
(2c ↑c N) ∈ Clos1 ({M}, {〈x, y〉 ∣ (x ∈ NC ∧ y ∈ NC ∧ y =
(2c ↑c x))})) |
30 | 29, 3 | eleqtrrd 2430 |
1
⊢ ((M ∈ NC ∧ N ∈ ( Spac ‘M) ∧ (N ↑c 0c)
∈ NC ) →
(2c ↑c N) ∈ ( Spac ‘M)) |