Step | Hyp | Ref
| Expression |
1 | | n0i 3920 |
. . . . . 6
|
2 | | mrsubco.s |
. . . . . . . . 9
mRSubst |
3 | | fvprc 6185 |
. . . . . . . . 9
mRSubst |
4 | 2, 3 | syl5eq 2668 |
. . . . . . . 8
|
5 | 4 | rneqd 5353 |
. . . . . . 7
|
6 | | rn0 5377 |
. . . . . . 7
|
7 | 5, 6 | syl6eq 2672 |
. . . . . 6
|
8 | 1, 7 | nsyl2 142 |
. . . . 5
|
9 | | eqid 2622 |
. . . . . 6
mCN mCN |
10 | | mrsubvrs.v |
. . . . . 6
mVR |
11 | | mrsubvrs.r |
. . . . . 6
mREx |
12 | 9, 10, 11 | mrexval 31398 |
. . . . 5
Word mCN |
13 | 8, 12 | syl 17 |
. . . 4
Word mCN |
14 | 13 | eleq2d 2687 |
. . 3
Word mCN |
15 | | fveq2 6191 |
. . . . . . . . 9
|
16 | 15 | rneqd 5353 |
. . . . . . . 8
|
17 | 16 | ineq1d 3813 |
. . . . . . 7
|
18 | | rneq 5351 |
. . . . . . . . . . . 12
|
19 | 18, 6 | syl6eq 2672 |
. . . . . . . . . . 11
|
20 | 19 | ineq1d 3813 |
. . . . . . . . . 10
|
21 | | 0in 3969 |
. . . . . . . . . 10
|
22 | 20, 21 | syl6eq 2672 |
. . . . . . . . 9
|
23 | 22 | iuneq1d 4545 |
. . . . . . . 8
|
24 | | 0iun 4577 |
. . . . . . . 8
|
25 | 23, 24 | syl6eq 2672 |
. . . . . . 7
|
26 | 17, 25 | eqeq12d 2637 |
. . . . . 6
|
27 | 26 | imbi2d 330 |
. . . . 5
|
28 | | fveq2 6191 |
. . . . . . . . 9
|
29 | 28 | rneqd 5353 |
. . . . . . . 8
|
30 | 29 | ineq1d 3813 |
. . . . . . 7
|
31 | | rneq 5351 |
. . . . . . . . 9
|
32 | 31 | ineq1d 3813 |
. . . . . . . 8
|
33 | 32 | iuneq1d 4545 |
. . . . . . 7
|
34 | 30, 33 | eqeq12d 2637 |
. . . . . 6
|
35 | 34 | imbi2d 330 |
. . . . 5
|
36 | | fveq2 6191 |
. . . . . . . . 9
++ ++ |
37 | 36 | rneqd 5353 |
. . . . . . . 8
++ ++ |
38 | 37 | ineq1d 3813 |
. . . . . . 7
++ ++
|
39 | | rneq 5351 |
. . . . . . . . 9
++ ++
|
40 | 39 | ineq1d 3813 |
. . . . . . . 8
++ ++ |
41 | 40 | iuneq1d 4545 |
. . . . . . 7
++ ++ |
42 | 38, 41 | eqeq12d 2637 |
. . . . . 6
++
++ ++ |
43 | 42 | imbi2d 330 |
. . . . 5
++
++
++
|
44 | | fveq2 6191 |
. . . . . . . . 9
|
45 | 44 | rneqd 5353 |
. . . . . . . 8
|
46 | 45 | ineq1d 3813 |
. . . . . . 7
|
47 | | rneq 5351 |
. . . . . . . . 9
|
48 | 47 | ineq1d 3813 |
. . . . . . . 8
|
49 | 48 | iuneq1d 4545 |
. . . . . . 7
|
50 | 46, 49 | eqeq12d 2637 |
. . . . . 6
|
51 | 50 | imbi2d 330 |
. . . . 5
|
52 | 2 | mrsub0 31413 |
. . . . . . . . 9
|
53 | 52 | rneqd 5353 |
. . . . . . . 8
|
54 | 53, 6 | syl6eq 2672 |
. . . . . . 7
|
55 | 54 | ineq1d 3813 |
. . . . . 6
|
56 | 55, 21 | syl6eq 2672 |
. . . . 5
|
57 | | uneq1 3760 |
. . . . . . . 8
|
58 | | simpl 473 |
. . . . . . . . . . . . . 14
Word mCN mCN |
59 | | simprl 794 |
. . . . . . . . . . . . . . 15
Word mCN mCN Word mCN |
60 | 13 | adantr 481 |
. . . . . . . . . . . . . . 15
Word mCN mCN Word mCN |
61 | 59, 60 | eleqtrrd 2704 |
. . . . . . . . . . . . . 14
Word mCN mCN |
62 | | simprr 796 |
. . . . . . . . . . . . . . . 16
Word mCN mCN mCN |
63 | 62 | s1cld 13383 |
. . . . . . . . . . . . . . 15
Word mCN mCN Word
mCN |
64 | 63, 60 | eleqtrrd 2704 |
. . . . . . . . . . . . . 14
Word mCN mCN |
65 | 2, 11 | mrsubccat 31415 |
. . . . . . . . . . . . . 14
++
++
|
66 | 58, 61, 64, 65 | syl3anc 1326 |
. . . . . . . . . . . . 13
Word mCN mCN ++ ++ |
67 | 66 | rneqd 5353 |
. . . . . . . . . . . 12
Word mCN mCN ++ ++
|
68 | 2, 11 | mrsubf 31414 |
. . . . . . . . . . . . . . . 16
|
69 | 68 | adantr 481 |
. . . . . . . . . . . . . . 15
Word mCN mCN |
70 | 69, 61 | ffvelrnd 6360 |
. . . . . . . . . . . . . 14
Word mCN mCN |
71 | 70, 60 | eleqtrd 2703 |
. . . . . . . . . . . . 13
Word mCN mCN Word mCN |
72 | 69, 64 | ffvelrnd 6360 |
. . . . . . . . . . . . . 14
Word mCN mCN |
73 | 72, 60 | eleqtrd 2703 |
. . . . . . . . . . . . 13
Word mCN mCN Word mCN |
74 | | ccatrn 13372 |
. . . . . . . . . . . . 13
Word
mCN
Word mCN ++
|
75 | 71, 73, 74 | syl2anc 693 |
. . . . . . . . . . . 12
Word mCN mCN ++
|
76 | 67, 75 | eqtrd 2656 |
. . . . . . . . . . 11
Word mCN mCN ++ |
77 | 76 | ineq1d 3813 |
. . . . . . . . . 10
Word mCN mCN ++ |
78 | | indir 3875 |
. . . . . . . . . 10
|
79 | 77, 78 | syl6eq 2672 |
. . . . . . . . 9
Word mCN mCN ++ |
80 | | ccatrn 13372 |
. . . . . . . . . . . . . . . 16
Word mCN Word mCN ++ |
81 | 59, 63, 80 | syl2anc 693 |
. . . . . . . . . . . . . . 15
Word mCN mCN ++
|
82 | | s1rn 13379 |
. . . . . . . . . . . . . . . . 17
mCN
|
83 | 82 | ad2antll 765 |
. . . . . . . . . . . . . . . 16
Word mCN mCN |
84 | 83 | uneq2d 3767 |
. . . . . . . . . . . . . . 15
Word mCN mCN
|
85 | 81, 84 | eqtrd 2656 |
. . . . . . . . . . . . . 14
Word mCN mCN ++
|
86 | 85 | ineq1d 3813 |
. . . . . . . . . . . . 13
Word mCN mCN ++ |
87 | | indir 3875 |
. . . . . . . . . . . . 13
|
88 | 86, 87 | syl6eq 2672 |
. . . . . . . . . . . 12
Word mCN mCN ++ |
89 | 88 | iuneq1d 4545 |
. . . . . . . . . . 11
Word mCN mCN ++ |
90 | | iunxun 4605 |
. . . . . . . . . . 11
|
91 | 89, 90 | syl6eq 2672 |
. . . . . . . . . 10
Word mCN mCN ++
|
92 | | simpr 477 |
. . . . . . . . . . . . . . . 16
Word mCN mCN
|
93 | 92 | snssd 4340 |
. . . . . . . . . . . . . . 15
Word mCN mCN
|
94 | | df-ss 3588 |
. . . . . . . . . . . . . . 15
|
95 | 93, 94 | sylib 208 |
. . . . . . . . . . . . . 14
Word mCN mCN
|
96 | 95 | iuneq1d 4545 |
. . . . . . . . . . . . 13
Word mCN mCN
|
97 | | vex 3203 |
. . . . . . . . . . . . . 14
|
98 | | s1eq 13380 |
. . . . . . . . . . . . . . . . 17
|
99 | 98 | fveq2d 6195 |
. . . . . . . . . . . . . . . 16
|
100 | 99 | rneqd 5353 |
. . . . . . . . . . . . . . 15
|
101 | 100 | ineq1d 3813 |
. . . . . . . . . . . . . 14
|
102 | 97, 101 | iunxsn 4603 |
. . . . . . . . . . . . 13
|
103 | 96, 102 | syl6eq 2672 |
. . . . . . . . . . . 12
Word mCN mCN
|
104 | | incom 3805 |
. . . . . . . . . . . . . . 15
|
105 | | simpr 477 |
. . . . . . . . . . . . . . . 16
Word mCN mCN
|
106 | | disjsn 4246 |
. . . . . . . . . . . . . . . 16
|
107 | 105, 106 | sylibr 224 |
. . . . . . . . . . . . . . 15
Word mCN mCN |
108 | 104, 107 | syl5eq 2668 |
. . . . . . . . . . . . . 14
Word mCN mCN |
109 | 108 | iuneq1d 4545 |
. . . . . . . . . . . . 13
Word mCN mCN |
110 | 58 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
Word mCN mCN |
111 | | eldif 3584 |
. . . . . . . . . . . . . . . . . . . . 21
mCN mCN |
112 | 111 | biimpri 218 |
. . . . . . . . . . . . . . . . . . . 20
mCN
mCN |
113 | 62, 112 | sylan 488 |
. . . . . . . . . . . . . . . . . . 19
Word mCN mCN mCN
|
114 | | difun2 4048 |
. . . . . . . . . . . . . . . . . . 19
mCN mCN |
115 | 113, 114 | syl6eleq 2711 |
. . . . . . . . . . . . . . . . . 18
Word mCN mCN mCN
|
116 | 2, 11, 10, 9 | mrsubcn 31416 |
. . . . . . . . . . . . . . . . . 18
mCN |
117 | 110, 115,
116 | syl2anc 693 |
. . . . . . . . . . . . . . . . 17
Word mCN mCN |
118 | 117 | rneqd 5353 |
. . . . . . . . . . . . . . . 16
Word mCN mCN |
119 | 83 | adantr 481 |
. . . . . . . . . . . . . . . 16
Word mCN mCN |
120 | 118, 119 | eqtrd 2656 |
. . . . . . . . . . . . . . 15
Word mCN mCN |
121 | 120 | ineq1d 3813 |
. . . . . . . . . . . . . 14
Word mCN mCN |
122 | 121, 108 | eqtrd 2656 |
. . . . . . . . . . . . 13
Word mCN mCN |
123 | 24, 109, 122 | 3eqtr4a 2682 |
. . . . . . . . . . . 12
Word mCN mCN |
124 | 103, 123 | pm2.61dan 832 |
. . . . . . . . . . 11
Word mCN mCN |
125 | 124 | uneq2d 3767 |
. . . . . . . . . 10
Word mCN mCN
|
126 | 91, 125 | eqtrd 2656 |
. . . . . . . . 9
Word mCN mCN ++ |
127 | 79, 126 | eqeq12d 2637 |
. . . . . . . 8
Word mCN mCN
++
++
|
128 | 57, 127 | syl5ibr 236 |
. . . . . . 7
Word mCN mCN
++
++
|
129 | 128 | expcom 451 |
. . . . . 6
Word mCN mCN
++
++
|
130 | 129 | a2d 29 |
. . . . 5
Word mCN mCN
++ ++ |
131 | 27, 35, 43, 51, 56, 130 | wrdind 13476 |
. . . 4
Word mCN
|
132 | 131 | com12 32 |
. . 3
Word mCN
|
133 | 14, 132 | sylbid 230 |
. 2
|
134 | 133 | imp 445 |
1
|