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

Theorem fpwwe2lem12 9040
Description: Lemma for fpwwe2 9042. (Contributed by Mario Carneiro, 18-May-2015.)
Hypotheses
Ref Expression
fpwwe2.1
fpwwe2.2
fpwwe2.3
fpwwe2.4
Assertion
Ref Expression
fpwwe2lem12
Distinct variable groups:   , , , ,   , , , ,   , , , ,   , ,   , , , ,

Proof of Theorem fpwwe2lem12
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fpwwe2.4 . . . . 5
2 vex 3112 . . . . . . . . 9
32eldm 5205 . . . . . . . 8
4 fpwwe2.1 . . . . . . . . . . . . . 14
5 fpwwe2.2 . . . . . . . . . . . . . 14
64, 5fpwwe2lem2 9031 . . . . . . . . . . . . 13
76simprbda 623 . . . . . . . . . . . 12
87simpld 459 . . . . . . . . . . 11
9 selpw 4019 . . . . . . . . . . 11
108, 9sylibr 212 . . . . . . . . . 10
1110ex 434 . . . . . . . . 9
1211exlimdv 1724 . . . . . . . 8
133, 12syl5bi 217 . . . . . . 7
1413ssrdv 3509 . . . . . 6
15 sspwuni 4416 . . . . . 6
1614, 15sylib 196 . . . . 5
171, 16syl5eqss 3547 . . . 4
18 vex 3112 . . . . . . . 8
1918elrn 5248 . . . . . . 7
207simprd 463 . . . . . . . . . . 11
214relopabi 5133 . . . . . . . . . . . . . . . 16
2221releldmi 5244 . . . . . . . . . . . . . . 15
2322adantl 466 . . . . . . . . . . . . . 14
24 elssuni 4279 . . . . . . . . . . . . . 14
2523, 24syl 16 . . . . . . . . . . . . 13
2625, 1syl6sseqr 3550 . . . . . . . . . . . 12
27 xpss12 5113 . . . . . . . . . . . 12
2826, 26, 27syl2anc 661 . . . . . . . . . . 11
2920, 28sstrd 3513 . . . . . . . . . 10
30 selpw 4019 . . . . . . . . . 10
3129, 30sylibr 212 . . . . . . . . 9
3231ex 434 . . . . . . . 8
3332exlimdv 1724 . . . . . . 7
3419, 33syl5bi 217 . . . . . 6
3534ssrdv 3509 . . . . 5
36 sspwuni 4416 . . . . 5
3735, 36sylib 196 . . . 4
3817, 37jca 532 . . 3
39 n0 3794 . . . . . . . . 9
40 ssel2 3498 . . . . . . . . . . . . . 14
4140adantl 466 . . . . . . . . . . . . 13
421eleq2i 2535 . . . . . . . . . . . . . 14
43 eluni2 4253 . . . . . . . . . . . . . 14
4442, 43bitri 249 . . . . . . . . . . . . 13
4541, 44sylib 196 . . . . . . . . . . . 12
462inex2 4594 . . . . . . . . . . . . . . . . . . 19
4746a1i 11 . . . . . . . . . . . . . . . . . 18
486simplbda 624 . . . . . . . . . . . . . . . . . . . . 21
4948simpld 459 . . . . . . . . . . . . . . . . . . . 20
5049ad2ant2r 746 . . . . . . . . . . . . . . . . . . 19
51 wefr 4874 . . . . . . . . . . . . . . . . . . 19
5250, 51syl 16 . . . . . . . . . . . . . . . . . 18
53 inss2 3718 . . . . . . . . . . . . . . . . . . 19
5453a1i 11 . . . . . . . . . . . . . . . . . 18
55 simplrr 762 . . . . . . . . . . . . . . . . . . 19
56 simprr 757 . . . . . . . . . . . . . . . . . . 19
57 inelcm 3881 . . . . . . . . . . . . . . . . . . 19
5855, 56, 57syl2anc 661 . . . . . . . . . . . . . . . . . 18
59 fri 4846 . . . . . . . . . . . . . . . . . 18
6047, 52, 54, 58, 59syl22anc 1229 . . . . . . . . . . . . . . . . 17
61 inss1 3717 . . . . . . . . . . . . . . . . . . . . 21
62 simprl 756 . . . . . . . . . . . . . . . . . . . . 21
6361, 62sseldi 3501 . . . . . . . . . . . . . . . . . . . 20
64 simplrr 762 . . . . . . . . . . . . . . . . . . . . . . 23
65 ralnex 2903 . . . . . . . . . . . . . . . . . . . . . . 23
6664, 65sylib 196 . . . . . . . . . . . . . . . . . . . . . 22
67 df-br 4453 . . . . . . . . . . . . . . . . . . . . . . . 24
68 eluni2 4253 . . . . . . . . . . . . . . . . . . . . . . . 24
6967, 68bitri 249 . . . . . . . . . . . . . . . . . . . . . . 23
70 vex 3112 . . . . . . . . . . . . . . . . . . . . . . . . . 26
7170elrn 5248 . . . . . . . . . . . . . . . . . . . . . . . . 25
72 df-br 4453 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
73 simprll 763 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
7473adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
75 simprr 757 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
76 simp-4l 767 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
77 simprl 756 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
7877ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
79 simprlr 764 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
80 simprr 757 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
814, 5fpwwe2lem2 9031 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45
8281adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
8380, 82mpbid 210 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
8483simpld 459 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
8584simprd 463 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
8676, 78, 79, 85syl12anc 1226 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
8786ssbrd 4493 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
8875, 87mpd 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
89 brxp 5035 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
9089simplbi 460 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
9188, 90syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
9291adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
9353, 62sseldi 3501 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
9493ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
95 simplrr 762 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
96 brinxp2 5066 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
9792, 94, 95, 96syl3anbrc 1180 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
98 simprr 757 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
9998breqd 4463 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
10097, 99mpbird 232 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
10176, 78, 20syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
102101adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
103102ssbrd 4493 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
104100, 103mpd 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
105 brxp 5035 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
106105simplbi 460 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
107104, 106syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
10874, 107elind 3687 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
109 breq1 4455 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
110109rspcev 3210 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
111108, 100, 110syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
11273adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
113 simprl 756 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
11491adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
115113, 114sseldd 3504 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
116112, 115elind 3687 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
117 simplrr 762 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
118 simprr 757 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
119 inss1 3717 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
120118, 119syl6eqss 3553 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
121120ssbrd 4493 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
122117, 121mpd 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
123116, 122, 110syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
1245adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
125 fpwwe2.3 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
126125adantlr 714 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
127 simprl 756 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
1284, 124, 126, 127, 80fpwwe2lem10 9038 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
12976, 78, 79, 128syl12anc 1226 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
130111, 123, 129mpjaodan 786 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
131130expr 615 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
13272, 131syl5bir 218 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
133132expr 615 . . . . . . . . . . . . . . . . . . . . . . . . . 26
134133exlimdv 1724 . . . . . . . . . . . . . . . . . . . . . . . . 25
13571, 134syl5bi 217 . . . . . . . . . . . . . . . . . . . . . . . 24
136135rexlimdv 2947 . . . . . . . . . . . . . . . . . . . . . . 23
13769, 136syl5bi 217 . . . . . . . . . . . . . . . . . . . . . 22
13866, 137mtod 177 . . . . . . . . . . . . . . . . . . . . 21
139138ralrimiva 2871 . . . . . . . . . . . . . . . . . . . 20
14063, 139jca 532 . . . . . . . . . . . . . . . . . . 19
141140ex 434 . . . . . . . . . . . . . . . . . 18
142141reximdv2 2928 . . . . . . . . . . . . . . . . 17
14360, 142mpd 15 . . . . . . . . . . . . . . . 16
144143exp32 605 . . . . . . . . . . . . . . 15
145144exlimdv 1724 . . . . . . . . . . . . . 14
1463, 145syl5bi 217 . . . . . . . . . . . . 13
147146rexlimdv 2947 . . . . . . . . . . . 12
14845, 147mpd 15 . . . . . . . . . . 11
149148expr 615 . . . . . . . . . 10
150149exlimdv 1724 . . . . . . . . 9
15139, 150syl5bi 217 . . . . . . . 8
152151expimpd 603 . . . . . . 7
153152alrimiv 1719 . . . . . 6
154 df-fr 4843 . . . . . 6