Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  br8d Structured version   Unicode version

Theorem br8d 25954
Description: Substitution for an eight-place predicate. (Contributed by Scott Fenton, 26-Sep-2013.) (Revised by Mario Carneiro, 3-May-2015.) (Revised by Thierry Arnoux, 21-Mar-2019.)
Hypotheses
Ref Expression
br8d.1  |-  ( a  =  A  ->  ( ps 
<->  ch ) )
br8d.2  |-  ( b  =  B  ->  ( ch 
<->  th ) )
br8d.3  |-  ( c  =  C  ->  ( th 
<->  ta ) )
br8d.4  |-  ( d  =  D  ->  ( ta 
<->  et ) )
br8d.5  |-  ( e  =  E  ->  ( et 
<->  ze ) )
br8d.6  |-  ( f  =  F  ->  ( ze 
<-> 
si ) )
br8d.7  |-  ( g  =  G  ->  ( si 
<->  rh ) )
br8d.8  |-  ( h  =  H  ->  ( rh 
<->  mu ) )
br8d.10  |-  ( ph  ->  R  =  { <. p ,  q >.  |  E. a  e.  P  E. b  e.  P  E. c  e.  P  E. d  e.  P  E. e  e.  P  E. f  e.  P  E. g  e.  P  E. h  e.  P  (
p  =  <. <. a ,  b >. ,  <. c ,  d >. >.  /\  q  =  <. <. e ,  f
>. ,  <. g ,  h >. >.  /\  ps ) } )
br8d.11  |-  ( ph  ->  A  e.  P )
br8d.12  |-  ( ph  ->  B  e.  P )
br8d.13  |-  ( ph  ->  C  e.  P )
br8d.14  |-  ( ph  ->  D  e.  P )
br8d.15  |-  ( ph  ->  E  e.  P )
br8d.16  |-  ( ph  ->  F  e.  P )
br8d.17  |-  ( ph  ->  G  e.  P )
br8d.18  |-  ( ph  ->  H  e.  P )
Assertion
Ref Expression
br8d  |-  ( ph  ->  ( <. <. A ,  B >. ,  <. C ,  D >. >. R <. <. E ,  F >. ,  <. G ,  H >. >. 
<->  mu ) )
Distinct variable groups:    a, b,
c, d, e, f, g, h, p, q, A    B, a, b, c, d, e, f, g, h, p, q    C, a, b, c, d, e, f, g, h, p, q    D, a, b, c, d, e, f, g, h, p, q    E, a, b, c, d, e, f, g, h, p, q    F, a, b, c, d, e, f, g, h, p, q    G, a, b, c, d, e, f, g, h, p, q    H, a, b, c, d, e, f, g, h, p, q    P, a, b, c, d, e, f, g, h, p, q    ch, a    th, b    ta, c    et, d    ze, e    si, f    rh, g    ps, p, q    mu, a, b, c, d, e, f, g, h
Allowed substitution hints:    ph( e, f, g, h, q, p, a, b, c, d)    ps( e, f, g, h, a, b, c, d)    ch( e, f, g, h, q, p, b, c, d)    th( e, f, g, h, q, p, a, c, d)    ta( e,
f, g, h, q, p, a, b, d)    et( e, f, g, h, q, p, a, b, c)    ze( f, g, h, q, p, a, b, c, d)    si( e,
g, h, q, p, a, b, c, d)    rh( e, f, h, q, p, a, b, c, d)    mu( q, p)    R( e, f, g, h, q, p, a, b, c, d)

Proof of Theorem br8d
StepHypRef Expression
1 br8d.10 . . . 4  |-  ( ph  ->  R  =  { <. p ,  q >.  |  E. a  e.  P  E. b  e.  P  E. c  e.  P  E. d  e.  P  E. e  e.  P  E. f  e.  P  E. g  e.  P  E. h  e.  P  (
p  =  <. <. a ,  b >. ,  <. c ,  d >. >.  /\  q  =  <. <. e ,  f
>. ,  <. g ,  h >. >.  /\  ps ) } )
21breqd 4315 . . 3  |-  ( ph  ->  ( <. <. A ,  B >. ,  <. C ,  D >. >. R <. <. E ,  F >. ,  <. G ,  H >. >. 
<-> 
<. <. A ,  B >. ,  <. C ,  D >. >. { <. p ,  q >.  |  E. a  e.  P  E. b  e.  P  E. c  e.  P  E. d  e.  P  E. e  e.  P  E. f  e.  P  E. g  e.  P  E. h  e.  P  (
p  =  <. <. a ,  b >. ,  <. c ,  d >. >.  /\  q  =  <. <. e ,  f
>. ,  <. g ,  h >. >.  /\  ps ) } <. <. E ,  F >. ,  <. G ,  H >. >. ) )
3 opex 4568 . . . 4  |-  <. <. A ,  B >. ,  <. C ,  D >. >.  e.  _V
4 opex 4568 . . . 4  |-  <. <. E ,  F >. ,  <. G ,  H >. >.  e.  _V
5 eqeq1 2449 . . . . . . . . . 10  |-  ( p  =  <. <. A ,  B >. ,  <. C ,  D >. >.  ->  ( p  =  <. <. a ,  b
>. ,  <. c ,  d >. >. 
<-> 
<. <. A ,  B >. ,  <. C ,  D >. >.  =  <. <. a ,  b >. ,  <. c ,  d >. >. )
)
653anbi1d 1293 . . . . . . . . 9  |-  ( p  =  <. <. A ,  B >. ,  <. C ,  D >. >.  ->  ( (
p  =  <. <. a ,  b >. ,  <. c ,  d >. >.  /\  q  =  <. <. e ,  f
>. ,  <. g ,  h >. >.  /\  ps )  <->  (
<. <. A ,  B >. ,  <. C ,  D >. >.  =  <. <. a ,  b >. ,  <. c ,  d >. >.  /\  q  =  <. <. e ,  f
>. ,  <. g ,  h >. >.  /\  ps )
) )
76rexbidv 2748 . . . . . . . 8  |-  ( p  =  <. <. A ,  B >. ,  <. C ,  D >. >.  ->  ( E. h  e.  P  (
p  =  <. <. a ,  b >. ,  <. c ,  d >. >.  /\  q  =  <. <. e ,  f
>. ,  <. g ,  h >. >.  /\  ps )  <->  E. h  e.  P  (
<. <. A ,  B >. ,  <. C ,  D >. >.  =  <. <. a ,  b >. ,  <. c ,  d >. >.  /\  q  =  <. <. e ,  f
>. ,  <. g ,  h >. >.  /\  ps )
) )
872rexbidv 2770 . . . . . . 7  |-  ( p  =  <. <. A ,  B >. ,  <. C ,  D >. >.  ->  ( E. f  e.  P  E. g  e.  P  E. h  e.  P  (
p  =  <. <. a ,  b >. ,  <. c ,  d >. >.  /\  q  =  <. <. e ,  f
>. ,  <. g ,  h >. >.  /\  ps )  <->  E. f  e.  P  E. g  e.  P  E. h  e.  P  ( <. <. A ,  B >. ,  <. C ,  D >. >.  =  <. <. a ,  b >. ,  <. c ,  d >. >.  /\  q  =  <. <. e ,  f
>. ,  <. g ,  h >. >.  /\  ps )
) )
982rexbidv 2770 . . . . . 6  |-  ( p  =  <. <. A ,  B >. ,  <. C ,  D >. >.  ->  ( E. d  e.  P  E. e  e.  P  E. f  e.  P  E. g  e.  P  E. h  e.  P  (
p  =  <. <. a ,  b >. ,  <. c ,  d >. >.  /\  q  =  <. <. e ,  f
>. ,  <. g ,  h >. >.  /\  ps )  <->  E. d  e.  P  E. e  e.  P  E. f  e.  P  E. g  e.  P  E. h  e.  P  ( <. <. A ,  B >. ,  <. C ,  D >. >.  =  <. <. a ,  b >. ,  <. c ,  d >. >.  /\  q  =  <. <. e ,  f
>. ,  <. g ,  h >. >.  /\  ps )
) )
1092rexbidv 2770 . . . . 5  |-  ( p  =  <. <. A ,  B >. ,  <. C ,  D >. >.  ->  ( E. b  e.  P  E. c  e.  P  E. d  e.  P  E. e  e.  P  E. f  e.  P  E. g  e.  P  E. h  e.  P  (
p  =  <. <. a ,  b >. ,  <. c ,  d >. >.  /\  q  =  <. <. e ,  f
>. ,  <. g ,  h >. >.  /\  ps )  <->  E. b  e.  P  E. c  e.  P  E. d  e.  P  E. e  e.  P  E. f  e.  P  E. g  e.  P  E. h  e.  P  ( <. <. A ,  B >. ,  <. C ,  D >. >.  =  <. <. a ,  b >. ,  <. c ,  d >. >.  /\  q  =  <. <. e ,  f
>. ,  <. g ,  h >. >.  /\  ps )
) )
1110rexbidv 2748 . . . 4  |-  ( p  =  <. <. A ,  B >. ,  <. C ,  D >. >.  ->  ( E. a  e.  P  E. b  e.  P  E. c  e.  P  E. d  e.  P  E. e  e.  P  E. f  e.  P  E. g  e.  P  E. h  e.  P  (
p  =  <. <. a ,  b >. ,  <. c ,  d >. >.  /\  q  =  <. <. e ,  f
>. ,  <. g ,  h >. >.  /\  ps )  <->  E. a  e.  P  E. b  e.  P  E. c  e.  P  E. d  e.  P  E. e  e.  P  E. f  e.  P  E. g  e.  P  E. h  e.  P  ( <. <. A ,  B >. ,  <. C ,  D >. >.  =  <. <. a ,  b >. ,  <. c ,  d >. >.  /\  q  =  <. <. e ,  f
>. ,  <. g ,  h >. >.  /\  ps )
) )
12 eqeq1 2449 . . . . . . . . . 10  |-  ( q  =  <. <. E ,  F >. ,  <. G ,  H >. >.  ->  ( q  =  <. <. e ,  f
>. ,  <. g ,  h >. >. 
<-> 
<. <. E ,  F >. ,  <. G ,  H >. >.  =  <. <. e ,  f >. ,  <. g ,  h >. >. )
)
13123anbi2d 1294 . . . . . . . . 9  |-  ( q  =  <. <. E ,  F >. ,  <. G ,  H >. >.  ->  ( ( <. <. A ,  B >. ,  <. C ,  D >. >.  =  <. <. a ,  b >. ,  <. c ,  d >. >.  /\  q  =  <. <. e ,  f
>. ,  <. g ,  h >. >.  /\  ps )  <->  (
<. <. A ,  B >. ,  <. C ,  D >. >.  =  <. <. a ,  b >. ,  <. c ,  d >. >.  /\  <. <. E ,  F >. , 
<. G ,  H >. >.  =  <. <. e ,  f
>. ,  <. g ,  h >. >.  /\  ps )
) )
1413rexbidv 2748 . . . . . . . 8  |-  ( q  =  <. <. E ,  F >. ,  <. G ,  H >. >.  ->  ( E. h  e.  P  ( <. <. A ,  B >. ,  <. C ,  D >. >.  =  <. <. a ,  b >. ,  <. c ,  d >. >.  /\  q  =  <. <. e ,  f
>. ,  <. g ,  h >. >.  /\  ps )  <->  E. h  e.  P  (
<. <. A ,  B >. ,  <. C ,  D >. >.  =  <. <. a ,  b >. ,  <. c ,  d >. >.  /\  <. <. E ,  F >. , 
<. G ,  H >. >.  =  <. <. e ,  f
>. ,  <. g ,  h >. >.  /\  ps )
) )
15142rexbidv 2770 . . . . . . 7  |-  ( q  =  <. <. E ,  F >. ,  <. G ,  H >. >.  ->  ( E. f  e.  P  E. g  e.  P  E. h  e.  P  ( <. <. A ,  B >. ,  <. C ,  D >. >.  =  <. <. a ,  b >. ,  <. c ,  d >. >.  /\  q  =  <. <. e ,  f
>. ,  <. g ,  h >. >.  /\  ps )  <->  E. f  e.  P  E. g  e.  P  E. h  e.  P  ( <. <. A ,  B >. ,  <. C ,  D >. >.  =  <. <. a ,  b >. ,  <. c ,  d >. >.  /\  <. <. E ,  F >. , 
<. G ,  H >. >.  =  <. <. e ,  f
>. ,  <. g ,  h >. >.  /\  ps )
) )
16152rexbidv 2770 . . . . . 6  |-  ( q  =  <. <. E ,  F >. ,  <. G ,  H >. >.  ->  ( E. d  e.  P  E. e  e.  P  E. f  e.  P  E. g  e.  P  E. h  e.  P  ( <. <. A ,  B >. ,  <. C ,  D >. >.  =  <. <. a ,  b >. ,  <. c ,  d >. >.  /\  q  =  <. <. e ,  f
>. ,  <. g ,  h >. >.  /\  ps )  <->  E. d  e.  P  E. e  e.  P  E. f  e.  P  E. g  e.  P  E. h  e.  P  ( <. <. A ,  B >. ,  <. C ,  D >. >.  =  <. <. a ,  b >. ,  <. c ,  d >. >.  /\  <. <. E ,  F >. , 
<. G ,  H >. >.  =  <. <. e ,  f
>. ,  <. g ,  h >. >.  /\  ps )
) )
17162rexbidv 2770 . . . . 5  |-  ( q  =  <. <. E ,  F >. ,  <. G ,  H >. >.  ->  ( E. b  e.  P  E. c  e.  P  E. d  e.  P  E. e  e.  P  E. f  e.  P  E. g  e.  P  E. h  e.  P  ( <. <. A ,  B >. ,  <. C ,  D >. >.  =  <. <. a ,  b >. ,  <. c ,  d >. >.  /\  q  =  <. <. e ,  f
>. ,  <. g ,  h >. >.  /\  ps )  <->  E. b  e.  P  E. c  e.  P  E. d  e.  P  E. e  e.  P  E. f  e.  P  E. g  e.  P  E. h  e.  P  ( <. <. A ,  B >. ,  <. C ,  D >. >.  =  <. <. a ,  b >. ,  <. c ,  d >. >.  /\  <. <. E ,  F >. , 
<. G ,  H >. >.  =  <. <. e ,  f
>. ,  <. g ,  h >. >.  /\  ps )
) )
1817rexbidv 2748 . . . 4  |-  ( q  =  <. <. E ,  F >. ,  <. G ,  H >. >.  ->  ( E. a  e.  P  E. b  e.  P  E. c  e.  P  E. d  e.  P  E. e  e.  P  E. f  e.  P  E. g  e.  P  E. h  e.  P  ( <. <. A ,  B >. ,  <. C ,  D >. >.  =  <. <. a ,  b >. ,  <. c ,  d >. >.  /\  q  =  <. <. e ,  f
>. ,  <. g ,  h >. >.  /\  ps )  <->  E. a  e.  P  E. b  e.  P  E. c  e.  P  E. d  e.  P  E. e  e.  P  E. f  e.  P  E. g  e.  P  E. h  e.  P  ( <. <. A ,  B >. ,  <. C ,  D >. >.  =  <. <. a ,  b >. ,  <. c ,  d >. >.  /\  <. <. E ,  F >. , 
<. G ,  H >. >.  =  <. <. e ,  f
>. ,  <. g ,  h >. >.  /\  ps )
) )
19 eqid 2443 . . . 4  |-  { <. p ,  q >.  |  E. a  e.  P  E. b  e.  P  E. c  e.  P  E. d  e.  P  E. e  e.  P  E. f  e.  P  E. g  e.  P  E. h  e.  P  (
p  =  <. <. a ,  b >. ,  <. c ,  d >. >.  /\  q  =  <. <. e ,  f
>. ,  <. g ,  h >. >.  /\  ps ) }  =  { <. p ,  q >.  |  E. a  e.  P  E. b  e.  P  E. c  e.  P  E. d  e.  P  E. e  e.  P  E. f  e.  P  E. g  e.  P  E. h  e.  P  (
p  =  <. <. a ,  b >. ,  <. c ,  d >. >.  /\  q  =  <. <. e ,  f
>. ,  <. g ,  h >. >.  /\  ps ) }
203, 4, 11, 18, 19brab 4623 . . 3  |-  ( <. <. A ,  B >. , 
<. C ,  D >. >. { <. p ,  q
>.  |  E. a  e.  P  E. b  e.  P  E. c  e.  P  E. d  e.  P  E. e  e.  P  E. f  e.  P  E. g  e.  P  E. h  e.  P  ( p  =  <. <. a ,  b
>. ,  <. c ,  d >. >.  /\  q  =  <. <. e ,  f
>. ,  <. g ,  h >. >.  /\  ps ) } <. <. E ,  F >. ,  <. G ,  H >. >. 
<->  E. a  e.  P  E. b  e.  P  E. c  e.  P  E. d  e.  P  E. e  e.  P  E. f  e.  P  E. g  e.  P  E. h  e.  P  ( <. <. A ,  B >. ,  <. C ,  D >. >.  =  <. <. a ,  b >. ,  <. c ,  d >. >.  /\  <. <. E ,  F >. , 
<. G ,  H >. >.  =  <. <. e ,  f
>. ,  <. g ,  h >. >.  /\  ps )
)
212, 20syl6bb 261 . 2  |-  ( ph  ->  ( <. <. A ,  B >. ,  <. C ,  D >. >. R <. <. E ,  F >. ,  <. G ,  H >. >. 
<->  E. a  e.  P  E. b  e.  P  E. c  e.  P  E. d  e.  P  E. e  e.  P  E. f  e.  P  E. g  e.  P  E. h  e.  P  ( <. <. A ,  B >. ,  <. C ,  D >. >.  =  <. <. a ,  b >. ,  <. c ,  d >. >.  /\  <. <. E ,  F >. , 
<. G ,  H >. >.  =  <. <. e ,  f
>. ,  <. g ,  h >. >.  /\  ps )
) )
22 br8d.11 . . 3  |-  ( ph  ->  A  e.  P )
23 br8d.12 . . 3  |-  ( ph  ->  B  e.  P )
24 br8d.13 . . 3  |-  ( ph  ->  C  e.  P )
25 br8d.14 . . 3  |-  ( ph  ->  D  e.  P )
26 br8d.15 . . 3  |-  ( ph  ->  E  e.  P )
27 br8d.16 . . 3  |-  ( ph  ->  F  e.  P )
28 br8d.17 . . 3  |-  ( ph  ->  G  e.  P )
29 br8d.18 . . 3  |-  ( ph  ->  H  e.  P )
30 opex 4568 . . . . . . . . . . . . . . 15  |-  <. a ,  b >.  e.  _V
31 opex 4568 . . . . . . . . . . . . . . 15  |-  <. c ,  d >.  e.  _V
3230, 31opth 4578 . . . . . . . . . . . . . 14  |-  ( <. <. a ,  b >. ,  <. c ,  d
>. >.  =  <. <. A ,  B >. ,  <. C ,  D >. >. 
<->  ( <. a ,  b
>.  =  <. A ,  B >.  /\  <. c ,  d >.  =  <. C ,  D >. )
)
33 vex 2987 . . . . . . . . . . . . . . . . 17  |-  a  e. 
_V
34 vex 2987 . . . . . . . . . . . . . . . . 17  |-  b  e. 
_V
3533, 34opth 4578 . . . . . . . . . . . . . . . 16  |-  ( <.
a ,  b >.  =  <. A ,  B >.  <-> 
( a  =  A  /\  b  =  B ) )
36 br8d.1 . . . . . . . . . . . . . . . . 17  |-  ( a  =  A  ->  ( ps 
<->  ch ) )
37 br8d.2 . . . . . . . . . . . . . . . . 17  |-  ( b  =  B  ->  ( ch 
<->  th ) )
3836, 37sylan9bb 699 . . . . . . . . . . . . . . . 16  |-  ( ( a  =  A  /\  b  =  B )  ->  ( ps  <->  th )
)
3935, 38sylbi 195 . . . . . . . . . . . . . . 15  |-  ( <.
a ,  b >.  =  <. A ,  B >.  ->  ( ps  <->  th )
)
40 vex 2987 . . . . . . . . . . . . . . . . 17  |-  c  e. 
_V
41 vex 2987 . . . . . . . . . . . . . . . . 17  |-  d  e. 
_V
4240, 41opth 4578 . . . . . . . . . . . . . . . 16  |-  ( <.
c ,  d >.  =  <. C ,  D >.  <-> 
( c  =  C  /\  d  =  D ) )
43 br8d.3 . . . . . . . . . . . . . . . . 17  |-  ( c  =  C  ->  ( th 
<->  ta ) )
44 br8d.4 . . . . . . . . . . . . . . . . 17  |-  ( d  =  D  ->  ( ta 
<->  et ) )
4543, 44sylan9bb 699 . . . . . . . . . . . . . . . 16  |-  ( ( c  =  C  /\  d  =  D )  ->  ( th  <->  et )
)
4642, 45sylbi 195 . . . . . . . . . . . . . . 15  |-  ( <.
c ,  d >.  =  <. C ,  D >.  ->  ( th  <->  et )
)
4739, 46sylan9bb 699 . . . . . . . . . . . . . 14  |-  ( (
<. a ,  b >.  =  <. A ,  B >.  /\  <. c ,  d
>.  =  <. C ,  D >. )  ->  ( ps 
<->  et ) )
4832, 47sylbi 195 . . . . . . . . . . . . 13  |-  ( <. <. a ,  b >. ,  <. c ,  d
>. >.  =  <. <. A ,  B >. ,  <. C ,  D >. >.  ->  ( ps  <->  et ) )
4948eqcoms 2446 . . . . . . . . . . . 12  |-  ( <. <. A ,  B >. , 
<. C ,  D >. >.  =  <. <. a ,  b
>. ,  <. c ,  d >. >.  ->  ( ps  <->  et ) )
50 opex 4568 . . . . . . . . . . . . . . 15  |-  <. e ,  f >.  e.  _V
51 opex 4568 . . . . . . . . . . . . . . 15  |-  <. g ,  h >.  e.  _V
5250, 51opth 4578 . . . . . . . . . . . . . 14  |-  ( <. <. e ,  f >. ,  <. g ,  h >. >.  =  <. <. E ,  F >. ,  <. G ,  H >. >. 
<->  ( <. e ,  f
>.  =  <. E ,  F >.  /\  <. g ,  h >.  =  <. G ,  H >. )
)
53 vex 2987 . . . . . . . . . . . . . . . . 17  |-  e  e. 
_V
54 vex 2987 . . . . . . . . . . . . . . . . 17  |-  f  e. 
_V
5553, 54opth 4578 . . . . . . . . . . . . . . . 16  |-  ( <.
e ,  f >.  =  <. E ,  F >.  <-> 
( e  =  E  /\  f  =  F ) )
56 br8d.5 . . . . . . . . . . . . . . . . 17  |-  ( e  =  E  ->  ( et 
<->  ze ) )
57 br8d.6 . . . . . . . . . . . . . . . . 17  |-  ( f  =  F  ->  ( ze 
<-> 
si ) )
5856, 57sylan9bb 699 . . . . . . . . . . . . . . . 16  |-  ( ( e  =  E  /\  f  =  F )  ->  ( et  <->  si )
)
5955, 58sylbi 195 . . . . . . . . . . . . . . 15  |-  ( <.
e ,  f >.  =  <. E ,  F >.  ->  ( et  <->  si )
)
60 vex 2987 . . . . . . . . . . . . . . . . 17  |-  g  e. 
_V
61 vex 2987 . . . . . . . . . . . . . . . . 17  |-  h  e. 
_V
6260, 61opth 4578 . . . . . . . . . . . . . . . 16  |-  ( <.
g ,  h >.  = 
<. G ,  H >.  <->  (
g  =  G  /\  h  =  H )
)
63 br8d.7 . . . . . . . . . . . . . . . . 17  |-  ( g  =  G  ->  ( si 
<->  rh ) )
64 br8d.8 . . . . . . . . . . . . . . . . 17  |-  ( h  =  H  ->  ( rh 
<->  mu ) )
6563, 64sylan9bb 699 . . . . . . . . . . . . . . . 16  |-  ( ( g  =  G  /\  h  =  H )  ->  ( si  <->  mu )
)
6662, 65sylbi 195 . . . . . . . . . . . . . . 15  |-  ( <.
g ,  h >.  = 
<. G ,  H >.  -> 
( si  <->  mu ) )
6759, 66sylan9bb 699 . . . . . . . . . . . . . 14  |-  ( (
<. e ,  f >.  =  <. E ,  F >.  /\  <. g ,  h >.  =  <. G ,  H >. )  ->  ( et  <->  mu ) )
6852, 67sylbi 195 . . . . . . . . . . . . 13  |-  ( <. <. e ,  f >. ,  <. g ,  h >. >.  =  <. <. E ,  F >. ,  <. G ,  H >. >.  ->  ( et  <->  mu ) )
6968eqcoms 2446 . . . . . . . . . . . 12  |-  ( <. <. E ,  F >. , 
<. G ,  H >. >.  =  <. <. e ,  f
>. ,  <. g ,  h >. >.  ->  ( et  <->  mu ) )
7049, 69sylan9bb 699 . . . . . . . . . . 11  |-  ( (
<. <. A ,  B >. ,  <. C ,  D >. >.  =  <. <. a ,  b >. ,  <. c ,  d >. >.  /\  <. <. E ,  F >. , 
<. G ,  H >. >.  =  <. <. e ,  f
>. ,  <. g ,  h >. >. )  ->  ( ps 
<->  mu ) )
7170biimp3a 1318 . . . . . . . . . 10  |-  ( (
<. <. A ,  B >. ,  <. C ,  D >. >.  =  <. <. a ,  b >. ,  <. c ,  d >. >.  /\  <. <. E ,  F >. , 
<. G ,  H >. >.  =  <. <. e ,  f
>. ,  <. g ,  h >. >.  /\  ps )  ->  mu )
7271a1i 11 . . . . . . . . 9  |-  ( ( ( ( ( ( ( ( A  e.  P  /\  B  e.  P )  /\  ( C  e.  P  /\  D  e.  P  /\  E  e.  P )  /\  ( F  e.  P  /\  G  e.  P  /\  H  e.  P
) )  /\  a  e.  P )  /\  (
b  e.  P  /\  c  e.  P )
)  /\  ( d  e.  P  /\  e  e.  P ) )  /\  ( f  e.  P  /\  g  e.  P
) )  /\  h  e.  P )  ->  (
( <. <. A ,  B >. ,  <. C ,  D >. >.  =  <. <. a ,  b >. ,  <. c ,  d >. >.  /\  <. <. E ,  F >. , 
<. G ,  H >. >.  =  <. <. e ,  f
>. ,  <. g ,  h >. >.  /\  ps )  ->  mu ) )
7372rexlimdva 2853 . . . . . . . 8  |-  ( ( ( ( ( ( ( A  e.  P  /\  B  e.  P
)  /\  ( C  e.  P  /\  D  e.  P  /\  E  e.  P )  /\  ( F  e.  P  /\  G  e.  P  /\  H  e.  P )
)  /\  a  e.  P )  /\  (
b  e.  P  /\  c  e.  P )
)  /\  ( d  e.  P  /\  e  e.  P ) )  /\  ( f  e.  P  /\  g  e.  P
) )  ->  ( E. h  e.  P  ( <. <. A ,  B >. ,  <. C ,  D >. >.  =  <. <. a ,  b >. ,  <. c ,  d >. >.  /\  <. <. E ,  F >. , 
<. G ,  H >. >.  =  <. <. e ,  f
>. ,  <. g ,  h >. >.  /\  ps )  ->  mu ) )
7473rexlimdvva 2860 . . . . . . 7  |-  ( ( ( ( ( ( A  e.  P  /\  B  e.  P )  /\  ( C  e.  P  /\  D  e.  P  /\  E  e.  P
)  /\  ( F  e.  P  /\  G  e.  P  /\  H  e.  P ) )  /\  a  e.  P )  /\  ( b  e.  P  /\  c  e.  P
) )  /\  (
d  e.  P  /\  e  e.  P )
)  ->  ( E. f  e.  P  E. g  e.  P  E. h  e.  P  ( <. <. A ,  B >. ,  <. C ,  D >. >.  =  <. <. a ,  b >. ,  <. c ,  d >. >.  /\  <. <. E ,  F >. , 
<. G ,  H >. >.  =  <. <. e ,  f
>. ,  <. g ,  h >. >.  /\  ps )  ->  mu ) )
7574rexlimdvva 2860 . . . . . 6  |-  ( ( ( ( ( A  e.  P  /\  B  e.  P )  /\  ( C  e.  P  /\  D  e.  P  /\  E  e.  P )  /\  ( F  e.  P  /\  G  e.  P  /\  H  e.  P
) )  /\  a  e.  P )  /\  (
b  e.  P  /\  c  e.  P )
)  ->  ( E. d  e.  P  E. e  e.  P  E. f  e.  P  E. g  e.  P  E. h  e.  P  ( <. <. A ,  B >. ,  <. C ,  D >. >.  =  <. <. a ,  b >. ,  <. c ,  d >. >.  /\  <. <. E ,  F >. , 
<. G ,  H >. >.  =  <. <. e ,  f
>. ,  <. g ,  h >. >.  /\  ps )  ->  mu ) )
7675rexlimdvva 2860 . . . . 5  |-  ( ( ( ( A  e.  P  /\  B  e.  P )  /\  ( C  e.  P  /\  D  e.  P  /\  E  e.  P )  /\  ( F  e.  P  /\  G  e.  P  /\  H  e.  P
) )  /\  a  e.  P )  ->  ( E. b  e.  P  E. c  e.  P  E. d  e.  P  E. e  e.  P  E. f  e.  P  E. g  e.  P  E. h  e.  P  ( <. <. A ,  B >. ,  <. C ,  D >. >.  =  <. <. a ,  b >. ,  <. c ,  d >. >.  /\  <. <. E ,  F >. , 
<. G ,  H >. >.  =  <. <. e ,  f
>. ,  <. g ,  h >. >.  /\  ps )  ->  mu ) )
7776rexlimdva 2853 . . . 4  |-  ( ( ( A  e.  P  /\  B  e.  P
)  /\  ( C  e.  P  /\  D  e.  P  /\  E  e.  P )  /\  ( F  e.  P  /\  G  e.  P  /\  H  e.  P )
)  ->  ( E. a  e.  P  E. b  e.  P  E. c  e.  P  E. d  e.  P  E. e  e.  P  E. f  e.  P  E. g  e.  P  E. h  e.  P  ( <. <. A ,  B >. ,  <. C ,  D >. >.  =  <. <. a ,  b >. ,  <. c ,  d >. >.  /\  <. <. E ,  F >. , 
<. G ,  H >. >.  =  <. <. e ,  f
>. ,  <. g ,  h >. >.  /\  ps )  ->  mu ) )
78 simpl1l 1039 . . . . . 6  |-  ( ( ( ( A  e.  P  /\  B  e.  P )  /\  ( C  e.  P  /\  D  e.  P  /\  E  e.  P )  /\  ( F  e.  P  /\  G  e.  P  /\  H  e.  P
) )  /\  mu )  ->  A  e.  P
)
79 simpl1r 1040 . . . . . 6  |-  ( ( ( ( A  e.  P  /\  B  e.  P )  /\  ( C  e.  P  /\  D  e.  P  /\  E  e.  P )  /\  ( F  e.  P  /\  G  e.  P  /\  H  e.  P
) )  /\  mu )  ->  B  e.  P
)
80 simpl21 1066 . . . . . 6  |-  ( ( ( ( A  e.  P  /\  B  e.  P )  /\  ( C  e.  P  /\  D  e.  P  /\  E  e.  P )  /\  ( F  e.  P  /\  G  e.  P  /\  H  e.  P
) )  /\  mu )  ->  C  e.  P
)
81 simpl22 1067 . . . . . . 7  |-  ( ( ( ( A  e.  P  /\  B  e.  P )  /\  ( C  e.  P  /\  D  e.  P  /\  E  e.  P )  /\  ( F  e.  P  /\  G  e.  P  /\  H  e.  P
) )  /\  mu )  ->  D  e.  P
)
82 simpl23 1068 . . . . . . 7  |-  ( ( ( ( A  e.  P  /\  B  e.  P )  /\  ( C  e.  P  /\  D  e.  P  /\  E  e.  P )  /\  ( F  e.  P  /\  G  e.  P  /\  H  e.  P
) )  /\  mu )  ->  E  e.  P
)
83 simpl31 1069 . . . . . . 7  |-  ( ( ( ( A  e.  P  /\  B  e.  P )  /\  ( C  e.  P  /\  D  e.  P  /\  E  e.  P )  /\  ( F  e.  P  /\  G  e.  P  /\  H  e.  P
) )  /\  mu )  ->  F  e.  P
)
84 simpl32 1070 . . . . . . . 8  |-  ( ( ( ( A  e.  P  /\  B  e.  P )  /\  ( C  e.  P  /\  D  e.  P  /\  E  e.  P )  /\  ( F  e.  P  /\  G  e.  P  /\  H  e.  P
) )  /\  mu )  ->  G  e.  P
)
85 simpl33 1071 . . . . . . . 8  |-  ( ( ( ( A  e.  P  /\  B  e.  P )  /\  ( C  e.  P  /\  D  e.  P  /\  E  e.  P )  /\  ( F  e.  P  /\  G  e.  P  /\  H  e.  P
) )  /\  mu )  ->  H  e.  P
)
86 eqidd 2444 . . . . . . . 8  |-  ( ( ( ( A  e.  P  /\  B  e.  P )  /\  ( C  e.  P  /\  D  e.  P  /\  E  e.  P )  /\  ( F  e.  P  /\  G  e.  P  /\  H  e.  P
) )  /\  mu )  ->  <. <. A ,  B >. ,  <. C ,  D >. >.  =  <. <. A ,  B >. ,  <. C ,  D >. >. )
87 eqidd 2444 . . . . . . . 8  |-  ( ( ( ( A  e.  P  /\  B  e.  P )  /\  ( C  e.  P  /\  D  e.  P  /\  E  e.  P )  /\  ( F  e.  P  /\  G  e.  P  /\  H  e.  P
) )  /\  mu )  ->  <. <. E ,  F >. ,  <. G ,  H >. >.  =  <. <. E ,  F >. ,  <. G ,  H >. >. )
88 simpr 461 . . . . . . . 8  |-  ( ( ( ( A  e.  P  /\  B  e.  P )  /\  ( C  e.  P  /\  D  e.  P  /\  E  e.  P )  /\  ( F  e.  P  /\  G  e.  P  /\  H  e.  P
) )  /\  mu )  ->  mu )
89 opeq1 4071 . . . . . . . . . . . 12  |-  ( g  =  G  ->  <. g ,  h >.  =  <. G ,  h >. )
9089opeq2d 4078 . . . . . . . . . . 11  |-  ( g  =  G  ->  <. <. E ,  F >. ,  <. g ,  h >. >.  =  <. <. E ,  F >. ,  <. G ,  h >. >. )
9190eqeq2d 2454 . . . . . . . . . 10  |-  ( g  =  G  ->  ( <. <. E ,  F >. ,  <. G ,  H >. >.  =  <. <. E ,  F >. ,  <. g ,  h >. >. 
<-> 
<. <. E ,  F >. ,  <. G ,  H >. >.  =  <. <. E ,  F >. ,  <. G ,  h >. >. ) )
9291, 633anbi23d 1292 . . . . . . . . 9  |-  ( g  =  G  ->  (
( <. <. A ,  B >. ,  <. C ,  D >. >.  =  <. <. A ,  B >. ,  <. C ,  D >. >.  /\  <. <. E ,  F >. ,  <. G ,  H >. >.  =  <. <. E ,  F >. ,  <. g ,  h >. >.  /\  si )  <->  (
<. <. A ,  B >. ,  <. C ,  D >. >.  =  <. <. A ,  B >. ,  <. C ,  D >. >.  /\  <. <. E ,  F >. ,  <. G ,  H >. >.  =  <. <. E ,  F >. ,  <. G ,  h >. >.  /\  rh )
) )
93 opeq2 4072 . . . . . . . . . . . 12  |-  ( h  =  H  ->  <. G ,  h >.  =  <. G ,  H >. )
9493opeq2d 4078 . . . . . . . . . . 11  |-  ( h  =  H  ->  <. <. E ,  F >. ,  <. G ,  h >. >.  =  <. <. E ,  F >. ,  <. G ,  H >. >. )
9594eqeq2d 2454 . . . . . . . . . 10  |-  ( h  =  H  ->  ( <. <. E ,  F >. ,  <. G ,  H >. >.  =  <. <. E ,  F >. ,  <. G ,  h >. >. 
<-> 
<. <. E ,  F >. ,  <. G ,  H >. >.  =  <. <. E ,  F >. ,  <. G ,  H >. >. ) )
9695, 643anbi23d 1292 . . . . . . . . 9  |-  ( h  =  H  ->  (
( <. <. A ,  B >. ,  <. C ,  D >. >.  =  <. <. A ,  B >. ,  <. C ,  D >. >.  /\  <. <. E ,  F >. ,  <. G ,  H >. >.  =  <. <. E ,  F >. ,  <. G ,  h >. >.  /\  rh )  <->  (
<. <. A ,  B >. ,  <. C ,  D >. >.  =  <. <. A ,  B >. ,  <. C ,  D >. >.  /\  <. <. E ,  F >. ,  <. G ,  H >. >.  =  <. <. E ,  F >. ,  <. G ,  H >. >.  /\  mu )
) )
9792, 96rspc2ev 3093 . . . . . . . 8  |-  ( ( G  e.  P  /\  H  e.  P  /\  ( <. <. A ,  B >. ,  <. C ,  D >. >.  =  <. <. A ,  B >. ,  <. C ,  D >. >.  /\  <. <. E ,  F >. ,  <. G ,  H >. >.  =  <. <. E ,  F >. ,  <. G ,  H >. >.  /\  mu )
)  ->  E. g  e.  P  E. h  e.  P  ( <. <. A ,  B >. , 
<. C ,  D >. >.  =  <. <. A ,  B >. ,  <. C ,  D >. >.  /\  <. <. E ,  F >. ,  <. G ,  H >. >.  =  <. <. E ,  F >. ,  <. g ,  h >. >.  /\  si )
)
9884, 85, 86, 87, 88, 97syl113anc 1230 . . . . . . 7  |-  ( ( ( ( A  e.  P  /\  B  e.  P )  /\  ( C  e.  P  /\  D  e.  P  /\  E  e.  P )  /\  ( F  e.  P  /\  G  e.  P  /\  H  e.  P
) )  /\  mu )  ->  E. g  e.  P  E. h  e.  P  ( <. <. A ,  B >. ,  <. C ,  D >. >.  =  <. <. A ,  B >. ,  <. C ,  D >. >.  /\  <. <. E ,  F >. ,  <. G ,  H >. >.  =  <. <. E ,  F >. ,  <. g ,  h >. >.  /\  si )
)
99 opeq2 4072 . . . . . . . . . . . 12  |-  ( d  =  D  ->  <. C , 
d >.  =  <. C ,  D >. )
10099opeq2d 4078 . . . . . . . . . . 11  |-  ( d  =  D  ->  <. <. A ,  B >. ,  <. C , 
d >. >.  =  <. <. A ,  B >. ,  <. C ,  D >. >. )
101100eqeq2d 2454 . . . . . . . . . 10  |-  ( d  =  D  ->  ( <. <. A ,  B >. ,  <. C ,  D >. >.  =  <. <. A ,  B >. ,  <. C , 
d >. >. 
<-> 
<. <. A ,  B >. ,  <. C ,  D >. >.  =  <. <. A ,  B >. ,  <. C ,  D >. >. ) )
102101, 443anbi13d 1291 . . . . . . . . 9  |-  ( d  =  D  ->  (
( <. <. A ,  B >. ,  <. C ,  D >. >.  =  <. <. A ,  B >. ,  <. C , 
d >. >.  /\  <. <. E ,  F >. ,  <. G ,  H >. >.  =  <. <. e ,  f >. ,  <. g ,  h >. >.  /\  ta ) 
<->  ( <. <. A ,  B >. ,  <. C ,  D >. >.  =  <. <. A ,  B >. ,  <. C ,  D >. >.  /\  <. <. E ,  F >. ,  <. G ,  H >. >.  =  <. <. e ,  f >. ,  <. g ,  h >. >.  /\  et ) ) )
1031022rexbidv 2770 . . . . . . . 8  |-  ( d  =  D  ->  ( E. g  e.  P  E. h  e.  P  ( <. <. A ,  B >. ,  <. C ,  D >. >.  =  <. <. A ,  B >. ,  <. C , 
d >. >.  /\  <. <. E ,  F >. ,  <. G ,  H >. >.  =  <. <. e ,  f >. ,  <. g ,  h >. >.  /\  ta ) 
<->  E. g  e.  P  E. h  e.  P  ( <. <. A ,  B >. ,  <. C ,  D >. >.  =  <. <. A ,  B >. ,  <. C ,  D >. >.  /\  <. <. E ,  F >. ,  <. G ,  H >. >.  =  <. <. e ,  f >. ,  <. g ,  h >. >.  /\  et ) ) )
104 opeq1 4071 . . . . . . . . . . . 12  |-  ( e  =  E  ->  <. e ,  f >.  =  <. E ,  f >. )
105104opeq1d 4077 . . . . . . . . . . 11  |-  ( e  =  E  ->  <. <. e ,  f >. ,  <. g ,  h >. >.  =  <. <. E ,  f >. , 
<. g ,  h >. >.
)
106105eqeq2d 2454 . . . . . . . . . 10  |-  ( e  =  E  ->  ( <. <. E ,  F >. ,  <. G ,  H >. >.  =  <. <. e ,  f >. ,  <. g ,  h >. >.  <->  <. <. E ,  F >. ,  <. G ,  H >. >.  =  <. <. E , 
f >. ,  <. g ,  h >. >. ) )
107106, 563anbi23d 1292 . . . . . . . . 9  |-  ( e  =  E  ->  (
( <. <. A ,  B >. ,  <. C ,  D >. >.  =  <. <. A ,  B >. ,  <. C ,  D >. >.  /\  <. <. E ,  F >. ,  <. G ,  H >. >.  =  <. <. e ,  f >. ,  <. g ,  h >. >.  /\  et ) 
<->  ( <. <. A ,  B >. ,  <. C ,  D >. >.  =  <. <. A ,  B >. ,  <. C ,  D >. >.  /\  <. <. E ,  F >. ,  <. G ,  H >. >.  =  <. <. E , 
f >. ,  <. g ,  h >. >.  /\  ze )
) )
1081072rexbidv 2770 . . . . . . . 8  |-  ( e  =  E  ->  ( E. g  e.  P  E. h  e.  P  ( <. <. A ,  B >. ,  <. C ,  D >. >.  =  <. <. A ,  B >. ,  <. C ,  D >. >.  /\  <. <. E ,  F >. ,  <. G ,  H >. >.  =  <. <. e ,  f >. ,  <. g ,  h >. >.  /\  et ) 
<->  E. g  e.  P  E. h  e.  P  ( <. <. A ,  B >. ,  <. C ,  D >. >.  =  <. <. A ,  B >. ,  <. C ,  D >. >.  /\  <. <. E ,  F >. ,  <. G ,  H >. >.  =  <. <. E , 
f >. ,  <. g ,  h >. >.  /\  ze )
) )
109 opeq2 4072 . . . . . . . . . . . 12  |-  ( f  =  F  ->  <. E , 
f >.  =  <. E ,  F >. )
110109opeq1d 4077 . . . . . . . . . . 11  |-  ( f  =  F  ->  <. <. E , 
f >. ,  <. g ,  h >. >.  =  <. <. E ,  F >. ,  <. g ,  h >. >. )
111110eqeq2d 2454 . . . . . . . . . 10  |-  ( f  =  F  ->  ( <. <. E ,  F >. ,  <. G ,  H >. >.  =  <. <. E , 
f >. ,  <. g ,  h >. >. 
<-> 
<. <. E ,  F >. ,  <. G ,  H >. >.  =  <. <. E ,  F >. ,  <. g ,  h >. >. ) )
112111, 573anbi23d 1292 . . . . . . . . 9  |-  ( f  =  F  ->  (
( <. <. A ,  B >. ,  <. C ,  D >. >.  =  <. <. A ,  B >. ,  <. C ,  D >. >.  /\  <. <. E ,  F >. ,  <. G ,  H >. >.  =  <. <. E , 
f >. ,  <. g ,  h >. >.  /\  ze )  <->  (
<. <. A ,  B >. ,  <. C ,  D >. >.  =  <. <. A ,  B >. ,  <. C ,  D >. >.  /\  <. <. E ,  F >. ,  <. G ,  H >. >.  =  <. <. E ,  F >. ,  <. g ,  h >. >.  /\  si )
) )
1131122rexbidv 2770 . . . . . . . 8  |-  ( f  =  F  ->  ( E. g  e.  P  E. h  e.  P  ( <. <. A ,  B >. ,  <. C ,  D >. >.  =  <. <. A ,  B >. ,  <. C ,  D >. >.  /\  <. <. E ,  F >. ,  <. G ,  H >. >.  =  <. <. E , 
f >. ,  <. g ,  h >. >.  /\  ze )  <->  E. g  e.  P  E. h  e.  P  ( <. <. A ,  B >. ,  <. C ,  D >. >.  =  <. <. A ,  B >. ,  <. C ,  D >. >.  /\  <. <. E ,  F >. ,  <. G ,  H >. >.  =  <. <. E ,  F >. ,  <. g ,  h >. >.  /\  si )
) )
114103, 108, 113rspc3ev 3095 . . . . . . 7  |-  ( ( ( D  e.  P  /\  E  e.  P  /\  F  e.  P
)  /\  E. g  e.  P  E. h  e.  P  ( <. <. A ,  B >. , 
<. C ,  D >. >.  =  <. <. A ,  B >. ,  <. C ,  D >. >.  /\  <. <. E ,  F >. ,  <. G ,  H >. >.  =  <. <. E ,  F >. ,  <. g ,  h >. >.  /\  si )
)  ->  E. d  e.  P  E. e  e.  P  E. f  e.  P  E. g  e.  P  E. h  e.  P  ( <. <. A ,  B >. , 
<. C ,  D >. >.  =  <. <. A ,  B >. ,  <. C ,  d
>. >.  /\  <. <. E ,  F >. ,  <. G ,  H >. >.  =  <. <. e ,  f >. ,  <. g ,  h >. >.  /\  ta ) )
11581, 82, 83, 98, 114syl31anc 1221 . . . . . 6  |-  ( ( ( ( A  e.  P  /\  B  e.  P )  /\  ( C  e.  P  /\  D  e.  P  /\  E  e.  P )  /\  ( F  e.  P  /\  G  e.  P  /\  H  e.  P
) )  /\  mu )  ->  E. d  e.  P  E. e  e.  P  E. f  e.  P  E. g  e.  P  E. h  e.  P  ( <. <. A ,  B >. ,  <. C ,  D >. >.  =  <. <. A ,  B >. ,  <. C , 
d >. >.  /\  <. <. E ,  F >. ,  <. G ,  H >. >.  =  <. <. e ,  f >. ,  <. g ,  h >. >.  /\  ta ) )
116 opeq1 4071 . . . . . . . . . . . . 13  |-  ( a  =  A  ->  <. a ,  b >.  =  <. A ,  b >. )
117116opeq1d 4077 . . . . . . . . . . . 12  |-  ( a  =  A  ->  <. <. a ,  b >. ,  <. c ,  d >. >.  =  <. <. A ,  b >. , 
<. c ,  d >. >. )
118117eqeq2d 2454 . . . . . . . . . . 11  |-  ( a  =  A  ->  ( <. <. A ,  B >. ,  <. C ,  D >. >.  =  <. <. a ,  b >. ,  <. c ,  d >. >.  <->  <. <. A ,  B >. ,  <. C ,  D >. >.  =  <. <. A , 
b >. ,  <. c ,  d >. >. )
)
119118, 363anbi13d 1291 . . . . . . . . . 10  |-  ( a  =  A  ->  (
( <. <. A ,  B >. ,  <. C ,  D >. >.  =  <. <. a ,  b >. ,  <. c ,  d >. >.  /\  <. <. E ,  F >. , 
<. G ,  H >. >.  =  <. <. e ,  f
>. ,  <. g ,  h >. >.  /\  ps )  <->  (
<. <. A ,  B >. ,  <. C ,  D >. >.  =  <. <. A , 
b >. ,  <. c ,  d >. >.  /\  <. <. E ,  F >. , 
<. G ,  H >. >.  =  <. <. e ,  f
>. ,  <. g ,  h >. >.  /\  ch )
) )
120119rexbidv 2748 . . . . . . . . 9  |-  ( a  =  A  ->  ( E. h  e.  P  ( <. <. A ,  B >. ,  <. C ,  D >. >.  =  <. <. a ,  b >. ,  <. c ,  d >. >.  /\  <. <. E ,  F >. , 
<. G ,  H >. >.  =  <. <. e ,  f
>. ,  <. g ,  h >. >.  /\  ps )  <->  E. h  e.  P  (
<. <. A ,  B >. ,  <. C ,  D >. >.  =  <. <. A , 
b >. ,  <. c ,  d >. >.  /\  <. <. E ,  F >. , 
<. G ,  H >. >.  =  <. <. e ,  f
>. ,  <. g ,  h >. >.  /\  ch )
) )
1211202rexbidv 2770 . . . . . . . 8  |-  ( a  =  A  ->  ( E. f  e.  P  E. g  e.  P  E. h  e.  P  ( <. <. A ,  B >. ,  <. C ,  D >. >.  =  <. <. a ,  b >. ,  <. c ,  d >. >.  /\  <. <. E ,  F >. , 
<. G ,  H >. >.  =  <. <. e ,  f
>. ,  <. g ,  h >. >.  /\  ps )  <->  E. f  e.  P  E. g  e.  P  E. h  e.  P  ( <. <. A ,  B >. ,  <. C ,  D >. >.  =  <. <. A , 
b >. ,  <. c ,  d >. >.  /\  <. <. E ,  F >. , 
<. G ,  H >. >.  =  <. <. e ,  f
>. ,  <. g ,  h >. >.  /\  ch )
) )
1221212rexbidv 2770 . . . . . . 7  |-  ( a  =  A  ->  ( E. d  e.  P  E. e  e.  P  E. f  e.  P  E. g  e.  P  E. h  e.  P  ( <. <. A ,  B >. ,  <. C ,  D >. >.  =  <. <. a ,  b >. ,  <. c ,  d >. >.  /\  <. <. E ,  F >. , 
<. G ,  H >. >.  =  <. <. e ,  f
>. ,  <. g ,  h >. >.  /\  ps )  <->  E. d  e.  P  E. e  e.  P  E. f  e.  P  E. g  e.  P  E. h  e.  P  ( <. <. A ,  B >. ,  <. C ,  D >. >.  =  <. <. A , 
b >. ,  <. c ,  d >. >.  /\  <. <. E ,  F >. , 
<. G ,  H >. >.  =  <. <. e ,  f
>. ,  <. g ,  h >. >.  /\  ch )
) )
123 opeq2 4072 . . . . . . . . . . . . 13  |-  ( b  =  B  ->  <. A , 
b >.  =  <. A ,  B >. )
124123opeq1d 4077 . . . . . . . . . . . 12  |-  ( b  =  B  ->  <. <. A , 
b >. ,  <. c ,  d >. >.  =  <. <. A ,  B >. , 
<. c ,  d >. >. )
125124eqeq2d 2454 . . . . . . . . . . 11  |-  ( b  =  B  ->  ( <. <. A ,  B >. ,  <. C ,  D >. >.  =  <. <. A , 
b >. ,  <. c ,  d >. >.  <->  <. <. A ,  B >. ,  <. C ,  D >. >.  =  <. <. A ,  B >. ,  <. c ,  d >. >. )
)
126125, 373anbi13d 1291 . . . . . . . . . 10  |-  ( b  =  B  ->  (
( <. <. A ,  B >. ,  <. C ,  D >. >.  =  <. <. A , 
b >. ,  <. c ,  d >. >.  /\  <. <. E ,  F >. , 
<. G ,  H >. >.  =  <. <. e ,  f
>. ,  <. g ,  h >. >.  /\  ch )  <->  (
<. <. A ,  B >. ,  <. C ,  D >. >.  =  <. <. A ,  B >. ,  <. c ,  d >. >.  /\  <. <. E ,  F >. , 
<. G ,  H >. >.  =  <. <. e ,  f
>. ,  <. g ,  h >. >.  /\  th )
) )
127126rexbidv 2748 . . . . . . . . 9  |-  ( b  =  B  ->  ( E. h  e.  P  ( <. <. A ,  B >. ,  <. C ,  D >. >.  =  <. <. A , 
b >. ,  <. c ,  d >. >.  /\  <. <. E ,  F >. , 
<. G ,  H >. >.  =  <. <. e ,  f
>. ,  <. g ,  h >. >.  /\  ch )  <->  E. h  e.  P  (
<. <. A ,  B >. ,  <. C ,  D >. >.  =  <. <. A ,  B >. ,  <. c ,  d >. >.  /\  <. <. E ,  F >. , 
<. G ,  H >. >.  =  <. <. e ,  f
>. ,  <. g ,  h >. >.  /\  th )
) )
1281272rexbidv 2770 . . . . . . . 8  |-  ( b  =  B  ->  ( E. f  e.  P  E. g  e.  P  E. h  e.  P  ( <. <. A ,  B >. ,  <. C ,  D >. >.  =  <. <. A , 
b >. ,  <. c ,  d >. >.  /\  <. <. E ,  F >. , 
<. G ,  H >. >.  =  <. <. e ,  f
>. ,  <. g ,  h >. >.  /\  ch )  <->  E. f  e.  P  E. g  e.  P  E. h  e.  P  ( <. <. A ,  B >. ,  <. C ,  D >. >.  =  <. <. A ,  B >. ,  <. c ,  d >. >.  /\  <. <. E ,  F >. , 
<. G ,  H >. >.  =  <. <. e ,  f
>. ,  <. g ,  h >. >.  /\  th )
) )
1291282rexbidv 2770 . . . . . . 7  |-  ( b  =  B  ->  ( E. d  e.  P  E. e  e.  P  E. f  e.  P  E. g  e.  P  E. h  e.  P  ( <. <. A ,  B >. ,  <. C ,  D >. >.  =  <. <. A , 
b >. ,  <. c ,  d >. >.  /\  <. <. E ,  F >. , 
<. G ,  H >. >.  =  <. <. e ,  f
>. ,  <. g ,  h >. >.  /\  ch )  <->  E. d  e.  P  E. e  e.  P  E. f  e.  P  E. g  e.  P  E. h  e.  P  ( <. <. A ,  B >. ,  <. C ,  D >. >.  =  <. <. A ,  B >. ,  <. c ,  d >. >.  /\  <. <. E ,  F >. , 
<. G ,  H >. >.  =  <. <. e ,  f
>. ,  <. g ,  h >. >.  /\  th )
) )
130 opeq1 4071 . . . . . . . . . . . . 13  |-  ( c  =  C  ->  <. c ,  d >.  =  <. C ,  d >. )
131130opeq2d 4078 . . . . . . . . . . . 12  |-  ( c  =  C  ->  <. <. A ,  B >. ,  <. c ,  d >. >.  =  <. <. A ,  B >. , 
<. C ,  d >. >. )
132131eqeq2d 2454 . . . . . . . . . . 11  |-  ( c  =  C  ->  ( <. <. A ,  B >. ,  <. C ,  D >. >.  =  <. <. A ,  B >. ,  <. c ,  d >. >.  <->  <. <. A ,  B >. ,  <. C ,  D >. >.  =  <. <. A ,  B >. ,  <. C , 
d >. >. ) )
133132, 433anbi13d 1291 . . . . . . . . . 10  |-  ( c  =  C  ->  (
( <. <. A ,  B >. ,  <. C ,  D >. >.  =  <. <. A ,  B >. ,  <. c ,  d >. >.  /\  <. <. E ,  F >. , 
<. G ,  H >. >.  =  <. <. e ,  f
>. ,  <. g ,  h >. >.  /\  th )  <->  (
<. <. A ,  B >. ,  <. C ,  D >. >.  =  <. <. A ,  B >. ,  <. C , 
d >. >.  /\  <. <. E ,  F >. ,  <. G ,  H >. >.  =  <. <. e ,  f >. ,  <. g ,  h >. >.  /\  ta ) ) )
134133rexbidv 2748 . . . . . . . . 9  |-  ( c  =  C  ->  ( E. h  e.  P  ( <. <. A ,  B >. ,  <. C ,  D >. >.  =  <. <. A ,  B >. ,  <. c ,  d >. >.  /\  <. <. E ,  F >. , 
<. G ,  H >. >.  =  <. <. e ,  f
>. ,  <. g ,  h >. >.  /\  th )  <->  E. h  e.  P  (
<. <. A ,  B >. ,  <. C ,  D >. >.  =  <. <. A ,  B >. ,  <. C , 
d >. >.  /\  <. <. E ,  F >. ,  <. G ,  H >. >.  =  <. <. e ,  f >. ,  <. g ,  h >. >.  /\  ta ) ) )
1351342rexbidv 2770 . . . . . . . 8  |-  ( c  =  C  ->  ( E. f  e.  P  E. g  e.  P  E. h  e.  P  ( <. <. A ,  B >. ,  <. C ,  D >. >.  =  <. <. A ,  B >. ,  <. c ,  d >. >.  /\  <. <. E ,  F >. , 
<. G ,  H >. >.  =  <. <. e ,  f
>. ,  <. g ,  h >. >.  /\  th )  <->  E. f  e.  P  E. g  e.  P  E. h  e.  P  ( <. <. A ,  B >. ,  <. C ,  D >. >.  =  <. <. A ,  B >. ,  <. C , 
d >. >.  /\  <. <. E ,  F >. ,  <. G ,  H >. >.  =  <. <. e ,  f >. ,  <. g ,  h >. >.  /\  ta ) ) )
1361352rexbidv 2770 . . . . . . 7  |-  ( c  =  C  ->  ( E. d  e.  P  E. e  e.  P  E. f  e.  P  E. g  e.  P  E. h  e.  P  ( <. <. A ,  B >. ,  <. C ,  D >. >.  =  <. <. A ,  B >. ,  <. c ,  d >. >.  /\  <. <. E ,  F >. , 
<. G ,  H >. >.  =  <. <. e ,  f
>. ,  <. g ,  h >. >.  /\  th )  <->  E. d  e.  P  E. e  e.  P  E. f  e.  P  E. g  e.  P  E. h  e.  P  ( <. <. A ,  B >. ,  <. C ,  D >. >.  =  <. <. A ,  B >. ,  <. C , 
d >. >.  /\  <. <. E ,  F >. ,  <. G ,  H >. >.  =  <. <. e ,  f >. ,  <. g ,  h >. >.  /\  ta ) ) )
137122, 129, 136rspc3ev 3095 . . . . . 6  |-  ( ( ( A  e.  P  /\  B  e.  P  /\  C  e.  P
)  /\  E. d  e.  P  E. e  e.  P  E. f  e.  P  E. g  e.  P  E. h  e.  P  ( <. <. A ,  B >. , 
<. C ,  D >. >.  =  <. <. A ,  B >. ,  <. C ,  d
>. >.  /\  <. <. E ,  F >. ,  <. G ,  H >. >.  =  <. <. e ,  f >. ,  <. g ,  h >. >.  /\  ta ) )  ->  E. a  e.  P  E. b  e.  P  E. c  e.  P  E. d  e.  P  E. e  e.  P  E. f  e.  P  E. g  e.  P  E. h  e.  P  ( <. <. A ,  B >. , 
<. C ,  D >. >.  =  <. <. a ,  b
>. ,  <. c ,  d >. >.  /\  <. <. E ,  F >. ,  <. G ,  H >. >.  =  <. <. e ,  f >. ,  <. g ,  h >. >.  /\  ps ) )
13878, 79, 80, 115, 137syl31anc 1221 . . . . 5  |-  ( ( ( ( A  e.  P  /\  B  e.  P )  /\  ( C  e.  P  /\  D  e.  P  /\  E  e.  P )  /\  ( F  e.  P  /\  G  e.  P  /\  H  e.  P
) )  /\  mu )  ->  E. a  e.  P  E. b  e.  P  E. c  e.  P  E. d  e.  P  E. e  e.  P  E. f  e.  P  E. g  e.  P  E. h  e.  P  ( <. <. A ,  B >. ,  <. C ,  D >. >.  =  <. <. a ,  b >. ,  <. c ,  d >. >.  /\  <. <. E ,  F >. , 
<. G ,  H >. >.  =  <. <. e ,  f
>. ,  <. g ,  h >. >.  /\  ps )
)
139138ex 434 . . . 4  |-  ( ( ( A  e.  P  /\  B  e.  P
)  /\  ( C  e.  P  /\  D  e.  P  /\  E  e.  P )  /\  ( F  e.  P  /\  G  e.  P  /\  H  e.  P )
)  ->  ( mu  ->  E. a  e.  P  E. b  e.  P  E. c  e.  P  E. d  e.  P  E. e  e.  P  E. f  e.  P  E. g  e.  P  E. h  e.  P  ( <. <. A ,  B >. ,  <. C ,  D >. >.  =  <. <. a ,  b >. ,  <. c ,  d >. >.  /\  <. <. E ,  F >. , 
<. G ,  H >. >.  =  <. <. e ,  f
>. ,  <. g ,  h >. >.  /\  ps )
) )
14077, 139impbid 191 . . 3  |-  ( ( ( A  e.  P  /\  B  e.  P
)  /\  ( C  e.  P  /\  D  e.  P  /\  E  e.  P )  /\  ( F  e.  P  /\  G  e.  P  /\  H  e.  P )
)  ->  ( E. a  e.  P  E. b  e.  P  E. c  e.  P  E. d  e.  P  E. e  e.  P  E. f  e.  P  E. g  e.  P  E. h  e.  P  ( <. <. A ,  B >. ,  <. C ,  D >. >.  =  <. <. a ,  b >. ,  <. c ,  d >. >.  /\  <. <. E ,  F >. , 
<. G ,  H >. >.  =  <. <. e ,  f
>. ,  <. g ,  h >. >.  /\  ps )  <->  mu ) )
14122, 23, 24, 25, 26, 27, 28, 29, 140syl233anc 1247 . 2  |-  ( ph  ->  ( E. a  e.  P  E. b  e.  P  E. c  e.  P  E. d  e.  P  E. e  e.  P  E. f  e.  P  E. g  e.  P  E. h  e.  P  ( <. <. A ,  B >. ,  <. C ,  D >. >.  =  <. <. a ,  b >. ,  <. c ,  d >. >.  /\  <. <. E ,  F >. , 
<. G ,  H >. >.  =  <. <. e ,  f
>. ,  <. g ,  h >. >.  /\  ps )  <->  mu ) )
14221, 141bitrd 253 1  |-  ( ph  ->  ( <. <. A ,  B >. ,  <. C ,  D >. >. R <. <. E ,  F >. ,  <. G ,  H >. >. 
<->  mu ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    /\ w3a 965    = wceq 1369    e. wcel 1756   E.wrex 2728   <.cop 3895   class class class wbr 4304   {copab 4361
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4425  ax-nul 4433  ax-pr 4543
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ne 2620  df-ral 2732  df-rex 2733  df-rab 2736  df-v 2986  df-dif 3343  df-un 3345  df-in 3347  df-ss 3354  df-nul 3650  df-if 3804  df-sn 3890  df-pr 3892  df-op 3896  df-br 4305  df-opab 4363
This theorem is referenced by:  brafs  27008
  Copyright terms: Public domain W3C validator