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

Theorem fpwwe2lem9 9081
 Description: Lemma for fpwwe2 9086. Given two well-orders and of parts of , one is an initial segment of the other. (The hypothesis is in order to break the symmetry of and .) (Contributed by Mario Carneiro, 15-May-2015.)
Hypotheses
Ref Expression
fpwwe2.1
fpwwe2.2
fpwwe2.3
fpwwe2lem9.x
fpwwe2lem9.y
fpwwe2lem9.m OrdIso
fpwwe2lem9.n OrdIso
fpwwe2lem9.s
Assertion
Ref Expression
fpwwe2lem9
Distinct variable groups:   ,,,,   ,,,,   ,,,,   ,,,,   ,,,,   ,,   ,,,,   ,,,,   ,,,,   ,,,,
Allowed substitution hints:   (,)

Proof of Theorem fpwwe2lem9
StepHypRef Expression
1 fpwwe2lem9.x . . . . . . . . 9
2 fpwwe2.1 . . . . . . . . . . 11
32relopabi 4964 . . . . . . . . . 10
43brrelexi 4880 . . . . . . . . 9
51, 4syl 17 . . . . . . . 8
6 fpwwe2.2 . . . . . . . . . . . 12
72, 6fpwwe2lem2 9075 . . . . . . . . . . 11
81, 7mpbid 215 . . . . . . . . . 10
98simprd 470 . . . . . . . . 9
109simpld 466 . . . . . . . 8
11 fpwwe2lem9.m . . . . . . . . 9 OrdIso
1211oiiso 8070 . . . . . . . 8
135, 10, 12syl2anc 673 . . . . . . 7
14 isof1o 6234 . . . . . . 7
1513, 14syl 17 . . . . . 6
16 f1ofo 5835 . . . . . 6
17 forn 5809 . . . . . 6
1815, 16, 173syl 18 . . . . 5
19 fpwwe2.3 . . . . . . 7
20 fpwwe2lem9.y . . . . . . 7
21 fpwwe2lem9.n . . . . . . 7 OrdIso
22 fpwwe2lem9.s . . . . . . 7
232, 6, 19, 1, 20, 11, 21, 22fpwwe2lem8 9080 . . . . . 6
2423rneqd 5068 . . . . 5
2518, 24eqtr3d 2507 . . . 4
26 df-ima 4852 . . . 4
2725, 26syl6eqr 2523 . . 3
28 imassrn 5185 . . . 4
293brrelexi 4880 . . . . . . . 8
3020, 29syl 17 . . . . . . 7
312, 6fpwwe2lem2 9075 . . . . . . . . . 10
3220, 31mpbid 215 . . . . . . . . 9
3332simprd 470 . . . . . . . 8
3433simpld 466 . . . . . . 7
3521oiiso 8070 . . . . . . 7
3630, 34, 35syl2anc 673 . . . . . 6
37 isof1o 6234 . . . . . 6
3836, 37syl 17 . . . . 5
39 f1ofo 5835 . . . . 5
40 forn 5809 . . . . 5
4138, 39, 403syl 18 . . . 4
4228, 41syl5sseq 3466 . . 3
4327, 42eqsstrd 3452 . 2
448simpld 466 . . . . . 6
4544simprd 470 . . . . 5
46 relxp 4947 . . . . 5
47 relss 4927 . . . . 5
4845, 46, 47mpisyl 21 . . . 4
49 inss2 3644 . . . . 5
50 relxp 4947 . . . . 5
51 relss 4927 . . . . 5
5249, 50, 51mp2 9 . . . 4
5348, 52jctir 547 . . 3
5445ssbrd 4437 . . . . . . 7
55 brxp 4870 . . . . . . 7
5654, 55syl6ib 234 . . . . . 6
57 brinxp2 4901 . . . . . . . 8
58 df-3an 1009 . . . . . . . 8
5957, 58bitri 257 . . . . . . 7
60 simprll 780 . . . . . . . . . . 11
61 simprr 774 . . . . . . . . . . . . . 14
62 isocnv 6239 . . . . . . . . . . . . . . . . 17
6336, 62syl 17 . . . . . . . . . . . . . . . 16
6463adantr 472 . . . . . . . . . . . . . . 15
6543adantr 472 . . . . . . . . . . . . . . . 16
66 simprlr 781 . . . . . . . . . . . . . . . 16
6765, 66sseldd 3419 . . . . . . . . . . . . . . 15
68 isorel 6235 . . . . . . . . . . . . . . 15
6964, 60, 67, 68syl12anc 1290 . . . . . . . . . . . . . 14
7061, 69mpbid 215 . . . . . . . . . . . . 13
71 fvex 5889 . . . . . . . . . . . . . 14
7271epelc 4752 . . . . . . . . . . . . 13
7370, 72sylib 201 . . . . . . . . . . . 12
7423adantr 472 . . . . . . . . . . . . . . . . 17
7574cnveqd 5015 . . . . . . . . . . . . . . . 16
76 isof1o 6234 . . . . . . . . . . . . . . . . . 18
77 f1ofn 5829 . . . . . . . . . . . . . . . . . 18
7864, 76, 773syl 18 . . . . . . . . . . . . . . . . 17
79 fnfun 5683 . . . . . . . . . . . . . . . . 17
80 funcnvres 5662 . . . . . . . . . . . . . . . . 17
8178, 79, 803syl 18 . . . . . . . . . . . . . . . 16
8275, 81eqtrd 2505 . . . . . . . . . . . . . . 15
8382fveq1d 5881 . . . . . . . . . . . . . 14
8427adantr 472 . . . . . . . . . . . . . . . 16
8566, 84eleqtrd 2551 . . . . . . . . . . . . . . 15
86 fvres 5893 . . . . . . . . . . . . . . 15
8785, 86syl 17 . . . . . . . . . . . . . 14
8883, 87eqtrd 2505 . . . . . . . . . . . . 13
89 isocnv 6239 . . . . . . . . . . . . . . . . 17
9013, 89syl 17 . . . . . . . . . . . . . . . 16
91 isof1o 6234 . . . . . . . . . . . . . . . 16
92 f1of 5828 . . . . . . . . . . . . . . . 16
9390, 91, 923syl 18 . . . . . . . . . . . . . . 15
9493adantr 472 . . . . . . . . . . . . . 14
9594, 66ffvelrnd 6038 . . . . . . . . . . . . 13
9688, 95eqeltrrd 2550 . . . . . . . . . . . 12
9711oicl 8062 . . . . . . . . . . . . 13
98 ordtr1 5473 . . . . . . . . . . . . 13
9997, 98ax-mp 5 . . . . . . . . . . . 12
10073, 96, 99syl2anc 673 . . . . . . . . . . 11
101 elpreima 6017 . . . . . . . . . . . 12
10278, 101syl 17 . . . . . . . . . . 11
10360, 100, 102mpbir2and 936 . . . . . . . . . 10
104 imacnvcnv 5307 . . . . . . . . . . 11
10584, 104syl6eqr 2523 . . . . . . . . . 10
106103, 105eleqtrrd 2552 . . . . . . . . 9
107106, 66jca 541 . . . . . . . 8
108107ex 441 . . . . . . 7
10959, 108syl5bi 225 . . . . . 6
11023adantr 472 . . . . . . . . . . . 12
111110cnveqd 5015 . . . . . . . . . . 11
112111fveq1d 5881 . . . . . . . . . 10
113111fveq1d 5881 . . . . . . . . . 10
114112, 113breq12d 4408 . . . . . . . . 9
115 isorel 6235 . . . . . . . . . 10
11690, 115sylan 479 . . . . . . . . 9
117 eqidd 2472 . . . . . . . . . . . . 13
118 isores3 6244 . . . . . . . . . . . . 13
11936, 22, 117, 118syl3anc 1292 . . . . . . . . . . . 12
120 isocnv 6239 . . . . . . . . . . . 12
121119, 120syl 17 . . . . . . . . . . 11
122121adantr 472 . . . . . . . . . 10
123 simprl 772 . . . . . . . . . . 11
12427adantr 472 . . . . . . . . . . 11
125123, 124eleqtrd 2551 . . . . . . . . . 10
126 simprr 774 . . . . . . . . . . 11
127126, 124eleqtrd 2551 . . . . . . . . . 10
128 isorel 6235 . . . . . . . . . 10
129122, 125, 127, 128syl12anc 1290 . . . . . . . . 9
130114, 116, 1293bitr4d 293 . . . . . . . 8
13143sselda 3418 . . . . . . . . . . . 12
132131adantrr 731 . . . . . . . . . . 11
133132, 126jca 541 . . . . . . . . . 10
134133biantrurd 516 . . . . . . . . 9
135134, 59syl6bbr 271 . . . . . . . 8
136130, 135bitrd 261 . . . . . . 7
137136ex 441 . . . . . 6
13856, 109, 137pm5.21ndd 361 . . . . 5
139 df-br 4396 . . . . 5
140 df-br 4396 . . . . 5
141138, 139, 1403bitr3g 295 . . . 4
142141eqrelrdv2 4939 . . 3
14353, 142mpancom 682 . 2
14443, 143jca 541 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 189   wa 376   w3a 1007   wceq 1452   wcel 1904  wral 2756  cvv 3031  wsbc 3255   cin 3389   wss 3390  csn 3959  cop 3965   class class class wbr 4395  copab 4453   cep 4748   wwe 4797   cxp 4837  ccnv 4838   cdm 4839   crn 4840   cres 4841  cima 4842   wrel 4844   word 5429   wfun 5583   wfn 5584  wf 5585  wfo 5587  wf1o 5588  cfv 5589   wiso 5590  (class class class)co 6308  OrdIsocoi 8042 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-8 1906  ax-9 1913  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-rep 4508  ax-sep 4518  ax-nul 4527  ax-pow 4579  ax-pr 4639  ax-un 6602 This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3or 1008  df-3an 1009  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-eu 2323  df-mo 2324  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ne 2643  df-ral 2761  df-rex 2762  df-reu 2763  df-rmo 2764  df-rab 2765  df-v 3033  df-sbc 3256  df-csb 3350  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-pss 3406  df-nul 3723  df-if 3873  df-pw 3944  df-sn 3960  df-pr 3962  df-tp 3964  df-op 3966  df-uni 4191  df-iun 4271  df-br 4396  df-opab 4455  df-mpt 4456  df-tr 4491  df-eprel 4750  df-id 4754  df-po 4760  df-so 4761  df-fr 4798  df-se 4799  df-we 4800  df-xp 4845  df-rel 4846  df-cnv 4847  df-co 4848  df-dm 4849  df-rn 4850  df-res 4851  df-ima 4852  df-pred 5387  df-ord 5433  df-on 5434  df-lim 5435  df-suc 5436  df-iota 5553  df-fun 5591  df-fn 5592  df-f 5593  df-f1 5594  df-fo 5595  df-f1o 5596  df-fv 5597  df-isom 5598  df-riota 6270  df-ov 6311  df-wrecs 7046  df-recs 7108  df-oi 8043 This theorem is referenced by:  fpwwe2lem10  9082
 Copyright terms: Public domain W3C validator