Step | Hyp | Ref
| Expression |
1 | | rdgeq2 7508 |
. . 3
|
2 | | ifeq1 4090 |
. . . . . . . . 9
|
3 | 2 | eqeq2d 2632 |
. . . . . . . 8
|
4 | 3 | ralbidv 2986 |
. . . . . . 7
|
5 | 4 | anbi2d 740 |
. . . . . 6
|
6 | 5 | rexbidv 3052 |
. . . . 5
|
7 | 6 | abbidv 2741 |
. . . 4
|
8 | 7 | unieqd 4446 |
. . 3
|
9 | 1, 8 | eqeq12d 2637 |
. 2
|
10 | | df-rdg 7506 |
. . 3
recs
|
11 | | dfrecs3 7469 |
. . 3
recs
|
12 | | vex 3203 |
. . . . . . . . . . . . 13
|
13 | 12 | resex 5443 |
. . . . . . . . . . . 12
|
14 | | eqeq1 2626 |
. . . . . . . . . . . . . . 15
|
15 | | relres 5426 |
. . . . . . . . . . . . . . . 16
|
16 | | reldm0 5343 |
. . . . . . . . . . . . . . . 16
|
17 | 15, 16 | ax-mp 5 |
. . . . . . . . . . . . . . 15
|
18 | 14, 17 | syl6bb 276 |
. . . . . . . . . . . . . 14
|
19 | | dmeq 5324 |
. . . . . . . . . . . . . . . 16
|
20 | | limeq 5735 |
. . . . . . . . . . . . . . . 16
|
21 | 19, 20 | syl 17 |
. . . . . . . . . . . . . . 15
|
22 | | rneq 5351 |
. . . . . . . . . . . . . . . . 17
|
23 | | df-ima 5127 |
. . . . . . . . . . . . . . . . 17
|
24 | 22, 23 | syl6eqr 2674 |
. . . . . . . . . . . . . . . 16
|
25 | 24 | unieqd 4446 |
. . . . . . . . . . . . . . 15
|
26 | | id 22 |
. . . . . . . . . . . . . . . . 17
|
27 | 19 | unieqd 4446 |
. . . . . . . . . . . . . . . . 17
|
28 | 26, 27 | fveq12d 6197 |
. . . . . . . . . . . . . . . 16
|
29 | 28 | fveq2d 6195 |
. . . . . . . . . . . . . . 15
|
30 | 21, 25, 29 | ifbieq12d 4113 |
. . . . . . . . . . . . . 14
|
31 | 18, 30 | ifbieq2d 4111 |
. . . . . . . . . . . . 13
|
32 | | eqid 2622 |
. . . . . . . . . . . . 13
|
33 | | vex 3203 |
. . . . . . . . . . . . . 14
|
34 | | imaexg 7103 |
. . . . . . . . . . . . . . . . 17
|
35 | 12, 34 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
|
36 | 35 | uniex 6953 |
. . . . . . . . . . . . . . 15
|
37 | | fvex 6201 |
. . . . . . . . . . . . . . 15
|
38 | 36, 37 | ifex 4156 |
. . . . . . . . . . . . . 14
|
39 | 33, 38 | ifex 4156 |
. . . . . . . . . . . . 13
|
40 | 31, 32, 39 | fvmpt 6282 |
. . . . . . . . . . . 12
|
41 | 13, 40 | ax-mp 5 |
. . . . . . . . . . 11
|
42 | | dmres 5419 |
. . . . . . . . . . . . 13
|
43 | | onelss 5766 |
. . . . . . . . . . . . . . . . 17
|
44 | 43 | imp 445 |
. . . . . . . . . . . . . . . 16
|
45 | 44 | 3adant2 1080 |
. . . . . . . . . . . . . . 15
|
46 | | fndm 5990 |
. . . . . . . . . . . . . . . 16
|
47 | 46 | 3ad2ant2 1083 |
. . . . . . . . . . . . . . 15
|
48 | 45, 47 | sseqtr4d 3642 |
. . . . . . . . . . . . . 14
|
49 | | df-ss 3588 |
. . . . . . . . . . . . . 14
|
50 | 48, 49 | sylib 208 |
. . . . . . . . . . . . 13
|
51 | 42, 50 | syl5eq 2668 |
. . . . . . . . . . . 12
|
52 | | eqeq1 2626 |
. . . . . . . . . . . . . 14
|
53 | | limeq 5735 |
. . . . . . . . . . . . . . 15
|
54 | | unieq 4444 |
. . . . . . . . . . . . . . . . 17
|
55 | 54 | fveq2d 6195 |
. . . . . . . . . . . . . . . 16
|
56 | 55 | fveq2d 6195 |
. . . . . . . . . . . . . . 15
|
57 | 53, 56 | ifbieq2d 4111 |
. . . . . . . . . . . . . 14
|
58 | 52, 57 | ifbieq2d 4111 |
. . . . . . . . . . . . 13
|
59 | | onelon 5748 |
. . . . . . . . . . . . . . . 16
|
60 | | eloni 5733 |
. . . . . . . . . . . . . . . 16
|
61 | 59, 60 | syl 17 |
. . . . . . . . . . . . . . 15
|
62 | 61 | 3adant2 1080 |
. . . . . . . . . . . . . 14
|
63 | | ordzsl 7045 |
. . . . . . . . . . . . . . 15
|
64 | | iftrue 4092 |
. . . . . . . . . . . . . . . . 17
|
65 | | iftrue 4092 |
. . . . . . . . . . . . . . . . 17
|
66 | 64, 65 | eqtr4d 2659 |
. . . . . . . . . . . . . . . 16
|
67 | | vex 3203 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
68 | 67 | sucid 5804 |
. . . . . . . . . . . . . . . . . . . . . 22
|
69 | | fvres 6207 |
. . . . . . . . . . . . . . . . . . . . . 22
|
70 | 68, 69 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . 21
|
71 | | eloni 5733 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
72 | | ordunisuc 7032 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
73 | 71, 72 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
|
74 | 73 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . 21
|
75 | 73 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . 21
|
76 | 70, 74, 75 | 3eqtr4a 2682 |
. . . . . . . . . . . . . . . . . . . 20
|
77 | 76 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . 19
|
78 | | nsuceq0 5805 |
. . . . . . . . . . . . . . . . . . . . . 22
|
79 | 78 | neii 2796 |
. . . . . . . . . . . . . . . . . . . . 21
|
80 | 79 | iffalsei 4096 |
. . . . . . . . . . . . . . . . . . . 20
|
81 | | nlimsucg 7042 |
. . . . . . . . . . . . . . . . . . . . 21
|
82 | | iffalse 4095 |
. . . . . . . . . . . . . . . . . . . . 21
|
83 | 67, 81, 82 | mp2b 10 |
. . . . . . . . . . . . . . . . . . . 20
|
84 | 80, 83 | eqtri 2644 |
. . . . . . . . . . . . . . . . . . 19
|
85 | 79 | iffalsei 4096 |
. . . . . . . . . . . . . . . . . . . 20
|
86 | | iffalse 4095 |
. . . . . . . . . . . . . . . . . . . . 21
|
87 | 67, 81, 86 | mp2b 10 |
. . . . . . . . . . . . . . . . . . . 20
|
88 | 85, 87 | eqtri 2644 |
. . . . . . . . . . . . . . . . . . 19
|
89 | 77, 84, 88 | 3eqtr4g 2681 |
. . . . . . . . . . . . . . . . . 18
|
90 | | eqeq1 2626 |
. . . . . . . . . . . . . . . . . . . 20
|
91 | | limeq 5735 |
. . . . . . . . . . . . . . . . . . . . 21
|
92 | | reseq2 5391 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
93 | | unieq 4444 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
94 | 92, 93 | fveq12d 6197 |
. . . . . . . . . . . . . . . . . . . . . 22
|
95 | 94 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . 21
|
96 | 91, 95 | ifbieq2d 4111 |
. . . . . . . . . . . . . . . . . . . 20
|
97 | 90, 96 | ifbieq2d 4111 |
. . . . . . . . . . . . . . . . . . 19
|
98 | 93 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . . 22
|
99 | 98 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . 21
|
100 | 91, 99 | ifbieq2d 4111 |
. . . . . . . . . . . . . . . . . . . 20
|
101 | 90, 100 | ifbieq2d 4111 |
. . . . . . . . . . . . . . . . . . 19
|
102 | 97, 101 | eqeq12d 2637 |
. . . . . . . . . . . . . . . . . 18
|
103 | 89, 102 | syl5ibrcom 237 |
. . . . . . . . . . . . . . . . 17
|
104 | 103 | rexlimiv 3027 |
. . . . . . . . . . . . . . . 16
|
105 | | iftrue 4092 |
. . . . . . . . . . . . . . . . . 18
|
106 | | df-lim 5728 |
. . . . . . . . . . . . . . . . . . . . 21
|
107 | 106 | simp2bi 1077 |
. . . . . . . . . . . . . . . . . . . 20
|
108 | 107 | neneqd 2799 |
. . . . . . . . . . . . . . . . . . 19
|
109 | 108 | iffalsed 4097 |
. . . . . . . . . . . . . . . . . 18
|
110 | | iftrue 4092 |
. . . . . . . . . . . . . . . . . 18
|
111 | 105, 109,
110 | 3eqtr4d 2666 |
. . . . . . . . . . . . . . . . 17
|
112 | 108 | iffalsed 4097 |
. . . . . . . . . . . . . . . . 17
|
113 | 111, 112 | eqtr4d 2659 |
. . . . . . . . . . . . . . . 16
|
114 | 66, 104, 113 | 3jaoi 1391 |
. . . . . . . . . . . . . . 15
|
115 | 63, 114 | sylbi 207 |
. . . . . . . . . . . . . 14
|
116 | 62, 115 | syl 17 |
. . . . . . . . . . . . 13
|
117 | 58, 116 | sylan9eqr 2678 |
. . . . . . . . . . . 12
|
118 | 51, 117 | mpdan 702 |
. . . . . . . . . . 11
|
119 | 41, 118 | syl5eq 2668 |
. . . . . . . . . 10
|
120 | 119 | eqeq2d 2632 |
. . . . . . . . 9
|
121 | 120 | 3expa 1265 |
. . . . . . . 8
|
122 | 121 | ralbidva 2985 |
. . . . . . 7
|
123 | 122 | pm5.32da 673 |
. . . . . 6
|
124 | 123 | rexbiia 3040 |
. . . . 5
|
125 | 124 | abbii 2739 |
. . . 4
|
126 | 125 | unieqi 4445 |
. . 3
|
127 | 10, 11, 126 | 3eqtri 2648 |
. 2
|
128 | 9, 127 | vtoclg 3266 |
1
|