Users' Mathboxes Mathbox for Scott Fenton < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  br6 Unicode version

Theorem br6 24114
Description: Substitution for an six-place predicate. (Contributed by Scott Fenton, 4-Oct-2013.) (Revised by Mario Carneiro, 3-May-2015.)
Hypotheses
Ref Expression
br6.1  |-  ( a  =  A  ->  ( ph 
<->  ps ) )
br6.2  |-  ( b  =  B  ->  ( ps 
<->  ch ) )
br6.3  |-  ( c  =  C  ->  ( ch 
<->  th ) )
br6.4  |-  ( d  =  D  ->  ( th 
<->  ta ) )
br6.5  |-  ( e  =  E  ->  ( ta 
<->  et ) )
br6.6  |-  ( f  =  F  ->  ( et 
<->  ze ) )
br6.7  |-  ( x  =  X  ->  P  =  Q )
br6.8  |-  R  =  { <. p ,  q
>.  |  E. x  e.  S  E. a  e.  P  E. b  e.  P  E. c  e.  P  E. d  e.  P  E. e  e.  P  E. f  e.  P  ( p  =  <. a ,  <. b ,  c >. >.  /\  q  =  <. d ,  <. e ,  f >. >.  /\  ph ) }
Assertion
Ref Expression
br6  |-  ( ( X  e.  S  /\  ( A  e.  Q  /\  B  e.  Q  /\  C  e.  Q
)  /\  ( D  e.  Q  /\  E  e.  Q  /\  F  e.  Q ) )  -> 
( <. A ,  <. B ,  C >. >. R <. D ,  <. E ,  F >. >. 
<->  ze ) )
Distinct variable groups:    ch, b    et, e    a, b, c, d, e, f, p, q, P    x, p, ph, q    ps, a    x, a, A, b, c, d, e, f, p, q    B, a, b, c, d, e, f, p, q, x    Q, a, b, c, d, e, f, x    C, a, b, c, d, e, f, p, q, x    D, a, b, c, d, e, f, p, q, x    X, a, b, c, d, e, f, x    E, a, b, c, d, e, f, p, q, x    ta, d    th, c    ze, a, b, c, d, e, f, x    F, a, b, c, d, e, f, p, q, x    S, a, b, c, d, e, f, p, q, x
Allowed substitution hints:    ph( e, f, a, b, c, d)    ps( x, e, f, q, p, b, c, d)    ch( x, e, f, q, p, a, c, d)    th( x, e, f, q, p, a, b, d)    ta( x, e, f, q, p, a, b, c)    et( x, f, q, p, a, b, c, d)    ze( q, p)    P( x)    Q( q, p)    R( x, e, f, q, p, a, b, c, d)    X( q, p)

Proof of Theorem br6
StepHypRef Expression
1 opex 4237 . . 3  |-  <. A ,  <. B ,  C >. >.  e.  _V
2 opex 4237 . . 3  |-  <. D ,  <. E ,  F >. >.  e.  _V
3 eqeq1 2289 . . . . . . . . 9  |-  ( p  =  <. A ,  <. B ,  C >. >.  ->  (
p  =  <. a ,  <. b ,  c
>. >. 
<-> 
<. A ,  <. B ,  C >. >.  =  <. a ,  <. b ,  c
>. >. ) )
4 eqcom 2285 . . . . . . . . 9  |-  ( <. A ,  <. B ,  C >. >.  =  <. a ,  <. b ,  c
>. >. 
<-> 
<. a ,  <. b ,  c >. >.  =  <. A ,  <. B ,  C >. >. )
53, 4syl6bb 252 . . . . . . . 8  |-  ( p  =  <. A ,  <. B ,  C >. >.  ->  (
p  =  <. a ,  <. b ,  c
>. >. 
<-> 
<. a ,  <. b ,  c >. >.  =  <. A ,  <. B ,  C >. >. ) )
653anbi1d 1256 . . . . . . 7  |-  ( p  =  <. A ,  <. B ,  C >. >.  ->  (
( p  =  <. a ,  <. b ,  c
>. >.  /\  q  =  <. d ,  <. e ,  f >. >.  /\  ph ) 
<->  ( <. a ,  <. b ,  c >. >.  =  <. A ,  <. B ,  C >. >.  /\  q  =  <. d ,  <. e ,  f >. >.  /\  ph ) ) )
76rexbidv 2564 . . . . . 6  |-  ( p  =  <. A ,  <. B ,  C >. >.  ->  ( E. f  e.  P  ( p  =  <. a ,  <. b ,  c
>. >.  /\  q  =  <. d ,  <. e ,  f >. >.  /\  ph ) 
<->  E. f  e.  P  ( <. a ,  <. b ,  c >. >.  =  <. A ,  <. B ,  C >. >.  /\  q  =  <. d ,  <. e ,  f >. >.  /\  ph ) ) )
872rexbidv 2586 . . . . 5  |-  ( p  =  <. A ,  <. B ,  C >. >.  ->  ( E. d  e.  P  E. e  e.  P  E. f  e.  P  ( p  =  <. a ,  <. b ,  c
>. >.  /\  q  =  <. d ,  <. e ,  f >. >.  /\  ph ) 
<->  E. d  e.  P  E. e  e.  P  E. f  e.  P  ( <. a ,  <. b ,  c >. >.  =  <. A ,  <. B ,  C >. >.  /\  q  =  <. d ,  <. e ,  f >. >.  /\  ph ) ) )
982rexbidv 2586 . . . 4  |-  ( p  =  <. A ,  <. B ,  C >. >.  ->  ( E. b  e.  P  E. c  e.  P  E. d  e.  P  E. e  e.  P  E. f  e.  P  ( p  =  <. a ,  <. b ,  c
>. >.  /\  q  =  <. d ,  <. e ,  f >. >.  /\  ph ) 
<->  E. b  e.  P  E. c  e.  P  E. d  e.  P  E. e  e.  P  E. f  e.  P  ( <. a ,  <. b ,  c >. >.  =  <. A ,  <. B ,  C >. >.  /\  q  =  <. d ,  <. e ,  f >. >.  /\  ph ) ) )
1092rexbidv 2586 . . 3  |-  ( p  =  <. A ,  <. B ,  C >. >.  ->  ( E. x  e.  S  E. a  e.  P  E. b  e.  P  E. c  e.  P  E. d  e.  P  E. e  e.  P  E. f  e.  P  ( p  =  <. a ,  <. b ,  c
>. >.  /\  q  =  <. d ,  <. e ,  f >. >.  /\  ph ) 
<->  E. x  e.  S  E. a  e.  P  E. b  e.  P  E. c  e.  P  E. d  e.  P  E. e  e.  P  E. f  e.  P  ( <. a ,  <. b ,  c >. >.  =  <. A ,  <. B ,  C >. >.  /\  q  =  <. d ,  <. e ,  f >. >.  /\  ph ) ) )
11 eqeq1 2289 . . . . . . . . 9  |-  ( q  =  <. D ,  <. E ,  F >. >.  ->  (
q  =  <. d ,  <. e ,  f
>. >. 
<-> 
<. D ,  <. E ,  F >. >.  =  <. d ,  <. e ,  f
>. >. ) )
12 eqcom 2285 . . . . . . . . 9  |-  ( <. D ,  <. E ,  F >. >.  =  <. d ,  <. e ,  f
>. >. 
<-> 
<. d ,  <. e ,  f >. >.  =  <. D ,  <. E ,  F >. >. )
1311, 12syl6bb 252 . . . . . . . 8  |-  ( q  =  <. D ,  <. E ,  F >. >.  ->  (
q  =  <. d ,  <. e ,  f
>. >. 
<-> 
<. d ,  <. e ,  f >. >.  =  <. D ,  <. E ,  F >. >. ) )
14133anbi2d 1257 . . . . . . 7  |-  ( q  =  <. D ,  <. E ,  F >. >.  ->  (
( <. a ,  <. b ,  c >. >.  =  <. A ,  <. B ,  C >. >.  /\  q  =  <. d ,  <. e ,  f >. >.  /\  ph ) 
<->  ( <. a ,  <. b ,  c >. >.  =  <. A ,  <. B ,  C >. >.  /\  <. d , 
<. e ,  f >. >.  =  <. D ,  <. E ,  F >. >.  /\  ph ) ) )
1514rexbidv 2564 . . . . . 6  |-  ( q  =  <. D ,  <. E ,  F >. >.  ->  ( E. f  e.  P  ( <. a ,  <. b ,  c >. >.  =  <. A ,  <. B ,  C >. >.  /\  q  =  <. d ,  <. e ,  f >. >.  /\  ph ) 
<->  E. f  e.  P  ( <. a ,  <. b ,  c >. >.  =  <. A ,  <. B ,  C >. >.  /\  <. d , 
<. e ,  f >. >.  =  <. D ,  <. E ,  F >. >.  /\  ph ) ) )
16152rexbidv 2586 . . . . 5  |-  ( q  =  <. D ,  <. E ,  F >. >.  ->  ( E. d  e.  P  E. e  e.  P  E. f  e.  P  ( <. a ,  <. b ,  c >. >.  =  <. A ,  <. B ,  C >. >.  /\  q  =  <. d ,  <. e ,  f >. >.  /\  ph ) 
<->  E. d  e.  P  E. e  e.  P  E. f  e.  P  ( <. a ,  <. b ,  c >. >.  =  <. A ,  <. B ,  C >. >.  /\  <. d , 
<. e ,  f >. >.  =  <. D ,  <. E ,  F >. >.  /\  ph ) ) )
17162rexbidv 2586 . . . 4  |-  ( q  =  <. D ,  <. E ,  F >. >.  ->  ( E. b  e.  P  E. c  e.  P  E. d  e.  P  E. e  e.  P  E. f  e.  P  ( <. a ,  <. b ,  c >. >.  =  <. A ,  <. B ,  C >. >.  /\  q  =  <. d ,  <. e ,  f >. >.  /\  ph ) 
<->  E. b  e.  P  E. c  e.  P  E. d  e.  P  E. e  e.  P  E. f  e.  P  ( <. a ,  <. b ,  c >. >.  =  <. A ,  <. B ,  C >. >.  /\  <. d , 
<. e ,  f >. >.  =  <. D ,  <. E ,  F >. >.  /\  ph ) ) )
18172rexbidv 2586 . . 3  |-  ( q  =  <. D ,  <. E ,  F >. >.  ->  ( E. x  e.  S  E. a  e.  P  E. b  e.  P  E. c  e.  P  E. d  e.  P  E. e  e.  P  E. f  e.  P  ( <. a ,  <. b ,  c >. >.  =  <. A ,  <. B ,  C >. >.  /\  q  =  <. d ,  <. e ,  f >. >.  /\  ph ) 
<->  E. x  e.  S  E. a  e.  P  E. b  e.  P  E. c  e.  P  E. d  e.  P  E. e  e.  P  E. f  e.  P  ( <. a ,  <. b ,  c >. >.  =  <. A ,  <. B ,  C >. >.  /\  <. d , 
<. e ,  f >. >.  =  <. D ,  <. E ,  F >. >.  /\  ph ) ) )
19 br6.8 . . 3  |-  R  =  { <. p ,  q
>.  |  E. x  e.  S  E. a  e.  P  E. b  e.  P  E. c  e.  P  E. d  e.  P  E. e  e.  P  E. f  e.  P  ( p  =  <. a ,  <. b ,  c >. >.  /\  q  =  <. d ,  <. e ,  f >. >.  /\  ph ) }
201, 2, 10, 18, 19brab 4287 . 2  |-  ( <. A ,  <. B ,  C >. >. R <. D ,  <. E ,  F >. >.  <->  E. x  e.  S  E. a  e.  P  E. b  e.  P  E. c  e.  P  E. d  e.  P  E. e  e.  P  E. f  e.  P  ( <. a ,  <. b ,  c >. >.  =  <. A ,  <. B ,  C >. >.  /\  <. d , 
<. e ,  f >. >.  =  <. D ,  <. E ,  F >. >.  /\  ph ) )
21 vex 2791 . . . . . . . . . . . 12  |-  a  e. 
_V
22 opex 4237 . . . . . . . . . . . 12  |-  <. b ,  c >.  e.  _V
2321, 22opth 4245 . . . . . . . . . . 11  |-  ( <.
a ,  <. b ,  c >. >.  =  <. A ,  <. B ,  C >. >. 
<->  ( a  =  A  /\  <. b ,  c
>.  =  <. B ,  C >. ) )
24 br6.1 . . . . . . . . . . . 12  |-  ( a  =  A  ->  ( ph 
<->  ps ) )
25 vex 2791 . . . . . . . . . . . . . 14  |-  b  e. 
_V
26 vex 2791 . . . . . . . . . . . . . 14  |-  c  e. 
_V
2725, 26opth 4245 . . . . . . . . . . . . 13  |-  ( <.
b ,  c >.  =  <. B ,  C >.  <-> 
( b  =  B  /\  c  =  C ) )
28 br6.2 . . . . . . . . . . . . . 14  |-  ( b  =  B  ->  ( ps 
<->  ch ) )
29 br6.3 . . . . . . . . . . . . . 14  |-  ( c  =  C  ->  ( ch 
<->  th ) )
3028, 29sylan9bb 680 . . . . . . . . . . . . 13  |-  ( ( b  =  B  /\  c  =  C )  ->  ( ps  <->  th )
)
3127, 30sylbi 187 . . . . . . . . . . . 12  |-  ( <.
b ,  c >.  =  <. B ,  C >.  ->  ( ps  <->  th )
)
3224, 31sylan9bb 680 . . . . . . . . . . 11  |-  ( ( a  =  A  /\  <.
b ,  c >.  =  <. B ,  C >. )  ->  ( ph  <->  th ) )
3323, 32sylbi 187 . . . . . . . . . 10  |-  ( <.
a ,  <. b ,  c >. >.  =  <. A ,  <. B ,  C >. >.  ->  ( ph  <->  th ) )
34 vex 2791 . . . . . . . . . . . 12  |-  d  e. 
_V
35 opex 4237 . . . . . . . . . . . 12  |-  <. e ,  f >.  e.  _V
3634, 35opth 4245 . . . . . . . . . . 11  |-  ( <.
d ,  <. e ,  f >. >.  =  <. D ,  <. E ,  F >. >. 
<->  ( d  =  D  /\  <. e ,  f
>.  =  <. E ,  F >. ) )
37 br6.4 . . . . . . . . . . . 12  |-  ( d  =  D  ->  ( th 
<->  ta ) )
38 vex 2791 . . . . . . . . . . . . . 14  |-  e  e. 
_V
39 vex 2791 . . . . . . . . . . . . . 14  |-  f  e. 
_V
4038, 39opth 4245 . . . . . . . . . . . . 13  |-  ( <.
e ,  f >.  =  <. E ,  F >.  <-> 
( e  =  E  /\  f  =  F ) )
41 br6.5 . . . . . . . . . . . . . 14  |-  ( e  =  E  ->  ( ta 
<->  et ) )
42 br6.6 . . . . . . . . . . . . . 14  |-  ( f  =  F  ->  ( et 
<->  ze ) )
4341, 42sylan9bb 680 . . . . . . . . . . . . 13  |-  ( ( e  =  E  /\  f  =  F )  ->  ( ta  <->  ze )
)
4440, 43sylbi 187 . . . . . . . . . . . 12  |-  ( <.
e ,  f >.  =  <. E ,  F >.  ->  ( ta  <->  ze )
)
4537, 44sylan9bb 680 . . . . . . . . . . 11  |-  ( ( d  =  D  /\  <.
e ,  f >.  =  <. E ,  F >. )  ->  ( th  <->  ze ) )
4636, 45sylbi 187 . . . . . . . . . 10  |-  ( <.
d ,  <. e ,  f >. >.  =  <. D ,  <. E ,  F >. >.  ->  ( th  <->  ze ) )
4733, 46sylan9bb 680 . . . . . . . . 9  |-  ( (
<. a ,  <. b ,  c >. >.  =  <. A ,  <. B ,  C >. >.  /\  <. d , 
<. e ,  f >. >.  =  <. D ,  <. E ,  F >. >. )  ->  ( ph  <->  ze )
)
4847biimp3a 1281 . . . . . . . 8  |-  ( (
<. a ,  <. b ,  c >. >.  =  <. A ,  <. B ,  C >. >.  /\  <. d , 
<. e ,  f >. >.  =  <. D ,  <. E ,  F >. >.  /\  ph )  ->  ze )
4948a1i 10 . . . . . . 7  |-  ( ( ( ( ( ( X  e.  S  /\  ( A  e.  Q  /\  B  e.  Q  /\  C  e.  Q
)  /\  ( D  e.  Q  /\  E  e.  Q  /\  F  e.  Q ) )  /\  ( x  e.  S  /\  a  e.  P
) )  /\  (
b  e.  P  /\  c  e.  P )
)  /\  ( d  e.  P  /\  e  e.  P ) )  /\  f  e.  P )  ->  ( ( <. a ,  <. b ,  c
>. >.  =  <. A ,  <. B ,  C >. >.  /\  <. d ,  <. e ,  f >. >.  =  <. D ,  <. E ,  F >. >.  /\  ph )  ->  ze ) )
5049rexlimdva 2667 . . . . . 6  |-  ( ( ( ( ( X  e.  S  /\  ( A  e.  Q  /\  B  e.  Q  /\  C  e.  Q )  /\  ( D  e.  Q  /\  E  e.  Q  /\  F  e.  Q
) )  /\  (
x  e.  S  /\  a  e.  P )
)  /\  ( b  e.  P  /\  c  e.  P ) )  /\  ( d  e.  P  /\  e  e.  P
) )  ->  ( E. f  e.  P  ( <. a ,  <. b ,  c >. >.  =  <. A ,  <. B ,  C >. >.  /\  <. d , 
<. e ,  f >. >.  =  <. D ,  <. E ,  F >. >.  /\  ph )  ->  ze ) )
5150rexlimdvva 2674 . . . . 5  |-  ( ( ( ( X  e.  S  /\  ( A  e.  Q  /\  B  e.  Q  /\  C  e.  Q )  /\  ( D  e.  Q  /\  E  e.  Q  /\  F  e.  Q )
)  /\  ( x  e.  S  /\  a  e.  P ) )  /\  ( b  e.  P  /\  c  e.  P
) )  ->  ( E. d  e.  P  E. e  e.  P  E. f  e.  P  ( <. a ,  <. b ,  c >. >.  =  <. A ,  <. B ,  C >. >.  /\  <. d , 
<. e ,  f >. >.  =  <. D ,  <. E ,  F >. >.  /\  ph )  ->  ze ) )
5251rexlimdvva 2674 . . . 4  |-  ( ( ( X  e.  S  /\  ( A  e.  Q  /\  B  e.  Q  /\  C  e.  Q
)  /\  ( D  e.  Q  /\  E  e.  Q  /\  F  e.  Q ) )  /\  ( x  e.  S  /\  a  e.  P
) )  ->  ( E. b  e.  P  E. c  e.  P  E. d  e.  P  E. e  e.  P  E. f  e.  P  ( <. a ,  <. b ,  c >. >.  =  <. A ,  <. B ,  C >. >.  /\  <. d , 
<. e ,  f >. >.  =  <. D ,  <. E ,  F >. >.  /\  ph )  ->  ze ) )
5352rexlimdvva 2674 . . 3  |-  ( ( X  e.  S  /\  ( A  e.  Q  /\  B  e.  Q  /\  C  e.  Q
)  /\  ( D  e.  Q  /\  E  e.  Q  /\  F  e.  Q ) )  -> 
( E. x  e.  S  E. a  e.  P  E. b  e.  P  E. c  e.  P  E. d  e.  P  E. e  e.  P  E. f  e.  P  ( <. a ,  <. b ,  c
>. >.  =  <. A ,  <. B ,  C >. >.  /\  <. d ,  <. e ,  f >. >.  =  <. D ,  <. E ,  F >. >.  /\  ph )  ->  ze ) )
54 simpl1 958 . . . . 5  |-  ( ( ( X  e.  S  /\  ( A  e.  Q  /\  B  e.  Q  /\  C  e.  Q
)  /\  ( D  e.  Q  /\  E  e.  Q  /\  F  e.  Q ) )  /\  ze )  ->  X  e.  S )
55 simpl2 959 . . . . . 6  |-  ( ( ( X  e.  S  /\  ( A  e.  Q  /\  B  e.  Q  /\  C  e.  Q
)  /\  ( D  e.  Q  /\  E  e.  Q  /\  F  e.  Q ) )  /\  ze )  ->  ( A  e.  Q  /\  B  e.  Q  /\  C  e.  Q ) )
56 opeq1 3796 . . . . . . . . . 10  |-  ( d  =  D  ->  <. d ,  <. e ,  f
>. >.  =  <. D ,  <. e ,  f >. >. )
5756eqeq1d 2291 . . . . . . . . 9  |-  ( d  =  D  ->  ( <. d ,  <. e ,  f >. >.  =  <. D ,  <. E ,  F >. >. 
<-> 
<. D ,  <. e ,  f >. >.  =  <. D ,  <. E ,  F >. >. ) )
5857, 373anbi23d 1255 . . . . . . . 8  |-  ( d  =  D  ->  (
( <. A ,  <. B ,  C >. >.  =  <. A ,  <. B ,  C >. >.  /\  <. d , 
<. e ,  f >. >.  =  <. D ,  <. E ,  F >. >.  /\  th ) 
<->  ( <. A ,  <. B ,  C >. >.  =  <. A ,  <. B ,  C >. >.  /\  <. D ,  <. e ,  f >. >.  =  <. D ,  <. E ,  F >. >.  /\  ta ) ) )
59 opeq1 3796 . . . . . . . . . . 11  |-  ( e  =  E  ->  <. e ,  f >.  =  <. E ,  f >. )
6059opeq2d 3803 . . . . . . . . . 10  |-  ( e  =  E  ->  <. D ,  <. e ,  f >. >.  =  <. D ,  <. E ,  f >. >. )
6160eqeq1d 2291 . . . . . . . . 9  |-  ( e  =  E  ->  ( <. D ,  <. e ,  f >. >.  =  <. D ,  <. E ,  F >. >. 
<-> 
<. D ,  <. E , 
f >. >.  =  <. D ,  <. E ,  F >. >.
) )
6261, 413anbi23d 1255 . . . . . . . 8  |-  ( e  =  E  ->  (
( <. A ,  <. B ,  C >. >.  =  <. A ,  <. B ,  C >. >.  /\  <. D ,  <. e ,  f >. >.  =  <. D ,  <. E ,  F >. >.  /\  ta ) 
<->  ( <. A ,  <. B ,  C >. >.  =  <. A ,  <. B ,  C >. >.  /\  <. D ,  <. E ,  f >. >.  =  <. D ,  <. E ,  F >. >.  /\  et ) ) )
63 opeq2 3797 . . . . . . . . . . . 12  |-  ( f  =  F  ->  <. E , 
f >.  =  <. E ,  F >. )
6463opeq2d 3803 . . . . . . . . . . 11  |-  ( f  =  F  ->  <. D ,  <. E ,  f >. >.  =  <. D ,  <. E ,  F >. >. )
6564eqeq1d 2291 . . . . . . . . . 10  |-  ( f  =  F  ->  ( <. D ,  <. E , 
f >. >.  =  <. D ,  <. E ,  F >. >.  <->  <. D ,  <. E ,  F >. >.  =  <. D ,  <. E ,  F >. >.
) )
6665, 423anbi23d 1255 . . . . . . . . 9  |-  ( f  =  F  ->  (
( <. A ,  <. B ,  C >. >.  =  <. A ,  <. B ,  C >. >.  /\  <. D ,  <. E ,  f >. >.  =  <. D ,  <. E ,  F >. >.  /\  et ) 
<->  ( <. A ,  <. B ,  C >. >.  =  <. A ,  <. B ,  C >. >.  /\  <. D ,  <. E ,  F >. >.  =  <. D ,  <. E ,  F >. >.  /\  ze ) ) )
67 eqid 2283 . . . . . . . . . . 11  |-  <. A ,  <. B ,  C >. >.  =  <. A ,  <. B ,  C >. >.
68 eqid 2283 . . . . . . . . . . 11  |-  <. D ,  <. E ,  F >. >.  =  <. D ,  <. E ,  F >. >.
6967, 68pm3.2i 441 . . . . . . . . . 10  |-  ( <. A ,  <. B ,  C >. >.  =  <. A ,  <. B ,  C >. >.  /\  <. D ,  <. E ,  F >. >.  =  <. D ,  <. E ,  F >. >. )
70 df-3an 936 . . . . . . . . . 10  |-  ( (
<. A ,  <. B ,  C >. >.  =  <. A ,  <. B ,  C >. >.  /\  <. D ,  <. E ,  F >. >.  =  <. D ,  <. E ,  F >. >.  /\  ze )  <->  ( ( <. A ,  <. B ,  C >. >.  =  <. A ,  <. B ,  C >. >.  /\  <. D ,  <. E ,  F >. >.  =  <. D ,  <. E ,  F >. >. )  /\  ze ) )
7169, 70mpbiran 884 . . . . . . . . 9  |-  ( (
<. A ,  <. B ,  C >. >.  =  <. A ,  <. B ,  C >. >.  /\  <. D ,  <. E ,  F >. >.  =  <. D ,  <. E ,  F >. >.  /\  ze )  <->  ze )
7266, 71syl6bb 252 . . . . . . . 8  |-  ( f  =  F  ->  (
( <. A ,  <. B ,  C >. >.  =  <. A ,  <. B ,  C >. >.  /\  <. D ,  <. E ,  f >. >.  =  <. D ,  <. E ,  F >. >.  /\  et ) 
<->  ze ) )
7358, 62, 72rspc3ev 2894 . . . . . . 7  |-  ( ( ( D  e.  Q  /\  E  e.  Q  /\  F  e.  Q
)  /\  ze )  ->  E. d  e.  Q  E. e  e.  Q  E. f  e.  Q  ( <. A ,  <. B ,  C >. >.  =  <. A ,  <. B ,  C >. >.  /\  <. d , 
<. e ,  f >. >.  =  <. D ,  <. E ,  F >. >.  /\  th ) )
74733ad2antl3 1119 . . . . . 6  |-  ( ( ( X  e.  S  /\  ( A  e.  Q  /\  B  e.  Q  /\  C  e.  Q
)  /\  ( D  e.  Q  /\  E  e.  Q  /\  F  e.  Q ) )  /\  ze )  ->  E. d  e.  Q  E. e  e.  Q  E. f  e.  Q  ( <. A ,  <. B ,  C >. >.  =  <. A ,  <. B ,  C >. >.  /\  <. d ,  <. e ,  f >. >.  =  <. D ,  <. E ,  F >. >.  /\  th )
)
75 opeq1 3796 . . . . . . . . . . 11  |-  ( a  =  A  ->  <. a ,  <. b ,  c
>. >.  =  <. A ,  <. b ,  c >. >. )
7675eqeq1d 2291 . . . . . . . . . 10  |-  ( a  =  A  ->  ( <. a ,  <. b ,  c >. >.  =  <. A ,  <. B ,  C >. >. 
<-> 
<. A ,  <. b ,  c >. >.  =  <. A ,  <. B ,  C >. >. ) )
7776, 243anbi13d 1254 . . . . . . . . 9  |-  ( a  =  A  ->  (
( <. a ,  <. b ,  c >. >.  =  <. A ,  <. B ,  C >. >.  /\  <. d , 
<. e ,  f >. >.  =  <. D ,  <. E ,  F >. >.  /\  ph ) 
<->  ( <. A ,  <. b ,  c >. >.  =  <. A ,  <. B ,  C >. >.  /\  <. d , 
<. e ,  f >. >.  =  <. D ,  <. E ,  F >. >.  /\  ps ) ) )
7877rexbidv 2564 . . . . . . . 8  |-  ( a  =  A  ->  ( E. f  e.  Q  ( <. a ,  <. b ,  c >. >.  =  <. A ,  <. B ,  C >. >.  /\  <. d , 
<. e ,  f >. >.  =  <. D ,  <. E ,  F >. >.  /\  ph ) 
<->  E. f  e.  Q  ( <. A ,  <. b ,  c >. >.  =  <. A ,  <. B ,  C >. >.  /\  <. d , 
<. e ,  f >. >.  =  <. D ,  <. E ,  F >. >.  /\  ps ) ) )
79782rexbidv 2586 . . . . . . 7  |-  ( a  =  A  ->  ( E. d  e.  Q  E. e  e.  Q  E. f  e.  Q  ( <. a ,  <. b ,  c >. >.  =  <. A ,  <. B ,  C >. >.  /\  <. d , 
<. e ,  f >. >.  =  <. D ,  <. E ,  F >. >.  /\  ph ) 
<->  E. d  e.  Q  E. e  e.  Q  E. f  e.  Q  ( <. A ,  <. b ,  c >. >.  =  <. A ,  <. B ,  C >. >.  /\  <. d , 
<. e ,  f >. >.  =  <. D ,  <. E ,  F >. >.  /\  ps ) ) )
80 opeq1 3796 . . . . . . . . . . . 12  |-  ( b  =  B  ->  <. b ,  c >.  =  <. B ,  c >. )
8180opeq2d 3803 . . . . . . . . . . 11  |-  ( b  =  B  ->  <. A ,  <. b ,  c >. >.  =  <. A ,  <. B ,  c >. >. )
8281eqeq1d 2291 . . . . . . . . . 10  |-  ( b  =  B  ->  ( <. A ,  <. b ,  c >. >.  =  <. A ,  <. B ,  C >. >. 
<-> 
<. A ,  <. B , 
c >. >.  =  <. A ,  <. B ,  C >. >.
) )
8382, 283anbi13d 1254 . . . . . . . . 9  |-  ( b  =  B  ->  (
( <. A ,  <. b ,  c >. >.  =  <. A ,  <. B ,  C >. >.  /\  <. d , 
<. e ,  f >. >.  =  <. D ,  <. E ,  F >. >.  /\  ps ) 
<->  ( <. A ,  <. B ,  c >. >.  =  <. A ,  <. B ,  C >. >.  /\  <. d , 
<. e ,  f >. >.  =  <. D ,  <. E ,  F >. >.  /\  ch ) ) )
8483rexbidv 2564 . . . . . . . 8  |-  ( b  =  B  ->  ( E. f  e.  Q  ( <. A ,  <. b ,  c >. >.  =  <. A ,  <. B ,  C >. >.  /\  <. d , 
<. e ,  f >. >.  =  <. D ,  <. E ,  F >. >.  /\  ps ) 
<->  E. f  e.  Q  ( <. A ,  <. B ,  c >. >.  =  <. A ,  <. B ,  C >. >.  /\  <. d , 
<. e ,  f >. >.  =  <. D ,  <. E ,  F >. >.  /\  ch ) ) )
85842rexbidv 2586 . . . . . . 7  |-  ( b  =  B  ->  ( E. d  e.  Q  E. e  e.  Q  E. f  e.  Q  ( <. A ,  <. b ,  c >. >.  =  <. A ,  <. B ,  C >. >.  /\  <. d , 
<. e ,  f >. >.  =  <. D ,  <. E ,  F >. >.  /\  ps ) 
<->  E. d  e.  Q  E. e  e.  Q  E. f  e.  Q  ( <. A ,  <. B ,  c >. >.  =  <. A ,  <. B ,  C >. >.  /\  <. d , 
<. e ,  f >. >.  =  <. D ,  <. E ,  F >. >.  /\  ch ) ) )
86 opeq2 3797 . . . . . . . . . . . 12  |-  ( c  =  C  ->  <. B , 
c >.  =  <. B ,  C >. )
8786opeq2d 3803 . . . . . . . . . . 11  |-  ( c  =  C  ->  <. A ,  <. B ,  c >. >.  =  <. A ,  <. B ,  C >. >. )
8887eqeq1d 2291 . . . . . . . . . 10  |-  ( c  =  C  ->  ( <. A ,  <. B , 
c >. >.  =  <. A ,  <. B ,  C >. >.  <->  <. A ,  <. B ,  C >. >.  =  <. A ,  <. B ,  C >. >.
) )
8988, 293anbi13d 1254 . . . . . . . . 9  |-  ( c  =  C  ->  (
( <. A ,  <. B ,  c >. >.  =  <. A ,  <. B ,  C >. >.  /\  <. d , 
<. e ,  f >. >.  =  <. D ,  <. E ,  F >. >.  /\  ch ) 
<->  ( <. A ,  <. B ,  C >. >.  =  <. A ,  <. B ,  C >. >.  /\  <. d , 
<. e ,  f >. >.  =  <. D ,  <. E ,  F >. >.  /\  th ) ) )
9089rexbidv 2564 . . . . . . . 8  |-  ( c  =  C  ->  ( E. f  e.  Q  ( <. A ,  <. B ,  c >. >.  =  <. A ,  <. B ,  C >. >.  /\  <. d , 
<. e ,  f >. >.  =  <. D ,  <. E ,  F >. >.  /\  ch ) 
<->  E. f  e.  Q  ( <. A ,  <. B ,  C >. >.  =  <. A ,  <. B ,  C >. >.  /\  <. d , 
<. e ,  f >. >.  =  <. D ,  <. E ,  F >. >.  /\  th ) ) )
91902rexbidv 2586 . . . . . . 7  |-  ( c  =  C  ->  ( E. d  e.  Q  E. e  e.  Q  E. f  e.  Q  ( <. A ,  <. B ,  c >. >.  =  <. A ,  <. B ,  C >. >.  /\  <. d , 
<. e ,  f >. >.  =  <. D ,  <. E ,  F >. >.  /\  ch ) 
<->  E. d  e.  Q  E. e  e.  Q  E. f  e.  Q  ( <. A ,  <. B ,  C >. >.  =  <. A ,  <. B ,  C >. >.  /\  <. d , 
<. e ,  f >. >.  =  <. D ,  <. E ,  F >. >.  /\  th ) ) )
9279, 85, 91rspc3ev 2894 . . . . . 6  |-  ( ( ( A  e.  Q  /\  B  e.  Q  /\  C  e.  Q
)  /\  E. d  e.  Q  E. e  e.  Q  E. f  e.  Q  ( <. A ,  <. B ,  C >. >.  =  <. A ,  <. B ,  C >. >.  /\  <. d ,  <. e ,  f >. >.  =  <. D ,  <. E ,  F >. >.  /\  th )
)  ->  E. a  e.  Q  E. b  e.  Q  E. c  e.  Q  E. d  e.  Q  E. e  e.  Q  E. f  e.  Q  ( <. a ,  <. b ,  c
>. >.  =  <. A ,  <. B ,  C >. >.  /\  <. d ,  <. e ,  f >. >.  =  <. D ,  <. E ,  F >. >.  /\  ph ) )
9355, 74, 92syl2anc 642 . . . . 5  |-  ( ( ( X  e.  S  /\  ( A  e.  Q  /\  B  e.  Q  /\  C  e.  Q
)  /\  ( D  e.  Q  /\  E  e.  Q  /\  F  e.  Q ) )  /\  ze )  ->  E. a  e.  Q  E. b  e.  Q  E. c  e.  Q  E. d  e.  Q  E. e  e.  Q  E. f  e.  Q  ( <. a ,  <. b ,  c
>. >.  =  <. A ,  <. B ,  C >. >.  /\  <. d ,  <. e ,  f >. >.  =  <. D ,  <. E ,  F >. >.  /\  ph ) )
94 br6.7 . . . . . . 7  |-  ( x  =  X  ->  P  =  Q )
9594rexeqdv 2743 . . . . . . . . . . 11  |-  ( x  =  X  ->  ( E. f  e.  P  ( <. a ,  <. b ,  c >. >.  =  <. A ,  <. B ,  C >. >.  /\  <. d , 
<. e ,  f >. >.  =  <. D ,  <. E ,  F >. >.  /\  ph ) 
<->  E. f  e.  Q  ( <. a ,  <. b ,  c >. >.  =  <. A ,  <. B ,  C >. >.  /\  <. d , 
<. e ,  f >. >.  =  <. D ,  <. E ,  F >. >.  /\  ph ) ) )
9694, 95rexeqbidv 2749 . . . . . . . . . 10  |-  ( x  =  X  ->  ( E. e  e.  P  E. f  e.  P  ( <. a ,  <. b ,  c >. >.  =  <. A ,  <. B ,  C >. >.  /\  <. d , 
<. e ,  f >. >.  =  <. D ,  <. E ,  F >. >.  /\  ph ) 
<->  E. e  e.  Q  E. f  e.  Q  ( <. a ,  <. b ,  c >. >.  =  <. A ,  <. B ,  C >. >.  /\  <. d , 
<. e ,  f >. >.  =  <. D ,  <. E ,  F >. >.  /\  ph ) ) )
9794, 96rexeqbidv 2749 . . . . . . . . 9  |-  ( x  =  X  ->  ( E. d  e.  P  E. e  e.  P  E. f  e.  P  ( <. a ,  <. b ,  c >. >.  =  <. A ,  <. B ,  C >. >.  /\  <. d , 
<. e ,  f >. >.  =  <. D ,  <. E ,  F >. >.  /\  ph ) 
<->  E. d  e.  Q  E. e  e.  Q  E. f  e.  Q  ( <. a ,  <. b ,  c >. >.  =  <. A ,  <. B ,  C >. >.  /\  <. d , 
<. e ,  f >. >.  =  <. D ,  <. E ,  F >. >.  /\  ph ) ) )
9894, 97rexeqbidv 2749 . . . . . . . 8  |-  ( x  =  X  ->  ( E. c  e.  P  E. d  e.  P  E. e  e.  P  E. f  e.  P  ( <. a ,  <. b ,  c >. >.  =  <. A ,  <. B ,  C >. >.  /\  <. d , 
<. e ,  f >. >.  =  <. D ,  <. E ,  F >. >.  /\  ph ) 
<->  E. c  e.  Q  E. d  e.  Q  E. e  e.  Q  E. f  e.  Q  ( <. a ,  <. b ,  c >. >.  =  <. A ,  <. B ,  C >. >.  /\  <. d , 
<. e ,  f >. >.  =  <. D ,  <. E ,  F >. >.  /\  ph ) ) )
9994, 98rexeqbidv 2749 . . . . . . 7  |-  ( x  =  X  ->  ( E. b  e.  P  E. c  e.  P  E. d  e.  P  E. e  e.  P  E. f  e.  P  ( <. a ,  <. b ,  c >. >.  =  <. A ,  <. B ,  C >. >.  /\  <. d , 
<. e ,  f >. >.  =  <. D ,  <. E ,  F >. >.  /\  ph ) 
<->  E. b  e.  Q  E. c  e.  Q  E. d  e.  Q  E. e  e.  Q  E. f  e.  Q  ( <. a ,  <. b ,  c >. >.  =  <. A ,  <. B ,  C >. >.  /\  <. d , 
<. e ,  f >. >.  =  <. D ,  <. E ,  F >. >.  /\  ph ) ) )
10094, 99rexeqbidv 2749 . . . . . 6  |-  ( x  =  X  ->  ( E. a  e.  P  E. b  e.  P  E. c  e.  P  E. d  e.  P  E. e  e.  P  E. f  e.  P  ( <. a ,  <. b ,  c >. >.  =  <. A ,  <. B ,  C >. >.  /\  <. d , 
<. e ,  f >. >.  =  <. D ,  <. E ,  F >. >.  /\  ph ) 
<->  E. a  e.  Q  E. b  e.  Q  E. c  e.  Q  E. d  e.  Q  E. e  e.  Q  E. f  e.  Q  ( <. a ,  <. b ,  c >. >.  =  <. A ,  <. B ,  C >. >.  /\  <. d , 
<. e ,  f >. >.  =  <. D ,  <. E ,  F >. >.  /\  ph ) ) )
101100rspcev 2884 . . . . 5  |-  ( ( X  e.  S  /\  E. a  e.  Q  E. b  e.  Q  E. c  e.  Q  E. d  e.  Q  E. e  e.  Q  E. f  e.  Q  ( <. a ,  <. b ,  c >. >.  =  <. A ,  <. B ,  C >. >.  /\  <. d , 
<. e ,  f >. >.  =  <. D ,  <. E ,  F >. >.  /\  ph ) )  ->  E. x  e.  S  E. a  e.  P  E. b  e.  P  E. c  e.  P  E. d  e.  P  E. e  e.  P  E. f  e.  P  ( <. a ,  <. b ,  c
>. >.  =  <. A ,  <. B ,  C >. >.  /\  <. d ,  <. e ,  f >. >.  =  <. D ,  <. E ,  F >. >.  /\  ph ) )
10254, 93, 101syl2anc 642 . . . 4  |-  ( ( ( X  e.  S  /\  ( A  e.  Q  /\  B  e.  Q  /\  C  e.  Q
)  /\  ( D  e.  Q  /\  E  e.  Q  /\  F  e.  Q ) )  /\  ze )  ->  E. x  e.  S  E. a  e.  P  E. b  e.  P  E. c  e.  P  E. d  e.  P  E. e  e.  P  E. f  e.  P  ( <. a ,  <. b ,  c
>. >.  =  <. A ,  <. B ,  C >. >.  /\  <. d ,  <. e ,  f >. >.  =  <. D ,  <. E ,  F >. >.  /\  ph ) )
103102ex 423 . . 3  |-  ( ( X  e.  S  /\  ( A  e.  Q  /\  B  e.  Q  /\  C  e.  Q
)  /\  ( D  e.  Q  /\  E  e.  Q  /\  F  e.  Q ) )  -> 
( ze  ->  E. x  e.  S  E. a  e.  P  E. b  e.  P  E. c  e.  P  E. d  e.  P  E. e  e.  P  E. f  e.  P  ( <. a ,  <. b ,  c
>. >.  =  <. A ,  <. B ,  C >. >.  /\  <. d ,  <. e ,  f >. >.  =  <. D ,  <. E ,  F >. >.  /\  ph ) ) )
10453, 103impbid 183 . 2  |-  ( ( X  e.  S  /\  ( A  e.  Q  /\  B  e.  Q  /\  C  e.  Q
)  /\  ( D  e.  Q  /\  E  e.  Q  /\  F  e.  Q ) )  -> 
( E. x  e.  S  E. a  e.  P  E. b  e.  P  E. c  e.  P  E. d  e.  P  E. e  e.  P  E. f  e.  P  ( <. a ,  <. b ,  c
>. >.  =  <. A ,  <. B ,  C >. >.  /\  <. d ,  <. e ,  f >. >.  =  <. D ,  <. E ,  F >. >.  /\  ph )  <->  ze )
)
10520, 104syl5bb 248 1  |-  ( ( X  e.  S  /\  ( A  e.  Q  /\  B  e.  Q  /\  C  e.  Q
)  /\  ( D  e.  Q  /\  E  e.  Q  /\  F  e.  Q ) )  -> 
( <. A ,  <. B ,  C >. >. R <. D ,  <. E ,  F >. >. 
<->  ze ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358    /\ w3a 934    = wceq 1623    e. wcel 1684   E.wrex 2544   <.cop 3643   class class class wbr 4023   {copab 4076
This theorem is referenced by:  brcgr3  24669
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-sep 4141  ax-nul 4149  ax-pr 4214
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-mo 2148  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-ral 2548  df-rex 2549  df-rab 2552  df-v 2790  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-br 4024  df-opab 4078
  Copyright terms: Public domain W3C validator