Step Hyp Ref
Expression 1 fpwwe2.1 . . . . . . . . . . 11
2 fpwwe2.2 . . . . . . . . . . 11
3 fpwwe2.3 . . . . . . . . . . 11
4 fpwwe2.4 . . . . . . . . . . 11
5 1 , 2 , 3 , 4 fpwwe2lem11 9039 . . . . . . . . . 10
6 ffun 5738 . . . . . . . . . 10
7 5 , 6 syl 16 . . . . . . . . 9
8 funbrfv2b 5917 . . . . . . . . 9
9 7 , 8 syl 16 . . . . . . . 8
10 9 simprbda 623 . . . . . . 7
11 10 adantrr 716 . . . . . 6
12 elssuni 4279 . . . . . . 7
13 12 , 4 syl6sseqr 3550 . . . . . 6
14 11 , 13 syl 16 . . . . 5
15 simpl 457 . . . . . . 7
16 15 a1i 11 . . . . . 6
17 simplrr 762 . . . . . . . . 9
18 2 adantr 465 . . . . . . . . . . . . . . 15
19 18 adantr 465 . . . . . . . . . . . . . 14
20 1 , 2 , 3 , 4 fpwwe2lem12 9040 . . . . . . . . . . . . . . . . . . 19
21 funfvbrb 6000 . . . . . . . . . . . . . . . . . . . 20
22 7 , 21 syl 16 . . . . . . . . . . . . . . . . . . 19
23 20 , 22 mpbid 210 . . . . . . . . . . . . . . . . . 18
24 1 , 2 fpwwe2lem2 9031 . . . . . . . . . . . . . . . . . 18
25 23 , 24 mpbid 210 . . . . . . . . . . . . . . . . 17
26 25 ad2antrr 725 . . . . . . . . . . . . . . . 16
27 26 simpld 459 . . . . . . . . . . . . . . 15
28 27 simpld 459 . . . . . . . . . . . . . 14
29 19 , 28 ssexd 4599 . . . . . . . . . . . . 13
30 difexg 4600 . . . . . . . . . . . . 13
31 29 , 30 syl 16 . . . . . . . . . . . 12
32 26 simprd 463 . . . . . . . . . . . . . 14
33 32 simpld 459 . . . . . . . . . . . . 13
34 wefr 4874 . . . . . . . . . . . . 13
35 33 , 34 syl 16 . . . . . . . . . . . 12
36 difssd 3631 . . . . . . . . . . . 12
37 fri 4846 . . . . . . . . . . . . 13
38 37 expr 615 . . . . . . . . . . . 12
39 31 , 35 , 36 , 38 syl21anc 1227 . . . . . . . . . . 11
40 ssdif0 3885 . . . . . . . . . . . . . . 15
41 indif1 3741 . . . . . . . . . . . . . . . 16
42 41 eqeq1i 2464 . . . . . . . . . . . . . . 15
43 disj 3867 . . . . . . . . . . . . . . . 16
44 vex 3112 . . . . . . . . . . . . . . . . . . 19
45 vex 3112 . . . . . . . . . . . . . . . . . . . 20
46 45 eliniseg 5371 . . . . . . . . . . . . . . . . . . 19
47 44 , 46 ax-mp 5 . . . . . . . . . . . . . . . . . 18
48 47 notbii 296 . . . . . . . . . . . . . . . . 17
49 48 ralbii 2888 . . . . . . . . . . . . . . . 16
50 43 , 49 bitri 249 . . . . . . . . . . . . . . 15
51 40 , 42 , 50 3bitr2i 273 . . . . . . . . . . . . . 14
52 cnvimass 5362 . . . . . . . . . . . . . . . . 17
53 27 simprd 463 . . . . . . . . . . . . . . . . . . 19
54 dmss 5207 . . . . . . . . . . . . . . . . . . 19
55 53 , 54 syl 16 . . . . . . . . . . . . . . . . . 18
56 dmxpid 5227 . . . . . . . . . . . . . . . . . 18
57 55 , 56 syl6sseq 3549 . . . . . . . . . . . . . . . . 17
58 52 , 57 syl5ss 3514 . . . . . . . . . . . . . . . 16
59 dfss1 3702 . . . . . . . . . . . . . . . 16
60 58 , 59 sylib 196 . . . . . . . . . . . . . . 15
61 60 sseq1d 3530 . . . . . . . . . . . . . 14
62 51 , 61 syl5bbr 259 . . . . . . . . . . . . 13
63 62 rexbidv 2968 . . . . . . . . . . . 12
64 eldifn 3626 . . . . . . . . . . . . . . . . . . . . . . . . 25
65 64 ad2antrl 727 . . . . . . . . . . . . . . . . . . . . . . . 24
66 eleq1 2529 . . . . . . . . . . . . . . . . . . . . . . . . 25
67 66 notbid 294 . . . . . . . . . . . . . . . . . . . . . . . 24
68 65 , 67 syl5ibrcom 222 . . . . . . . . . . . . . . . . . . . . . . 23
69 68 con2d 115 . . . . . . . . . . . . . . . . . . . . . 22
70 69 imp 429 . . . . . . . . . . . . . . . . . . . . 21
71 65 adantr 465 . . . . . . . . . . . . . . . . . . . . . 22
72 simprr 757 . . . . . . . . . . . . . . . . . . . . . . . . . 26
73 72 ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . 25
74 73 breqd 4463 . . . . . . . . . . . . . . . . . . . . . . . 24
75 eldifi 3625 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
76 75 ad2antrl 727 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
77 76 adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . 26
78 simpr 461 . . . . . . . . . . . . . . . . . . . . . . . . . 26
79 brxp 5035 . . . . . . . . . . . . . . . . . . . . . . . . . 26
80 77 , 78 , 79 sylanbrc 664 . . . . . . . . . . . . . . . . . . . . . . . . 25
81 brin 4501 . . . . . . . . . . . . . . . . . . . . . . . . . 26
82 81 rbaib 906 . . . . . . . . . . . . . . . . . . . . . . . . 25
83 80 , 82 syl 16 . . . . . . . . . . . . . . . . . . . . . . . 24
84 74 , 83 bitrd 253 . . . . . . . . . . . . . . . . . . . . . . 23
85 1 , 2 fpwwe2lem2 9031 . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
86 85 biimpa 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
87 86 adantrr 716 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
88 87 simpld 459 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
89 88 simprd 463 . . . . . . . . . . . . . . . . . . . . . . . . . 26
90 89 ad3antrrr 729 . . . . . . . . . . . . . . . . . . . . . . . . 25
91 90 ssbrd 4493 . . . . . . . . . . . . . . . . . . . . . . . 24
92 brxp 5035 . . . . . . . . . . . . . . . . . . . . . . . . 25
93 92 simplbi 460 . . . . . . . . . . . . . . . . . . . . . . . 24
94 91 , 93 syl6 33 . . . . . . . . . . . . . . . . . . . . . . 23
95 84 , 94 sylbird 235 . . . . . . . . . . . . . . . . . . . . . 22
96 71 , 95 mtod 177 . . . . . . . . . . . . . . . . . . . . 21
97 33 ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . 23
98 weso 4875 . . . . . . . . . . . . . . . . . . . . . . 23
99 97 , 98 syl 16 . . . . . . . . . . . . . . . . . . . . . 22
100 14 ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . 23
101 100 sselda 3503 . . . . . . . . . . . . . . . . . . . . . 22
102 sotric 4831 . . . . . . . . . . . . . . . . . . . . . . 23
103 ioran 490 . . . . . . . . . . . . . . . . . . . . . . 23
104 102 , 103 syl6bb 261 . . . . . . . . . . . . . . . . . . . . . 22
105 99 , 101 , 77 , 104 syl12anc 1226 . . . . . . . . . . . . . . . . . . . . 21
106 70 , 96 , 105 mpbir2and 922 . . . . . . . . . . . . . . . . . . . 20
107 106 , 47 sylibr 212 . . . . . . . . . . . . . . . . . . 19
108 107 ex 434 . . . . . . . . . . . . . . . . . 18
109 108 ssrdv 3509 . . . . . . . . . . . . . . . . 17
110 simprr 757 . . . . . . . . . . . . . . . . 17
111 109 , 110 eqssd 3520 . . . . . . . . . . . . . . . 16
112 in32 3709 . . . . . . . . . . . . . . . . . 18
113 simplrr 762 . . . . . . . . . . . . . . . . . . . 20
114 113 ineq1d 3698 . . . . . . . . . . . . . . . . . . 19
115 89 ad2antrr 725 . . . . . . . . . . . . . . . . . . . 20
116 df-ss 3489 . . . . . . . . . . . . . . . . . . . 20
117 115 , 116 sylib 196 . . . . . . . . . . . . . . . . . . 19
118 114 , 117 eqtr3d 2500 . . . . . . . . . . . . . . . . . 18
119 inss2 3718 . . . . . . . . . . . . . . . . . . . 20
120 xpss1 5116 . . . . . . . . . . . . . . . . . . . . 21
121 100 , 120 syl 16 . . . . . . . . . . . . . . . . . . . 20
122 119 , 121 syl5ss 3514 . . . . . . . . . . . . . . . . . . 19
123 df-ss 3489 . . . . . . . . . . . . . . . . . . 19
124 122 , 123 sylib 196 . . . . . . . . . . . . . . . . . 18
125 112 , 118 ,
124 3eqtr3a 2522 . . . . . . . . . . . . . . . . 17
126 111 sqxpeqd 5030 . . . . . . . . . . . . . . . . . 18
127 126 ineq2d 3699 . . . . . . . . . . . . . . . . 17
128 125 , 127 eqtrd 2498 . . . . . . . . . . . . . . . 16
129 111 , 128 oveq12d 6314 . . . . . . . . . . . . . . 15
130 19 adantr 465 . . . . . . . . . . . . . . . . 17
131 23 adantr 465 . . . . . . . . . . . . . . . . . 18
132 131 ad2antrr 725 . . . . . . . . . . . . . . . . 17
133 1 , 130 , 132 fpwwe2lem3 9032 . . . . . . . . . . . . . . . 16
134 76 , 133 mpdan 668 . . . . . . . . . . . . . . 15
135 129 , 134 eqtrd 2498 . . . . . . . . . . . . . 14
136 135 , 65 eqneltrd 2566 . . . . . . . . . . . . 13
137 136 rexlimdvaa 2950 . . . . . . . . . . . 12
138 63 , 137 sylbid 215 . . . . . . . . . . 11
139 39 , 138 syld 44 . . . . . . . . . 10
140 139 necon4ad 2677 . . . . . . . . 9
141 17 , 140 mpd 15 . . . . . . . 8
142 ssdif0 3885 . . . . . . . 8
143 141 , 142 sylibr 212 . . . . . . 7
