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

Theorem omxpenlem 7201
 Description: Lemma for omxpen 7202. (Contributed by Mario Carneiro, 3-Mar-2013.) (Revised by Mario Carneiro, 25-May-2015.)
Hypothesis
Ref Expression
omxpenlem.1
Assertion
Ref Expression
omxpenlem
Distinct variable groups:   ,,   ,,
Allowed substitution hints:   (,)

Proof of Theorem omxpenlem
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eloni 4583 . . . . . . . . 9
21ad2antlr 708 . . . . . . . 8
3 simprl 733 . . . . . . . 8
4 ordsucss 4790 . . . . . . . 8
52, 3, 4sylc 58 . . . . . . 7
6 onelon 4598 . . . . . . . . . 10
76ad2ant2lr 729 . . . . . . . . 9
8 suceloni 4785 . . . . . . . . 9
97, 8syl 16 . . . . . . . 8
10 simplr 732 . . . . . . . 8
11 simpll 731 . . . . . . . 8
12 omwordi 6806 . . . . . . . 8
139, 10, 11, 12syl3anc 1184 . . . . . . 7
145, 13mpd 15 . . . . . 6
15 simprr 734 . . . . . . . 8
16 onelon 4598 . . . . . . . . . 10
1716ad2ant2rl 730 . . . . . . . . 9
18 omcl 6772 . . . . . . . . . 10
1911, 7, 18syl2anc 643 . . . . . . . . 9
20 oaord 6782 . . . . . . . . 9
2117, 11, 19, 20syl3anc 1184 . . . . . . . 8
2215, 21mpbid 202 . . . . . . 7
23 omsuc 6762 . . . . . . . 8
2411, 7, 23syl2anc 643 . . . . . . 7
2522, 24eleqtrrd 2512 . . . . . 6
2614, 25sseldd 3341 . . . . 5
2726ralrimivva 2790 . . . 4
28 omxpenlem.1 . . . . 5
2928fmpt2 6410 . . . 4
3027, 29sylib 189 . . 3
31 ffn 5583 . . 3
3230, 31syl 16 . 2
33 simpll 731 . . . . . . 7
34 omcl 6772 . . . . . . . 8
35 onelon 4598 . . . . . . . 8
3634, 35sylan 458 . . . . . . 7
37 noel 3624 . . . . . . . . . . . 12
38 oveq1 6080 . . . . . . . . . . . . . 14
39 om0r 6775 . . . . . . . . . . . . . 14
4038, 39sylan9eqr 2489 . . . . . . . . . . . . 13
4140eleq2d 2502 . . . . . . . . . . . 12
4237, 41mtbiri 295 . . . . . . . . . . 11
4342ex 424 . . . . . . . . . 10
4443necon2ad 2646 . . . . . . . . 9
4544adantl 453 . . . . . . . 8
4645imp 419 . . . . . . 7
47 omeu 6820 . . . . . . 7
4833, 36, 46, 47syl3anc 1184 . . . . . 6
49 vex 2951 . . . . . . . . 9
50 vex 2951 . . . . . . . . 9
5149, 50brcnv 5047 . . . . . . . 8
52 eleq1 2495 . . . . . . . . . . . . . . . . 17
5352biimpac 473 . . . . . . . . . . . . . . . 16
546ex 424 . . . . . . . . . . . . . . . . . . . 20
5554ad2antlr 708 . . . . . . . . . . . . . . . . . . 19
56 simplll 735 . . . . . . . . . . . . . . . . . . . . . . . 24
57 simpr 448 . . . . . . . . . . . . . . . . . . . . . . . 24
5856, 57, 18syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . 23
59 simplrr 738 . . . . . . . . . . . . . . . . . . . . . . . 24
6056, 59, 16syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . 23
61 oaword1 6787 . . . . . . . . . . . . . . . . . . . . . . 23
6258, 60, 61syl2anc 643 . . . . . . . . . . . . . . . . . . . . . 22
63 simplrl 737 . . . . . . . . . . . . . . . . . . . . . 22
6434ad2antrr 707 . . . . . . . . . . . . . . . . . . . . . . 23
65 ontr2 4620 . . . . . . . . . . . . . . . . . . . . . . 23
6658, 64, 65syl2anc 643 . . . . . . . . . . . . . . . . . . . . . 22
6762, 63, 66mp2and 661 . . . . . . . . . . . . . . . . . . . . 21
68 simpllr 736 . . . . . . . . . . . . . . . . . . . . . 22
69 ne0i 3626 . . . . . . . . . . . . . . . . . . . . . . . . . 26
7063, 69syl 16 . . . . . . . . . . . . . . . . . . . . . . . . 25
71 on0eln0 4628 . . . . . . . . . . . . . . . . . . . . . . . . . 26
7264, 71syl 16 . . . . . . . . . . . . . . . . . . . . . . . . 25
7370, 72mpbird 224 . . . . . . . . . . . . . . . . . . . . . . . 24
74 om00el 6811 . . . . . . . . . . . . . . . . . . . . . . . . 25
7574ad2antrr 707 . . . . . . . . . . . . . . . . . . . . . . . 24
7673, 75mpbid 202 . . . . . . . . . . . . . . . . . . . . . . 23
7776simpld 446 . . . . . . . . . . . . . . . . . . . . . 22
78 omord2 6802 . . . . . . . . . . . . . . . . . . . . . 22
7957, 68, 56, 77, 78syl31anc 1187 . . . . . . . . . . . . . . . . . . . . 21
8067, 79mpbird 224 . . . . . . . . . . . . . . . . . . . 20
8180ex 424 . . . . . . . . . . . . . . . . . . 19
8255, 81impbid 184 . . . . . . . . . . . . . . . . . 18
8382expr 599 . . . . . . . . . . . . . . . . 17
8483pm5.32rd 622 . . . . . . . . . . . . . . . 16
8553, 84sylan2 461 . . . . . . . . . . . . . . 15
8685expr 599 . . . . . . . . . . . . . 14
8786pm5.32rd 622 . . . . . . . . . . . . 13
88 eqcom 2437 . . . . . . . . . . . . . 14
8988anbi2i 676 . . . . . . . . . . . . 13
9087, 89syl6bb 253 . . . . . . . . . . . 12
9190anbi2d 685 . . . . . . . . . . 11
92 an12 773 . . . . . . . . . . 11
9391, 92syl6bb 253 . . . . . . . . . 10
94932exbidv 1638 . . . . . . . . 9
95 df-mpt2 6078 . . . . . . . . . . . 12
96 dfoprab2 6113 . . . . . . . . . . . 12
9728, 95, 963eqtri 2459 . . . . . . . . . . 11
9897breqi 4210 . . . . . . . . . 10
99 df-br 4205 . . . . . . . . . 10
100 opabid 4453 . . . . . . . . . 10
10198, 99, 1003bitri 263 . . . . . . . . 9
102 r2ex 2735 . . . . . . . . 9
10394, 101, 1023bitr4g 280 . . . . . . . 8
10451, 103syl5bb 249 . . . . . . 7
105104eubidv 2288 . . . . . 6
10648, 105mpbird 224 . . . . 5
107106ralrimiva 2781 . . . 4
108 fnres 5553 . . . 4
109107, 108sylibr 204 . . 3
110 relcnv 5234 . . . . 5
111 df-rn 4881 . . . . . 6
112 frn 5589 . . . . . . 7
11330, 112syl 16 . . . . . 6
114111, 113syl5eqssr 3385 . . . . 5
115 relssres 5175 . . . . 5
116110, 114, 115sylancr 645 . . . 4
117116fneq1d 5528 . . 3
118109, 117mpbid 202 . 2
119 dff1o4 5674 . 2
12032, 118, 119sylanbrc 646 1
 Colors of variables: wff set class Syntax hints:   wn 3   wi 4   wb 177   wa 359  wex 1550   wceq 1652   wcel 1725  weu 2280   wne 2598  wral 2697  wrex 2698   wss 3312  c0 3620  cop 3809   class class class wbr 4204  copab 4257   word 4572  con0 4573   csuc 4575   cxp 4868  ccnv 4869   cdm 4870   crn 4871   cres 4872   wrel 4875   wfn 5441  wf 5442  wf1o 5445  (class class class)co 6073  coprab 6074   cmpt2 6075   coa 6713   comu 6714 This theorem is referenced by:  omxpen  7202  omf1o  7203  infxpenc  7891 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-13 1727  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416  ax-rep 4312  ax-sep 4322  ax-nul 4330  ax-pow 4369  ax-pr 4395  ax-un 4693 This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2284  df-mo 2285  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-ral 2702  df-rex 2703  df-reu 2704  df-rmo 2705  df-rab 2706  df-v 2950  df-sbc 3154  df-csb 3244  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-pss 3328  df-nul 3621  df-if 3732  df-pw 3793  df-sn 3812  df-pr 3813  df-tp 3814  df-op 3815  df-uni 4008  df-int 4043  df-iun 4087  df-br 4205  df-opab 4259  df-mpt 4260  df-tr 4295  df-eprel 4486  df-id 4490  df-po 4495  df-so 4496  df-fr 4533  df-we 4535  df-ord 4576  df-on 4577  df-lim 4578  df-suc 4579  df-om 4838  df-xp 4876  df-rel 4877  df-cnv 4878  df-co 4879  df-dm 4880  df-rn 4881  df-res 4882  df-ima 4883  df-iota 5410  df-fun 5448  df-fn 5449  df-f 5450  df-f1 5451  df-fo 5452  df-f1o 5453  df-fv 5454  df-ov 6076  df-oprab 6077  df-mpt2 6078  df-1st 6341  df-2nd 6342  df-recs 6625  df-rdg 6660  df-1o 6716  df-oadd 6720  df-omul 6721
 Copyright terms: Public domain W3C validator