Step | Hyp | Ref
| Expression |
1 | | 0cex 4392 |
. . . . . 6
⊢
0c ∈
V |
2 | 1 | snss 3838 |
. . . . 5
⊢
(0c ∈ a ↔ {0c} ⊆ a) |
3 | | dfss2 3262 |
. . . . . 6
⊢ (((x ∈ V ↦ (x
+c 1c)) “ a) ⊆ a ↔ ∀z(z ∈ ((x ∈ V ↦ (x
+c 1c)) “ a) → z
∈ a)) |
4 | | ralcom4 2877 |
. . . . . . 7
⊢ (∀y ∈ a ∀z(((x ∈ V ↦ (x
+c 1c)) ‘y) = z →
z ∈
a) ↔ ∀z∀y ∈ a (((x ∈ V ↦ (x
+c 1c)) ‘y) = z →
z ∈
a)) |
5 | | eqid 2353 |
. . . . . . . . . . . . 13
⊢ (x ∈ V ↦ (x
+c 1c)) = (x ∈ V ↦ (x
+c 1c)) |
6 | 5 | fnmpt 5689 |
. . . . . . . . . . . 12
⊢ (∀x ∈ V (x
+c 1c) ∈
V → (x ∈ V ↦ (x +c 1c)) Fn
V) |
7 | | vex 2862 |
. . . . . . . . . . . . . 14
⊢ x ∈
V |
8 | | 1cex 4142 |
. . . . . . . . . . . . . 14
⊢
1c ∈
V |
9 | 7, 8 | addcex 4394 |
. . . . . . . . . . . . 13
⊢ (x +c 1c) ∈ V |
10 | 9 | a1i 10 |
. . . . . . . . . . . 12
⊢ (x ∈ V →
(x +c
1c) ∈ V) |
11 | 6, 10 | mprg 2683 |
. . . . . . . . . . 11
⊢ (x ∈ V ↦ (x
+c 1c)) Fn V |
12 | | ssv 3291 |
. . . . . . . . . . 11
⊢ a ⊆
V |
13 | | fvelimab 5370 |
. . . . . . . . . . 11
⊢ (((x ∈ V ↦ (x
+c 1c)) Fn V ∧ a ⊆ V) → (z
∈ ((x
∈ V ↦
(x +c
1c)) “ a) ↔
∃y ∈ a ((x ∈ V ↦ (x
+c 1c)) ‘y) = z)) |
14 | 11, 12, 13 | mp2an 653 |
. . . . . . . . . 10
⊢ (z ∈ ((x ∈ V ↦ (x
+c 1c)) “ a) ↔ ∃y ∈ a ((x ∈ V ↦ (x
+c 1c)) ‘y) = z) |
15 | 14 | imbi1i 315 |
. . . . . . . . 9
⊢ ((z ∈ ((x ∈ V ↦ (x
+c 1c)) “ a) → z
∈ a)
↔ (∃y ∈ a ((x ∈ V ↦ (x +c 1c))
‘y) = z → z ∈ a)) |
16 | | r19.23v 2730 |
. . . . . . . . 9
⊢ (∀y ∈ a (((x ∈ V ↦ (x
+c 1c)) ‘y) = z →
z ∈
a) ↔ (∃y ∈ a ((x ∈ V ↦ (x
+c 1c)) ‘y) = z →
z ∈
a)) |
17 | 15, 16 | bitr4i 243 |
. . . . . . . 8
⊢ ((z ∈ ((x ∈ V ↦ (x
+c 1c)) “ a) → z
∈ a)
↔ ∀y ∈ a (((x ∈ V ↦ (x +c 1c))
‘y) = z → z ∈ a)) |
18 | 17 | albii 1566 |
. . . . . . 7
⊢ (∀z(z ∈ ((x ∈ V ↦ (x
+c 1c)) “ a) → z
∈ a)
↔ ∀z∀y ∈ a (((x ∈ V ↦ (x +c 1c))
‘y) = z → z ∈ a)) |
19 | 4, 18 | bitr4i 243 |
. . . . . 6
⊢ (∀y ∈ a ∀z(((x ∈ V ↦ (x
+c 1c)) ‘y) = z →
z ∈
a) ↔ ∀z(z ∈ ((x ∈ V ↦ (x
+c 1c)) “ a) → z
∈ a)) |
20 | | vex 2862 |
. . . . . . . . . . . . 13
⊢ y ∈
V |
21 | | addceq1 4383 |
. . . . . . . . . . . . . 14
⊢ (x = y →
(x +c
1c) = (y
+c 1c)) |
22 | 20, 8 | addcex 4394 |
. . . . . . . . . . . . . 14
⊢ (y +c 1c) ∈ V |
23 | 21, 5, 22 | fvmpt 5700 |
. . . . . . . . . . . . 13
⊢ (y ∈ V →
((x ∈ V
↦ (x
+c 1c)) ‘y) = (y
+c 1c)) |
24 | 20, 23 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ ((x ∈ V ↦ (x
+c 1c)) ‘y) = (y
+c 1c) |
25 | 24 | eqeq1i 2360 |
. . . . . . . . . . 11
⊢ (((x ∈ V ↦ (x
+c 1c)) ‘y) = z ↔
(y +c
1c) = z) |
26 | | eqcom 2355 |
. . . . . . . . . . 11
⊢ ((y +c 1c) =
z ↔ z = (y
+c 1c)) |
27 | 25, 26 | bitri 240 |
. . . . . . . . . 10
⊢ (((x ∈ V ↦ (x
+c 1c)) ‘y) = z ↔
z = (y
+c 1c)) |
28 | 27 | imbi1i 315 |
. . . . . . . . 9
⊢ ((((x ∈ V ↦ (x
+c 1c)) ‘y) = z →
z ∈
a) ↔ (z = (y
+c 1c) → z ∈ a)) |
29 | 28 | albii 1566 |
. . . . . . . 8
⊢ (∀z(((x ∈ V ↦ (x
+c 1c)) ‘y) = z →
z ∈
a) ↔ ∀z(z = (y
+c 1c) → z ∈ a)) |
30 | | eleq1 2413 |
. . . . . . . . 9
⊢ (z = (y
+c 1c) → (z ∈ a ↔ (y
+c 1c) ∈
a)) |
31 | 22, 30 | ceqsalv 2885 |
. . . . . . . 8
⊢ (∀z(z = (y
+c 1c) → z ∈ a) ↔ (y
+c 1c) ∈
a) |
32 | 29, 31 | bitri 240 |
. . . . . . 7
⊢ (∀z(((x ∈ V ↦ (x
+c 1c)) ‘y) = z →
z ∈
a) ↔ (y +c 1c) ∈ a) |
33 | 32 | ralbii 2638 |
. . . . . 6
⊢ (∀y ∈ a ∀z(((x ∈ V ↦ (x
+c 1c)) ‘y) = z →
z ∈
a) ↔ ∀y ∈ a (y +c 1c) ∈ a) |
34 | 3, 19, 33 | 3bitr2ri 265 |
. . . . 5
⊢ (∀y ∈ a (y +c 1c) ∈ a ↔
((x ∈ V
↦ (x
+c 1c)) “ a) ⊆ a) |
35 | 2, 34 | anbi12i 678 |
. . . 4
⊢
((0c ∈ a ∧ ∀y ∈ a (y +c 1c) ∈ a) ↔
({0c} ⊆ a ∧ ((x ∈ V ↦ (x
+c 1c)) “ a) ⊆ a)) |
36 | 35 | abbii 2465 |
. . 3
⊢ {a ∣
(0c ∈ a ∧ ∀y ∈ a (y +c 1c) ∈ a)} =
{a ∣
({0c} ⊆ a ∧ ((x ∈ V ↦ (x
+c 1c)) “ a) ⊆ a)} |
37 | 36 | inteqi 3930 |
. 2
⊢ ∩{a ∣ (0c ∈ a ∧ ∀y ∈ a (y
+c 1c) ∈
a)} = ∩{a ∣
({0c} ⊆ a ∧ ((x ∈ V ↦ (x
+c 1c)) “ a) ⊆ a)} |
38 | | df-nnc 4379 |
. 2
⊢ Nn = ∩{a ∣
(0c ∈ a ∧ ∀y ∈ a (y +c 1c) ∈ a)} |
39 | | df-clos1 5873 |
. 2
⊢ Clos1 ({0c}, (x ∈ V ↦ (x
+c 1c))) = ∩{a ∣ ({0c} ⊆ a ∧ ((x ∈ V ↦ (x +c 1c))
“ a) ⊆ a)} |
40 | 37, 38, 39 | 3eqtr4i 2383 |
1
⊢ Nn = Clos1
({0c}, (x ∈ V ↦ (x +c
1c))) |