Step | Hyp | Ref
| Expression |
1 | | nncex 4396 |
. . 3
⊢ Nn ∈
V |
2 | | inexg 4100 |
. . 3
⊢ (( Nn ∈ V ∧ A ∈ V) → (
Nn ∩ A)
∈ V) |
3 | 1, 2 | mpan 651 |
. 2
⊢ (A ∈ V → ( Nn ∩
A) ∈
V) |
4 | | peano1 4402 |
. . 3
⊢
0c ∈ Nn |
5 | | elin 3219 |
. . . 4
⊢
(0c ∈ ( Nn ∩ A) ↔
(0c ∈ Nn ∧
0c ∈ A)) |
6 | 5 | biimpri 197 |
. . 3
⊢
((0c ∈ Nn ∧
0c ∈ A) → 0c ∈ ( Nn ∩ A)) |
7 | 4, 6 | mpan 651 |
. 2
⊢
(0c ∈ A → 0c ∈ ( Nn ∩ A)) |
8 | | elin 3219 |
. . . . . 6
⊢ (x ∈ ( Nn ∩ A) ↔
(x ∈
Nn ∧ x ∈ A)) |
9 | 8 | imbi1i 315 |
. . . . 5
⊢ ((x ∈ ( Nn ∩ A) →
(x +c
1c) ∈ A) ↔ ((x
∈ Nn ∧ x ∈ A) →
(x +c
1c) ∈ A)) |
10 | | impexp 433 |
. . . . 5
⊢ (((x ∈ Nn ∧ x ∈ A) → (x
+c 1c) ∈
A) ↔ (x ∈ Nn → (x ∈ A →
(x +c
1c) ∈ A))) |
11 | 9, 10 | bitri 240 |
. . . 4
⊢ ((x ∈ ( Nn ∩ A) →
(x +c
1c) ∈ A) ↔ (x
∈ Nn →
(x ∈
A → (x +c 1c) ∈ A))) |
12 | | inss1 3475 |
. . . . . . . 8
⊢ ( Nn ∩ A) ⊆ Nn |
13 | 12 | sseli 3269 |
. . . . . . 7
⊢ (x ∈ ( Nn ∩ A) →
x ∈ Nn ) |
14 | | peano2 4403 |
. . . . . . 7
⊢ (x ∈ Nn → (x
+c 1c) ∈
Nn ) |
15 | 13, 14 | syl 15 |
. . . . . 6
⊢ (x ∈ ( Nn ∩ A) →
(x +c
1c) ∈ Nn ) |
16 | | elin 3219 |
. . . . . . . 8
⊢ ((x +c 1c) ∈ ( Nn ∩ A) ↔ ((x
+c 1c) ∈
Nn ∧ (x +c 1c) ∈ A)) |
17 | 16 | biimpri 197 |
. . . . . . 7
⊢ (((x +c 1c) ∈ Nn ∧ (x
+c 1c) ∈
A) → (x +c 1c) ∈ ( Nn ∩ A)) |
18 | 17 | a1i 10 |
. . . . . 6
⊢ (x ∈ ( Nn ∩ A) →
(((x +c
1c) ∈ Nn ∧ (x +c 1c) ∈ A) →
(x +c
1c) ∈ ( Nn ∩ A))) |
19 | 15, 18 | mpand 656 |
. . . . 5
⊢ (x ∈ ( Nn ∩ A) →
((x +c
1c) ∈ A → (x
+c 1c) ∈
( Nn ∩ A))) |
20 | 19 | a2i 12 |
. . . 4
⊢ ((x ∈ ( Nn ∩ A) →
(x +c
1c) ∈ A) → (x
∈ ( Nn ∩
A) → (x +c 1c) ∈ ( Nn ∩ A))) |
21 | 11, 20 | sylbir 204 |
. . 3
⊢ ((x ∈ Nn → (x ∈ A →
(x +c
1c) ∈ A)) → (x
∈ ( Nn ∩
A) → (x +c 1c) ∈ ( Nn ∩ A))) |
22 | 21 | ralimi2 2686 |
. 2
⊢ (∀x ∈ Nn (x ∈ A → (x
+c 1c) ∈
A) → ∀x ∈ ( Nn ∩ A)(x
+c 1c) ∈
( Nn ∩ A)) |
23 | | df-nnc 4379 |
. . . 4
⊢ Nn = ∩{y ∣
(0c ∈ y ∧ ∀x ∈ y (x +c 1c) ∈ y)} |
24 | | eleq2 2414 |
. . . . . . . . 9
⊢ (y = ( Nn ∩ A) → (0c ∈ y ↔
0c ∈ ( Nn ∩ A))) |
25 | | eleq2 2414 |
. . . . . . . . . 10
⊢ (y = ( Nn ∩ A) → ((x
+c 1c) ∈
y ↔ (x +c 1c) ∈ ( Nn ∩ A))) |
26 | 25 | raleqbi1dv 2815 |
. . . . . . . . 9
⊢ (y = ( Nn ∩ A) → (∀x ∈ y (x +c 1c) ∈ y ↔
∀x
∈ ( Nn ∩
A)(x
+c 1c) ∈
( Nn ∩ A))) |
27 | 24, 26 | anbi12d 691 |
. . . . . . . 8
⊢ (y = ( Nn ∩ A) → ((0c ∈ y ∧ ∀x ∈ y (x
+c 1c) ∈
y) ↔ (0c ∈ ( Nn ∩ A) ∧ ∀x ∈ ( Nn ∩ A)(x
+c 1c) ∈
( Nn ∩ A)))) |
28 | 27 | elabg 2986 |
. . . . . . 7
⊢ (( Nn ∩ A) ∈ V → (( Nn ∩
A) ∈
{y ∣
(0c ∈ y ∧ ∀x ∈ y (x +c 1c) ∈ y)} ↔
(0c ∈ ( Nn ∩ A) ∧ ∀x ∈ ( Nn ∩ A)(x +c 1c) ∈ ( Nn ∩ A)))) |
29 | 28 | biimprd 214 |
. . . . . 6
⊢ (( Nn ∩ A) ∈ V → ((0c ∈ ( Nn ∩ A) ∧ ∀x ∈ ( Nn ∩ A)(x
+c 1c) ∈
( Nn ∩ A))
→ ( Nn ∩ A) ∈ {y ∣
(0c ∈ y ∧ ∀x ∈ y (x +c 1c) ∈ y)})) |
30 | 29 | 3impib 1149 |
. . . . 5
⊢ ((( Nn ∩ A) ∈ V ∧
0c ∈ ( Nn ∩ A) ∧ ∀x ∈ ( Nn ∩ A)(x +c 1c) ∈ ( Nn ∩ A)) → ( Nn ∩
A) ∈
{y ∣
(0c ∈ y ∧ ∀x ∈ y (x +c 1c) ∈ y)}) |
31 | | intss1 3941 |
. . . . 5
⊢ (( Nn ∩ A) ∈ {y ∣ (0c ∈ y ∧ ∀x ∈ y (x
+c 1c) ∈
y)} → ∩{y ∣ (0c ∈ y ∧ ∀x ∈ y (x
+c 1c) ∈
y)} ⊆ (
Nn ∩ A)) |
32 | 30, 31 | syl 15 |
. . . 4
⊢ ((( Nn ∩ A) ∈ V ∧
0c ∈ ( Nn ∩ A) ∧ ∀x ∈ ( Nn ∩ A)(x +c 1c) ∈ ( Nn ∩ A)) → ∩{y ∣
(0c ∈ y ∧ ∀x ∈ y (x +c 1c) ∈ y)} ⊆ ( Nn ∩ A)) |
33 | 23, 32 | syl5eqss 3315 |
. . 3
⊢ ((( Nn ∩ A) ∈ V ∧
0c ∈ ( Nn ∩ A) ∧ ∀x ∈ ( Nn ∩ A)(x +c 1c) ∈ ( Nn ∩ A)) → Nn ⊆ ( Nn ∩ A)) |
34 | | inss2 3476 |
. . 3
⊢ ( Nn ∩ A) ⊆ A |
35 | 33, 34 | syl6ss 3284 |
. 2
⊢ ((( Nn ∩ A) ∈ V ∧
0c ∈ ( Nn ∩ A) ∧ ∀x ∈ ( Nn ∩ A)(x +c 1c) ∈ ( Nn ∩ A)) → Nn ⊆ A) |
36 | 3, 7, 22, 35 | syl3an 1224 |
1
⊢ ((A ∈ V ∧
0c ∈ A ∧ ∀x ∈ Nn (x ∈ A → (x
+c 1c) ∈
A)) → Nn
⊆ A) |