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

Theorem erovlem 6134
Description: Lemma for eroprf 6135. (Contributed by Jeff Madsen, 10-Jun-2010.) (Revised by Mario Carneiro, 30-Dec-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  .+
eropr.12  .+^  { <. <. , 
>. ,  >.  |  p  q  p R  q S  p  .+  q T }
Assertion
Ref Expression
erovlem  .+^  J ,  K  |->  iota p  q  p R  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,,,,
Allowed substitution hints:    C(,,,, t, s, r, q, p)    .+^ (,,,, 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 erovlem
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 simpl 102 . . . . . . . 8  p R  q S  p  .+  q T  p R  q S
21reximi 2410 . . . . . . 7  q  p R  q S  p  .+  q T  q  p R  q S
32reximi 2410 . . . . . 6  p  q  p R 
q S  p  .+  q T  p  q  p R  q S
4 eropr.1 . . . . . . . . . 10  J  /. R
54eleq2i 2101 . . . . . . . . 9  J  /. R
6 vex 2554 . . . . . . . . . 10 
_V
76elqs 6093 . . . . . . . . 9  /. R  p  p R
85, 7bitri 173 . . . . . . . 8  J  p  p R
9 eropr.2 . . . . . . . . . 10  K  /. S
109eleq2i 2101 . . . . . . . . 9  K  /. S
11 vex 2554 . . . . . . . . . 10 
_V
1211elqs 6093 . . . . . . . . 9  /. S  q 
q S
1310, 12bitri 173 . . . . . . . 8  K  q 
q S
148, 13anbi12i 433 . . . . . . 7  J  K  p  p R  q 
q S
15 reeanv 2473 . . . . . . 7  p  q  p R  q S  p  p R  q  q S
1614, 15bitr4i 176 . . . . . 6  J  K  p  q  p R  q S
173, 16sylibr 137 . . . . 5  p  q  p R 
q S  p  .+  q T  J  K
1817pm4.71ri 372 . . . 4  p  q  p R 
q S  p  .+  q T  J  K  p  q  p R  q S  p  .+  q T
19 eropr.3 . . . . . . . 8  T  Z
20 eropr.4 . . . . . . . 8  R  Er  U
21 eropr.5 . . . . . . . 8  S  Er  V
22 eropr.6 . . . . . . . 8  T  Er  W
23 eropr.7 . . . . . . . 8  C_  U
24 eropr.8 . . . . . . . 8  C_  V
25 eropr.9 . . . . . . . 8  C  C_  W
26 eropr.10 . . . . . . . 8  .+  :  X.  --> C
27 eropr.11 . . . . . . . 8  r  s 
t  r R s  t S  r  .+  t T s  .+
284, 9, 19, 20, 21, 22, 23, 24, 25, 26, 27eroveu 6133 . . . . . . 7  J  K  p  q  p R 
q S  p  .+  q T
29 iota1 4824 . . . . . . 7  p  q  p R 
q S  p  .+  q T  p  q  p R  q S  p  .+  q T  iota p  q  p R  q S  p  .+  q T
3028, 29syl 14 . . . . . 6  J  K  p  q  p R  q S  p  .+  q T  iota p  q  p R  q S  p  .+  q T
31 eqcom 2039 . . . . . 6 
iota p  q  p R 
q S  p  .+  q T  iota p  q  p R 
q S  p  .+  q T
3230, 31syl6bb 185 . . . . 5  J  K  p  q  p R  q S  p  .+  q T  iota p  q  p R 
q S  p  .+  q T
3332pm5.32da 425 . . . 4  J  K  p  q  p R 
q S  p  .+  q T  J  K  iota p  q  p R 
q S  p  .+  q T
3418, 33syl5bb 181 . . 3  p  q  p R 
q S  p  .+  q T  J  K  iota p  q  p R 
q S  p  .+  q T
3534oprabbidv 5501 . 2  { <. <. , 
>. ,  >.  |  p  q  p R  q S  p  .+  q T }  { <. <. , 
>. ,  >.  |  J  K  iota p  q  p R 
q S  p  .+  q T }
36 eropr.12 . 2  .+^  { <. <. , 
>. ,  >.  |  p  q  p R  q S  p  .+  q T }
37 df-mpt2 5460 . . 3  J ,  K  |->  iota p  q  p R  q S  p  .+  q T  { <. <. ,  >. ,  >.  |  J  K 
iota p  q  p R 
q S  p  .+  q T }
38 nfv 1418 . . . 4  F/  J  K 
iota p  q  p R 
q S  p  .+  q T
39 nfv 1418 . . . . 5  F/  J  K
40 nfiota1 4812 . . . . . 6  F/_ iota p  q  p R 
q S  p  .+  q T
4140nfeq2 2186 . . . . 5  F/  iota p  q  p R  q S  p  .+  q T
4239, 41nfan 1454 . . . 4  F/  J  K  iota p  q  p R 
q S  p  .+  q T
43 eqeq1 2043 . . . . 5  iota p  q  p R  q S  p  .+  q T  iota p  q  p R  q S  p  .+  q T
4443anbi2d 437 . . . 4  J  K 
iota p  q  p R 
q S  p  .+  q T  J  K  iota p  q  p R 
q S  p  .+  q T
4538, 42, 44cbvoprab3 5522 . . 3  { <. <. ,  >. ,  >.  |  J  K 
iota p  q  p R 
q S  p  .+  q T }  { <. <. , 
>. ,  >.  |  J  K  iota p  q  p R 
q S  p  .+  q T }
4637, 45eqtr4i 2060 . 2  J ,  K  |->  iota p  q  p R  q S  p  .+  q T  { <. <. ,  >. ,  >.  |  J  K 
iota p  q  p R 
q S  p  .+  q T }
4735, 36, 463eqtr4g 2094 1  .+^  J ,  K  |->  iota p  q  p R  q S  p  .+  q T
Colors of variables: wff set class
Syntax hints:   wi 4   wa 97   wb 98   wceq 1242   wcel 1390  weu 1897  wrex 2301    C_ wss 2911   class class class wbr 3755    X. cxp 4286   iotacio 4808   -->wf 4841  (class class class)co 5455   {coprab 5456    |-> cmpt2 5457    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-bnd 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-oprab 5459  df-mpt2 5460  df-er 6042  df-ec 6044  df-qs 6048
This theorem is referenced by:  eroprf  6135
  Copyright terms: Public domain W3C validator