Step | Hyp | Ref
| Expression |
1 | | nmembers1lem1 6268 |
. 2
![{](lbrace.gif) ![{](lbrace.gif) Nn 1c c c ![n](_n.gif) ![)](rp.gif) Tc Tc
![n](_n.gif) ![_V](rmcv.gif) |
2 | | breq2 4643 |
. . . . 5
![(](lp.gif) 0c ![(](lp.gif) c c 0c![)](rp.gif) ![)](rp.gif) |
3 | 2 | anbi2d 684 |
. . . 4
![(](lp.gif) 0c ![(](lp.gif) 1c c c ![n](_n.gif) 1c c c 0c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
4 | 3 | rabbidv 2851 |
. . 3
![(](lp.gif) 0c ![{](lbrace.gif) Nn 1c c c ![n](_n.gif) ![)](rp.gif) ![{](lbrace.gif)
Nn 1c c c 0c![)](rp.gif) ![}](rbrace.gif) ![)](rp.gif) |
5 | | tceq 6158 |
. . . 4
![(](lp.gif) 0c Tc Tc
0c![)](rp.gif) |
6 | | tceq 6158 |
. . . 4
Tc
Tc 0c Tc Tc
Tc Tc
0c![)](rp.gif) |
7 | 5, 6 | syl 15 |
. . 3
![(](lp.gif) 0c Tc Tc
Tc Tc 0c![)](rp.gif) |
8 | 4, 7 | eleq12d 2421 |
. 2
![(](lp.gif) 0c ![(](lp.gif) ![{](lbrace.gif) Nn 1c c
c ![n](_n.gif) ![)](rp.gif) Tc Tc
![{](lbrace.gif) Nn 1c c c
0c![)](rp.gif) Tc Tc
0c![)](rp.gif) ![)](rp.gif) |
9 | | breq2 4643 |
. . . . 5
![(](lp.gif) ![(](lp.gif) c c ![a](_a.gif) ![)](rp.gif) ![)](rp.gif) |
10 | 9 | anbi2d 684 |
. . . 4
![(](lp.gif) ![(](lp.gif) 1c c c ![n](_n.gif) 1c c c ![a](_a.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
11 | 10 | rabbidv 2851 |
. . 3
![(](lp.gif) ![{](lbrace.gif)
Nn 1c c c ![n](_n.gif) ![)](rp.gif) ![{](lbrace.gif)
Nn 1c c c ![a](_a.gif) ![)](rp.gif) ![}](rbrace.gif) ![)](rp.gif) |
12 | | tceq 6158 |
. . . 4
![(](lp.gif) Tc
Tc ![a](_a.gif) ![)](rp.gif) |
13 | | tceq 6158 |
. . . 4
Tc
Tc Tc Tc
Tc Tc ![a](_a.gif) ![)](rp.gif) |
14 | 12, 13 | syl 15 |
. . 3
![(](lp.gif) Tc Tc
Tc Tc
![a](_a.gif) ![)](rp.gif) |
15 | 11, 14 | eleq12d 2421 |
. 2
![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif)
Nn 1c c c ![n](_n.gif) ![)](rp.gif) Tc Tc
![{](lbrace.gif) Nn 1c c c ![a](_a.gif) ![)](rp.gif) Tc Tc
![a](_a.gif) ![)](rp.gif) ![)](rp.gif) |
16 | | breq2 4643 |
. . . . 5
![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) c c ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
17 | 16 | anbi2d 684 |
. . . 4
![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) 1c c c ![n](_n.gif) 1c c c ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
18 | 17 | rabbidv 2851 |
. . 3
![(](lp.gif) ![(](lp.gif) 1c ![{](lbrace.gif) Nn 1c c c ![n](_n.gif) ![)](rp.gif) ![{](lbrace.gif)
Nn 1c c c ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) ![}](rbrace.gif) ![)](rp.gif) |
19 | | tceq 6158 |
. . . 4
![(](lp.gif) ![(](lp.gif) 1c Tc Tc ![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) |
20 | | tceq 6158 |
. . . 4
Tc
Tc ![(](lp.gif)
1c
Tc Tc
Tc Tc
![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) |
21 | 19, 20 | syl 15 |
. . 3
![(](lp.gif) ![(](lp.gif) 1c Tc Tc
Tc Tc ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) |
22 | 18, 21 | eleq12d 2421 |
. 2
![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) ![{](lbrace.gif) Nn 1c c
c ![n](_n.gif) ![)](rp.gif) Tc Tc
![{](lbrace.gif) Nn 1c c c ![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) Tc Tc
![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
23 | | breq2 4643 |
. . . . 5
![(](lp.gif) ![(](lp.gif) c c ![N](_cn.gif) ![)](rp.gif) ![)](rp.gif) |
24 | 23 | anbi2d 684 |
. . . 4
![(](lp.gif) ![(](lp.gif) 1c c c ![n](_n.gif) 1c c c ![N](_cn.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
25 | 24 | rabbidv 2851 |
. . 3
![(](lp.gif) ![{](lbrace.gif)
Nn 1c c c ![n](_n.gif) ![)](rp.gif) ![{](lbrace.gif)
Nn 1c c c ![N](_cn.gif) ![)](rp.gif) ![}](rbrace.gif) ![)](rp.gif) |
26 | | tceq 6158 |
. . . 4
![(](lp.gif) Tc
Tc ![N](_cn.gif) ![)](rp.gif) |
27 | | tceq 6158 |
. . . 4
Tc
Tc Tc Tc
Tc Tc ![N](_cn.gif) ![)](rp.gif) |
28 | 26, 27 | syl 15 |
. . 3
![(](lp.gif) Tc Tc
Tc Tc
![N](_cn.gif) ![)](rp.gif) |
29 | 25, 28 | eleq12d 2421 |
. 2
![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif)
Nn 1c c c ![n](_n.gif) ![)](rp.gif) Tc Tc
![{](lbrace.gif) Nn 1c c c ![N](_cn.gif) ![)](rp.gif) Tc Tc
![N](_cn.gif) ![)](rp.gif) ![)](rp.gif) |
30 | | nmembers1lem2 6269 |
. . 3
![{](lbrace.gif) Nn 1c c c
0c![)](rp.gif)
0c |
31 | | tc0c 6163 |
. . . . 5
Tc 0c 0c |
32 | | tceq 6158 |
. . . . 5
Tc 0c 0c Tc Tc
0c
Tc 0c![)](rp.gif) |
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
![{](lbrace.gif) Nn 1c c c
0c![)](rp.gif) Tc Tc
0c |
36 | | nntccl 6170 |
. . . 4
![(](lp.gif) Nn Tc Nn ![)](rp.gif) |
37 | | nntccl 6170 |
. . . 4
Tc
Nn Tc Tc
Nn ![)](rp.gif) |
38 | 36, 37 | syl 15 |
. . 3
![(](lp.gif) Nn Tc Tc
Nn ![)](rp.gif) |
39 | | nmembers1lem3 6270 |
. . . 4
![(](lp.gif) ![(](lp.gif) Nn Tc Tc
Nn ![(](lp.gif) ![{](lbrace.gif)
Nn 1c c c ![a](_a.gif) ![)](rp.gif) Tc Tc
![{](lbrace.gif) Nn 1c c c ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) Tc Tc 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
40 | | nnnc 6146 |
. . . . . . 7
![(](lp.gif) Nn NC ![)](rp.gif) |
41 | | 1cnc 6139 |
. . . . . . . . . . 11
1c
NC |
42 | | tcdi 6164 |
. . . . . . . . . . 11
![(](lp.gif) ![(](lp.gif) NC 1c NC Tc ![(](lp.gif)
1c
Tc Tc 1c![)](rp.gif) ![)](rp.gif) |
43 | 41, 42 | mpan2 652 |
. . . . . . . . . 10
![(](lp.gif) NC Tc ![(](lp.gif) 1c
Tc Tc 1c![)](rp.gif) ![)](rp.gif) |
44 | | tc1c 6165 |
. . . . . . . . . . 11
Tc 1c 1c |
45 | 44 | addceq2i 4387 |
. . . . . . . . . 10
Tc Tc 1c Tc 1c![)](rp.gif) |
46 | 43, 45 | syl6eq 2401 |
. . . . . . . . 9
![(](lp.gif) NC Tc ![(](lp.gif) 1c
Tc 1c![)](rp.gif) ![)](rp.gif) |
47 | | tceq 6158 |
. . . . . . . . 9
Tc ![(](lp.gif)
1c
Tc 1c Tc Tc
![(](lp.gif) 1c
Tc Tc 1c![)](rp.gif) ![)](rp.gif) |
48 | 46, 47 | syl 15 |
. . . . . . . 8
![(](lp.gif) NC Tc Tc ![(](lp.gif)
1c
Tc Tc 1c![)](rp.gif) ![)](rp.gif) |
49 | | tccl 6160 |
. . . . . . . . . 10
![(](lp.gif) NC Tc NC ![)](rp.gif) |
50 | | tcdi 6164 |
. . . . . . . . . . 11
![(](lp.gif) Tc NC 1c
NC Tc Tc 1c
Tc Tc Tc 1c![)](rp.gif) ![)](rp.gif) |
51 | 41, 50 | mpan2 652 |
. . . . . . . . . 10
Tc
NC Tc Tc 1c Tc Tc
Tc 1c![)](rp.gif) ![)](rp.gif) |
52 | 49, 51 | syl 15 |
. . . . . . . . 9
![(](lp.gif) NC Tc Tc 1c Tc Tc
Tc 1c![)](rp.gif) ![)](rp.gif) |
53 | 44 | addceq2i 4387 |
. . . . . . . . 9
Tc Tc
Tc 1c
Tc Tc 1c![)](rp.gif) |
54 | 52, 53 | syl6eq 2401 |
. . . . . . . 8
![(](lp.gif) NC Tc Tc 1c Tc Tc
1c![)](rp.gif) ![)](rp.gif) |
55 | 48, 54 | eqtrd 2385 |
. . . . . . 7
![(](lp.gif) NC Tc Tc ![(](lp.gif)
1c
Tc Tc
1c![)](rp.gif) ![)](rp.gif) |
56 | 40, 55 | syl 15 |
. . . . . 6
![(](lp.gif) Nn Tc Tc ![(](lp.gif)
1c
Tc Tc
1c![)](rp.gif) ![)](rp.gif) |
57 | 56 | eleq2d 2420 |
. . . . 5
![(](lp.gif) Nn ![(](lp.gif) ![{](lbrace.gif) Nn 1c c
c ![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) Tc Tc
![(](lp.gif) 1c ![{](lbrace.gif) Nn 1c c c ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) Tc Tc 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
58 | 57 | adantr 451 |
. . . 4
![(](lp.gif) ![(](lp.gif) Nn Tc Tc
Nn ![(](lp.gif) ![{](lbrace.gif)
Nn 1c c c ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) Tc Tc
![(](lp.gif) 1c ![{](lbrace.gif) Nn 1c c c ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) Tc Tc 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
59 | 39, 58 | sylibrd 225 |
. . 3
![(](lp.gif) ![(](lp.gif) Nn Tc Tc
Nn ![(](lp.gif) ![{](lbrace.gif)
Nn 1c c c ![a](_a.gif) ![)](rp.gif) Tc Tc
![{](lbrace.gif) Nn 1c c c ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) Tc Tc
![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
60 | 38, 59 | mpdan 649 |
. 2
![(](lp.gif) Nn ![(](lp.gif) ![{](lbrace.gif) Nn 1c c
c ![a](_a.gif) ![)](rp.gif) Tc Tc
![{](lbrace.gif) Nn 1c c c ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) Tc Tc
![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
61 | 1, 8, 15, 22, 29, 35, 60 | finds 4411 |
1
![(](lp.gif) Nn ![{](lbrace.gif) Nn 1c c c ![N](_cn.gif) ![)](rp.gif) Tc Tc
![N](_cn.gif) ![)](rp.gif) |