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

Theorem pmltpclem2 22151
 Description: Lemma for pmltpc 22152. (Contributed by Mario Carneiro, 1-Jul-2014.)
Hypotheses
Ref Expression
pmltpc.1
pmltpc.2
pmltpc.3
pmltpc.4
pmltpc.5
pmltpc.6
pmltpc.7
pmltpc.8
pmltpc.9
pmltpc.10
Assertion
Ref Expression
pmltpclem2
Distinct variable groups:   ,,,   ,,,   ,,   ,,,   ,,,   ,,
Allowed substitution hints:   (,,)   ()   ()

Proof of Theorem pmltpclem2
StepHypRef Expression
1 pmltpc.5 . . . . 5
21ad2antrr 724 . . . 4
3 pmltpc.3 . . . . 5
43ad2antrr 724 . . . 4
5 pmltpc.4 . . . . 5
65ad2antrr 724 . . . 4
7 simpr 459 . . . 4
8 pmltpc.1 . . . . . . . . . . 11
9 reex 9612 . . . . . . . . . . . 12
109, 9elpm2 7487 . . . . . . . . . . 11
118, 10sylib 196 . . . . . . . . . 10
1211simpld 457 . . . . . . . . 9
13 pmltpc.2 . . . . . . . . . 10
1413, 5sseldd 3442 . . . . . . . . 9
1512, 14ffvelrnd 6009 . . . . . . . 8
16 pmltpc.9 . . . . . . . . 9
1713, 3sseldd 3442 . . . . . . . . . . 11
1812, 17ffvelrnd 6009 . . . . . . . . . 10
1915, 18ltnled 9763 . . . . . . . . 9
2016, 19mpbird 232 . . . . . . . 8
2115, 20gtned 9751 . . . . . . 7
22 fveq2 5848 . . . . . . . . 9
2322eqcomd 2410 . . . . . . . 8
2423necon3i 2643 . . . . . . 7
2521, 24syl 17 . . . . . 6
2611simprd 461 . . . . . . . 8
2726, 17sseldd 3442 . . . . . . 7
2826, 14sseldd 3442 . . . . . . 7
29 pmltpc.7 . . . . . . 7
3027, 28, 29leltned 9769 . . . . . 6
3125, 30mpbird 232 . . . . 5
3231ad2antrr 724 . . . 4
33 simplr 754 . . . . . 6
3420ad2antrr 724 . . . . . 6
3533, 34jca 530 . . . . 5
3635orcd 390 . . . 4
372, 4, 6, 7, 32, 36pmltpclem1 22150 . . 3
383ad2antrr 724 . . . 4
391ad2antrr 724 . . . 4
40 pmltpc.6 . . . . 5
4140ad2antrr 724 . . . 4
4213, 1sseldd 3442 . . . . . . . . 9
4312, 42ffvelrnd 6009 . . . . . . . 8
4443ad2antrr 724 . . . . . . 7
45 simplr 754 . . . . . . 7
4644, 45gtned 9751 . . . . . 6
47 fveq2 5848 . . . . . . . 8
4847eqcomd 2410 . . . . . . 7
4948necon3i 2643 . . . . . 6
5046, 49syl 17 . . . . 5
5127ad2antrr 724 . . . . . 6
5226, 42sseldd 3442 . . . . . . 7
5352ad2antrr 724 . . . . . 6
54 simpr 459 . . . . . 6
5551, 53, 54leltned 9769 . . . . 5
5650, 55mpbird 232 . . . 4
57 pmltpc.10 . . . . . . . . 9
5813, 40sseldd 3442 . . . . . . . . . . 11
5912, 58ffvelrnd 6009 . . . . . . . . . 10
6043, 59ltnled 9763 . . . . . . . . 9
6157, 60mpbird 232 . . . . . . . 8
6243, 61gtned 9751 . . . . . . 7
63 fveq2 5848 . . . . . . . 8
6463necon3i 2643 . . . . . . 7
6562, 64syl 17 . . . . . 6
6626, 58sseldd 3442 . . . . . . 7
67 pmltpc.8 . . . . . . 7
6852, 66, 67leltned 9769 . . . . . 6
6965, 68mpbird 232 . . . . 5
7069ad2antrr 724 . . . 4
7161ad2antrr 724 . . . . . 6
7245, 71jca 530 . . . . 5
7372olcd 391 . . . 4
7438, 39, 41, 56, 70, 73pmltpclem1 22150 . . 3
7552adantr 463 . . 3
7627adantr 463 . . 3
7737, 74, 75, 76ltlecasei 9723 . 2
783ad2antrr 724 . . . 4
795ad2antrr 724 . . . 4
8040ad2antrr 724 . . . 4
8131ad2antrr 724 . . . 4
82 simpr 459 . . . 4
8320ad2antrr 724 . . . . . 6
8415adantr 463 . . . . . . . 8
8518adantr 463 . . . . . . . 8
8659adantr 463 . . . . . . . 8
8720adantr 463 . . . . . . . 8
8843adantr 463 . . . . . . . . 9
89 simpr 459 . . . . . . . . 9
9061adantr 463 . . . . . . . . 9
9185, 88, 86, 89, 90lelttrd 9773 . . . . . . . 8
9284, 85, 86, 87, 91lttrd 9776 . . . . . . 7
9392adantr 463 . . . . . 6
9483, 93jca 530 . . . . 5
9594olcd 391 . . . 4
9678, 79, 80, 81, 82, 95pmltpclem1 22150 . . 3
971ad2antrr 724 . . . 4
9840ad2antrr 724 . . . 4
995ad2antrr 724 . . . 4
10069ad2antrr 724 . . . 4
10115ad2antrr 724 . . . . . . 7
10292adantr 463 . . . . . . 7
103101, 102gtned 9751 . . . . . 6
104 fveq2 5848 . . . . . . . 8
105104eqcomd 2410 . . . . . . 7
106105necon3i 2643 . . . . . 6
107103, 106syl 17 . . . . 5
10866ad2antrr 724 . . . . . 6
10928ad2antrr 724 . . . . . 6
110 simpr 459 . . . . . 6
111108, 109, 110leltned 9769 . . . . 5
112107, 111mpbird 232 . . . 4
11361ad2antrr 724 . . . . . 6
114113, 102jca 530 . . . . 5
115114orcd 390 . . . 4
11697, 98, 99, 100, 112, 115pmltpclem1 22150 . . 3
11728adantr 463 . . 3
11866adantr 463 . . 3
11996, 116, 117, 118ltlecasei 9723 . 2
12077, 119, 43, 18ltlecasei 9723 1
 Colors of variables: wff setvar class Syntax hints:   wn 3   wi 4   wo 366   wa 367   w3a 974   wceq 1405   wcel 1842   wne 2598  wrex 2754   wss 3413   class class class wbr 4394   cdm 4822  wf 5564  cfv 5568  (class class class)co 6277   cpm 7457  cr 9520   clt 9657   cle 9658 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-8 1844  ax-9 1846  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380  ax-sep 4516  ax-nul 4524  ax-pow 4571  ax-pr 4629  ax-un 6573  ax-cnex 9577  ax-resscn 9578  ax-pre-lttri 9595  ax-pre-lttrn 9596 This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 975  df-3an 976  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-eu 2242  df-mo 2243  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ne 2600  df-nel 2601  df-ral 2758  df-rex 2759  df-rab 2762  df-v 3060  df-sbc 3277  df-csb 3373  df-dif 3416  df-un 3418  df-in 3420  df-ss 3427  df-nul 3738  df-if 3885  df-pw 3956  df-sn 3972  df-pr 3974  df-op 3978  df-uni 4191  df-br 4395  df-opab 4453  df-mpt 4454  df-id 4737  df-po 4743  df-so 4744  df-xp 4828  df-rel 4829  df-cnv 4830  df-co 4831  df-dm 4832  df-rn 4833  df-res 4834  df-ima 4835  df-iota 5532  df-fun 5570  df-fn 5571  df-f 5572  df-f1 5573  df-fo 5574  df-f1o 5575  df-fv 5576  df-ov 6280  df-oprab 6281  df-mpt2 6282  df-er 7347  df-pm 7459  df-en 7554  df-dom 7555  df-sdom 7556  df-pnf 9659  df-mnf 9660  df-xr 9661  df-ltxr 9662  df-le 9663 This theorem is referenced by:  pmltpc  22152
 Copyright terms: Public domain W3C validator