Step | Hyp | Ref
| Expression |
1 | | stoweidlem27.4 |
. . . 4
|
2 | | stoweidlem27.5 |
. . . 4
|
3 | | fnex 6481 |
. . . 4
|
4 | 1, 2, 3 | syl2anc 693 |
. . 3
|
5 | | stoweidlem27.7 |
. . . . 5
|
6 | | f1ofn 6138 |
. . . . 5
|
7 | 5, 6 | syl 17 |
. . . 4
|
8 | | ovex 6678 |
. . . 4
|
9 | | fnex 6481 |
. . . 4
|
10 | 7, 8, 9 | sylancl 694 |
. . 3
|
11 | | coexg 7117 |
. . 3
|
12 | 4, 10, 11 | syl2anc 693 |
. 2
|
13 | | stoweidlem27.3 |
. . 3
|
14 | | f1of 6137 |
. . . . . 6
|
15 | 5, 14 | syl 17 |
. . . . 5
|
16 | | fnfco 6069 |
. . . . 5
|
17 | 1, 15, 16 | syl2anc 693 |
. . . 4
|
18 | | rncoss 5386 |
. . . . 5
|
19 | | fvelrnb 6243 |
. . . . . . . . . . 11
|
20 | 1, 19 | syl 17 |
. . . . . . . . . 10
|
21 | 20 | biimpa 501 |
. . . . . . . . 9
|
22 | | stoweidlem27.10 |
. . . . . . . . . . . . . 14
|
23 | | stoweidlem27.1 |
. . . . . . . . . . . . . . . . 17
|
24 | | nfmpt1 4747 |
. . . . . . . . . . . . . . . . 17
|
25 | 23, 24 | nfcxfr 2762 |
. . . . . . . . . . . . . . . 16
|
26 | 25 | nfrn 5368 |
. . . . . . . . . . . . . . 15
|
27 | 26 | nfcri 2758 |
. . . . . . . . . . . . . 14
|
28 | 22, 27 | nfan 1828 |
. . . . . . . . . . . . 13
|
29 | | stoweidlem27.6 |
. . . . . . . . . . . . . . . . 17
|
30 | 29 | ad2antrr 762 |
. . . . . . . . . . . . . . . 16
|
31 | | simpr 477 |
. . . . . . . . . . . . . . . 16
|
32 | 30, 31 | eleqtrd 2703 |
. . . . . . . . . . . . . . 15
|
33 | | nfcv 2764 |
. . . . . . . . . . . . . . . 16
|
34 | | stoweidlem27.11 |
. . . . . . . . . . . . . . . 16
|
35 | | nfv 1843 |
. . . . . . . . . . . . . . . 16
|
36 | | fveq1 6190 |
. . . . . . . . . . . . . . . . . . 19
|
37 | 36 | breq2d 4665 |
. . . . . . . . . . . . . . . . . 18
|
38 | 37 | rabbidv 3189 |
. . . . . . . . . . . . . . . . 17
|
39 | 38 | eqeq2d 2632 |
. . . . . . . . . . . . . . . 16
|
40 | 33, 34, 35, 39 | elrabf 3360 |
. . . . . . . . . . . . . . 15
|
41 | 32, 40 | sylib 208 |
. . . . . . . . . . . . . 14
|
42 | 41 | simpld 475 |
. . . . . . . . . . . . 13
|
43 | | simpr 477 |
. . . . . . . . . . . . . 14
|
44 | 23 | elrnmpt 5372 |
. . . . . . . . . . . . . . 15
|
45 | 43, 44 | syl 17 |
. . . . . . . . . . . . . 14
|
46 | 43, 45 | mpbid 222 |
. . . . . . . . . . . . 13
|
47 | 28, 42, 46 | r19.29af 3076 |
. . . . . . . . . . . 12
|
48 | 47 | adantlr 751 |
. . . . . . . . . . 11
|
49 | | eleq1 2689 |
. . . . . . . . . . 11
|
50 | 48, 49 | syl5ibcom 235 |
. . . . . . . . . 10
|
51 | 50 | reximdva 3017 |
. . . . . . . . 9
|
52 | 21, 51 | mpd 15 |
. . . . . . . 8
|
53 | | idd 24 |
. . . . . . . . . 10
|
54 | 53 | a1i 11 |
. . . . . . . . 9
|
55 | 54 | rexlimdv 3030 |
. . . . . . . 8
|
56 | 52, 55 | mpd 15 |
. . . . . . 7
|
57 | 56 | ex 450 |
. . . . . 6
|
58 | 57 | ssrdv 3609 |
. . . . 5
|
59 | 18, 58 | syl5ss 3614 |
. . . 4
|
60 | | df-f 5892 |
. . . 4
|
61 | 17, 59, 60 | sylanbrc 698 |
. . 3
|
62 | | stoweidlem27.9 |
. . . 4
|
63 | | stoweidlem27.8 |
. . . . . . . . 9
|
64 | 63 | sselda 3603 |
. . . . . . . 8
|
65 | | eluni 4439 |
. . . . . . . 8
|
66 | 64, 65 | sylib 208 |
. . . . . . 7
|
67 | | nfv 1843 |
. . . . . . . . 9
|
68 | 22, 67 | nfan 1828 |
. . . . . . . 8
|
69 | 23 | funmpt2 5927 |
. . . . . . . . . . . . . 14
|
70 | 23 | dmeqi 5325 |
. . . . . . . . . . . . . . . . 17
|
71 | | stoweidlem27.2 |
. . . . . . . . . . . . . . . . . . . . . 22
|
72 | 34 | rabexgf 39183 |
. . . . . . . . . . . . . . . . . . . . . 22
|
73 | 71, 72 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
|
74 | 73 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
|
75 | 74 | ex 450 |
. . . . . . . . . . . . . . . . . . 19
|
76 | 22, 75 | ralrimi 2957 |
. . . . . . . . . . . . . . . . . 18
|
77 | | dmmptg 5632 |
. . . . . . . . . . . . . . . . . 18
|
78 | 76, 77 | syl 17 |
. . . . . . . . . . . . . . . . 17
|
79 | 70, 78 | syl5eq 2668 |
. . . . . . . . . . . . . . . 16
|
80 | 79 | eleq2d 2687 |
. . . . . . . . . . . . . . 15
|
81 | 80 | biimpar 502 |
. . . . . . . . . . . . . 14
|
82 | | fvelrn 6352 |
. . . . . . . . . . . . . 14
|
83 | 69, 81, 82 | sylancr 695 |
. . . . . . . . . . . . 13
|
84 | 83 | adantrl 752 |
. . . . . . . . . . . 12
|
85 | 15 | ad2antrr 762 |
. . . . . . . . . . . . . . . 16
|
86 | | simprl 794 |
. . . . . . . . . . . . . . . 16
|
87 | | fvco3 6275 |
. . . . . . . . . . . . . . . 16
|
88 | 85, 86, 87 | syl2anc 693 |
. . . . . . . . . . . . . . 15
|
89 | | fveq2 6191 |
. . . . . . . . . . . . . . . 16
|
90 | 89 | ad2antll 765 |
. . . . . . . . . . . . . . 15
|
91 | 88, 90 | eqtrd 2656 |
. . . . . . . . . . . . . 14
|
92 | | eleq1 2689 |
. . . . . . . . . . . . . . . . . . 19
|
93 | 92 | anbi2d 740 |
. . . . . . . . . . . . . . . . . 18
|
94 | | eleq2 2690 |
. . . . . . . . . . . . . . . . . . 19
|
95 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . 20
|
96 | 95 | eleq1d 2686 |
. . . . . . . . . . . . . . . . . . 19
|
97 | 94, 96 | bitrd 268 |
. . . . . . . . . . . . . . . . . 18
|
98 | 93, 97 | imbi12d 334 |
. . . . . . . . . . . . . . . . 17
|
99 | 98, 29 | vtoclg 3266 |
. . . . . . . . . . . . . . . 16
|
100 | 99 | anabsi7 860 |
. . . . . . . . . . . . . . 15
|
101 | 100 | adantr 481 |
. . . . . . . . . . . . . 14
|
102 | 91, 101 | eqeltrd 2701 |
. . . . . . . . . . . . 13
|
103 | | f1ofo 6144 |
. . . . . . . . . . . . . . . . 17
|
104 | | forn 6118 |
. . . . . . . . . . . . . . . . 17
|
105 | 5, 103, 104 | 3syl 18 |
. . . . . . . . . . . . . . . 16
|
106 | 105 | eleq2d 2687 |
. . . . . . . . . . . . . . 15
|
107 | 106 | biimpar 502 |
. . . . . . . . . . . . . 14
|
108 | 7 | adantr 481 |
. . . . . . . . . . . . . . 15
|
109 | | fvelrnb 6243 |
. . . . . . . . . . . . . . 15
|
110 | 108, 109 | syl 17 |
. . . . . . . . . . . . . 14
|
111 | 107, 110 | mpbid 222 |
. . . . . . . . . . . . 13
|
112 | 102, 111 | reximddv 3018 |
. . . . . . . . . . . 12
|
113 | 84, 112 | syldan 487 |
. . . . . . . . . . 11
|
114 | | simplrl 800 |
. . . . . . . . . . . . . . . 16
|
115 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . . 22
|
116 | 23 | fvmpt2 6291 |
. . . . . . . . . . . . . . . . . . . . . 22
|
117 | 115, 74, 116 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . 21
|
118 | 117 | eleq2d 2687 |
. . . . . . . . . . . . . . . . . . . 20
|
119 | 118 | biimpa 501 |
. . . . . . . . . . . . . . . . . . 19
|
120 | 119 | adantlrl 756 |
. . . . . . . . . . . . . . . . . 18
|
121 | | nfcv 2764 |
. . . . . . . . . . . . . . . . . . 19
|
122 | | nfv 1843 |
. . . . . . . . . . . . . . . . . . 19
|
123 | | fveq1 6190 |
. . . . . . . . . . . . . . . . . . . . . 22
|
124 | 123 | breq2d 4665 |
. . . . . . . . . . . . . . . . . . . . 21
|
125 | 124 | rabbidv 3189 |
. . . . . . . . . . . . . . . . . . . 20
|
126 | 125 | eqeq2d 2632 |
. . . . . . . . . . . . . . . . . . 19
|
127 | 121, 34, 122, 126 | elrabf 3360 |
. . . . . . . . . . . . . . . . . 18
|
128 | 120, 127 | sylib 208 |
. . . . . . . . . . . . . . . . 17
|
129 | 128 | simprd 479 |
. . . . . . . . . . . . . . . 16
|
130 | 114, 129 | eleqtrd 2703 |
. . . . . . . . . . . . . . 15
|
131 | | rabid 3116 |
. . . . . . . . . . . . . . 15
|
132 | 130, 131 | sylib 208 |
. . . . . . . . . . . . . 14
|
133 | 132 | simprd 479 |
. . . . . . . . . . . . 13
|
134 | 133 | ex 450 |
. . . . . . . . . . . 12
|
135 | 134 | reximdv 3016 |
. . . . . . . . . . 11
|
136 | 113, 135 | mpd 15 |
. . . . . . . . . 10
|
137 | 136 | ex 450 |
. . . . . . . . 9
|
138 | 137 | adantr 481 |
. . . . . . . 8
|
139 | 68, 138 | eximd 2085 |
. . . . . . 7
|
140 | 66, 139 | mpd 15 |
. . . . . 6
|
141 | | nfv 1843 |
. . . . . . 7
|
142 | | idd 24 |
. . . . . . 7
|
143 | 68, 141, 142 | exlimd 2087 |
. . . . . 6
|
144 | 140, 143 | mpd 15 |
. . . . 5
|
145 | 144 | ex 450 |
. . . 4
|
146 | 62, 145 | ralrimi 2957 |
. . 3
|
147 | 13, 61, 146 | jca32 558 |
. 2
|
148 | | feq1 6026 |
. . . . 5
|
149 | | fveq1 6190 |
. . . . . . . . 9
|
150 | 149 | fveq1d 6193 |
. . . . . . . 8
|
151 | 150 | breq2d 4665 |
. . . . . . 7
|
152 | 151 | rexbidv 3052 |
. . . . . 6
|
153 | 152 | ralbidv 2986 |
. . . . 5
|
154 | 148, 153 | anbi12d 747 |
. . . 4
|
155 | 154 | anbi2d 740 |
. . 3
|
156 | 155 | spcegv 3294 |
. 2
|
157 | 12, 147, 156 | sylc 65 |
1
|