Step | Hyp | Ref
| Expression |
1 | | nmembers1lem1 6268 |
. 2
⊢ {n ∣ {m ∈ Nn ∣
(1c ≤c m
∧ m
≤c n)} ∈ Tc Tc n}
∈ V |
2 | | breq2 4643 |
. . . . 5
⊢ (n = 0c → (m ≤c n ↔ m
≤c 0c)) |
3 | 2 | anbi2d 684 |
. . . 4
⊢ (n = 0c →
((1c ≤c m
∧ m
≤c n) ↔
(1c ≤c m
∧ m
≤c 0c))) |
4 | 3 | rabbidv 2851 |
. . 3
⊢ (n = 0c → {m ∈ Nn ∣
(1c ≤c m
∧ m
≤c n)} = {m ∈ Nn ∣
(1c ≤c m
∧ m
≤c 0c)}) |
5 | | tceq 6158 |
. . . 4
⊢ (n = 0c → Tc n =
Tc
0c) |
6 | | tceq 6158 |
. . . 4
⊢ ( Tc n =
Tc 0c → Tc Tc
n = Tc Tc
0c) |
7 | 5, 6 | syl 15 |
. . 3
⊢ (n = 0c → Tc Tc
n = Tc Tc
0c) |
8 | 4, 7 | eleq12d 2421 |
. 2
⊢ (n = 0c → ({m ∈ Nn ∣
(1c ≤c m
∧ m
≤c n)} ∈ Tc Tc n
↔ {m ∈ Nn ∣ (1c ≤c m ∧ m ≤c 0c)} ∈ Tc Tc 0c)) |
9 | | breq2 4643 |
. . . . 5
⊢ (n = a →
(m ≤c n ↔ m
≤c a)) |
10 | 9 | anbi2d 684 |
. . . 4
⊢ (n = a →
((1c ≤c m
∧ m
≤c n) ↔
(1c ≤c m
∧ m
≤c a))) |
11 | 10 | rabbidv 2851 |
. . 3
⊢ (n = a →
{m ∈
Nn ∣
(1c ≤c m
∧ m
≤c n)} = {m ∈ Nn ∣
(1c ≤c m
∧ m
≤c a)}) |
12 | | tceq 6158 |
. . . 4
⊢ (n = a →
Tc n = Tc
a) |
13 | | tceq 6158 |
. . . 4
⊢ ( Tc n =
Tc a → Tc
Tc n = Tc Tc a) |
14 | 12, 13 | syl 15 |
. . 3
⊢ (n = a →
Tc Tc n =
Tc Tc a) |
15 | 11, 14 | eleq12d 2421 |
. 2
⊢ (n = a →
({m ∈
Nn ∣
(1c ≤c m
∧ m
≤c n)} ∈ Tc Tc n
↔ {m ∈ Nn ∣ (1c ≤c m ∧ m ≤c a)} ∈ Tc Tc
a)) |
16 | | breq2 4643 |
. . . . 5
⊢ (n = (a
+c 1c) → (m ≤c n ↔ m
≤c (a +c
1c))) |
17 | 16 | anbi2d 684 |
. . . 4
⊢ (n = (a
+c 1c) → ((1c
≤c m ∧ m
≤c n) ↔
(1c ≤c m
∧ m
≤c (a +c
1c)))) |
18 | 17 | rabbidv 2851 |
. . 3
⊢ (n = (a
+c 1c) → {m ∈ Nn ∣
(1c ≤c m
∧ m
≤c n)} = {m ∈ Nn ∣
(1c ≤c m
∧ m
≤c (a +c
1c))}) |
19 | | tceq 6158 |
. . . 4
⊢ (n = (a
+c 1c) → Tc n =
Tc (a +c
1c)) |
20 | | tceq 6158 |
. . . 4
⊢ ( Tc n =
Tc (a +c 1c) →
Tc Tc n =
Tc Tc (a
+c 1c)) |
21 | 19, 20 | syl 15 |
. . 3
⊢ (n = (a
+c 1c) → Tc Tc
n = Tc Tc
(a +c
1c)) |
22 | 18, 21 | eleq12d 2421 |
. 2
⊢ (n = (a
+c 1c) → ({m ∈ Nn ∣
(1c ≤c m
∧ m
≤c n)} ∈ Tc Tc n
↔ {m ∈ Nn ∣ (1c ≤c m ∧ m ≤c (a +c 1c))} ∈ Tc Tc (a
+c 1c))) |
23 | | breq2 4643 |
. . . . 5
⊢ (n = N →
(m ≤c n ↔ m
≤c N)) |
24 | 23 | anbi2d 684 |
. . . 4
⊢ (n = N →
((1c ≤c m
∧ m
≤c n) ↔
(1c ≤c m
∧ m
≤c N))) |
25 | 24 | rabbidv 2851 |
. . 3
⊢ (n = N →
{m ∈
Nn ∣
(1c ≤c m
∧ m
≤c n)} = {m ∈ Nn ∣
(1c ≤c m
∧ m
≤c N)}) |
26 | | tceq 6158 |
. . . 4
⊢ (n = N →
Tc n = Tc
N) |
27 | | tceq 6158 |
. . . 4
⊢ ( Tc n =
Tc N → Tc
Tc n = Tc Tc N) |
28 | 26, 27 | syl 15 |
. . 3
⊢ (n = N →
Tc Tc n =
Tc Tc N) |
29 | 25, 28 | eleq12d 2421 |
. 2
⊢ (n = N →
({m ∈
Nn ∣
(1c ≤c m
∧ m
≤c n)} ∈ Tc Tc n
↔ {m ∈ Nn ∣ (1c ≤c m ∧ m ≤c N)} ∈ Tc Tc
N)) |
30 | | nmembers1lem2 6269 |
. . 3
⊢ {m ∈ Nn ∣
(1c ≤c m
∧ m
≤c 0c)} ∈
0c |
31 | | tc0c 6163 |
. . . . 5
⊢ Tc 0c =
0c |
32 | | tceq 6158 |
. . . . 5
⊢ ( Tc 0c =
0c → Tc Tc 0c = Tc 0c) |
33 | 31, 32 | ax-mp 5 |
. . . 4
⊢ Tc Tc
0c = Tc
0c |
34 | 33, 31 | eqtri 2373 |
. . 3
⊢ Tc Tc
0c = 0c |
35 | 30, 34 | eleqtrri 2426 |
. 2
⊢ {m ∈ Nn ∣
(1c ≤c m
∧ m
≤c 0c)} ∈
Tc Tc 0c |
36 | | nntccl 6170 |
. . . 4
⊢ (a ∈ Nn → Tc
a ∈ Nn ) |
37 | | nntccl 6170 |
. . . 4
⊢ ( Tc a
∈ Nn →
Tc Tc a
∈ Nn
) |
38 | 36, 37 | syl 15 |
. . 3
⊢ (a ∈ Nn → Tc
Tc a ∈ Nn ) |
39 | | nmembers1lem3 6270 |
. . . 4
⊢ ((a ∈ Nn ∧ Tc Tc
a ∈ Nn ) → ({m
∈ Nn ∣ (1c ≤c m ∧ m ≤c a)} ∈ Tc Tc
a → {m ∈ Nn ∣
(1c ≤c m
∧ m
≤c (a +c
1c))} ∈ ( Tc Tc
a +c
1c))) |
40 | | nnnc 6146 |
. . . . . . 7
⊢ (a ∈ Nn → a ∈ NC
) |
41 | | 1cnc 6139 |
. . . . . . . . . . 11
⊢
1c ∈ NC |
42 | | tcdi 6164 |
. . . . . . . . . . 11
⊢ ((a ∈ NC ∧
1c ∈ NC ) → Tc
(a +c
1c) = ( Tc a +c Tc 1c)) |
43 | 41, 42 | mpan2 652 |
. . . . . . . . . 10
⊢ (a ∈ NC → Tc
(a +c
1c) = ( Tc a +c Tc 1c)) |
44 | | tc1c 6165 |
. . . . . . . . . . 11
⊢ Tc 1c =
1c |
45 | 44 | addceq2i 4387 |
. . . . . . . . . 10
⊢ ( Tc a
+c Tc
1c) = ( Tc a +c
1c) |
46 | 43, 45 | syl6eq 2401 |
. . . . . . . . 9
⊢ (a ∈ NC → Tc
(a +c
1c) = ( Tc a +c
1c)) |
47 | | tceq 6158 |
. . . . . . . . 9
⊢ ( Tc (a
+c 1c) = ( Tc a
+c 1c) → Tc Tc
(a +c
1c) = Tc ( Tc a
+c 1c)) |
48 | 46, 47 | syl 15 |
. . . . . . . 8
⊢ (a ∈ NC → Tc
Tc (a +c 1c) = Tc ( Tc a
+c 1c)) |
49 | | tccl 6160 |
. . . . . . . . . 10
⊢ (a ∈ NC → Tc
a ∈ NC ) |
50 | | tcdi 6164 |
. . . . . . . . . . 11
⊢ (( Tc a
∈ NC ∧ 1c ∈ NC ) → Tc ( Tc a
+c 1c) = ( Tc Tc
a +c Tc 1c)) |
51 | 41, 50 | mpan2 652 |
. . . . . . . . . 10
⊢ ( Tc a
∈ NC →
Tc ( Tc a
+c 1c) = ( Tc Tc
a +c Tc 1c)) |
52 | 49, 51 | syl 15 |
. . . . . . . . 9
⊢ (a ∈ NC → Tc (
Tc a +c 1c) = (
Tc Tc a
+c Tc
1c)) |
53 | 44 | addceq2i 4387 |
. . . . . . . . 9
⊢ ( Tc Tc
a +c Tc 1c) = ( Tc Tc
a +c
1c) |
54 | 52, 53 | syl6eq 2401 |
. . . . . . . 8
⊢ (a ∈ NC → Tc (
Tc a +c 1c) = (
Tc Tc a
+c 1c)) |
55 | 48, 54 | eqtrd 2385 |
. . . . . . 7
⊢ (a ∈ NC → Tc
Tc (a +c 1c) = (
Tc Tc a
+c 1c)) |
56 | 40, 55 | syl 15 |
. . . . . 6
⊢ (a ∈ Nn → Tc
Tc (a +c 1c) = (
Tc Tc a
+c 1c)) |
57 | 56 | eleq2d 2420 |
. . . . 5
⊢ (a ∈ Nn → ({m ∈ Nn ∣ (1c ≤c m ∧ m ≤c (a +c 1c))} ∈ Tc Tc (a
+c 1c) ↔ {m ∈ Nn ∣
(1c ≤c m
∧ m
≤c (a +c
1c))} ∈ ( Tc Tc
a +c
1c))) |
58 | 57 | adantr 451 |
. . . 4
⊢ ((a ∈ Nn ∧ Tc Tc
a ∈ Nn ) → ({m
∈ Nn ∣ (1c ≤c m ∧ m ≤c (a +c 1c))} ∈ Tc Tc (a
+c 1c) ↔ {m ∈ Nn ∣
(1c ≤c m
∧ m
≤c (a +c
1c))} ∈ ( Tc Tc
a +c
1c))) |
59 | 39, 58 | sylibrd 225 |
. . 3
⊢ ((a ∈ Nn ∧ Tc Tc
a ∈ Nn ) → ({m
∈ Nn ∣ (1c ≤c m ∧ m ≤c a)} ∈ Tc Tc
a → {m ∈ Nn ∣
(1c ≤c m
∧ m
≤c (a +c
1c))} ∈ Tc Tc
(a +c
1c))) |
60 | 38, 59 | mpdan 649 |
. 2
⊢ (a ∈ Nn → ({m ∈ Nn ∣ (1c ≤c m ∧ m ≤c a)} ∈ Tc Tc
a → {m ∈ Nn ∣
(1c ≤c m
∧ m
≤c (a +c
1c))} ∈ Tc Tc
(a +c
1c))) |
61 | 1, 8, 15, 22, 29, 35, 60 | finds 4411 |
1
⊢ (N ∈ Nn → {m ∈ Nn ∣ (1c ≤c m ∧ m ≤c N)} ∈ Tc Tc
N) |