MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  wunex2 Unicode version

Theorem wunex2 9137
Description: Construct a weak universe from a given set. (Contributed by Mario Carneiro, 2-Jan-2017.)
Hypotheses
Ref Expression
wunex2.f
wunex2.u
Assertion
Ref Expression
wunex2
Distinct variable group:   , ,

Proof of Theorem wunex2
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 wunex2.u . . . . . . . 8
21eleq2i 2535 . . . . . . 7
3 frfnom 7119 . . . . . . . . 9
4 wunex2.f . . . . . . . . . 10
54fneq1i 5680 . . . . . . . . 9
63, 5mpbir 209 . . . . . . . 8
7 fnunirn 6165 . . . . . . . 8
86, 7ax-mp 5 . . . . . . 7
92, 8bitri 249 . . . . . 6
10 elssuni 4279 . . . . . . . . . . 11
1110ad2antll 728 . . . . . . . . . 10
12 ssun2 3667 . . . . . . . . . . 11
13 ssun1 3666 . . . . . . . . . . 11
1412, 13sstri 3512 . . . . . . . . . 10
1511, 14syl6ss 3515 . . . . . . . . 9
16 simprl 756 . . . . . . . . . 10
17 fvex 5881 . . . . . . . . . . . 12
1817uniex 6596 . . . . . . . . . . . 12
1917, 18unex 6598 . . . . . . . . . . 11
20 prex 4694 . . . . . . . . . . . . 13
2117mptex 6143 . . . . . . . . . . . . . 14
2221rnex 6734 . . . . . . . . . . . . 13
2320, 22unex 6598 . . . . . . . . . . . 12
2417, 23iunex 6780 . . . . . . . . . . 11
2519, 24unex 6598 . . . . . . . . . 10
26 id 22 . . . . . . . . . . . . 13
27 unieq 4257 . . . . . . . . . . . . 13
2826, 27uneq12d 3658 . . . . . . . . . . . 12
29 pweq 4015 . . . . . . . . . . . . . . . 16
30 unieq 4257 . . . . . . . . . . . . . . . 16
3129, 30preq12d 4117 . . . . . . . . . . . . . . 15
32 preq2 4110 . . . . . . . . . . . . . . . . . 18
3332cbvmptv 4543 . . . . . . . . . . . . . . . . 17
34 preq1 4109 . . . . . . . . . . . . . . . . . 18
3534mpteq2dv 4539 . . . . . . . . . . . . . . . . 17
3633, 35syl5eq 2510 . . . . . . . . . . . . . . . 16
3736rneqd 5235 . . . . . . . . . . . . . . 15
3831, 37uneq12d 3658 . . . . . . . . . . . . . 14
3938cbviunv 4369 . . . . . . . . . . . . 13
40 mpteq1 4532 . . . . . . . . . . . . . . . 16
4140rneqd 5235 . . . . . . . . . . . . . . 15
4241uneq2d 3657 . . . . . . . . . . . . . 14
4326, 42iuneq12d 4356 . . . . . . . . . . . . 13
4439, 43syl5eq 2510 . . . . . . . . . . . 12
4528, 44uneq12d 3658 . . . . . . . . . . 11
46 id 22 . . . . . . . . . . . . 13
47 unieq 4257 . . . . . . . . . . . . 13
4846, 47uneq12d 3658 . . . . . . . . . . . 12
49 mpteq1 4532 . . . . . . . . . . . . . . 15
5049rneqd 5235 . . . . . . . . . . . . . 14
5150uneq2d 3657 . . . . . . . . . . . . 13
5246, 51iuneq12d 4356 . . . . . . . . . . . 12
5348, 52uneq12d 3658 . . . . . . . . . . 11
544, 45, 53frsucmpt2 7124 . . . . . . . . . 10
5516, 25, 54sylancl 662 . . . . . . . . 9
5615, 55sseqtr4d 3540 . . . . . . . 8
57 fvssunirn 5894 . . . . . . . . 9
5857, 1sseqtr4i 3536 . . . . . . . 8
5956, 58syl6ss 3515 . . . . . . 7
6059rexlimdvaa 2950 . . . . . 6
619, 60syl5bi 217 . . . . 5
6261ralrimiv 2869 . . . 4
63 dftr3 4549 . . . 4
6462, 63sylibr 212 . . 3
65 1on 7156 . . . . . . . 8
66 unexg 6601 . . . . . . . 8
6765, 66mpan2 671 . . . . . . 7
684fveq1i 5872 . . . . . . . 8
69 fr0g 7120 . . . . . . . 8
7068, 69syl5eq 2510 . . . . . . 7
7167, 70syl 16 . . . . . 6
72 fvssunirn 5894 . . . . . . 7
7372, 1sseqtr4i 3536 . . . . . 6
7471, 73syl6eqssr 3554 . . . . 5
7574unssbd 3681 . . . 4
76 1n0 7164 . . . 4
77 ssn0 3818 . . . 4
7875, 76, 77sylancl 662 . . 3
79 pweq 4015 . . . . . . . . . . . . . . 15
80 unieq 4257 . . . . . . . . . . . . . . 15
8179, 80preq12d 4117 . . . . . . . . . . . . . 14
82 preq1 4109 . . . . . . . . . . . . . . . 16
8382mpteq2dv 4539 . . . . . . . . . . . . . . 15
8483rneqd 5235 . . . . . . . . . . . . . 14
8581, 84uneq12d 3658 . . . . . . . . . . . . 13
8685ssiun2s 4374 . . . . . . . . . . . 12
8786ad2antll 728 . . . . . . . . . . 11
88 ssun2 3667 . . . . . . . . . . . . 13
8988, 55syl5sseqr 3552 . . . . . . . . . . . 12
9089, 58syl6ss 3515 . . . . . . . . . . 11
9187, 90sstrd 3513 . . . . . . . . . 10
9291unssad 3680 . . . . . . . . 9
93 vex 3112 . . . . . . . . . . 11
9493pwex 4635 . . . . . . . . . 10
9593uniex 6596 . . . . . . . . . 10
9694, 95prss 4184 . . . . . . . . 9
9792, 96sylibr 212 . . . . . . . 8
9897simprd 463 . . . . . . 7
9997simpld 459 . . . . . . 7
1001eleq2i 2535 . . . . . . . . . 10
101 fnunirn 6165 . . . . . . . . . . 11
1026, 101ax-mp 5 . . . . . . . . . 10
103100, 102bitri 249 . . . . . . . . 9
104 simplrl 761 . . . . . . . . . . . . . . . . 17
105 simprl 756 . . . . . . . . . . . . . . . . 17
106 ordom 6709 . . . . . . . . . . . . . . . . . 18
107 ordunel 6662 . . . . . . . . . . . . . . . . . 18
108106, 107mp3an1 1311 . . . . . . . . . . . . . . . . 17
109104, 105, 108syl2anc 661 . . . . . . . . . . . . . . . 16
110 ssun1 3666 . . . . . . . . . . . . . . . . 17
111 fveq2 5871 . . . . . . . . . . . . . . . . . . 19
112111sseq2d 3531 . . . . . . . . . . . . . . . . . 18
113 fveq2 5871 . . . . . . . . . . . . . . . . . . 19
114113sseq2d 3531 . . . . . . . . . . . . . . . . . 18
115 fveq2 5871 . . . . . . . . . . . . . . . . . . 19
116115sseq2d 3531 . . . . . . . . . . . . . . . . . 18
117 fveq2 5871 . . . . . . . . . . . . . . . . . . 19
118117sseq2d 3531 . . . . . . . . . . . . . . . . . 18
119 ssid 3522 . . . . . . . . . . . . . . . . . . 19
120119a1i 11 . . . . . . . . . . . . . . . . . 18
121 fveq2 5871 . . . . . . . . . . . . . . . . . . . . . 22
122 suceq 4948 . . . . . . . . . . . . . . . . . . . . . . 23
123122fveq2d 5875 . . . . . . . . . . . . . . . . . . . . . 22
124121, 123sseq12d 3532 . . . . . . . . . . . . . . . . . . . . 21
125 ssun1 3666 . . . . . . . . . . . . . . . . . . . . . . 23
126125, 13sstri 3512 . . . . . . . . . . . . . . . . . . . . . 22
12725, 54mpan2 671 . . . . . . . . . . . . . . . . . . . . . 22
128126, 127syl5sseqr 3552 . . . . . . . . . . . . . . . . . . . . 21
129124, 128vtoclga 3173 . . . . . . . . . . . . . . . . . . . 20
130129ad2antrr 725 . . . . . . . . . . . . . . . . . . 19
131 sstr2 3510 . . . . . . . . . . . . . . . . . . 19
132130, 131syl5com 30 . . . . . . . . . . . . . . . . . 18
133112, 114, 116, 118, 120, 132findsg 6727 . . . . . . . . . . . . . . . . 17
134110, 133mpan2 671 . . . . . . . . . . . . . . . 16
135109, 104, 134syl2anc 661 . . . . . . . . . . . . . . 15
136 simplrr 762 . . . . . . . . . . . . . . 15
137135, 136sseldd 3504 . . . . . . . . . . . . . 14
13882mpteq2dv 4539 . . . . . . . . . . . . . . . . 17
139138rneqd 5235 . . . . . . . . . . . . . . . 16
14081, 139uneq12d 3658 . . . . . . . . . . . . . . 15
141140ssiun2s 4374 . . . . . . . . . . . . . 14
142137, 141syl 16 . . . . . . . . . . . . 13
143 ssun2 3667 . . . . . . . . . . . . . . 15
144 fvex 5881 . . . . . . . . . . . . . . . . . 18
145144uniex 6596 . . . . . . . . . . . . . . . . . 18
146144, 145unex 6598 . . . . . . . . . . . . . . . . 17
147144mptex 6143 . . . . . . . . . . . . . . . . . . . 20
148147rnex 6734 . . . . . . . . . . . . . . . . . . 19
14920, 148unex 6598 . . . . . . . . . . . . . . . . . 18
150144, 149iunex 6780 . . . . . . . . . . . . . . . . 17
151146, 150unex 6598 . . . . . . . . . . . . . . . 16
152 id 22 . . . . . . . . . . . . . . . . . . 19
153 unieq 4257 . . . . . . . . . . . . . . . . . . 19
154152, 153uneq12d 3658 . . . . . . . . . . . . . . . . . 18
155 mpteq1 4532 . . . . . . . . . . . . . . . . . . . . 21
156155rneqd 5235 . . . . . . . . . . . . . . . . . . . 20
157156uneq2d 3657 . . . . . . . . . . . . . . . . . . 19
158152, 157iuneq12d 4356 . . . . . . . . . . . . . . . . . 18
159154, 158uneq12d 3658 . . . . . . . . . . . . . . . . 17
1604, 45, 159frsucmpt2 7124 . . . . . . . . . . . . . . . 16
161109, 151, 160sylancl 662 . . . . . . . . . . . . . . 15
162143, 161syl5sseqr 3552 . . . . . . . . . . . . . 14
163 fvssunirn 5894 . . . . . . . . . . . . . . 15
164163, 1sseqtr4i 3536 . . . . . . . . . . . . . 14
165162, 164syl6ss 3515 . . . . . . . . . . . . 13
166142, 165sstrd 3513 . . . . . . . . . . . 12
167166unssbd 3681 . . . . . . . . . . 11
168 ssun2 3667 . . . . . . . . . . . . . . . . . . 19
169 id 22 . . . . . . . . . . . . . . . . . . 19
170168, 169syl5sseqr 3552 . . . . . . . . . . . . . . . . . 18
171170biantrud 507 . . . . . . . . . . . . . . . . 17
172171bicomd 201 . . . . . . . . . . . . . . . 16
173 fveq2 5871 . . . . . . . . . . . . . . . . 17
174173sseq2d 3531 . . . . . . . . . . . . . . . 16
175172, 174imbi12d 320 . . . . . . . . . . . . . . 15
176 eleq1 2529 . . . . . . . . . . . . . . . . . . . 20
177176anbi2d 703 . . . . . . . . . . . . . . . . . . 19
178 sseq1 3524 . . . . . . . . . . . . . . . . . . 19
179177, 178anbi12d 710 . . . . . . . . . . . . . . . . . 18
180 fveq2 5871 . . . . . . . . . . . . . . . . . . 19
181180sseq1d 3530 . . . . . . . . . . . . . . . . . 18
182179, 181imbi12d 320 . . . . . . . . . . . . . . . . 17
183112, 114, 116, 114, 120, 132findsg 6727 . . . . . . . . . . . . . . . . 17
184182, 183chvarv 2014 . . . . . . . . . . . . . . . 16
185184expl 618 . . . . . . . . . . . . . . 15
186175, 185vtoclga 3173 . . . . . . . . . . . . . 14
187109, 105, 186sylc 60 . . . . . . . . . . . . 13
188 simprr 757 . . . . . . . . . . . . 13
189187, 188sseldd 3504 . . . . . . . . . . . 12
190 prex 4694 . . . . . . . . . . . 12
191 eqid 2457 . . . . . . . . . . . . 13
192 preq2 4110 . . . . . . . . . . . . 13
193191, 192elrnmpt1s 5255 . . . . . . . . . . . 12
194189, 190, 193sylancl 662 . . . . . . . . . . 11
195167, 194sseldd 3504 . . . . . . . . . 10
196195rexlimdvaa 2950 . . . . . . . . 9
197103, 196syl5bi 217 . . . . . . . 8
198197ralrimiv 2869 . . . . . . 7
19998, 99, 1983jca 1176 . . . . . 6
200199rexlimdvaa 2950 . . . . 5
2019, 200syl5bi 217 . . . 4
202201ralrimiv 2869 . . 3
203 rdgfun 7101 . . . . . . . . 9
204 omex 8081 . . . . . . . . 9
205 resfunexg 6137 . . . . . . . . 9