Proof of Theorem ramub1lem1
Step | Hyp | Ref
| Expression |
1 | | ramub1.v |
. . . . . . . 8
|
2 | | ramub1.w |
. . . . . . . 8
|
3 | 1, 2 | sstrd 3613 |
. . . . . . 7
|
4 | 3 | difss2d 3740 |
. . . . . 6
|
5 | | ramub1.x |
. . . . . . 7
|
6 | 5 | snssd 4340 |
. . . . . 6
|
7 | 4, 6 | unssd 3789 |
. . . . 5
|
8 | | ramub1.4 |
. . . . . 6
|
9 | | elpw2g 4827 |
. . . . . 6
|
10 | 8, 9 | syl 17 |
. . . . 5
|
11 | 7, 10 | mpbird 247 |
. . . 4
|
12 | 11 | adantr 481 |
. . 3
|
13 | | iftrue 4092 |
. . . . . . 7
|
14 | 13 | adantl 482 |
. . . . . 6
|
15 | | ramub1.9 |
. . . . . . 7
|
16 | 15 | adantr 481 |
. . . . . 6
|
17 | 14, 16 | eqbrtrrd 4677 |
. . . . 5
|
18 | | ramub1.f |
. . . . . . . . 9
|
19 | | ramub1.d |
. . . . . . . . 9
|
20 | 18, 19 | ffvelrnd 6360 |
. . . . . . . 8
|
21 | 20 | adantr 481 |
. . . . . . 7
|
22 | 21 | nnred 11035 |
. . . . . 6
|
23 | | 1red 10055 |
. . . . . 6
|
24 | | ssfi 8180 |
. . . . . . . . 9
|
25 | 8, 4, 24 | syl2anc 693 |
. . . . . . . 8
|
26 | | hashcl 13147 |
. . . . . . . 8
|
27 | | nn0re 11301 |
. . . . . . . 8
|
28 | 25, 26, 27 | 3syl 18 |
. . . . . . 7
|
29 | 28 | adantr 481 |
. . . . . 6
|
30 | 22, 23, 29 | lesubaddd 10624 |
. . . . 5
|
31 | 17, 30 | mpbid 222 |
. . . 4
|
32 | | fveq2 6191 |
. . . . 5
|
33 | | snidg 4206 |
. . . . . . . 8
|
34 | 5, 33 | syl 17 |
. . . . . . 7
|
35 | 3 | sseld 3602 |
. . . . . . . 8
|
36 | | eldifn 3733 |
. . . . . . . 8
|
37 | 35, 36 | syl6 35 |
. . . . . . 7
|
38 | 34, 37 | mt2d 131 |
. . . . . 6
|
39 | | hashunsng 13181 |
. . . . . . 7
|
40 | 5, 39 | syl 17 |
. . . . . 6
|
41 | 25, 38, 40 | mp2and 715 |
. . . . 5
|
42 | 32, 41 | breqan12rd 4670 |
. . . 4
|
43 | 31, 42 | mpbird 247 |
. . 3
|
44 | | snfi 8038 |
. . . . . . 7
|
45 | | unfi 8227 |
. . . . . . 7
|
46 | 25, 44, 45 | sylancl 694 |
. . . . . 6
|
47 | | ramub1.m |
. . . . . . 7
|
48 | 47 | nnnn0d 11351 |
. . . . . 6
|
49 | | ramub1.3 |
. . . . . . 7
|
50 | 49 | hashbcval 15706 |
. . . . . 6
|
51 | 46, 48, 50 | syl2anc 693 |
. . . . 5
|
52 | 51 | adantr 481 |
. . . 4
|
53 | | simpl1l 1112 |
. . . . . . . 8
|
54 | 49 | hashbcval 15706 |
. . . . . . . . . 10
|
55 | 25, 48, 54 | syl2anc 693 |
. . . . . . . . 9
|
56 | | ramub1.s |
. . . . . . . . 9
|
57 | 55, 56 | eqsstr3d 3640 |
. . . . . . . 8
|
58 | 53, 57 | syl 17 |
. . . . . . 7
|
59 | | simpr 477 |
. . . . . . . 8
|
60 | | simpl3 1066 |
. . . . . . . 8
|
61 | | rabid 3116 |
. . . . . . . 8
|
62 | 59, 60, 61 | sylanbrc 698 |
. . . . . . 7
|
63 | 58, 62 | sseldd 3604 |
. . . . . 6
|
64 | | simpl2 1065 |
. . . . . . . . . . . 12
|
65 | 64 | elpwid 4170 |
. . . . . . . . . . 11
|
66 | | simpl1l 1112 |
. . . . . . . . . . . 12
|
67 | 66, 7 | syl 17 |
. . . . . . . . . . 11
|
68 | 65, 67 | sstrd 3613 |
. . . . . . . . . 10
|
69 | | vex 3203 |
. . . . . . . . . . 11
|
70 | 69 | elpw 4164 |
. . . . . . . . . 10
|
71 | 68, 70 | sylibr 224 |
. . . . . . . . 9
|
72 | | simpl3 1066 |
. . . . . . . . 9
|
73 | | rabid 3116 |
. . . . . . . . 9
|
74 | 71, 72, 73 | sylanbrc 698 |
. . . . . . . 8
|
75 | 49 | hashbcval 15706 |
. . . . . . . . . 10
|
76 | 8, 48, 75 | syl2anc 693 |
. . . . . . . . 9
|
77 | 66, 76 | syl 17 |
. . . . . . . 8
|
78 | 74, 77 | eleqtrrd 2704 |
. . . . . . 7
|
79 | 2 | difss2d 3740 |
. . . . . . . . . . . . . . 15
|
80 | | ssfi 8180 |
. . . . . . . . . . . . . . 15
|
81 | 8, 79, 80 | syl2anc 693 |
. . . . . . . . . . . . . 14
|
82 | | nnm1nn0 11334 |
. . . . . . . . . . . . . . 15
|
83 | 47, 82 | syl 17 |
. . . . . . . . . . . . . 14
|
84 | 49 | hashbcval 15706 |
. . . . . . . . . . . . . 14
|
85 | 81, 83, 84 | syl2anc 693 |
. . . . . . . . . . . . 13
|
86 | | ramub1.8 |
. . . . . . . . . . . . 13
|
87 | 85, 86 | eqsstr3d 3640 |
. . . . . . . . . . . 12
|
88 | 66, 87 | syl 17 |
. . . . . . . . . . 11
|
89 | | uncom 3757 |
. . . . . . . . . . . . . . . 16
|
90 | 65, 89 | syl6sseq 3651 |
. . . . . . . . . . . . . . 15
|
91 | | ssundif 4052 |
. . . . . . . . . . . . . . 15
|
92 | 90, 91 | sylib 208 |
. . . . . . . . . . . . . 14
|
93 | 66, 1 | syl 17 |
. . . . . . . . . . . . . 14
|
94 | 92, 93 | sstrd 3613 |
. . . . . . . . . . . . 13
|
95 | | difexg 4808 |
. . . . . . . . . . . . . . 15
|
96 | 69, 95 | ax-mp 5 |
. . . . . . . . . . . . . 14
|
97 | 96 | elpw 4164 |
. . . . . . . . . . . . 13
|
98 | 94, 97 | sylibr 224 |
. . . . . . . . . . . 12
|
99 | 66, 8 | syl 17 |
. . . . . . . . . . . . . . . . 17
|
100 | | ssfi 8180 |
. . . . . . . . . . . . . . . . 17
|
101 | 99, 68, 100 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
|
102 | | diffi 8192 |
. . . . . . . . . . . . . . . 16
|
103 | 101, 102 | syl 17 |
. . . . . . . . . . . . . . 15
|
104 | | hashcl 13147 |
. . . . . . . . . . . . . . 15
|
105 | | nn0cn 11302 |
. . . . . . . . . . . . . . 15
|
106 | 103, 104,
105 | 3syl 18 |
. . . . . . . . . . . . . 14
|
107 | | ax-1cn 9994 |
. . . . . . . . . . . . . 14
|
108 | | pncan 10287 |
. . . . . . . . . . . . . 14
|
109 | 106, 107,
108 | sylancl 694 |
. . . . . . . . . . . . 13
|
110 | | neldifsnd 4322 |
. . . . . . . . . . . . . . . 16
|
111 | | hashunsng 13181 |
. . . . . . . . . . . . . . . . 17
|
112 | 66, 5, 111 | 3syl 18 |
. . . . . . . . . . . . . . . 16
|
113 | 103, 110,
112 | mp2and 715 |
. . . . . . . . . . . . . . 15
|
114 | | undif1 4043 |
. . . . . . . . . . . . . . . . . 18
|
115 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . . 22
|
116 | 64, 115 | eldifd 3585 |
. . . . . . . . . . . . . . . . . . . . 21
|
117 | | elpwunsn 4224 |
. . . . . . . . . . . . . . . . . . . . 21
|
118 | 116, 117 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
|
119 | 118 | snssd 4340 |
. . . . . . . . . . . . . . . . . . 19
|
120 | | ssequn2 3786 |
. . . . . . . . . . . . . . . . . . 19
|
121 | 119, 120 | sylib 208 |
. . . . . . . . . . . . . . . . . 18
|
122 | 114, 121 | syl5req 2669 |
. . . . . . . . . . . . . . . . 17
|
123 | 122 | fveq2d 6195 |
. . . . . . . . . . . . . . . 16
|
124 | 123, 72 | eqtr3d 2658 |
. . . . . . . . . . . . . . 15
|
125 | 113, 124 | eqtr3d 2658 |
. . . . . . . . . . . . . 14
|
126 | 125 | oveq1d 6665 |
. . . . . . . . . . . . 13
|
127 | 109, 126 | eqtr3d 2658 |
. . . . . . . . . . . 12
|
128 | | fveq2 6191 |
. . . . . . . . . . . . . 14
|
129 | 128 | eqeq1d 2624 |
. . . . . . . . . . . . 13
|
130 | 129 | elrab 3363 |
. . . . . . . . . . . 12
|
131 | 98, 127, 130 | sylanbrc 698 |
. . . . . . . . . . 11
|
132 | 88, 131 | sseldd 3604 |
. . . . . . . . . 10
|
133 | | ramub1.h |
. . . . . . . . . . . 12
|
134 | 133 | mptiniseg 5629 |
. . . . . . . . . . 11
|
135 | 66, 19, 134 | 3syl 18 |
. . . . . . . . . 10
|
136 | 132, 135 | eleqtrd 2703 |
. . . . . . . . 9
|
137 | | uneq1 3760 |
. . . . . . . . . . . . 13
|
138 | 137 | fveq2d 6195 |
. . . . . . . . . . . 12
|
139 | 138 | eqeq1d 2624 |
. . . . . . . . . . 11
|
140 | 139 | elrab 3363 |
. . . . . . . . . 10
|
141 | 140 | simprbi 480 |
. . . . . . . . 9
|
142 | 136, 141 | syl 17 |
. . . . . . . 8
|
143 | 122 | fveq2d 6195 |
. . . . . . . 8
|
144 | | simpl1r 1113 |
. . . . . . . 8
|
145 | 142, 143,
144 | 3eqtr4d 2666 |
. . . . . . 7
|
146 | | ramub1.6 |
. . . . . . . . 9
|
147 | | ffn 6045 |
. . . . . . . . 9
|
148 | 146, 147 | syl 17 |
. . . . . . . 8
|
149 | | fniniseg 6338 |
. . . . . . . 8
|
150 | 66, 148, 149 | 3syl 18 |
. . . . . . 7
|
151 | 78, 145, 150 | mpbir2and 957 |
. . . . . 6
|
152 | 63, 151 | pm2.61dan 832 |
. . . . 5
|
153 | 152 | rabssdv 3682 |
. . . 4
|
154 | 52, 153 | eqsstrd 3639 |
. . 3
|
155 | | fveq2 6191 |
. . . . . 6
|
156 | 155 | breq2d 4665 |
. . . . 5
|
157 | | oveq1 6657 |
. . . . . 6
|
158 | 157 | sseq1d 3632 |
. . . . 5
|
159 | 156, 158 | anbi12d 747 |
. . . 4
|
160 | 159 | rspcev 3309 |
. . 3
|
161 | 12, 43, 154, 160 | syl12anc 1324 |
. 2
|
162 | | elpw2g 4827 |
. . . . . 6
|
163 | 8, 162 | syl 17 |
. . . . 5
|
164 | 4, 163 | mpbird 247 |
. . . 4
|
165 | 164 | adantr 481 |
. . 3
|
166 | | ifnefalse 4098 |
. . . . 5
|
167 | 166 | adantl 482 |
. . . 4
|
168 | 15 | adantr 481 |
. . . 4
|
169 | 167, 168 | eqbrtrrd 4677 |
. . 3
|
170 | 56 | adantr 481 |
. . 3
|
171 | | fveq2 6191 |
. . . . . 6
|
172 | 171 | breq2d 4665 |
. . . . 5
|
173 | | oveq1 6657 |
. . . . . 6
|
174 | 173 | sseq1d 3632 |
. . . . 5
|
175 | 172, 174 | anbi12d 747 |
. . . 4
|
176 | 175 | rspcev 3309 |
. . 3
|
177 | 165, 169,
170, 176 | syl12anc 1324 |
. 2
|
178 | 161, 177 | pm2.61dane 2881 |
1
|