Step Hyp Ref
Expression 1 cnfcom2OLD.1 . . . . . 6
2 n0i 3789 . . . . . 6
3 1 , 2 syl 16 . . . . 5
4 cnfcomOLD.f . . . . . . . . . . . . . 14
5 cnfcomOLD.s . . . . . . . . . . . . . . . . 17
6 omelon 8084 . . . . . . . . . . . . . . . . . 18
7 6 a1i 11 . . . . . . . . . . . . . . . . 17
8 cnfcomOLD.a . . . . . . . . . . . . . . . . 17
9 5 , 7 , 8 cantnff1o 8158 . . . . . . . . . . . . . . . 16
10 f1ocnv 5833 . . . . . . . . . . . . . . . 16
11 f1of 5821 . . . . . . . . . . . . . . . 16
12 9 , 10 , 11 3syl 20 . . . . . . . . . . . . . . 15
13 cnfcomOLD.b . . . . . . . . . . . . . . 15
14 12 , 13 ffvelrnd 6032 . . . . . . . . . . . . . 14
15 4 , 14 syl5eqel 2549 . . . . . . . . . . . . 13
16 5 , 7 , 8 cantnfsOLD 8136 . . . . . . . . . . . . 13
17 15 , 16 mpbid 210 . . . . . . . . . . . 12
18 17 simpld 459 . . . . . . . . . . 11
19 18 adantr 465 . . . . . . . . . 10
20 19 feqmptd 5926 . . . . . . . . 9
21 dif0 3898 . . . . . . . . . . . 12
22 21 eleq2i 2535 . . . . . . . . . . 11
23 df1o2 7161 . . . . . . . . . . . . . . . 16
24 23 difeq2i 3618 . . . . . . . . . . . . . . 15
25 24 imaeq2i 5340 . . . . . . . . . . . . . 14
26 simpr 461 . . . . . . . . . . . . . . . . 17
27 cnvimass 5362 . . . . . . . . . . . . . . . . . . . . 21
28 fdm 5740 . . . . . . . . . . . . . . . . . . . . . 22
29 18 , 28 syl 16 . . . . . . . . . . . . . . . . . . . . 21
30 27 , 29 syl5sseq 3551 . . . . . . . . . . . . . . . . . . . 20
31 8 , 30 ssexd 4599 . . . . . . . . . . . . . . . . . . 19
32 cnfcomOLD.g . . . . . . . . . . . . . . . . . . . . 21
33 5 , 7 , 8 , 32 , 15 cantnfclOLD 8137 . . . . . . . . . . . . . . . . . . . 20
34 33 simpld 459 . . . . . . . . . . . . . . . . . . 19
35 32 oien 7984 . . . . . . . . . . . . . . . . . . 19
36 31 , 34 , 35 syl2anc 661 . . . . . . . . . . . . . . . . . 18
37 36 adantr 465 . . . . . . . . . . . . . . . . 17
38 26 , 37 eqbrtrrd 4474 . . . . . . . . . . . . . . . 16
39 38 ensymd 7586 . . . . . . . . . . . . . . 15
40 en0 7598 . . . . . . . . . . . . . . 15
41 39 , 40 sylib 196 . . . . . . . . . . . . . 14
42 25 , 41 syl5eqr 2512 . . . . . . . . . . . . 13
43 ss0b 3815 . . . . . . . . . . . . 13
44 42 , 43 sylibr 212 . . . . . . . . . . . 12
45 19 , 44 suppssrOLD 6021 . . . . . . . . . . 11
46 22 , 45 sylan2br 476 . . . . . . . . . 10
47 46 mpteq2dva 4538 . . . . . . . . 9
48 20 , 47 eqtrd 2498 . . . . . . . 8
49 fconstmpt 5048 . . . . . . . 8
50 48 , 49 syl6eqr 2516 . . . . . . 7
51 50 fveq2d 5875 . . . . . 6
52 4 fveq2i 5874 . . . . . . . 8
53 f1ocnvfv2 6183 . . . . . . . . 9
54 9 , 13 , 53 syl2anc 661 . . . . . . . 8
55 52 , 54 syl5eq 2510 . . . . . . 7
56 55 adantr 465 . . . . . 6
57 peano1 6719 . . . . . . . . 9
58 57 a1i 11 . . . . . . . 8
59 5 , 7 , 8 , 58 cantnf0 8115 . . . . . . 7
60 59 adantr 465 . . . . . 6
61 51 , 56 , 60 3eqtr3d 2506 . . . . 5
62 3 , 61 mtand 659 . . . 4
63 33 simprd 463 . . . . 5
64 nnlim 6713 . . . . 5
65 63 , 64 syl 16 . . . 4
66 ioran 490 . . . 4
67 62 , 65 , 66 sylanbrc 664 . . 3
68 32 oicl 7975 . . . 4
69 unizlim 4999 . . . 4
70 68 , 69 ax-mp 5 . . 3
71 67 , 70 sylnibr 305 . 2
72 orduniorsuc 6665 . . . 4
73 68 , 72 mp1i 12 . . 3
74 73 ord 377 . 2
75 71 , 74 mpd 15 1
