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

Theorem eroveu 7425
Description: Lemma for erov 7427 and eroprf 7428. (Contributed by Jeff Madsen, 10-Jun-2010.) (Revised by Mario Carneiro, 9-Jul-2014.)
Hypotheses
Ref Expression
eropr.1
eropr.2
eropr.3
eropr.4
eropr.5
eropr.6
eropr.7
eropr.8
eropr.9
eropr.10
eropr.11
Assertion
Ref Expression
eroveu
Distinct variable groups:   , , , , , , ,   , , , , , , ,   J, , ,   , , , , , , ,   , , ,   S, , , , , , ,   , , , , , , ,   , , , , , , ,   , , , , , , ,   , , , , , , ,   , , , , , , ,

Proof of Theorem eroveu
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 elqsi 7384 . . . . . . . 8
2 eropr.1 . . . . . . . 8
31, 2eleq2s 2565 . . . . . . 7
4 elqsi 7384 . . . . . . . 8
5 eropr.2 . . . . . . . 8
64, 5eleq2s 2565 . . . . . . 7
73, 6anim12i 566 . . . . . 6
87adantl 466 . . . . 5
9 reeanv 3025 . . . . 5
108, 9sylibr 212 . . . 4
11 eropr.3 . . . . . . . 8
1211adantr 465 . . . . . . 7
13 ecexg 7334 . . . . . . 7
14 elisset 3120 . . . . . . 7
1512, 13, 143syl 20 . . . . . 6
1615biantrud 507 . . . . 5
17162rexbidv 2975 . . . 4
1810, 17mpbid 210 . . 3
19 19.42v 1775 . . . . . . . 8
2019bicomi 202 . . . . . . 7
2120rexbii 2959 . . . . . 6
22 rexcom4 3129 . . . . . 6
2321, 22bitri 249 . . . . 5
2423rexbii 2959 . . . 4
25 rexcom4 3129 . . . 4
2624, 25bitri 249 . . 3
2718, 26sylib 196 . 2
28 reeanv 3025 . . . . . 6
29 eceq1 7366 . . . . . . . . . . 11
3029eqeq2d 2471 . . . . . . . . . 10
3130anbi1d 704 . . . . . . . . 9
32 oveq1 6303 . . . . . . . . . . 11
3332eceq1d 7367 . . . . . . . . . 10
3433eqeq2d 2471 . . . . . . . . 9
3531, 34anbi12d 710 . . . . . . . 8
36 eceq1 7366 . . . . . . . . . . 11
3736eqeq2d 2471 . . . . . . . . . 10
3837anbi2d 703 . . . . . . . . 9
39 oveq2 6304 . . . . . . . . . . 11
4039eceq1d 7367 . . . . . . . . . 10
4140eqeq2d 2471 . . . . . . . . 9
4238, 41anbi12d 710 . . . . . . . 8
4335, 42cbvrex2v 3093 . . . . . . 7
44 eceq1 7366 . . . . . . . . . . 11
4544eqeq2d 2471 . . . . . . . . . 10
4645anbi1d 704 . . . . . . . . 9
47 oveq1 6303 . . . . . . . . . . 11
4847eceq1d 7367 . . . . . . . . . 10
4948eqeq2d 2471 . . . . . . . . 9
5046, 49anbi12d 710 . . . . . . . 8
51 eceq1 7366 . . . . . . . . . . 11
5251eqeq2d 2471 . . . . . . . . . 10
5352anbi2d 703 . . . . . . . . 9
54 oveq2 6304 . . . . . . . . . . 11
5554eceq1d 7367 . . . . . . . . . 10
5655eqeq2d 2471 . . . . . . . . 9
5753, 56anbi12d 710 . . . . . . . 8
5850, 57cbvrex2v 3093 . . . . . . 7
5943, 58anbi12i 697 . . . . . 6
6028, 59bitr4i 252 . . . . 5
61 reeanv 3025 . . . . . . 7
62 eropr.11 . . . . . . . . . . . . . 14
63 eropr.4 . . . . . . . . . . . . . . . . 17
6463adantr 465 . . . . . . . . . . . . . . . 16
65 eropr.7 . . . . . . . . . . . . . . . . . 18
6665adantr 465 . . . . . . . . . . . . . . . . 17
67 simprll 763 . . . . . . . . . . . . . . . . 17
6866, 67sseldd 3504 . . . . . . . . . . . . . . . 16
6964, 68erth 7375 . . . . . . . . . . . . . . 15
70 eropr.5 . . . . . . . . . . . . . . . . 17
7170adantr 465 . . . . . . . . . . . . . . . 16
72 eropr.8 . . . . . . . . . . . . . . . . . 18
7372adantr 465 . . . . . . . . . . . . . . . . 17
74 simprrl 765 . . . . . . . . . . . . . . . . 17
7573, 74sseldd 3504 . . . . . . . . . . . . . . . 16
7671, 75erth 7375 . . . . . . . . . . . . . . 15
7769, 76anbi12d 710 . . . . . . . . . . . . . 14
78 eropr.6 . . . . . . . . . . . . . . . 16
7978adantr 465 . . . . . . . . . . . . . . 15
80 eropr.9 . . . . . . . . . . . . . . . . 17
8180adantr 465 . . . . . . . . . . . . . . . 16
82 eropr.10 . . . . . . . . . . . . . . . . . 18
8382adantr 465 . . . . . . . . . . . . . . . . 17
8483, 67, 74fovrnd 6447 . . . . . . . . . . . . . . . 16
8581, 84sseldd 3504 . . . . . . . . . . . . . . 15
8679, 85erth 7375 . . . . . . . . . . . . . 14
8762, 77, 863imtr3d 267 . . . . . . . . . . . . 13
88 eqeq2 2472 . . . . . . . . . . . . . 14
8988biimprcd 225 . . . . . . . . . . . . 13
9087, 89syl6 33 . . . . . . . . . . . 12
9190impd 431 . . . . . . . . . . 11
92 eqeq1 2461 . . . . . . . . . . . . . . 15
93 eqeq1 2461 . . . . . . . . . . . . . . 15
9492, 93bi2anan9 873 . . . . . . . . . . . . . 14
9594anbi1d 704 . . . . . . . . . . . . 13
9695adantr 465 . . . . . . . . . . . 12
97 eqeq1 2461 . . . . . . . . . . . . 13
9897adantl 466 . . . . . . . . . . . 12
9996, 98imbi12d 320 . . . . . . . . . . 11
10091, 99syl5ibrcom 222 . . . . . . . . . 10
101100impd 431 . . . . . . . . 9
102101anassrs 648 . . . . . . . 8
103102rexlimdvva 2956 . . . . . . 7
10461, 103syl5bir 218 . . . . . 6
105104rexlimdvva 2956 . . . . 5
10660, 105syl5bir 218 . . . 4
107106adantr 465 . . 3
108107alrimivv 1720 . 2
109 eqeq1 2461 . . . . 5
110109anbi2d 703 . . . 4
1111102rexbidv 2975 . . 3
112111eu4 2338 . 2
11327, 108, 112sylanbrc 664 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  /\wa 369  A.wal 1393  =wceq 1395  E.wex 1612  e.wcel 1818  E!weu 2282  E.wrex 2808   cvv 3109  C_wss 3475   class class class wbr 4452  X.cxp 5002  -->wf 5589  (class class class)co 6296  Erwer 7327  [cec 7328  /.cqs 7329
This theorem is referenced by:  erovlem  7426  erov  7427  eroprf  7428
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-8 1820  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573  ax-nul 4581  ax-pr 4691  ax-un 6592
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-eu 2286  df-mo 2287  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-sbc 3328  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-uni 4250  df-br 4453  df-opab 4511  df-id 4800  df-xp 5010  df-rel 5011  df-cnv 5012  df-co 5013  df-dm 5014  df-rn 5015  df-res 5016  df-ima 5017  df-iota 5556  df-fun 5595  df-fn 5596  df-f 5597  df-fv 5601  df-ov 6299  df-er 7330  df-ec 7332  df-qs 7336
  Copyright terms: Public domain W3C validator