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

Theorem fpwwe2 9042
Description: Given any function from well-orderings of subsets of to , there is a unique well-ordered subset which "agrees" with in the sense that each initial segment maps to its upper bound, and such that the entire set maps to an element of the set (so that it cannot be extended without losing the well-ordering). This theorem can be used to prove dfac8a 8432. Theorem 1.1 of [KanamoriPincus] p. 415. (Contributed by Mario Carneiro, 18-May-2015.)
Hypotheses
Ref Expression
fpwwe2.1
fpwwe2.2
fpwwe2.3
fpwwe2.4
Assertion
Ref Expression
fpwwe2
Distinct variable groups:   , , , ,   , , , ,   , , , ,   , ,   , , , ,   , , , ,   , , , ,

Proof of Theorem fpwwe2
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fpwwe2.1 . . . . . . . . . . 11
2 fpwwe2.2 . . . . . . . . . . 11
3 fpwwe2.3 . . . . . . . . . . 11
4 fpwwe2.4 . . . . . . . . . . 11
51, 2, 3, 4fpwwe2lem11 9039 . . . . . . . . . 10
6 ffun 5738 . . . . . . . . . 10
75, 6syl 16 . . . . . . . . 9
8 funbrfv2b 5917 . . . . . . . . 9
97, 8syl 16 . . . . . . . 8
109simprbda 623 . . . . . . 7
1110adantrr 716 . . . . . 6
12 elssuni 4279 . . . . . . 7
1312, 4syl6sseqr 3550 . . . . . 6
1411, 13syl 16 . . . . 5
15 simpl 457 . . . . . . 7
1615a1i 11 . . . . . 6
17 simplrr 762 . . . . . . . . 9
182adantr 465 . . . . . . . . . . . . . . 15
1918adantr 465 . . . . . . . . . . . . . 14
201, 2, 3, 4fpwwe2lem12 9040 . . . . . . . . . . . . . . . . . . 19
21 funfvbrb 6000 . . . . . . . . . . . . . . . . . . . 20
227, 21syl 16 . . . . . . . . . . . . . . . . . . 19
2320, 22mpbid 210 . . . . . . . . . . . . . . . . . 18
241, 2fpwwe2lem2 9031 . . . . . . . . . . . . . . . . . 18
2523, 24mpbid 210 . . . . . . . . . . . . . . . . 17
2625ad2antrr 725 . . . . . . . . . . . . . . . 16
2726simpld 459 . . . . . . . . . . . . . . 15
2827simpld 459 . . . . . . . . . . . . . 14
2919, 28ssexd 4599 . . . . . . . . . . . . 13
30 difexg 4600 . . . . . . . . . . . . 13
3129, 30syl 16 . . . . . . . . . . . 12
3226simprd 463 . . . . . . . . . . . . . 14
3332simpld 459 . . . . . . . . . . . . 13
34 wefr 4874 . . . . . . . . . . . . 13
3533, 34syl 16 . . . . . . . . . . . 12
36 difssd 3631 . . . . . . . . . . . 12
37 fri 4846 . . . . . . . . . . . . 13
3837expr 615 . . . . . . . . . . . 12
3931, 35, 36, 38syl21anc 1227 . . . . . . . . . . 11
40 ssdif0 3885 . . . . . . . . . . . . . . 15
41 indif1 3741 . . . . . . . . . . . . . . . 16
4241eqeq1i 2464 . . . . . . . . . . . . . . 15
43 disj 3867 . . . . . . . . . . . . . . . 16
44 vex 3112 . . . . . . . . . . . . . . . . . . 19
45 vex 3112 . . . . . . . . . . . . . . . . . . . 20
4645eliniseg 5371 . . . . . . . . . . . . . . . . . . 19
4744, 46ax-mp 5 . . . . . . . . . . . . . . . . . 18
4847notbii 296 . . . . . . . . . . . . . . . . 17
4948ralbii 2888 . . . . . . . . . . . . . . . 16
5043, 49bitri 249 . . . . . . . . . . . . . . 15
5140, 42, 503bitr2i 273 . . . . . . . . . . . . . 14
52 cnvimass 5362 . . . . . . . . . . . . . . . . 17
5327simprd 463 . . . . . . . . . . . . . . . . . . 19
54 dmss 5207 . . . . . . . . . . . . . . . . . . 19
5553, 54syl 16 . . . . . . . . . . . . . . . . . 18
56 dmxpid 5227 . . . . . . . . . . . . . . . . . 18
5755, 56syl6sseq 3549 . . . . . . . . . . . . . . . . 17
5852, 57syl5ss 3514 . . . . . . . . . . . . . . . 16
59 dfss1 3702 . . . . . . . . . . . . . . . 16
6058, 59sylib 196 . . . . . . . . . . . . . . 15
6160sseq1d 3530 . . . . . . . . . . . . . 14
6251, 61syl5bbr 259 . . . . . . . . . . . . 13
6362rexbidv 2968 . . . . . . . . . . . 12
64 eldifn 3626 . . . . . . . . . . . . . . . . . . . . . . . . 25
6564ad2antrl 727 . . . . . . . . . . . . . . . . . . . . . . . 24
66 eleq1 2529 . . . . . . . . . . . . . . . . . . . . . . . . 25
6766notbid 294 . . . . . . . . . . . . . . . . . . . . . . . 24
6865, 67syl5ibrcom 222 . . . . . . . . . . . . . . . . . . . . . . 23
6968con2d 115 . . . . . . . . . . . . . . . . . . . . . 22
7069imp 429 . . . . . . . . . . . . . . . . . . . . 21
7165adantr 465 . . . . . . . . . . . . . . . . . . . . . 22
72 simprr 757 . . . . . . . . . . . . . . . . . . . . . . . . . 26
7372ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . 25
7473breqd 4463 . . . . . . . . . . . . . . . . . . . . . . . 24
75 eldifi 3625 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
7675ad2antrl 727 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
7776adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . 26
78 simpr 461 . . . . . . . . . . . . . . . . . . . . . . . . . 26
79 brxp 5035 . . . . . . . . . . . . . . . . . . . . . . . . . 26
8077, 78, 79sylanbrc 664 . . . . . . . . . . . . . . . . . . . . . . . . 25
81 brin 4501 . . . . . . . . . . . . . . . . . . . . . . . . . 26
8281rbaib 906 . . . . . . . . . . . . . . . . . . . . . . . . 25
8380, 82syl 16 . . . . . . . . . . . . . . . . . . . . . . . 24
8474, 83bitrd 253 . . . . . . . . . . . . . . . . . . . . . . 23
851, 2fpwwe2lem2 9031 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
8685biimpa 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
8786adantrr 716 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
8887simpld 459 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
8988simprd 463 . . . . . . . . . . . . . . . . . . . . . . . . . 26
9089ad3antrrr 729 . . . . . . . . . . . . . . . . . . . . . . . . 25
9190ssbrd 4493 . . . . . . . . . . . . . . . . . . . . . . . 24
92 brxp 5035 . . . . . . . . . . . . . . . . . . . . . . . . 25
9392simplbi 460 . . . . . . . . . . . . . . . . . . . . . . . 24
9491, 93syl6 33 . . . . . . . . . . . . . . . . . . . . . . 23
9584, 94sylbird 235 . . . . . . . . . . . . . . . . . . . . . 22
9671, 95mtod 177 . . . . . . . . . . . . . . . . . . . . 21
9733ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . 23
98 weso 4875 . . . . . . . . . . . . . . . . . . . . . . 23
9997, 98syl 16 . . . . . . . . . . . . . . . . . . . . . 22
10014ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . 23
101100sselda 3503 . . . . . . . . . . . . . . . . . . . . . 22
102 sotric 4831 . . . . . . . . . . . . . . . . . . . . . . 23
103 ioran 490 . . . . . . . . . . . . . . . . . . . . . . 23
104102, 103syl6bb 261 . . . . . . . . . . . . . . . . . . . . . 22
10599, 101, 77, 104syl12anc 1226 . . . . . . . . . . . . . . . . . . . . 21
10670, 96, 105mpbir2and 922 . . . . . . . . . . . . . . . . . . . 20
107106, 47sylibr 212 . . . . . . . . . . . . . . . . . . 19
108107ex 434 . . . . . . . . . . . . . . . . . 18
109108ssrdv 3509 . . . . . . . . . . . . . . . . 17
110 simprr 757 . . . . . . . . . . . . . . . . 17
111109, 110eqssd 3520 . . . . . . . . . . . . . . . 16
112 in32 3709 . . . . . . . . . . . . . . . . . 18
113 simplrr 762 . . . . . . . . . . . . . . . . . . . 20
114113ineq1d 3698 . . . . . . . . . . . . . . . . . . 19
11589ad2antrr 725 . . . . . . . . . . . . . . . . . . . 20
116 df-ss 3489 . . . . . . . . . . . . . . . . . . . 20
117115, 116sylib 196 . . . . . . . . . . . . . . . . . . 19
118114, 117eqtr3d 2500 . . . . . . . . . . . . . . . . . 18
119 inss2 3718 . . . . . . . . . . . . . . . . . . . 20
120 xpss1 5116 . . . . . . . . . . . . . . . . . . . . 21
121100, 120syl 16 . . . . . . . . . . . . . . . . . . . 20
122119, 121syl5ss 3514 . . . . . . . . . . . . . . . . . . 19
123 df-ss 3489 . . . . . . . . . . . . . . . . . . 19
124122, 123sylib 196 . . . . . . . . . . . . . . . . . 18
125112, 118, 1243eqtr3a 2522 . . . . . . . . . . . . . . . . 17
126111sqxpeqd 5030 . . . . . . . . . . . . . . . . . 18
127126ineq2d 3699 . . . . . . . . . . . . . . . . 17
128125, 127eqtrd 2498 . . . . . . . . . . . . . . . 16
129111, 128oveq12d 6314 . . . . . . . . . . . . . . 15
13019adantr 465 . . . . . . . . . . . . . . . . 17
13123adantr 465 . . . . . . . . . . . . . . . . . 18
132131ad2antrr 725 . . . . . . . . . . . . . . . . 17
1331, 130, 132fpwwe2lem3 9032 . . . . . . . . . . . . . . . 16
13476, 133mpdan 668 . . . . . . . . . . . . . . 15
135129, 134eqtrd 2498 . . . . . . . . . . . . . 14
136135, 65eqneltrd 2566 . . . . . . . . . . . . 13
137136rexlimdvaa 2950 . . . . . . . . . . . 12
13863, 137sylbid 215 . . . . . . . . . . 11
13939, 138syld 44 . . . . . . . . . 10
140139necon4ad 2677 . . . . . . . . 9
14117, 140mpd 15 . . . . . . . 8
142 ssdif0 3885 . . . . . . . 8
143141, 142sylibr 212 . . . . . . 7