Step Hyp Ref
Expression 1 cantnfsOLD.2 . . . . . 6
2 cantnfsOLD.3 . . . . . . 7
3 cantnfsOLD.1 . . . . . . . . 9
4 oemapvalOLD.t . . . . . . . . 9
5 oemapvalOLD.3 . . . . . . . . 9
6 oemapvalOLD.4 . . . . . . . . 9
7 oemapvalOLD.5 . . . . . . . . 9
8 oemapvalOLD.6 . . . . . . . . 9
9 3 , 1 , 2 , 4 , 5 , 6 , 7 , 8 oemapvali 8124 . . . . . . . 8
10 9 simp1d 1008 . . . . . . 7
11 onelon 4908 . . . . . . 7
12 2 , 10 , 11 syl2anc 661 . . . . . 6
13 oecl 7206 . . . . . 6
14 1 , 12 , 13 syl2anc 661 . . . . 5
15 3 , 1 , 2 cantnfsOLD 8136 . . . . . . . . 9
16 6 , 15 mpbid 210 . . . . . . . 8
17 16 simpld 459 . . . . . . 7
18 17 , 10 ffvelrnd 6032 . . . . . 6
19 onelon 4908 . . . . . 6
20 1 , 18 , 19 syl2anc 661 . . . . 5
21 omcl 7205 . . . . 5
22 14 , 20 , 21 syl2anc 661 . . . 4
23 cnvimass 5362 . . . . . . . . . . . 12
24 fdm 5740 . . . . . . . . . . . . 13
25 17 , 24 syl 16 . . . . . . . . . . . 12
26 23 , 25 syl5sseq 3551 . . . . . . . . . . 11
27 2 , 26 ssexd 4599 . . . . . . . . . 10
28 cantnflem1OLD.o . . . . . . . . . . . 12
29 3 , 1 , 2 , 28 , 6 cantnfclOLD 8137 . . . . . . . . . . 11
30 29 simpld 459 . . . . . . . . . 10
31 28 oiiso 7983 . . . . . . . . . 10
32 27 , 30 , 31 syl2anc 661 . . . . . . . . 9
33 isof1o 6221 . . . . . . . . 9
34 32 , 33 syl 16 . . . . . . . 8
35 f1ocnv 5833 . . . . . . . 8
36 f1of 5821 . . . . . . . 8
37 34 , 35 , 36 3syl 20 . . . . . . 7
38 3 , 1 , 2 , 4 , 5 , 6 , 7 , 8 cantnflem1aOLD 8148 . . . . . . 7
39 37 , 38 ffvelrnd 6032 . . . . . 6
40 29 simprd 463 . . . . . 6
41 elnn 6710 . . . . . 6
42 39 , 40 , 41 syl2anc 661 . . . . 5
43 cantnflem1OLD.h . . . . . . 7
44 43 cantnfvalf 8105 . . . . . 6
45 44 ffvelrni 6030 . . . . 5
46 42 , 45 syl 16 . . . 4
47 oaword1 7220 . . . 4
48 22 , 46 , 47 syl2anc 661 . . 3
49 3 , 1 , 2 , 28 , 6 , 43 cantnfsucOLD 8140 . . . . 5
50 42 , 49 mpdan 668 . . . 4
51 f1ocnvfv2 6183 . . . . . . . 8
52 34 , 38 , 51 syl2anc 661 . . . . . . 7
53 52 oveq2d 6312 . . . . . 6
54 52 fveq2d 5875 . . . . . 6
55 53 , 54 oveq12d 6314 . . . . 5
56 55 oveq1d 6311 . . . 4
57 50 , 56 eqtrd 2498 . . 3
58 48 , 57 sseqtr4d 3540 . 2
59 onss 6626 . . . . . . . . . . 11
60 2 , 59 syl 16 . . . . . . . . . 10
61 60 sselda 3503 . . . . . . . . 9
62 12 adantr 465 . . . . . . . . 9
63 onsseleq 4924 . . . . . . . . 9
64 61 , 62 , 63 syl2anc 661 . . . . . . . 8
65 orcom 387 . . . . . . . 8
66 64 , 65 syl6bb 261 . . . . . . 7
67 66 ifbid 3963 . . . . . 6
68 67 mpteq2dva 4538 . . . . 5
69 68 fveq2d 5875 . . . 4
70 3 , 1 , 2 cantnfsOLD 8136 . . . . . . . . . . . 12
71 5 , 70 mpbid 210 . . . . . . . . . . 11
72 71 simpld 459 . . . . . . . . . 10
73 72 ffvelrnda 6031 . . . . . . . . 9
74 ne0i 3790 . . . . . . . . . . . 12
75 18 , 74 syl 16 . . . . . . . . . . 11
76 on0eln0 4938 . . . . . . . . . . . 12
77 1 , 76 syl 16 . . . . . . . . . . 11
78 75 , 77 mpbird 232 . . . . . . . . . 10
79 78 adantr 465 . . . . . . . . 9
80 ifcl 3983 . . . . . . . . 9
81 73 , 79 , 80 syl2anc 661 . . . . . . . 8
82 eqid 2457 . . . . . . . 8
83 81 , 82 fmptd 6055 . . . . . . 7
84 71 simprd 463 . . . . . . . 8
85 df1o2 7161 . . . . . . . . . . 11
86 85 difeq2i 3618 . . . . . . . . . 10
87 86 imaeq2i 5340 . . . . . . . . 9
88 86 imaeq2i 5340 . . . . . . . . . . . . . 14
89 eqimss2 3556 . . . . . . . . . . . . . 14
90 88 , 89 mp1i 12 . . . . . . . . . . . . 13
91 72 , 90 suppssrOLD 6021 . . . . . . . . . . . 12
92 91 ifeq1d 3959 . . . . . . . . . . 11
93 ifid 3978 . . . . . . . . . . 11
94 92 , 93 syl6eq 2514 . . . . . . . . . 10
95 94 suppss2OLD 6530 . . . . . . . . 9
96 87 , 95 syl5eqss 3547 . . . . . . . 8
97 ssfi 7760 . . . . . . . 8
98 84 , 96 , 97 syl2anc 661 . . . . . . 7
99 3 , 1 , 2 cantnfsOLD 8136 . . . . . . 7
100 83 , 98 , 99 mpbir2and 922 . . . . . 6
101 72 , 10 ffvelrnd 6032 . . . . . 6
102 eldifn 3626 . . . . . . . . . 10
103 102 adantl 466 . . . . . . . . 9
104 iffalse 3950 . . . . . . . . 9
105 103 , 104 syl 16 . . . . . . . 8
106 105 suppss2OLD 6530 . . . . . . 7
107 87 , 106 syl5eqss 3547 . . . . . 6
108 fveq2 5871 . . . . . . . . . . 11
109 108 adantl 466 . . . . . . . . . 10
110 109 ifeq1da 3971 . . . . . . . . 9
111 eleq1 2529 . . . . . . . . . . . 12
112 fveq2 5871 . . . . . . . . . . . 12
113 111 , 112 ifbieq1d 3964 . . . . . . . . . . 11
114 fvex 5881 . . . . . . . . . . . 12
115 0ex 4582 . . . . . . . . . . . 12
116 114 , 115 ifex 4010 . . . . . . . . . . 11
117 113 , 82 , 116 fvmpt 5956 . . . . . . . . . 10
118 117 ifeq2d 3960 . . . . . . . . 9
119 110 , 118 eqtr3d 2500 . . . . . . . 8
120 ifor 3988 . . . . . . . 8
121 119 , 120 syl6reqr 2517 . . . . . . 7
122 121 mpteq2ia 4534 . . . . . 6
123 3 , 1 , 2 , 100 , 10 , 101 , 107 , 122 cantnfp1OLD 8147 . . . . 5
124 123 simprd 463 . . . 4
125 69 , 124 eqtrd 2498 . . 3
126 onelon 4908 . . . . . . 7
127 1 , 101 , 126 syl2anc 661 . . . . . 6
128 omsuc 7195 . . . . . 6
129 14 , 127 , 128 syl2anc 661 . . . . 5
130 eloni 4893 . . . . . . . 8
131 20 , 130 syl 16 . . . . . . 7
132 9 simp2d 1009 . . . . . . 7
133 ordsucss 6653 . . . . . . 7
134 131 , 132 ,
133 sylc 60 . . . . . 6
135 suceloni 6648 . . . . . . . 8
136 127 , 135 syl 16 . . . . . . 7
137 omwordi 7239 . . . . . . 7
138 136 , 20 , 14 , 137 syl3anc 1228 . . . . . 6
139 134 , 138 mpd 15 . . . . 5
140 129 , 139 eqsstr3d 3538 . . . 4
141 3 , 1 , 2 , 100 , 78 , 12 , 107 cantnflt2OLD 8143 . . . . 5
142 onelon 4908 . . . . . . 7
143 14 , 141 , 142 syl2anc 661 . . . . . 6
144 omcl 7205 . . . . . . 7
145 14 , 127 , 144 syl2anc 661 . . . . . 6
146 oaord 7215 . . . . . 6
147 143 , 14 , 145 , 146 syl3anc 1228 . . . . 5
148 141 , 147 mpbid 210 . . . 4
149 140 , 148 sseldd 3504 . . 3
150 125 , 149 eqeltrd 2545 . 2
151 58 , 150 sseldd 3504 1
