Step | Hyp | Ref
| Expression |
1 | | omex 8540 |
. . . . 5
|
2 | 1 | 0dom 8090 |
. . . 4
|
3 | | breq1 4656 |
. . . 4
|
4 | 2, 3 | mpbiri 248 |
. . 3
|
5 | 4 | a1d 25 |
. 2
|
6 | | n0 3931 |
. . 3
|
7 | | ne0i 3921 |
. . . . . . . . . 10
|
8 | | unieq 4444 |
. . . . . . . . . . . 12
|
9 | | uni0 4465 |
. . . . . . . . . . . 12
|
10 | 8, 9 | syl6eq 2672 |
. . . . . . . . . . 11
|
11 | 10 | necon3i 2826 |
. . . . . . . . . 10
|
12 | 7, 11 | syl 17 |
. . . . . . . . 9
|
13 | 12 | adantl 482 |
. . . . . . . 8
|
14 | | simpl1 1064 |
. . . . . . . . 9
|
15 | | reldom 7961 |
. . . . . . . . . 10
|
16 | 15 | brrelexi 5158 |
. . . . . . . . 9
|
17 | | 0sdomg 8089 |
. . . . . . . . 9
|
18 | 14, 16, 17 | 3syl 18 |
. . . . . . . 8
|
19 | 13, 18 | mpbird 247 |
. . . . . . 7
|
20 | | fodomr 8111 |
. . . . . . 7
|
21 | 19, 14, 20 | syl2anc 693 |
. . . . . 6
|
22 | | omelon 8543 |
. . . . . . . . . . . 12
|
23 | | onenon 8775 |
. . . . . . . . . . . 12
|
24 | 22, 23 | ax-mp 5 |
. . . . . . . . . . 11
|
25 | | xpnum 8777 |
. . . . . . . . . . 11
|
26 | 24, 24, 25 | mp2an 708 |
. . . . . . . . . 10
|
27 | | simplrr 801 |
. . . . . . . . . . . . . . . . . . 19
|
28 | | fof 6115 |
. . . . . . . . . . . . . . . . . . 19
|
29 | 27, 28 | syl 17 |
. . . . . . . . . . . . . . . . . 18
|
30 | | simprl 794 |
. . . . . . . . . . . . . . . . . 18
|
31 | 29, 30 | ffvelrnd 6360 |
. . . . . . . . . . . . . . . . 17
|
32 | 31 | adantr 481 |
. . . . . . . . . . . . . . . 16
|
33 | | elssuni 4467 |
. . . . . . . . . . . . . . . 16
|
34 | 32, 33 | syl 17 |
. . . . . . . . . . . . . . 15
|
35 | 31, 33 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
|
36 | | simpll3 1102 |
. . . . . . . . . . . . . . . . . . . . 21
|
37 | | soss 5053 |
. . . . . . . . . . . . . . . . . . . . 21
|
38 | 35, 36, 37 | sylc 65 |
. . . . . . . . . . . . . . . . . . . 20
|
39 | | simpll2 1101 |
. . . . . . . . . . . . . . . . . . . . 21
|
40 | 39, 31 | sseldd 3604 |
. . . . . . . . . . . . . . . . . . . 20
|
41 | | finnisoeu 8936 |
. . . . . . . . . . . . . . . . . . . 20
|
42 | 38, 40, 41 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . 19
|
43 | | iotacl 5874 |
. . . . . . . . . . . . . . . . . . 19
|
44 | 42, 43 | syl 17 |
. . . . . . . . . . . . . . . . . 18
|
45 | | iotaex 5868 |
. . . . . . . . . . . . . . . . . . 19
|
46 | | isoeq1 6567 |
. . . . . . . . . . . . . . . . . . 19
|
47 | | isoeq1 6567 |
. . . . . . . . . . . . . . . . . . . 20
|
48 | 47 | cbvabv 2747 |
. . . . . . . . . . . . . . . . . . 19
|
49 | 45, 46, 48 | elab2 3354 |
. . . . . . . . . . . . . . . . . 18
|
50 | 44, 49 | sylib 208 |
. . . . . . . . . . . . . . . . 17
|
51 | | isof1o 6573 |
. . . . . . . . . . . . . . . . 17
|
52 | | f1of 6137 |
. . . . . . . . . . . . . . . . 17
|
53 | 50, 51, 52 | 3syl 18 |
. . . . . . . . . . . . . . . 16
|
54 | 53 | ffvelrnda 6359 |
. . . . . . . . . . . . . . 15
|
55 | 34, 54 | sseldd 3604 |
. . . . . . . . . . . . . 14
|
56 | | simprl 794 |
. . . . . . . . . . . . . . 15
|
57 | 56 | ad2antrr 762 |
. . . . . . . . . . . . . 14
|
58 | 55, 57 | ifclda 4120 |
. . . . . . . . . . . . 13
|
59 | 58 | ralrimivva 2971 |
. . . . . . . . . . . 12
|
60 | | eqid 2622 |
. . . . . . . . . . . . 13
|
61 | 60 | fmpt2 7237 |
. . . . . . . . . . . 12
|
62 | 59, 61 | sylib 208 |
. . . . . . . . . . 11
|
63 | | eluni 4439 |
. . . . . . . . . . . . 13
|
64 | | simplrr 801 |
. . . . . . . . . . . . . . . . 17
|
65 | | simprr 796 |
. . . . . . . . . . . . . . . . 17
|
66 | | foelrn 6378 |
. . . . . . . . . . . . . . . . 17
|
67 | 64, 65, 66 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
|
68 | | simprrl 804 |
. . . . . . . . . . . . . . . . . . . 20
|
69 | | ordom 7074 |
. . . . . . . . . . . . . . . . . . . . . 22
|
70 | | simpll2 1101 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
71 | | simplrr 801 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
72 | 71, 28 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
73 | 72, 68 | ffvelrnd 6360 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
74 | 70, 73 | sseldd 3604 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
75 | | ficardom 8787 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
76 | 74, 75 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
|
77 | | ordelss 5739 |
. . . . . . . . . . . . . . . . . . . . . 22
|
78 | 69, 76, 77 | sylancr 695 |
. . . . . . . . . . . . . . . . . . . . 21
|
79 | | elssuni 4467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
80 | 73, 79 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
81 | | simpll3 1102 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
82 | | soss 5053 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
83 | 80, 81, 82 | sylc 65 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
84 | | finnisoeu 8936 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
85 | 83, 74, 84 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
86 | | iotacl 5874 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
87 | 85, 86 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
88 | | iotaex 5868 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
89 | | isoeq1 6567 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
90 | | isoeq1 6567 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
91 | 90 | cbvabv 2747 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
92 | 88, 89, 91 | elab2 3354 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
93 | 87, 92 | sylib 208 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
94 | | isof1o 6573 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
95 | 93, 94 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
96 | | f1ocnv 6149 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
97 | | f1of 6137 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
98 | 95, 96, 97 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . 22
|
99 | | simprll 802 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
100 | | simprrr 805 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
101 | 99, 100 | eleqtrd 2703 |
. . . . . . . . . . . . . . . . . . . . . 22
|
102 | 98, 101 | ffvelrnd 6360 |
. . . . . . . . . . . . . . . . . . . . 21
|
103 | 78, 102 | sseldd 3604 |
. . . . . . . . . . . . . . . . . . . 20
|
104 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
105 | 104 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
106 | 105 | eleq2d 2687 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
107 | | isoeq4 6570 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
108 | 105, 107 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
109 | | isoeq5 6571 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
110 | 104, 109 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
111 | 108, 110 | bitrd 268 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
112 | 111 | iotabidv 5872 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
113 | 112 | fveq1d 6193 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
114 | 106, 113 | ifbieq1d 4109 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
115 | | eleq1 2689 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
116 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
117 | 115, 116 | ifbieq1d 4109 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
118 | | fvex 6201 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
119 | | vex 3203 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
120 | 118, 119 | ifex 4156 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
121 | 114, 117,
60, 120 | ovmpt2 6796 |
. . . . . . . . . . . . . . . . . . . . . 22
|
122 | 68, 103, 121 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . 21
|
123 | 102 | iftrued 4094 |
. . . . . . . . . . . . . . . . . . . . 21
|
124 | | f1ocnvfv2 6533 |
. . . . . . . . . . . . . . . . . . . . . 22
|
125 | 95, 101, 124 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . 21
|
126 | 122, 123,
125 | 3eqtrrd 2661 |
. . . . . . . . . . . . . . . . . . . 20
|
127 | | rspceov 6692 |
. . . . . . . . . . . . . . . . . . . 20
|
128 | 68, 103, 126, 127 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . 19
|
129 | 128 | expr 643 |
. . . . . . . . . . . . . . . . . 18
|
130 | 129 | expd 452 |
. . . . . . . . . . . . . . . . 17
|
131 | 130 | rexlimdv 3030 |
. . . . . . . . . . . . . . . 16
|
132 | 67, 131 | mpd 15 |
. . . . . . . . . . . . . . 15
|
133 | 132 | ex 450 |
. . . . . . . . . . . . . 14
|
134 | 133 | exlimdv 1861 |
. . . . . . . . . . . . 13
|
135 | 63, 134 | syl5bi 232 |
. . . . . . . . . . . 12
|
136 | 135 | ralrimiv 2965 |
. . . . . . . . . . 11
|
137 | | foov 6808 |
. . . . . . . . . . 11
|
138 | 62, 136, 137 | sylanbrc 698 |
. . . . . . . . . 10
|
139 | | fodomnum 8880 |
. . . . . . . . . 10
|
140 | 26, 138, 139 | mpsyl 68 |
. . . . . . . . 9
|
141 | | xpomen 8838 |
. . . . . . . . 9
|
142 | | domentr 8015 |
. . . . . . . . 9
|
143 | 140, 141,
142 | sylancl 694 |
. . . . . . . 8
|
144 | 143 | expr 643 |
. . . . . . 7
|
145 | 144 | exlimdv 1861 |
. . . . . 6
|
146 | 21, 145 | mpd 15 |
. . . . 5
|
147 | 146 | expcom 451 |
. . . 4
|
148 | 147 | exlimiv 1858 |
. . 3
|
149 | 6, 148 | sylbi 207 |
. 2
|
150 | 5, 149 | pm2.61ine 2877 |
1
|