Step | Hyp | Ref
| Expression |
1 | | elequ2 2004 |
. . . . . . 7
|
2 | | elequ2 2004 |
. . . . . . . 8
|
3 | 2 | notbid 308 |
. . . . . . 7
|
4 | 1, 3 | bi2anan9r 918 |
. . . . . 6
|
5 | | elequ2 2004 |
. . . . . . . . 9
|
6 | | elequ2 2004 |
. . . . . . . . 9
|
7 | 5, 6 | bi2bian9 919 |
. . . . . . . 8
|
8 | 7 | imbi2d 330 |
. . . . . . 7
|
9 | 8 | ralbidv 2986 |
. . . . . 6
|
10 | 4, 9 | anbi12d 747 |
. . . . 5
|
11 | 10 | rexbidv 3052 |
. . . 4
|
12 | | elequ1 1997 |
. . . . . . 7
|
13 | | elequ1 1997 |
. . . . . . . 8
|
14 | 13 | notbid 308 |
. . . . . . 7
|
15 | 12, 14 | anbi12d 747 |
. . . . . 6
|
16 | | breq2 4657 |
. . . . . . . . 9
|
17 | 16 | imbi1d 331 |
. . . . . . . 8
|
18 | 17 | ralbidv 2986 |
. . . . . . 7
|
19 | | breq1 4656 |
. . . . . . . . 9
|
20 | | elequ1 1997 |
. . . . . . . . . 10
|
21 | | elequ1 1997 |
. . . . . . . . . 10
|
22 | 20, 21 | bibi12d 335 |
. . . . . . . . 9
|
23 | 19, 22 | imbi12d 334 |
. . . . . . . 8
|
24 | 23 | cbvralv 3171 |
. . . . . . 7
|
25 | 18, 24 | syl6bb 276 |
. . . . . 6
|
26 | 15, 25 | anbi12d 747 |
. . . . 5
|
27 | 26 | cbvrexv 3172 |
. . . 4
|
28 | 11, 27 | syl6bb 276 |
. . 3
|
29 | 28 | cbvopabv 4722 |
. 2
|
30 | | nfcv 2764 |
. . 3
|
31 | | nfcv 2764 |
. . . 4
|
32 | | nfcv 2764 |
. . . 4
|
33 | | nfopab1 4719 |
. . . 4
|
34 | 31, 32, 33 | nfsup 8357 |
. . 3
|
35 | | fveq2 6191 |
. . . 4
|
36 | 35 | supeq1d 8352 |
. . 3
|
37 | 30, 34, 36 | cbvmpt 4749 |
. 2
|
38 | | nfcv 2764 |
. . . 4
|
39 | | nffvmpt1 6199 |
. . . 4
|
40 | | rneq 5351 |
. . . . . 6
|
41 | 40 | difeq2d 3728 |
. . . . 5
|
42 | 41 | fveq2d 6195 |
. . . 4
|
43 | 38, 39, 42 | cbvmpt 4749 |
. . 3
|
44 | | recseq 7470 |
. . 3
recs
recs
|
45 | 43, 44 | ax-mp 5 |
. 2
recs
recs
|
46 | | nfv 1843 |
. . 3
recs
recs
|
47 | | nfv 1843 |
. . 3
recs
recs
|
48 | | nfmpt1 4747 |
. . . . . . . 8
|
49 | 48 | nfrecs 7471 |
. . . . . . 7
recs
|
50 | 49 | nfcnv 5301 |
. . . . . 6
recs
|
51 | | nfcv 2764 |
. . . . . 6
|
52 | 50, 51 | nfima 5474 |
. . . . 5
recs
|
53 | 52 | nfint 4486 |
. . . 4
recs
|
54 | | nfcv 2764 |
. . . . . 6
|
55 | 50, 54 | nfima 5474 |
. . . . 5
recs
|
56 | 55 | nfint 4486 |
. . . 4
recs
|
57 | 53, 56 | nfel 2777 |
. . 3
recs
recs
|
58 | | nfcv 2764 |
. . . . . . . . 9
|
59 | | nfcv 2764 |
. . . . . . . . . . . 12
|
60 | | nfcv 2764 |
. . . . . . . . . . . 12
|
61 | | nfopab2 4720 |
. . . . . . . . . . . 12
|
62 | 59, 60, 61 | nfsup 8357 |
. . . . . . . . . . 11
|
63 | 58, 62 | nfmpt 4746 |
. . . . . . . . . 10
|
64 | | nfcv 2764 |
. . . . . . . . . 10
|
65 | 63, 64 | nffv 6198 |
. . . . . . . . 9
|
66 | 58, 65 | nfmpt 4746 |
. . . . . . . 8
|
67 | 66 | nfrecs 7471 |
. . . . . . 7
recs
|
68 | 67 | nfcnv 5301 |
. . . . . 6
recs
|
69 | | nfcv 2764 |
. . . . . 6
|
70 | 68, 69 | nfima 5474 |
. . . . 5
recs
|
71 | 70 | nfint 4486 |
. . . 4
recs
|
72 | | nfcv 2764 |
. . . . . 6
|
73 | 68, 72 | nfima 5474 |
. . . . 5
recs
|
74 | 73 | nfint 4486 |
. . . 4
recs
|
75 | 71, 74 | nfel 2777 |
. . 3
recs
recs
|
76 | | sneq 4187 |
. . . . . 6
|
77 | 76 | imaeq2d 5466 |
. . . . 5
recs
recs
|
78 | 77 | inteqd 4480 |
. . . 4
recs
recs
|
79 | | sneq 4187 |
. . . . . 6
|
80 | 79 | imaeq2d 5466 |
. . . . 5
recs
recs
|
81 | 80 | inteqd 4480 |
. . . 4
recs
recs
|
82 | | eleq12 2691 |
. . . 4
recs
recs
recs
recs
recs
recs
recs
recs
|
83 | 78, 81, 82 | syl2an 494 |
. . 3
recs
recs
recs
recs
|
84 | 46, 47, 57, 75, 83 | cbvopab 4721 |
. 2
recs
recs
recs
recs
|
85 | | fveq2 6191 |
. . . . 5
|
86 | | fveq2 6191 |
. . . . 5
|
87 | 85, 86 | breqan12d 4669 |
. . . 4
|
88 | 85, 86 | eqeqan12d 2638 |
. . . . 5
|
89 | | simpl 473 |
. . . . . 6
|
90 | | suceq 5790 |
. . . . . . . . 9
|
91 | 85, 90 | syl 17 |
. . . . . . . 8
|
92 | 91 | adantr 481 |
. . . . . . 7
|
93 | 92 | fveq2d 6195 |
. . . . . 6
|
94 | | simpr 477 |
. . . . . 6
|
95 | 89, 93, 94 | breq123d 4667 |
. . . . 5
|
96 | 88, 95 | anbi12d 747 |
. . . 4
|
97 | 87, 96 | orbi12d 746 |
. . 3
|
98 | 97 | cbvopabv 4722 |
. 2
|
99 | | eqid 2622 |
. 2
recs
recs
recs
recs
|
100 | | dmeq 5324 |
. . . . . . 7
|
101 | 100 | unieqd 4446 |
. . . . . . 7
|
102 | 100, 101 | eqeq12d 2637 |
. . . . . 6
|
103 | | fveq1 6190 |
. . . . . . . . . 10
|
104 | 103 | breqd 4664 |
. . . . . . . . 9
|
105 | 104 | anbi2d 740 |
. . . . . . . 8
|
106 | 105 | orbi2d 738 |
. . . . . . 7
|
107 | 106 | opabbidv 4716 |
. . . . . 6
|
108 | | eqidd 2623 |
. . . . . . . . . . . . . . . 16
|
109 | 100 | fveq2d 6195 |
. . . . . . . . . . . . . . . 16
|
110 | 101 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . 18
|
111 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
112 | 111, 101 | fveq12d 6197 |
. . . . . . . . . . . . . . . . . . . . . 22
|
113 | 112 | breqd 4664 |
. . . . . . . . . . . . . . . . . . . . 21
|
114 | 113 | imbi1d 331 |
. . . . . . . . . . . . . . . . . . . 20
|
115 | 110, 114 | raleqbidv 3152 |
. . . . . . . . . . . . . . . . . . 19
|
116 | 115 | anbi2d 740 |
. . . . . . . . . . . . . . . . . 18
|
117 | 110, 116 | rexeqbidv 3153 |
. . . . . . . . . . . . . . . . 17
|
118 | 117 | opabbidv 4716 |
. . . . . . . . . . . . . . . 16
|
119 | 108, 109,
118 | supeq123d 8356 |
. . . . . . . . . . . . . . 15
|
120 | 119 | mpteq2dv 4745 |
. . . . . . . . . . . . . 14
|
121 | 109 | difeq1d 3727 |
. . . . . . . . . . . . . 14
|
122 | 120, 121 | fveq12d 6197 |
. . . . . . . . . . . . 13
|
123 | 122 | mpteq2dv 4745 |
. . . . . . . . . . . 12
|
124 | | recseq 7470 |
. . . . . . . . . . . 12
recs
recs
|
125 | 123, 124 | syl 17 |
. . . . . . . . . . 11
recs
recs
|
126 | 125 | cnveqd 5298 |
. . . . . . . . . 10
recs
recs
|
127 | 126 | imaeq1d 5465 |
. . . . . . . . 9
recs
recs
|
128 | 127 | inteqd 4480 |
. . . . . . . 8
recs
recs
|
129 | 126 | imaeq1d 5465 |
. . . . . . . . 9
recs
recs
|
130 | 129 | inteqd 4480 |
. . . . . . . 8
recs
recs
|
131 | 128, 130 | eleq12d 2695 |
. . . . . . 7
recs
recs
recs
recs
|
132 | 131 | opabbidv 4716 |
. . . . . 6
recs
recs
recs
recs
|
133 | 102, 107,
132 | ifbieq12d 4113 |
. . . . 5
recs
recs
recs
recs
|
134 | 109 | sqxpeqd 5141 |
. . . . 5
|
135 | 133, 134 | ineq12d 3815 |
. . . 4
recs
recs
recs
recs
|
136 | 135 | cbvmptv 4750 |
. . 3
recs
recs
recs
recs
|
137 | | recseq 7470 |
. . 3
recs
recs
recs
recs
recs
recs
recs
recs
recs
recs
|
138 | 136, 137 | ax-mp 5 |
. 2
recs recs
recs
recs
recs
recs
|
139 | | aomclem8.a |
. 2
|
140 | | aomclem8.y |
. . 3
|
141 | | neeq1 2856 |
. . . . 5
|
142 | | fveq2 6191 |
. . . . . 6
|
143 | | pweq 4161 |
. . . . . . . 8
|
144 | 143 | ineq1d 3813 |
. . . . . . 7
|
145 | 144 | difeq1d 3727 |
. . . . . 6
|
146 | 142, 145 | eleq12d 2695 |
. . . . 5
|
147 | 141, 146 | imbi12d 334 |
. . . 4
|
148 | 147 | cbvralv 3171 |
. . 3
|
149 | 140, 148 | sylib 208 |
. 2
|
150 | 29, 37, 45, 84, 98, 99, 138, 139, 149 | aomclem7 37630 |
1
|