Step | Hyp | Ref
| Expression |
1 | | nn0ex 11298 |
. . . . . 6
|
2 | | fvex 6201 |
. . . . . . 7
|
3 | | snex 4908 |
. . . . . . 7
|
4 | 2, 3 | xpex 6962 |
. . . . . 6
|
5 | 1, 4 | iunex 7147 |
. . . . 5
|
6 | | heibor.4 |
. . . . . . . . 9
|
7 | 6 | relopabi 5245 |
. . . . . . . 8
|
8 | | 1st2nd 7214 |
. . . . . . . 8
|
9 | 7, 8 | mpan 706 |
. . . . . . 7
|
10 | 9 | eleq1d 2686 |
. . . . . . . . . . 11
|
11 | | df-br 4654 |
. . . . . . . . . . 11
|
12 | 10, 11 | syl6bbr 278 |
. . . . . . . . . 10
|
13 | | heibor.1 |
. . . . . . . . . . 11
|
14 | | heibor.3 |
. . . . . . . . . . 11
|
15 | | fvex 6201 |
. . . . . . . . . . 11
|
16 | | fvex 6201 |
. . . . . . . . . . 11
|
17 | 13, 14, 6, 15, 16 | heiborlem2 33611 |
. . . . . . . . . 10
|
18 | 12, 17 | syl6bb 276 |
. . . . . . . . 9
|
19 | 18 | ibi 256 |
. . . . . . . 8
|
20 | 16 | snid 4208 |
. . . . . . . . . . . 12
|
21 | | opelxp 5146 |
. . . . . . . . . . . 12
|
22 | 20, 21 | mpbiran2 954 |
. . . . . . . . . . 11
|
23 | | fveq2 6191 |
. . . . . . . . . . . . . 14
|
24 | | sneq 4187 |
. . . . . . . . . . . . . 14
|
25 | 23, 24 | xpeq12d 5140 |
. . . . . . . . . . . . 13
|
26 | 25 | eleq2d 2687 |
. . . . . . . . . . . 12
|
27 | 26 | rspcev 3309 |
. . . . . . . . . . 11
|
28 | 22, 27 | sylan2br 493 |
. . . . . . . . . 10
|
29 | | eliun 4524 |
. . . . . . . . . 10
|
30 | 28, 29 | sylibr 224 |
. . . . . . . . 9
|
31 | 30 | 3adant3 1081 |
. . . . . . . 8
|
32 | 19, 31 | syl 17 |
. . . . . . 7
|
33 | 9, 32 | eqeltrd 2701 |
. . . . . 6
|
34 | 33 | ssriv 3607 |
. . . . 5
|
35 | | ssdomg 8001 |
. . . . 5
|
36 | 5, 34, 35 | mp2 9 |
. . . 4
|
37 | | nn0ennn 12778 |
. . . . . . 7
|
38 | | nnenom 12779 |
. . . . . . 7
|
39 | 37, 38 | entri 8010 |
. . . . . 6
|
40 | | endom 7982 |
. . . . . 6
|
41 | 39, 40 | ax-mp 5 |
. . . . 5
|
42 | | vex 3203 |
. . . . . . . 8
|
43 | 2, 42 | xpsnen 8044 |
. . . . . . 7
|
44 | | inss2 3834 |
. . . . . . . . 9
|
45 | | heibor.7 |
. . . . . . . . . 10
|
46 | 45 | ffvelrnda 6359 |
. . . . . . . . 9
|
47 | 44, 46 | sseldi 3601 |
. . . . . . . 8
|
48 | | isfinite 8549 |
. . . . . . . . 9
|
49 | | sdomdom 7983 |
. . . . . . . . 9
|
50 | 48, 49 | sylbi 207 |
. . . . . . . 8
|
51 | 47, 50 | syl 17 |
. . . . . . 7
|
52 | | endomtr 8014 |
. . . . . . 7
|
53 | 43, 51, 52 | sylancr 695 |
. . . . . 6
|
54 | 53 | ralrimiva 2966 |
. . . . 5
|
55 | | iunctb 9396 |
. . . . 5
|
56 | 41, 54, 55 | sylancr 695 |
. . . 4
|
57 | | domtr 8009 |
. . . 4
|
58 | 36, 56, 57 | sylancr 695 |
. . 3
|
59 | 19 | simp1d 1073 |
. . . . . . . . 9
|
60 | | peano2nn0 11333 |
. . . . . . . . 9
|
61 | 59, 60 | syl 17 |
. . . . . . . 8
|
62 | | ffvelrn 6357 |
. . . . . . . 8
|
63 | 45, 61, 62 | syl2an 494 |
. . . . . . 7
|
64 | 44, 63 | sseldi 3601 |
. . . . . 6
|
65 | | iunin2 4584 |
. . . . . . . 8
|
66 | | heibor.8 |
. . . . . . . . . . 11
|
67 | | oveq1 6657 |
. . . . . . . . . . . . . . . 16
|
68 | 67 | cbviunv 4559 |
. . . . . . . . . . . . . . 15
|
69 | | fveq2 6191 |
. . . . . . . . . . . . . . . 16
|
70 | 69 | iuneq1d 4545 |
. . . . . . . . . . . . . . 15
|
71 | 68, 70 | syl5eq 2668 |
. . . . . . . . . . . . . 14
|
72 | | oveq2 6658 |
. . . . . . . . . . . . . . 15
|
73 | 72 | iuneq2d 4547 |
. . . . . . . . . . . . . 14
|
74 | 71, 73 | eqtrd 2656 |
. . . . . . . . . . . . 13
|
75 | 74 | eqeq2d 2632 |
. . . . . . . . . . . 12
|
76 | 75 | rspccva 3308 |
. . . . . . . . . . 11
|
77 | 66, 61, 76 | syl2an 494 |
. . . . . . . . . 10
|
78 | 77 | ineq2d 3814 |
. . . . . . . . 9
|
79 | 9 | fveq2d 6195 |
. . . . . . . . . . . . . 14
|
80 | | df-ov 6653 |
. . . . . . . . . . . . . 14
|
81 | 79, 80 | syl6eqr 2674 |
. . . . . . . . . . . . 13
|
82 | 81 | adantl 482 |
. . . . . . . . . . . 12
|
83 | | inss1 3833 |
. . . . . . . . . . . . . . . 16
|
84 | | ffvelrn 6357 |
. . . . . . . . . . . . . . . . 17
|
85 | 45, 59, 84 | syl2an 494 |
. . . . . . . . . . . . . . . 16
|
86 | 83, 85 | sseldi 3601 |
. . . . . . . . . . . . . . 15
|
87 | 86 | elpwid 4170 |
. . . . . . . . . . . . . 14
|
88 | 19 | simp2d 1074 |
. . . . . . . . . . . . . . 15
|
89 | 88 | adantl 482 |
. . . . . . . . . . . . . 14
|
90 | 87, 89 | sseldd 3604 |
. . . . . . . . . . . . 13
|
91 | 59 | adantl 482 |
. . . . . . . . . . . . 13
|
92 | | oveq1 6657 |
. . . . . . . . . . . . . 14
|
93 | | oveq2 6658 |
. . . . . . . . . . . . . . . 16
|
94 | 93 | oveq2d 6666 |
. . . . . . . . . . . . . . 15
|
95 | 94 | oveq2d 6666 |
. . . . . . . . . . . . . 14
|
96 | | heibor.5 |
. . . . . . . . . . . . . 14
|
97 | | ovex 6678 |
. . . . . . . . . . . . . 14
|
98 | 92, 95, 96, 97 | ovmpt2 6796 |
. . . . . . . . . . . . 13
|
99 | 90, 91, 98 | syl2anc 693 |
. . . . . . . . . . . 12
|
100 | 82, 99 | eqtrd 2656 |
. . . . . . . . . . 11
|
101 | | heibor.6 |
. . . . . . . . . . . . . . 15
|
102 | | cmetmet 23084 |
. . . . . . . . . . . . . . 15
|
103 | 101, 102 | syl 17 |
. . . . . . . . . . . . . 14
|
104 | | metxmet 22139 |
. . . . . . . . . . . . . 14
|
105 | 103, 104 | syl 17 |
. . . . . . . . . . . . 13
|
106 | 105 | adantr 481 |
. . . . . . . . . . . 12
|
107 | | 2nn 11185 |
. . . . . . . . . . . . . . . 16
|
108 | | nnexpcl 12873 |
. . . . . . . . . . . . . . . 16
|
109 | 107, 91, 108 | sylancr 695 |
. . . . . . . . . . . . . . 15
|
110 | 109 | nnrpd 11870 |
. . . . . . . . . . . . . 14
|
111 | 110 | rpreccld 11882 |
. . . . . . . . . . . . 13
|
112 | 111 | rpxrd 11873 |
. . . . . . . . . . . 12
|
113 | | blssm 22223 |
. . . . . . . . . . . 12
|
114 | 106, 90, 112, 113 | syl3anc 1326 |
. . . . . . . . . . 11
|
115 | 100, 114 | eqsstrd 3639 |
. . . . . . . . . 10
|
116 | | df-ss 3588 |
. . . . . . . . . 10
|
117 | 115, 116 | sylib 208 |
. . . . . . . . 9
|
118 | 78, 117 | eqtr3d 2658 |
. . . . . . . 8
|
119 | 65, 118 | syl5eq 2668 |
. . . . . . 7
|
120 | | eqimss2 3658 |
. . . . . . 7
|
121 | 119, 120 | syl 17 |
. . . . . 6
|
122 | 19 | simp3d 1075 |
. . . . . . . 8
|
123 | 81, 122 | eqeltrd 2701 |
. . . . . . 7
|
124 | 123 | adantl 482 |
. . . . . 6
|
125 | | fvex 6201 |
. . . . . . . 8
|
126 | 125 | inex1 4799 |
. . . . . . 7
|
127 | 13, 14, 126 | heiborlem1 33610 |
. . . . . 6
|
128 | 64, 121, 124, 127 | syl3anc 1326 |
. . . . 5
|
129 | 83, 63 | sseldi 3601 |
. . . . . . . . . . . 12
|
130 | 129 | elpwid 4170 |
. . . . . . . . . . 11
|
131 | 13 | mopnuni 22246 |
. . . . . . . . . . . . 13
|
132 | 105, 131 | syl 17 |
. . . . . . . . . . . 12
|
133 | 132 | adantr 481 |
. . . . . . . . . . 11
|
134 | 130, 133 | sseqtrd 3641 |
. . . . . . . . . 10
|
135 | 134 | sselda 3603 |
. . . . . . . . 9
|
136 | 135 | adantrr 753 |
. . . . . . . 8
|
137 | 61 | adantl 482 |
. . . . . . . . . 10
|
138 | | id 22 |
. . . . . . . . . 10
|
139 | | snfi 8038 |
. . . . . . . . . . . 12
|
140 | | inss2 3834 |
. . . . . . . . . . . . 13
|
141 | | ovex 6678 |
. . . . . . . . . . . . . . 15
|
142 | 141 | unisn 4451 |
. . . . . . . . . . . . . 14
|
143 | | uniiun 4573 |
. . . . . . . . . . . . . 14
|
144 | 142, 143 | eqtr3i 2646 |
. . . . . . . . . . . . 13
|
145 | 140, 144 | sseqtri 3637 |
. . . . . . . . . . . 12
|
146 | | vex 3203 |
. . . . . . . . . . . . 13
|
147 | 13, 14, 146 | heiborlem1 33610 |
. . . . . . . . . . . 12
|
148 | 139, 145,
147 | mp3an12 1414 |
. . . . . . . . . . 11
|
149 | | eleq1 2689 |
. . . . . . . . . . . 12
|
150 | 141, 149 | rexsn 4223 |
. . . . . . . . . . 11
|
151 | 148, 150 | sylib 208 |
. . . . . . . . . 10
|
152 | | ovex 6678 |
. . . . . . . . . . . 12
|
153 | 13, 14, 6, 42, 152 | heiborlem2 33611 |
. . . . . . . . . . 11
|
154 | 153 | biimpri 218 |
. . . . . . . . . 10
|
155 | 137, 138,
151, 154 | syl3an 1368 |
. . . . . . . . 9
|
156 | 155 | 3expb 1266 |
. . . . . . . 8
|
157 | | simprr 796 |
. . . . . . . 8
|
158 | 136, 156,
157 | jca32 558 |
. . . . . . 7
|
159 | 158 | ex 450 |
. . . . . 6
|
160 | 159 | reximdv2 3014 |
. . . . 5
|
161 | 128, 160 | mpd 15 |
. . . 4
|
162 | 161 | ralrimiva 2966 |
. . 3
|
163 | | fvex 6201 |
. . . . . 6
|
164 | 13, 163 | eqeltri 2697 |
. . . . 5
|
165 | 164 | uniex 6953 |
. . . 4
|
166 | | breq1 4656 |
. . . . 5
|
167 | | oveq1 6657 |
. . . . . . 7
|
168 | 167 | ineq2d 3814 |
. . . . . 6
|
169 | 168 | eleq1d 2686 |
. . . . 5
|
170 | 166, 169 | anbi12d 747 |
. . . 4
|
171 | 165, 170 | axcc4dom 9263 |
. . 3
|
172 | 58, 162, 171 | syl2anc 693 |
. 2
|
173 | | exsimpr 1796 |
. 2
|
174 | 172, 173 | syl 17 |
1
|