ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  eroveu Structured version   Unicode version

Theorem eroveu 6133
Description: Lemma for eroprf 6135. (Contributed by Jeff Madsen, 10-Jun-2010.) (Revised by Mario Carneiro, 9-Jul-2014.)
Hypotheses
Ref Expression
eropr.1  J  /. R
eropr.2  K  /. S
eropr.3  T  Z
eropr.4  R  Er  U
eropr.5  S  Er  V
eropr.6  T  Er  W
eropr.7  C_  U
eropr.8  C_  V
eropr.9  C  C_  W
eropr.10  .+  :  X.  --> C
eropr.11  r  s 
t  r R s  t S  r  .+  t T s  .+
Assertion
Ref Expression
eroveu  X  J  Y  K  p  q  X  p R  Y 
q S  p  .+  q T
Distinct variable groups:    q, p, r, s, t,,,   , p, q, r, s, t,,    J, p, q,    R, p, q, r, s, t,,    K, p, q,    S, p, q, r, s, t,,    .+ , p, q, r, s, t,,   , p, q, r, s, t,,    T, p, q, r, s, t,,    X, p, q, r, s, t,,    Y, p, q, r, s, t,,
Allowed substitution hints:    C(,, t, s, r, q, p)    U(,, t, s, r, q, p)    J(, t, s, r)    K(, t, s, r)    V(,, t, s, r, q, p)    W(,, t, s, r, q, p)    Z(,, t, s, r, q, p)

Proof of Theorem eroveu
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 elqsi 6094 . . . . . . . 8  X  /. R  p  X  p R
2 eropr.1 . . . . . . . 8  J  /. R
31, 2eleq2s 2129 . . . . . . 7  X  J  p  X  p R
4 elqsi 6094 . . . . . . . 8  Y  /. S  q  Y 
q S
5 eropr.2 . . . . . . . 8  K  /. S
64, 5eleq2s 2129 . . . . . . 7  Y  K  q  Y  q S
73, 6anim12i 321 . . . . . 6  X  J  Y  K  p  X  p R  q  Y  q S
87adantl 262 . . . . 5  X  J  Y  K  p  X  p R  q  Y 
q S
9 reeanv 2473 . . . . 5  p  q  X  p R  Y  q S  p  X  p R  q  Y  q S
108, 9sylibr 137 . . . 4  X  J  Y  K  p  q  X  p R  Y  q S
11 eropr.3 . . . . . . . 8  T  Z
1211adantr 261 . . . . . . 7  X  J  Y  K 
T  Z
13 ecexg 6046 . . . . . . 7  T  Z  p  .+  q T  _V
14 elisset 2562 . . . . . . 7  p  .+  q T  _V  p  .+  q T
1512, 13, 143syl 17 . . . . . 6  X  J  Y  K  p  .+  q T
1615biantrud 288 . . . . 5  X  J  Y  K  X  p R  Y  q S  X  p R  Y  q S  p  .+  q T
17162rexbidv 2343 . . . 4  X  J  Y  K  p  q  X  p R  Y  q S  p  q  X  p R  Y  q S  p 
.+  q T
1810, 17mpbid 135 . . 3  X  J  Y  K  p  q  X  p R  Y  q S  p 
.+  q T
19 19.42v 1783 . . . . . . . 8  X  p R  Y  q S  p  .+  q T  X  p R  Y  q S  p  .+  q T
2019bicomi 123 . . . . . . 7  X  p R  Y  q S  p 
.+  q T  X  p R  Y  q S  p  .+  q T
2120rexbii 2325 . . . . . 6  q  X  p R  Y  q S  p 
.+  q T  q  X  p R  Y  q S  p  .+  q T
22 rexcom4 2571 . . . . . 6  q  X  p R  Y  q S  p  .+  q T  q  X  p R  Y  q S  p  .+  q T
2321, 22bitri 173 . . . . 5  q  X  p R  Y  q S  p 
.+  q T  q  X  p R  Y  q S  p  .+  q T
2423rexbii 2325 . . . 4  p  q  X  p R  Y 
q S  p  .+  q T  p  q  X  p R  Y  q S  p  .+  q T
25 rexcom4 2571 . . . 4  p  q  X  p R  Y  q S  p  .+  q T  p  q  X  p R  Y  q S  p  .+  q T
2624, 25bitri 173 . . 3  p  q  X  p R  Y 
q S  p  .+  q T  p  q  X  p R  Y  q S  p  .+  q T
2718, 26sylib 127 . 2  X  J  Y  K  p  q  X  p R  Y 
q S  p  .+  q T
28 reeanv 2473 . . . . . 6  r  s  t  X  r R  Y  t S  r  .+  t T  X 
s R  Y  S  s  .+  T  r  t  X  r R  Y  t S  r  .+  t T  s  X 
s R  Y  S  s  .+  T
29 eceq1 6077 . . . . . . . . . . 11  p  r  p R 
r R
3029eqeq2d 2048 . . . . . . . . . 10  p  r  X  p R  X  r R
3130anbi1d 438 . . . . . . . . 9  p  r  X  p R  Y  q S  X 
r R  Y  q S
32 oveq1 5462 . . . . . . . . . . 11  p  r  p  .+  q  r  .+  q
3332eceq1d 6078 . . . . . . . . . 10  p  r  p  .+  q T  r  .+  q T
3433eqeq2d 2048 . . . . . . . . 9  p  r  p  .+  q T 
r  .+  q T
3531, 34anbi12d 442 . . . . . . . 8  p  r  X  p R  Y  q S  p  .+  q T  X  r R  Y  q S  r  .+  q T
36 eceq1 6077 . . . . . . . . . . 11  q  t 
q S  t S
3736eqeq2d 2048 . . . . . . . . . 10  q  t  Y  q S  Y  t S
3837anbi2d 437 . . . . . . . . 9  q  t  X 
r R  Y  q S  X  r R  Y  t S
39 oveq2 5463 . . . . . . . . . . 11  q  t 
r  .+  q  r  .+  t
4039eceq1d 6078 . . . . . . . . . 10  q  t  r  .+  q T  r  .+  t T
4140eqeq2d 2048 . . . . . . . . 9  q  t 
r  .+  q T  r  .+  t T
4238, 41anbi12d 442 . . . . . . . 8  q  t  X 
r R  Y  q S  r  .+  q T  X  r R  Y 
t S  r  .+  t T
4335, 42cbvrex2v 2536 . . . . . . 7  p  q  X  p R  Y 
q S  p  .+  q T  r  t  X  r R  Y  t S  r  .+  t T
44 eceq1 6077 . . . . . . . . . . 11  p  s  p R 
s R
4544eqeq2d 2048 . . . . . . . . . 10  p  s  X  p R  X  s R
4645anbi1d 438 . . . . . . . . 9  p  s  X  p R  Y  q S  X 
s R  Y  q S
47 oveq1 5462 . . . . . . . . . . 11  p  s  p  .+  q  s  .+  q
4847eceq1d 6078 . . . . . . . . . 10  p  s  p  .+  q T  s  .+  q T
4948eqeq2d 2048 . . . . . . . . 9  p  s  p  .+  q T 
s  .+  q T
5046, 49anbi12d 442 . . . . . . . 8  p  s  X  p R  Y  q S  p  .+  q T  X  s R  Y  q S  s  .+  q T
51 eceq1 6077 . . . . . . . . . . 11  q 
q S  S
5251eqeq2d 2048 . . . . . . . . . 10  q  Y  q S  Y  S
5352anbi2d 437 . . . . . . . . 9  q  X 
s R  Y  q S  X  s R  Y  S
54 oveq2 5463 . . . . . . . . . . 11  q 
s  .+  q  s  .+
5554eceq1d 6078 . . . . . . . . . 10  q  s  .+  q T  s  .+  T
5655eqeq2d 2048 . . . . . . . . 9  q 
s  .+  q T  s  .+  T
5753, 56anbi12d 442 . . . . . . . 8  q  X 
s R  Y  q S  s  .+  q T  X  s R  Y  S 
s  .+  T
5850, 57cbvrex2v 2536 . . . . . . 7  p  q  X  p R  Y 
q S  p  .+  q T  s  X  s R  Y  S  s  .+  T
5943, 58anbi12i 433 . . . . . 6  p  q  X  p R  Y  q S  p  .+  q T  p  q  X  p R  Y  q S  p  .+  q T  r  t  X  r R  Y  t S  r  .+  t T  s  X 
s R  Y  S  s  .+  T
6028, 59bitr4i 176 . . . . 5  r  s  t  X  r R  Y  t S  r  .+  t T  X 
s R  Y  S  s  .+  T  p  q  X  p R  Y 
q S  p  .+  q T  p  q  X  p R  Y  q S  p  .+  q T
61 reeanv 2473 . . . . . . 7  t  X  r R  Y  t S  r  .+  t T  X 
s R  Y  S  s  .+  T  t  X  r R  Y  t S  r  .+  t T  X 
s R  Y  S  s  .+  T
62 eropr.11 . . . . . . . . . . . . . 14  r  s 
t  r R s  t S  r  .+  t T s  .+
63 eropr.4 . . . . . . . . . . . . . . . . 17  R  Er  U
6463adantr 261 . . . . . . . . . . . . . . . 16  r  s 
t  R  Er  U
65 eropr.7 . . . . . . . . . . . . . . . . . 18  C_  U
6665adantr 261 . . . . . . . . . . . . . . . . 17  r  s 
t  C_  U
67 simprll 489 . . . . . . . . . . . . . . . . 17  r  s 
t  r
6866, 67sseldd 2940 . . . . . . . . . . . . . . . 16  r  s 
t  r  U
6964, 68erth 6086 . . . . . . . . . . . . . . 15  r  s 
t 
r R s  r R 
s R
70 eropr.5 . . . . . . . . . . . . . . . . 17  S  Er  V
7170adantr 261 . . . . . . . . . . . . . . . 16  r  s 
t  S  Er  V
72 eropr.8 . . . . . . . . . . . . . . . . . 18  C_  V
7372adantr 261 . . . . . . . . . . . . . . . . 17  r  s 
t  C_  V
74 simprrl 491 . . . . . . . . . . . . . . . . 17  r  s 
t  t
7573, 74sseldd 2940 . . . . . . . . . . . . . . . 16  r  s 
t  t  V
7671, 75erth 6086 . . . . . . . . . . . . . . 15  r  s 
t 
t S  t S  S
7769, 76anbi12d 442 . . . . . . . . . . . . . 14  r  s 
t  r R s  t S  r R  s R  t S  S
78 eropr.6 . . . . . . . . . . . . . . . 16  T  Er  W
7978adantr 261 . . . . . . . . . . . . . . 15  r  s 
t  T  Er  W
80 eropr.9 . . . . . . . . . . . . . . . . 17  C  C_  W
8180adantr 261 . . . . . . . . . . . . . . . 16  r  s 
t  C  C_  W
82 eropr.10 . . . . . . . . . . . . . . . . . 18  .+  :  X.  --> C
8382adantr 261 . . . . . . . . . . . . . . . . 17  r  s 
t  .+  :  X. 
--> C
8483, 67, 74fovrnd 5587 . . . . . . . . . . . . . . . 16  r  s 
t 
r  .+  t  C
8581, 84sseldd 2940 . . . . . . . . . . . . . . 15  r  s 
t 
r  .+  t  W
8679, 85erth 6086 . . . . . . . . . . . . . 14  r  s 
t  r  .+  t T s  .+ 
r  .+  t T  s  .+  T
8762, 77, 863imtr3d 191 . . . . . . . . . . . . 13  r  s 
t  r R  s R  t S  S  r 
.+  t T 
s  .+  T
88 eqeq2 2046 . . . . . . . . . . . . . 14  s 
.+  T 
r  .+  t T  r  .+  t T  s  .+  T
8988biimprcd 149 . . . . . . . . . . . . 13  r  .+  t T  s  .+  T 
s  .+  T 
r  .+  t T
9087, 89syl6 29 . . . . . . . . . . . 12  r  s 
t  r R  s R  t S  S  s  .+  T  r  .+  t T
9190impd 242 . . . . . . . . . . 11  r  s 
t  r R  s R  t S  S 
s  .+  T  r  .+  t T
92 eqeq1 2043 . . . . . . . . . . . . . . 15  X  r R  X  s R  r R  s R
93 eqeq1 2043 . . . . . . . . . . . . . . 15  Y  t S  Y  S  t S  S
9492, 93bi2anan9 538 . . . . . . . . . . . . . 14  X  r R  Y  t S  X  s R  Y  S  r R  s R  t S  S
9594anbi1d 438 . . . . . . . . . . . . 13  X  r R  Y  t S  X  s R  Y  S  s  .+  T  r R  s R  t S  S  s  .+  T
9695adantr 261 . . . . . . . . . . . 12  X 
r R  Y  t S  r  .+  t T  X  s R  Y  S  s  .+  T  r R  s R  t S  S  s  .+  T
97 eqeq1 2043 . . . . . . . . . . . . 13  r 
.+  t T  r 
.+  t T
9897adantl 262 . . . . . . . . . . . 12  X 
r R  Y  t S  r  .+  t T  r 
.+  t T
9996, 98imbi12d 223 . . . . . . . . . . 11  X 
r R  Y  t S  r  .+  t T  X 
s R  Y  S  s  .+  T 
r R  s R  t S  S  s  .+  T  r  .+  t T
10091, 99syl5ibrcom 146 . . . . . . . . . 10  r  s 
t  X 
r R  Y  t S  r  .+  t T  X  s R  Y  S  s  .+  T
101100impd 242 . . . . . . . . 9  r  s 
t  X  r R  Y 
t S  r  .+  t T  X 
s R  Y  S  s  .+  T
102101anassrs 380 . . . . . . . 8 
r  s  t  X  r R  Y  t S  r  .+  t T  X 
s R  Y  S  s  .+  T
103102rexlimdvva 2434 . . . . . . 7  r  s  t  X  r R  Y 
t S  r  .+  t T  X 
s R  Y  S  s  .+  T
10461, 103syl5bir 142 . . . . . 6  r  s  t  X  r R  Y  t S  r  .+  t T  X 
s R  Y  S  s  .+  T
105104rexlimdvva 2434 . . . . 5  r  s  t  X  r R  Y  t S  r  .+  t T  X 
s R  Y  S  s  .+  T
10660, 105syl5bir 142 . . . 4  p  q  X  p R  Y 
q S  p  .+  q T  p  q  X  p R  Y  q S  p  .+  q T
107106adantr 261 . . 3  X  J  Y  K  p  q  X  p R  Y 
q S  p  .+  q T  p  q  X  p R  Y  q S  p  .+  q T
108107alrimivv 1752 . 2  X  J  Y  K  p  q  X  p R  Y 
q S  p  .+  q T  p  q  X  p R  Y  q S  p  .+  q T
109 eqeq1 2043 . . . . 5  p  .+  q T  p  .+  q T
110109anbi2d 437 . . . 4  X  p R  Y  q S  p  .+  q T  X  p R  Y  q S  p  .+  q T
1111102rexbidv 2343 . . 3  p  q  X  p R  Y  q S  p  .+  q T  p  q  X  p R  Y 
q S  p  .+  q T
112111eu4 1959 . 2  p  q  X  p R  Y 
q S  p  .+  q T  p  q  X  p R  Y  q S  p  .+  q T  p  q  X  p R  Y 
q S  p  .+  q T  p  q  X  p R  Y  q S  p  .+  q T
11327, 108, 112sylanbrc 394 1  X  J  Y  K  p  q  X  p R  Y 
q S  p  .+  q T
Colors of variables: wff set class
Syntax hints:   wi 4   wa 97   wb 98  wal 1240   wceq 1242  wex 1378   wcel 1390  weu 1897  wrex 2301   _Vcvv 2551    C_ wss 2911   class class class wbr 3755    X. cxp 4286   -->wf 4841  (class class class)co 5455    Er wer 6039  cec 6040   /.cqs 6041
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bndl 1396  ax-4 1397  ax-13 1401  ax-14 1402  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019  ax-sep 3866  ax-pow 3918  ax-pr 3935  ax-un 4136
This theorem depends on definitions:  df-bi 110  df-3an 886  df-tru 1245  df-nf 1347  df-sb 1643  df-eu 1900  df-mo 1901  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-ral 2305  df-rex 2306  df-v 2553  df-sbc 2759  df-un 2916  df-in 2918  df-ss 2925  df-pw 3353  df-sn 3373  df-pr 3374  df-op 3376  df-uni 3572  df-br 3756  df-opab 3810  df-id 4021  df-xp 4294  df-rel 4295  df-cnv 4296  df-co 4297  df-dm 4298  df-rn 4299  df-res 4300  df-ima 4301  df-iota 4810  df-fun 4847  df-fn 4848  df-f 4849  df-fv 4853  df-ov 5458  df-er 6042  df-ec 6044  df-qs 6048
This theorem is referenced by:  erovlem  6134  eroprf  6135
  Copyright terms: Public domain W3C validator