Step | Hyp | Ref
| Expression |
1 | | elex 2867 |
. 2
⊢ (S ∈ V → S ∈ V) |
2 | | spacval 6282 |
. . . . 5
⊢ (M ∈ NC → ( Spac
‘M) = Clos1
({M}, {〈p, q〉 ∣ (p ∈ NC ∧ q ∈ NC ∧ q =
(2c ↑c p))})) |
3 | 2 | adantr 451 |
. . . 4
⊢ ((M ∈ NC ∧ S ∈ V) → (
Spac ‘M) = Clos1 ({M}, {〈p, q〉 ∣ (p ∈ NC ∧ q ∈ NC ∧ q = (2c ↑c
p))})) |
4 | 3 | adantr 451 |
. . 3
⊢ (((M ∈ NC ∧ S ∈ V) ∧ (M ∈ S ∧ ∀x ∈ ( Spac ‘M)((x ∈ S ∧ (x
↑c 0c) ∈ NC ) →
(2c ↑c x) ∈ S))) → ( Spac ‘M) = Clos1 ({M}, {〈p, q〉 ∣ (p ∈ NC ∧ q ∈ NC ∧ q = (2c ↑c
p))})) |
5 | | simplr 731 |
. . . 4
⊢ (((M ∈ NC ∧ S ∈ V) ∧ (M ∈ S ∧ ∀x ∈ ( Spac ‘M)((x ∈ S ∧ (x
↑c 0c) ∈ NC ) →
(2c ↑c x) ∈ S))) → S
∈ V) |
6 | | snssi 3852 |
. . . . . 6
⊢ (M ∈ S → {M}
⊆ S) |
7 | 6 | adantr 451 |
. . . . 5
⊢ ((M ∈ S ∧ ∀x ∈ ( Spac
‘M)((x ∈ S ∧ (x ↑c 0c)
∈ NC ) →
(2c ↑c x) ∈ S)) → {M}
⊆ S) |
8 | 7 | adantl 452 |
. . . 4
⊢ (((M ∈ NC ∧ S ∈ V) ∧ (M ∈ S ∧ ∀x ∈ ( Spac ‘M)((x ∈ S ∧ (x
↑c 0c) ∈ NC ) →
(2c ↑c x) ∈ S))) → {M}
⊆ S) |
9 | | spacssnc 6284 |
. . . . . . . . . . 11
⊢ (M ∈ NC → ( Spac
‘M) ⊆ NC
) |
10 | 9 | sseld 3272 |
. . . . . . . . . 10
⊢ (M ∈ NC → (x ∈ ( Spac
‘M) → x ∈ NC )) |
11 | | 2nc 6168 |
. . . . . . . . . . . . . . . . . . . 20
⊢
2c ∈ NC |
12 | | ceclr 6187 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((2c ∈ NC ∧ x ∈ NC ∧
(2c ↑c x) ∈ NC ) → ((2c
↑c 0c) ∈ NC ∧ (x
↑c 0c) ∈ NC
)) |
13 | 12 | simprd 449 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((2c ∈ NC ∧ x ∈ NC ∧
(2c ↑c x) ∈ NC ) → (x
↑c 0c) ∈ NC
) |
14 | 11, 13 | mp3an1 1264 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((x ∈ NC ∧
(2c ↑c x) ∈ NC ) → (x
↑c 0c) ∈ NC
) |
15 | 14 | ex 423 |
. . . . . . . . . . . . . . . . . 18
⊢ (x ∈ NC → ((2c
↑c x) ∈ NC → (x ↑c 0c)
∈ NC
)) |
16 | 15 | imim1d 69 |
. . . . . . . . . . . . . . . . 17
⊢ (x ∈ NC → (((x
↑c 0c) ∈ NC →
(2c ↑c x) ∈ S) → ((2c
↑c x) ∈ NC →
(2c ↑c x) ∈ S))) |
17 | 16 | a1dd 42 |
. . . . . . . . . . . . . . . 16
⊢ (x ∈ NC → (((x
↑c 0c) ∈ NC →
(2c ↑c x) ∈ S) → (x
∈ NC →
((2c ↑c x) ∈ NC → (2c
↑c x) ∈ S)))) |
18 | 17 | adantl 452 |
. . . . . . . . . . . . . . 15
⊢ ((M ∈ NC ∧ x ∈ NC ) → (((x
↑c 0c) ∈ NC →
(2c ↑c x) ∈ S) → (x
∈ NC →
((2c ↑c x) ∈ NC → (2c
↑c x) ∈ S)))) |
19 | | 3anass 938 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((x ∈ NC ∧ z ∈ NC ∧ z = (2c ↑c
x)) ↔ (x ∈ NC ∧ (z ∈ NC ∧ z = (2c ↑c
x)))) |
20 | 19 | imbi1i 315 |
. . . . . . . . . . . . . . . . . 18
⊢ (((x ∈ NC ∧ z ∈ NC ∧ z = (2c ↑c
x)) → z ∈ S) ↔ ((x
∈ NC ∧ (z ∈ NC ∧ z =
(2c ↑c x))) → z
∈ S)) |
21 | | impexp 433 |
. . . . . . . . . . . . . . . . . 18
⊢ (((x ∈ NC ∧ (z ∈ NC ∧ z = (2c ↑c
x))) → z ∈ S) ↔ (x
∈ NC →
((z ∈
NC ∧ z = (2c ↑c
x)) → z ∈ S))) |
22 | 20, 21 | bitri 240 |
. . . . . . . . . . . . . . . . 17
⊢ (((x ∈ NC ∧ z ∈ NC ∧ z = (2c ↑c
x)) → z ∈ S) ↔ (x
∈ NC →
((z ∈
NC ∧ z = (2c ↑c
x)) → z ∈ S))) |
23 | 22 | albii 1566 |
. . . . . . . . . . . . . . . 16
⊢ (∀z((x ∈ NC ∧ z ∈ NC ∧ z = (2c ↑c
x)) → z ∈ S) ↔ ∀z(x ∈ NC → ((z ∈ NC ∧ z =
(2c ↑c x)) → z
∈ S))) |
24 | | 19.21v 1890 |
. . . . . . . . . . . . . . . . 17
⊢ (∀z(x ∈ NC → ((z ∈ NC ∧ z =
(2c ↑c x)) → z
∈ S))
↔ (x ∈ NC → ∀z((z ∈ NC ∧ z = (2c ↑c
x)) → z ∈ S))) |
25 | | impexp 433 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((z ∈ NC ∧ z = (2c ↑c
x)) → z ∈ S) ↔ (z
∈ NC →
(z = (2c
↑c x) →
z ∈
S))) |
26 | | bi2.04 350 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((z ∈ NC → (z =
(2c ↑c x) → z
∈ S))
↔ (z = (2c
↑c x) →
(z ∈
NC → z
∈ S))) |
27 | 25, 26 | bitri 240 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((z ∈ NC ∧ z = (2c ↑c
x)) → z ∈ S) ↔ (z =
(2c ↑c x) → (z
∈ NC →
z ∈
S))) |
28 | 27 | albii 1566 |
. . . . . . . . . . . . . . . . . . 19
⊢ (∀z((z ∈ NC ∧ z = (2c ↑c
x)) → z ∈ S) ↔ ∀z(z = (2c ↑c
x) → (z ∈ NC → z ∈ S))) |
29 | | ovex 5551 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(2c ↑c x) ∈
V |
30 | | eleq1 2413 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (z = (2c ↑c
x) → (z ∈ NC ↔ (2c
↑c x) ∈ NC
)) |
31 | | eleq1 2413 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (z = (2c ↑c
x) → (z ∈ S ↔ (2c
↑c x) ∈ S)) |
32 | 30, 31 | imbi12d 311 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (z = (2c ↑c
x) → ((z ∈ NC → z ∈ S) ↔
((2c ↑c x) ∈ NC → (2c
↑c x) ∈ S))) |
33 | 29, 32 | ceqsalv 2885 |
. . . . . . . . . . . . . . . . . . 19
⊢ (∀z(z = (2c ↑c
x) → (z ∈ NC → z ∈ S)) ↔
((2c ↑c x) ∈ NC → (2c
↑c x) ∈ S)) |
34 | 28, 33 | bitri 240 |
. . . . . . . . . . . . . . . . . 18
⊢ (∀z((z ∈ NC ∧ z = (2c ↑c
x)) → z ∈ S) ↔ ((2c
↑c x) ∈ NC →
(2c ↑c x) ∈ S)) |
35 | 34 | imbi2i 303 |
. . . . . . . . . . . . . . . . 17
⊢ ((x ∈ NC → ∀z((z ∈ NC ∧ z =
(2c ↑c x)) → z
∈ S))
↔ (x ∈ NC →
((2c ↑c x) ∈ NC → (2c
↑c x) ∈ S))) |
36 | 24, 35 | bitri 240 |
. . . . . . . . . . . . . . . 16
⊢ (∀z(x ∈ NC → ((z ∈ NC ∧ z =
(2c ↑c x)) → z
∈ S))
↔ (x ∈ NC →
((2c ↑c x) ∈ NC → (2c
↑c x) ∈ S))) |
37 | 23, 36 | bitri 240 |
. . . . . . . . . . . . . . 15
⊢ (∀z((x ∈ NC ∧ z ∈ NC ∧ z = (2c ↑c
x)) → z ∈ S) ↔ (x
∈ NC →
((2c ↑c x) ∈ NC → (2c
↑c x) ∈ S))) |
38 | 18, 37 | syl6ibr 218 |
. . . . . . . . . . . . . 14
⊢ ((M ∈ NC ∧ x ∈ NC ) → (((x
↑c 0c) ∈ NC →
(2c ↑c x) ∈ S) → ∀z((x ∈ NC ∧ z ∈ NC ∧ z = (2c ↑c
x)) → z ∈ S))) |
39 | | vex 2862 |
. . . . . . . . . . . . . . . . 17
⊢ x ∈
V |
40 | | vex 2862 |
. . . . . . . . . . . . . . . . 17
⊢ z ∈
V |
41 | | eleq1 2413 |
. . . . . . . . . . . . . . . . . 18
⊢ (p = x →
(p ∈
NC ↔ x
∈ NC
)) |
42 | | oveq2 5531 |
. . . . . . . . . . . . . . . . . . 19
⊢ (p = x →
(2c ↑c p) = (2c ↑c
x)) |
43 | 42 | eqeq2d 2364 |
. . . . . . . . . . . . . . . . . 18
⊢ (p = x →
(q = (2c
↑c p) ↔
q = (2c
↑c x))) |
44 | 41, 43 | 3anbi13d 1254 |
. . . . . . . . . . . . . . . . 17
⊢ (p = x →
((p ∈
NC ∧ q ∈ NC ∧ q = (2c ↑c
p)) ↔ (x ∈ NC ∧ q ∈ NC ∧ q = (2c ↑c
x)))) |
45 | | eleq1 2413 |
. . . . . . . . . . . . . . . . . 18
⊢ (q = z →
(q ∈
NC ↔ z
∈ NC
)) |
46 | | eqeq1 2359 |
. . . . . . . . . . . . . . . . . 18
⊢ (q = z →
(q = (2c
↑c x) ↔
z = (2c
↑c x))) |
47 | 45, 46 | 3anbi23d 1255 |
. . . . . . . . . . . . . . . . 17
⊢ (q = z →
((x ∈
NC ∧ q ∈ NC ∧ q = (2c ↑c
x)) ↔ (x ∈ NC ∧ z ∈ NC ∧ z = (2c ↑c
x)))) |
48 | | eqid 2353 |
. . . . . . . . . . . . . . . . 17
⊢ {〈p, q〉 ∣ (p ∈ NC ∧ q ∈ NC ∧ q =
(2c ↑c p))} = {〈p, q〉 ∣ (p ∈ NC ∧ q ∈ NC ∧ q = (2c ↑c
p))} |
49 | 39, 40, 44, 47, 48 | brab 4709 |
. . . . . . . . . . . . . . . 16
⊢ (x{〈p, q〉 ∣ (p ∈ NC ∧ q ∈ NC ∧ q = (2c ↑c
p))}z
↔ (x ∈ NC ∧ z ∈ NC ∧ z =
(2c ↑c x))) |
50 | 49 | imbi1i 315 |
. . . . . . . . . . . . . . 15
⊢ ((x{〈p, q〉 ∣ (p ∈ NC ∧ q ∈ NC ∧ q = (2c ↑c
p))}z
→ z ∈ S) ↔
((x ∈
NC ∧ z ∈ NC ∧ z = (2c ↑c
x)) → z ∈ S)) |
51 | 50 | albii 1566 |
. . . . . . . . . . . . . 14
⊢ (∀z(x{〈p, q〉 ∣ (p ∈ NC ∧ q ∈ NC ∧ q = (2c ↑c
p))}z
→ z ∈ S) ↔
∀z((x ∈ NC ∧ z ∈ NC ∧ z =
(2c ↑c x)) → z
∈ S)) |
52 | 38, 51 | syl6ibr 218 |
. . . . . . . . . . . . 13
⊢ ((M ∈ NC ∧ x ∈ NC ) → (((x
↑c 0c) ∈ NC →
(2c ↑c x) ∈ S) → ∀z(x{〈p, q〉 ∣ (p ∈ NC ∧ q ∈ NC ∧ q = (2c ↑c
p))}z
→ z ∈ S))) |
53 | 52 | imim2d 48 |
. . . . . . . . . . . 12
⊢ ((M ∈ NC ∧ x ∈ NC ) → ((x
∈ S
→ ((x ↑c
0c) ∈ NC → (2c
↑c x) ∈ S)) →
(x ∈
S → ∀z(x{〈p, q〉 ∣ (p ∈ NC ∧ q ∈ NC ∧ q = (2c ↑c
p))}z
→ z ∈ S)))) |
54 | | impexp 433 |
. . . . . . . . . . . 12
⊢ (((x ∈ S ∧ (x ↑c 0c)
∈ NC ) →
(2c ↑c x) ∈ S) ↔ (x
∈ S
→ ((x ↑c
0c) ∈ NC → (2c
↑c x) ∈ S))) |
55 | | impexp 433 |
. . . . . . . . . . . . . 14
⊢ (((x ∈ S ∧ x{〈p, q〉 ∣ (p ∈ NC ∧ q ∈ NC ∧ q = (2c ↑c
p))}z)
→ z ∈ S) ↔
(x ∈
S → (x{〈p, q〉 ∣ (p ∈ NC ∧ q ∈ NC ∧ q = (2c ↑c
p))}z
→ z ∈ S))) |
56 | 55 | albii 1566 |
. . . . . . . . . . . . 13
⊢ (∀z((x ∈ S ∧ x{〈p, q〉 ∣ (p ∈ NC ∧ q ∈ NC ∧ q = (2c ↑c
p))}z)
→ z ∈ S) ↔
∀z(x ∈ S →
(x{〈p, q〉 ∣ (p ∈ NC ∧ q ∈ NC ∧ q =
(2c ↑c p))}z →
z ∈
S))) |
57 | | 19.21v 1890 |
. . . . . . . . . . . . 13
⊢ (∀z(x ∈ S → (x{〈p, q〉 ∣ (p ∈ NC ∧ q ∈ NC ∧ q = (2c ↑c
p))}z
→ z ∈ S)) ↔
(x ∈
S → ∀z(x{〈p, q〉 ∣ (p ∈ NC ∧ q ∈ NC ∧ q = (2c ↑c
p))}z
→ z ∈ S))) |
58 | 56, 57 | bitri 240 |
. . . . . . . . . . . 12
⊢ (∀z((x ∈ S ∧ x{〈p, q〉 ∣ (p ∈ NC ∧ q ∈ NC ∧ q = (2c ↑c
p))}z)
→ z ∈ S) ↔
(x ∈
S → ∀z(x{〈p, q〉 ∣ (p ∈ NC ∧ q ∈ NC ∧ q = (2c ↑c
p))}z
→ z ∈ S))) |
59 | 53, 54, 58 | 3imtr4g 261 |
. . . . . . . . . . 11
⊢ ((M ∈ NC ∧ x ∈ NC ) → (((x
∈ S ∧ (x
↑c 0c) ∈ NC ) →
(2c ↑c x) ∈ S) → ∀z((x ∈ S ∧ x{〈p, q〉 ∣ (p ∈ NC ∧ q ∈ NC ∧ q = (2c ↑c
p))}z)
→ z ∈ S))) |
60 | 59 | ex 423 |
. . . . . . . . . 10
⊢ (M ∈ NC → (x ∈ NC →
(((x ∈
S ∧
(x ↑c
0c) ∈ NC ) → (2c
↑c x) ∈ S) →
∀z((x ∈ S ∧ x{〈p, q〉 ∣ (p ∈ NC ∧ q ∈ NC ∧ q =
(2c ↑c p))}z) →
z ∈
S)))) |
61 | 10, 60 | syld 40 |
. . . . . . . . 9
⊢ (M ∈ NC → (x ∈ ( Spac
‘M) → (((x ∈ S ∧ (x ↑c 0c)
∈ NC ) →
(2c ↑c x) ∈ S) → ∀z((x ∈ S ∧ x{〈p, q〉 ∣ (p ∈ NC ∧ q ∈ NC ∧ q = (2c ↑c
p))}z)
→ z ∈ S)))) |
62 | 61 | imp 418 |
. . . . . . . 8
⊢ ((M ∈ NC ∧ x ∈ ( Spac ‘M)) → (((x
∈ S ∧ (x
↑c 0c) ∈ NC ) →
(2c ↑c x) ∈ S) → ∀z((x ∈ S ∧ x{〈p, q〉 ∣ (p ∈ NC ∧ q ∈ NC ∧ q = (2c ↑c
p))}z)
→ z ∈ S))) |
63 | 62 | ralimdva 2692 |
. . . . . . 7
⊢ (M ∈ NC → (∀x ∈ ( Spac ‘M)((x ∈ S ∧ (x
↑c 0c) ∈ NC ) →
(2c ↑c x) ∈ S) → ∀x ∈ ( Spac
‘M)∀z((x ∈ S ∧ x{〈p, q〉 ∣ (p ∈ NC ∧ q ∈ NC ∧ q = (2c ↑c
p))}z)
→ z ∈ S))) |
64 | | raleq 2807 |
. . . . . . . 8
⊢ (( Spac ‘M) = Clos1 ({M}, {〈p, q〉 ∣ (p ∈ NC ∧ q ∈ NC ∧ q = (2c ↑c
p))}) → (∀x ∈ ( Spac
‘M)∀z((x ∈ S ∧ x{〈p, q〉 ∣ (p ∈ NC ∧ q ∈ NC ∧ q = (2c ↑c
p))}z)
→ z ∈ S) ↔
∀x
∈ Clos1
({M}, {〈p, q〉 ∣ (p ∈ NC ∧ q ∈ NC ∧ q =
(2c ↑c p))})∀z((x ∈ S ∧ x{〈p, q〉 ∣ (p ∈ NC ∧ q ∈ NC ∧ q =
(2c ↑c p))}z) →
z ∈
S))) |
65 | 2, 64 | syl 15 |
. . . . . . 7
⊢ (M ∈ NC → (∀x ∈ ( Spac ‘M)∀z((x ∈ S ∧ x{〈p, q〉 ∣ (p ∈ NC ∧ q ∈ NC ∧ q =
(2c ↑c p))}z) →
z ∈
S) ↔ ∀x ∈ Clos1 ({M}, {〈p, q〉 ∣ (p ∈ NC ∧ q ∈ NC ∧ q = (2c ↑c
p))})∀z((x ∈ S ∧ x{〈p, q〉 ∣ (p ∈ NC ∧ q ∈ NC ∧ q = (2c ↑c
p))}z)
→ z ∈ S))) |
66 | 63, 65 | sylibd 205 |
. . . . . 6
⊢ (M ∈ NC → (∀x ∈ ( Spac ‘M)((x ∈ S ∧ (x
↑c 0c) ∈ NC ) →
(2c ↑c x) ∈ S) → ∀x ∈ Clos1 ({M}, {〈p, q〉 ∣ (p ∈ NC ∧ q ∈ NC ∧ q = (2c ↑c
p))})∀z((x ∈ S ∧ x{〈p, q〉 ∣ (p ∈ NC ∧ q ∈ NC ∧ q = (2c ↑c
p))}z)
→ z ∈ S))) |
67 | 66 | imp 418 |
. . . . 5
⊢ ((M ∈ NC ∧ ∀x ∈ ( Spac
‘M)((x ∈ S ∧ (x ↑c 0c)
∈ NC ) →
(2c ↑c x) ∈ S)) → ∀x ∈ Clos1 ({M}, {〈p, q〉 ∣ (p ∈ NC ∧ q ∈ NC ∧ q = (2c ↑c
p))})∀z((x ∈ S ∧ x{〈p, q〉 ∣ (p ∈ NC ∧ q ∈ NC ∧ q = (2c ↑c
p))}z)
→ z ∈ S)) |
68 | 67 | ad2ant2rl 729 |
. . . 4
⊢ (((M ∈ NC ∧ S ∈ V) ∧ (M ∈ S ∧ ∀x ∈ ( Spac ‘M)((x ∈ S ∧ (x
↑c 0c) ∈ NC ) →
(2c ↑c x) ∈ S))) → ∀x ∈ Clos1 ({M}, {〈p, q〉 ∣ (p ∈ NC ∧ q ∈ NC ∧ q = (2c ↑c
p))})∀z((x ∈ S ∧ x{〈p, q〉 ∣ (p ∈ NC ∧ q ∈ NC ∧ q = (2c ↑c
p))}z)
→ z ∈ S)) |
69 | | snex 4111 |
. . . . 5
⊢ {M} ∈
V |
70 | | spacvallem1 6281 |
. . . . 5
⊢ {〈p, q〉 ∣ (p ∈ NC ∧ q ∈ NC ∧ q =
(2c ↑c p))} ∈
V |
71 | | eqid 2353 |
. . . . 5
⊢ Clos1 ({M}, {〈p, q〉 ∣ (p ∈ NC ∧ q ∈ NC ∧ q =
(2c ↑c p))}) = Clos1
({M}, {〈p, q〉 ∣ (p ∈ NC ∧ q ∈ NC ∧ q =
(2c ↑c p))}) |
72 | 69, 70, 71 | clos1induct 5880 |
. . . 4
⊢ ((S ∈ V ∧ {M} ⊆ S ∧ ∀x ∈ Clos1 ({M}, {〈p, q〉 ∣ (p ∈ NC ∧ q ∈ NC ∧ q =
(2c ↑c p))})∀z((x ∈ S ∧ x{〈p, q〉 ∣ (p ∈ NC ∧ q ∈ NC ∧ q =
(2c ↑c p))}z) →
z ∈
S)) → Clos1
({M}, {〈p, q〉 ∣ (p ∈ NC ∧ q ∈ NC ∧ q =
(2c ↑c p))}) ⊆ S) |
73 | 5, 8, 68, 72 | syl3anc 1182 |
. . 3
⊢ (((M ∈ NC ∧ S ∈ V) ∧ (M ∈ S ∧ ∀x ∈ ( Spac ‘M)((x ∈ S ∧ (x
↑c 0c) ∈ NC ) →
(2c ↑c x) ∈ S))) → Clos1
({M}, {〈p, q〉 ∣ (p ∈ NC ∧ q ∈ NC ∧ q =
(2c ↑c p))}) ⊆ S) |
74 | 4, 73 | eqsstrd 3305 |
. 2
⊢ (((M ∈ NC ∧ S ∈ V) ∧ (M ∈ S ∧ ∀x ∈ ( Spac ‘M)((x ∈ S ∧ (x
↑c 0c) ∈ NC ) →
(2c ↑c x) ∈ S))) → ( Spac ‘M) ⊆ S) |
75 | 1, 74 | sylanl2 632 |
1
⊢ (((M ∈ NC ∧ S ∈ V) ∧ (M ∈ S ∧ ∀x ∈ ( Spac
‘M)((x ∈ S ∧ (x ↑c 0c)
∈ NC ) →
(2c ↑c x) ∈ S))) → ( Spac ‘M) ⊆ S) |