Metamath Proof Explorer

Theorem br8

Description: Substitution for an eight-place predicate. (Contributed by Scott Fenton, 26-Sep-2013) (Revised by Mario Carneiro, 3-May-2015)

Ref Expression
Hypotheses br8.1 
|- ( a = A -> ( ph <-> ps ) )
br8.2 
|- ( b = B -> ( ps <-> ch ) )
br8.3 
|- ( c = C -> ( ch <-> th ) )
br8.4 
|- ( d = D -> ( th <-> ta ) )
br8.5 
|- ( e = E -> ( ta <-> et ) )
br8.6 
|- ( f = F -> ( et <-> ze ) )
br8.7 
|- ( g = G -> ( ze <-> si ) )
br8.8 
|- ( h = H -> ( si <-> rh ) )
br8.9 
|- ( x = X -> P = Q )
br8.10 
|- 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 E. g e. P E. h e. P ( p = <. <. a , b >. , <. c , d >. >. /\ q = <. <. e , f >. , <. g , h >. >. /\ ph ) }
Assertion br8 
|- ( ( ( X e. S /\ A e. Q /\ B e. Q ) /\ ( C e. Q /\ D e. Q /\ E e. Q ) /\ ( F e. Q /\ G e. Q /\ H e. Q ) ) -> ( <. <. A , B >. , <. C , D >. >. R <. <. E , F >. , <. G , H >. >. <-> rh ) )

Proof

Step Hyp Ref Expression
1 br8.1 
 |-  ( a = A -> ( ph <-> ps ) )
2 br8.2 
 |-  ( b = B -> ( ps <-> ch ) )
3 br8.3 
 |-  ( c = C -> ( ch <-> th ) )
4 br8.4 
 |-  ( d = D -> ( th <-> ta ) )
5 br8.5 
 |-  ( e = E -> ( ta <-> et ) )
6 br8.6 
 |-  ( f = F -> ( et <-> ze ) )
7 br8.7 
 |-  ( g = G -> ( ze <-> si ) )
8 br8.8 
 |-  ( h = H -> ( si <-> rh ) )
9 br8.9 
 |-  ( x = X -> P = Q )
10 br8.10 
 |-  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 E. g e. P E. h e. P ( p = <. <. a , b >. , <. c , d >. >. /\ q = <. <. e , f >. , <. g , h >. >. /\ ph ) }
11 opex 
 |-  <. <. A , B >. , <. C , D >. >. e. _V
12 opex 
 |-  <. <. E , F >. , <. G , H >. >. e. _V
13 eqeq1 
 |-  ( p = <. <. A , B >. , <. C , D >. >. -> ( p = <. <. a , b >. , <. c , d >. >. <-> <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. ) )
14 13 3anbi1d 
 |-  ( p = <. <. A , B >. , <. C , D >. >. -> ( ( p = <. <. a , b >. , <. c , d >. >. /\ q = <. <. e , f >. , <. g , h >. >. /\ ph ) <-> ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. /\ q = <. <. e , f >. , <. g , h >. >. /\ ph ) ) )
15 14 rexbidv 
 |-  ( p = <. <. A , B >. , <. C , D >. >. -> ( E. h e. P ( p = <. <. a , b >. , <. c , d >. >. /\ q = <. <. e , f >. , <. g , h >. >. /\ ph ) <-> E. h e. P ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. /\ q = <. <. e , f >. , <. g , h >. >. /\ ph ) ) )
16 15 2rexbidv 
 |-  ( 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 >. >. /\ ph ) <-> 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 >. >. /\ ph ) ) )
17 16 2rexbidv 
 |-  ( 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 >. >. /\ ph ) <-> 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 >. >. /\ ph ) ) )
18 17 2rexbidv 
 |-  ( 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 >. >. /\ ph ) <-> 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 >. >. /\ ph ) ) )
19 18 2rexbidv 
 |-  ( p = <. <. A , B >. , <. C , D >. >. -> ( 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 E. g e. P E. h e. P ( p = <. <. a , b >. , <. c , d >. >. /\ q = <. <. e , f >. , <. g , h >. >. /\ 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 E. g e. P E. h e. P ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. /\ q = <. <. e , f >. , <. g , h >. >. /\ ph ) ) )
20 eqeq1 
 |-  ( q = <. <. E , F >. , <. G , H >. >. -> ( q = <. <. e , f >. , <. g , h >. >. <-> <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. ) )
21 20 3anbi2d 
 |-  ( q = <. <. E , F >. , <. G , H >. >. -> ( ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. /\ q = <. <. e , f >. , <. g , h >. >. /\ ph ) <-> ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ph ) ) )
22 21 rexbidv 
 |-  ( q = <. <. E , F >. , <. G , H >. >. -> ( E. h e. P ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. /\ q = <. <. e , f >. , <. g , h >. >. /\ ph ) <-> E. h e. P ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ph ) ) )
23 22 2rexbidv 
 |-  ( 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 >. >. /\ ph ) <-> 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 >. >. /\ ph ) ) )
24 23 2rexbidv 
 |-  ( 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 >. >. /\ ph ) <-> 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 >. >. /\ ph ) ) )
25 24 2rexbidv 
 |-  ( 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 >. >. /\ ph ) <-> 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 >. >. /\ ph ) ) )
26 25 2rexbidv 
 |-  ( q = <. <. E , F >. , <. G , H >. >. -> ( 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 E. g e. P E. h e. P ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. /\ q = <. <. e , f >. , <. g , h >. >. /\ 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 E. g e. P E. h e. P ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ph ) ) )
27 11 12 19 26 10 brab 
 |-  ( <. <. A , B >. , <. C , D >. >. R <. <. E , F >. , <. G , H >. >. <-> 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 E. g e. P E. h e. P ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ph ) )
28 opex 
 |-  <. a , b >. e. _V
29 opex 
 |-  <. c , d >. e. _V
30 28 29 opth 
 |-  ( <. <. a , b >. , <. c , d >. >. = <. <. A , B >. , <. C , D >. >. <-> ( <. a , b >. = <. A , B >. /\ <. c , d >. = <. C , D >. ) )
31 vex 
 |-  a e. _V
32 vex 
 |-  b e. _V
33 31 32 opth 
 |-  ( <. a , b >. = <. A , B >. <-> ( a = A /\ b = B ) )
34 1 2 sylan9bb 
 |-  ( ( a = A /\ b = B ) -> ( ph <-> ch ) )
35 33 34 sylbi 
 |-  ( <. a , b >. = <. A , B >. -> ( ph <-> ch ) )
36 vex 
 |-  c e. _V
37 vex 
 |-  d e. _V
38 36 37 opth 
 |-  ( <. c , d >. = <. C , D >. <-> ( c = C /\ d = D ) )
39 3 4 sylan9bb 
 |-  ( ( c = C /\ d = D ) -> ( ch <-> ta ) )
40 38 39 sylbi 
 |-  ( <. c , d >. = <. C , D >. -> ( ch <-> ta ) )
41 35 40 sylan9bb 
 |-  ( ( <. a , b >. = <. A , B >. /\ <. c , d >. = <. C , D >. ) -> ( ph <-> ta ) )
42 30 41 sylbi 
 |-  ( <. <. a , b >. , <. c , d >. >. = <. <. A , B >. , <. C , D >. >. -> ( ph <-> ta ) )
43 42 eqcoms 
 |-  ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. -> ( ph <-> ta ) )
44 opex 
 |-  <. e , f >. e. _V
45 opex 
 |-  <. g , h >. e. _V
46 44 45 opth 
 |-  ( <. <. e , f >. , <. g , h >. >. = <. <. E , F >. , <. G , H >. >. <-> ( <. e , f >. = <. E , F >. /\ <. g , h >. = <. G , H >. ) )
47 vex 
 |-  e e. _V
48 vex 
 |-  f e. _V
49 47 48 opth 
 |-  ( <. e , f >. = <. E , F >. <-> ( e = E /\ f = F ) )
50 5 6 sylan9bb 
 |-  ( ( e = E /\ f = F ) -> ( ta <-> ze ) )
51 49 50 sylbi 
 |-  ( <. e , f >. = <. E , F >. -> ( ta <-> ze ) )
52 vex 
 |-  g e. _V
53 vex 
 |-  h e. _V
54 52 53 opth 
 |-  ( <. g , h >. = <. G , H >. <-> ( g = G /\ h = H ) )
55 7 8 sylan9bb 
 |-  ( ( g = G /\ h = H ) -> ( ze <-> rh ) )
56 54 55 sylbi 
 |-  ( <. g , h >. = <. G , H >. -> ( ze <-> rh ) )
57 51 56 sylan9bb 
 |-  ( ( <. e , f >. = <. E , F >. /\ <. g , h >. = <. G , H >. ) -> ( ta <-> rh ) )
58 46 57 sylbi 
 |-  ( <. <. e , f >. , <. g , h >. >. = <. <. E , F >. , <. G , H >. >. -> ( ta <-> rh ) )
59 58 eqcoms 
 |-  ( <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. -> ( ta <-> rh ) )
60 43 59 sylan9bb 
 |-  ( ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. ) -> ( ph <-> rh ) )
61 60 biimp3a 
 |-  ( ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ph ) -> rh )
62 61 a1i 
 |-  ( ( ( ( ( ( ( ( X e. S /\ A e. Q /\ B e. Q ) /\ ( C e. Q /\ D e. Q /\ E e. Q ) /\ ( F e. Q /\ G e. Q /\ H e. Q ) ) /\ ( x e. S /\ 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 >. >. /\ ph ) -> rh ) )
63 62 rexlimdva 
 |-  ( ( ( ( ( ( ( X e. S /\ A e. Q /\ B e. Q ) /\ ( C e. Q /\ D e. Q /\ E e. Q ) /\ ( F e. Q /\ G e. Q /\ H e. Q ) ) /\ ( x e. S /\ 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 >. >. /\ ph ) -> rh ) )
64 63 rexlimdvva 
 |-  ( ( ( ( ( ( X e. S /\ A e. Q /\ B e. Q ) /\ ( C e. Q /\ D e. Q /\ E e. Q ) /\ ( F e. Q /\ G e. Q /\ H e. Q ) ) /\ ( x e. S /\ 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 >. >. /\ ph ) -> rh ) )
65 64 rexlimdvva 
 |-  ( ( ( ( ( X e. S /\ A e. Q /\ B e. Q ) /\ ( C e. Q /\ D e. Q /\ E e. Q ) /\ ( F e. Q /\ G e. Q /\ H 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 E. g e. P E. h e. P ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ph ) -> rh ) )
66 65 rexlimdvva 
 |-  ( ( ( ( X e. S /\ A e. Q /\ B e. Q ) /\ ( C e. Q /\ D e. Q /\ E e. Q ) /\ ( F e. Q /\ G e. Q /\ H 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 E. g e. P E. h e. P ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ph ) -> rh ) )
67 66 rexlimdvva 
 |-  ( ( ( X e. S /\ A e. Q /\ B e. Q ) /\ ( C e. Q /\ D e. Q /\ E e. Q ) /\ ( F e. Q /\ G e. Q /\ H 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 E. g e. P E. h e. P ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ph ) -> rh ) )
68 simpl11 
 |-  ( ( ( ( X e. S /\ A e. Q /\ B e. Q ) /\ ( C e. Q /\ D e. Q /\ E e. Q ) /\ ( F e. Q /\ G e. Q /\ H e. Q ) ) /\ rh ) -> X e. S )
69 simpl12 
 |-  ( ( ( ( X e. S /\ A e. Q /\ B e. Q ) /\ ( C e. Q /\ D e. Q /\ E e. Q ) /\ ( F e. Q /\ G e. Q /\ H e. Q ) ) /\ rh ) -> A e. Q )
70 simpl13 
 |-  ( ( ( ( X e. S /\ A e. Q /\ B e. Q ) /\ ( C e. Q /\ D e. Q /\ E e. Q ) /\ ( F e. Q /\ G e. Q /\ H e. Q ) ) /\ rh ) -> B e. Q )
71 simpl21 
 |-  ( ( ( ( X e. S /\ A e. Q /\ B e. Q ) /\ ( C e. Q /\ D e. Q /\ E e. Q ) /\ ( F e. Q /\ G e. Q /\ H e. Q ) ) /\ rh ) -> C e. Q )
72 simpl22 
 |-  ( ( ( ( X e. S /\ A e. Q /\ B e. Q ) /\ ( C e. Q /\ D e. Q /\ E e. Q ) /\ ( F e. Q /\ G e. Q /\ H e. Q ) ) /\ rh ) -> D e. Q )
73 simpl23 
 |-  ( ( ( ( X e. S /\ A e. Q /\ B e. Q ) /\ ( C e. Q /\ D e. Q /\ E e. Q ) /\ ( F e. Q /\ G e. Q /\ H e. Q ) ) /\ rh ) -> E e. Q )
74 simpl31 
 |-  ( ( ( ( X e. S /\ A e. Q /\ B e. Q ) /\ ( C e. Q /\ D e. Q /\ E e. Q ) /\ ( F e. Q /\ G e. Q /\ H e. Q ) ) /\ rh ) -> F e. Q )
75 simpl32 
 |-  ( ( ( ( X e. S /\ A e. Q /\ B e. Q ) /\ ( C e. Q /\ D e. Q /\ E e. Q ) /\ ( F e. Q /\ G e. Q /\ H e. Q ) ) /\ rh ) -> G e. Q )
76 simpl33 
 |-  ( ( ( ( X e. S /\ A e. Q /\ B e. Q ) /\ ( C e. Q /\ D e. Q /\ E e. Q ) /\ ( F e. Q /\ G e. Q /\ H e. Q ) ) /\ rh ) -> H e. Q )
77 eqidd 
 |-  ( ( ( ( X e. S /\ A e. Q /\ B e. Q ) /\ ( C e. Q /\ D e. Q /\ E e. Q ) /\ ( F e. Q /\ G e. Q /\ H e. Q ) ) /\ rh ) -> <. <. A , B >. , <. C , D >. >. = <. <. A , B >. , <. C , D >. >. )
78 eqidd 
 |-  ( ( ( ( X e. S /\ A e. Q /\ B e. Q ) /\ ( C e. Q /\ D e. Q /\ E e. Q ) /\ ( F e. Q /\ G e. Q /\ H e. Q ) ) /\ rh ) -> <. <. E , F >. , <. G , H >. >. = <. <. E , F >. , <. G , H >. >. )
79 simpr 
 |-  ( ( ( ( X e. S /\ A e. Q /\ B e. Q ) /\ ( C e. Q /\ D e. Q /\ E e. Q ) /\ ( F e. Q /\ G e. Q /\ H e. Q ) ) /\ rh ) -> rh )
80 opeq1 
 |-  ( g = G -> <. g , h >. = <. G , h >. )
81 80 opeq2d 
 |-  ( g = G -> <. <. E , F >. , <. g , h >. >. = <. <. E , F >. , <. G , h >. >. )
82 81 eqeq2d 
 |-  ( g = G -> ( <. <. E , F >. , <. G , H >. >. = <. <. E , F >. , <. g , h >. >. <-> <. <. E , F >. , <. G , H >. >. = <. <. E , F >. , <. G , h >. >. ) )
83 82 7 3anbi23d 
 |-  ( g = G -> ( ( <. <. 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 ) ) )
84 opeq2 
 |-  ( h = H -> <. G , h >. = <. G , H >. )
85 84 opeq2d 
 |-  ( h = H -> <. <. E , F >. , <. G , h >. >. = <. <. E , F >. , <. G , H >. >. )
86 85 eqeq2d 
 |-  ( h = H -> ( <. <. E , F >. , <. G , H >. >. = <. <. E , F >. , <. G , h >. >. <-> <. <. E , F >. , <. G , H >. >. = <. <. E , F >. , <. G , H >. >. ) )
87 86 8 3anbi23d 
 |-  ( h = H -> ( ( <. <. 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 ) ) )
88 83 87 rspc2ev 
 |-  ( ( G e. Q /\ H e. Q /\ ( <. <. A , B >. , <. C , D >. >. = <. <. A , B >. , <. C , D >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. E , F >. , <. G , H >. >. /\ rh ) ) -> E. g e. Q E. h e. Q ( <. <. A , B >. , <. C , D >. >. = <. <. A , B >. , <. C , D >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. E , F >. , <. g , h >. >. /\ ze ) )
89 75 76 77 78 79 88 syl113anc 
 |-  ( ( ( ( X e. S /\ A e. Q /\ B e. Q ) /\ ( C e. Q /\ D e. Q /\ E e. Q ) /\ ( F e. Q /\ G e. Q /\ H e. Q ) ) /\ rh ) -> E. g e. Q E. h e. Q ( <. <. A , B >. , <. C , D >. >. = <. <. A , B >. , <. C , D >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. E , F >. , <. g , h >. >. /\ ze ) )
90 opeq2 
 |-  ( d = D -> <. C , d >. = <. C , D >. )
91 90 opeq2d 
 |-  ( d = D -> <. <. A , B >. , <. C , d >. >. = <. <. A , B >. , <. C , D >. >. )
92 91 eqeq2d 
 |-  ( d = D -> ( <. <. A , B >. , <. C , D >. >. = <. <. A , B >. , <. C , d >. >. <-> <. <. A , B >. , <. C , D >. >. = <. <. A , B >. , <. C , D >. >. ) )
93 92 4 3anbi13d 
 |-  ( d = D -> ( ( <. <. 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 ) ) )
94 93 2rexbidv 
 |-  ( d = D -> ( E. g e. Q E. h e. Q ( <. <. A , B >. , <. C , D >. >. = <. <. A , B >. , <. C , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ th ) <-> E. g e. Q E. h e. Q ( <. <. A , B >. , <. C , D >. >. = <. <. A , B >. , <. C , D >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ta ) ) )
95 opeq1 
 |-  ( e = E -> <. e , f >. = <. E , f >. )
96 95 opeq1d 
 |-  ( e = E -> <. <. e , f >. , <. g , h >. >. = <. <. E , f >. , <. g , h >. >. )
97 96 eqeq2d 
 |-  ( e = E -> ( <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. <-> <. <. E , F >. , <. G , H >. >. = <. <. E , f >. , <. g , h >. >. ) )
98 97 5 3anbi23d 
 |-  ( e = E -> ( ( <. <. 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 ) ) )
99 98 2rexbidv 
 |-  ( e = E -> ( E. g e. Q E. h e. Q ( <. <. A , B >. , <. C , D >. >. = <. <. A , B >. , <. C , D >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ta ) <-> E. g e. Q E. h e. Q ( <. <. A , B >. , <. C , D >. >. = <. <. A , B >. , <. C , D >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. E , f >. , <. g , h >. >. /\ et ) ) )
100 opeq2 
 |-  ( f = F -> <. E , f >. = <. E , F >. )
101 100 opeq1d 
 |-  ( f = F -> <. <. E , f >. , <. g , h >. >. = <. <. E , F >. , <. g , h >. >. )
102 101 eqeq2d 
 |-  ( f = F -> ( <. <. E , F >. , <. G , H >. >. = <. <. E , f >. , <. g , h >. >. <-> <. <. E , F >. , <. G , H >. >. = <. <. E , F >. , <. g , h >. >. ) )
103 102 6 3anbi23d 
 |-  ( f = F -> ( ( <. <. 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 ) ) )
104 103 2rexbidv 
 |-  ( f = F -> ( E. g e. Q E. h e. Q ( <. <. A , B >. , <. C , D >. >. = <. <. A , B >. , <. C , D >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. E , f >. , <. g , h >. >. /\ et ) <-> E. g e. Q E. h e. Q ( <. <. A , B >. , <. C , D >. >. = <. <. A , B >. , <. C , D >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. E , F >. , <. g , h >. >. /\ ze ) ) )
105 94 99 104 rspc3ev 
 |-  ( ( ( D e. Q /\ E e. Q /\ F e. Q ) /\ E. g e. Q E. h e. Q ( <. <. A , B >. , <. C , D >. >. = <. <. A , B >. , <. C , D >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. E , F >. , <. g , h >. >. /\ ze ) ) -> E. d e. Q E. e e. Q E. f e. Q E. g e. Q E. h e. Q ( <. <. A , B >. , <. C , D >. >. = <. <. A , B >. , <. C , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ th ) )
106 72 73 74 89 105 syl31anc 
 |-  ( ( ( ( X e. S /\ A e. Q /\ B e. Q ) /\ ( C e. Q /\ D e. Q /\ E e. Q ) /\ ( F e. Q /\ G e. Q /\ H e. Q ) ) /\ rh ) -> E. d e. Q E. e e. Q E. f e. Q E. g e. Q E. h e. Q ( <. <. A , B >. , <. C , D >. >. = <. <. A , B >. , <. C , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ th ) )
107 opeq1 
 |-  ( a = A -> <. a , b >. = <. A , b >. )
108 107 opeq1d 
 |-  ( a = A -> <. <. a , b >. , <. c , d >. >. = <. <. A , b >. , <. c , d >. >. )
109 108 eqeq2d 
 |-  ( a = A -> ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. <-> <. <. A , B >. , <. C , D >. >. = <. <. A , b >. , <. c , d >. >. ) )
110 109 1 3anbi13d 
 |-  ( a = A -> ( ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ph ) <-> ( <. <. A , B >. , <. C , D >. >. = <. <. A , b >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ps ) ) )
111 110 rexbidv 
 |-  ( a = A -> ( E. h e. Q ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ph ) <-> E. h e. Q ( <. <. A , B >. , <. C , D >. >. = <. <. A , b >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ps ) ) )
112 111 2rexbidv 
 |-  ( a = A -> ( E. f e. Q E. g e. Q E. h e. Q ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ph ) <-> E. f e. Q E. g e. Q E. h e. Q ( <. <. A , B >. , <. C , D >. >. = <. <. A , b >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ps ) ) )
113 112 2rexbidv 
 |-  ( a = A -> ( E. d e. Q E. e e. Q E. f e. Q E. g e. Q E. h e. Q ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ph ) <-> E. d e. Q E. e e. Q E. f e. Q E. g e. Q E. h e. Q ( <. <. A , B >. , <. C , D >. >. = <. <. A , b >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ps ) ) )
114 opeq2 
 |-  ( b = B -> <. A , b >. = <. A , B >. )
115 114 opeq1d 
 |-  ( b = B -> <. <. A , b >. , <. c , d >. >. = <. <. A , B >. , <. c , d >. >. )
116 115 eqeq2d 
 |-  ( b = B -> ( <. <. A , B >. , <. C , D >. >. = <. <. A , b >. , <. c , d >. >. <-> <. <. A , B >. , <. C , D >. >. = <. <. A , B >. , <. c , d >. >. ) )
117 116 2 3anbi13d 
 |-  ( b = B -> ( ( <. <. 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 ) ) )
118 117 rexbidv 
 |-  ( b = B -> ( E. h e. Q ( <. <. A , B >. , <. C , D >. >. = <. <. A , b >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ps ) <-> E. h e. Q ( <. <. A , B >. , <. C , D >. >. = <. <. A , B >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ch ) ) )
119 118 2rexbidv 
 |-  ( b = B -> ( E. f e. Q E. g e. Q E. h e. Q ( <. <. A , B >. , <. C , D >. >. = <. <. A , b >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ps ) <-> E. f e. Q E. g e. Q E. h e. Q ( <. <. A , B >. , <. C , D >. >. = <. <. A , B >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ch ) ) )
120 119 2rexbidv 
 |-  ( b = B -> ( E. d e. Q E. e e. Q E. f e. Q E. g e. Q E. h e. Q ( <. <. A , B >. , <. C , D >. >. = <. <. A , b >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ps ) <-> E. d e. Q E. e e. Q E. f e. Q E. g e. Q E. h e. Q ( <. <. A , B >. , <. C , D >. >. = <. <. A , B >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ch ) ) )
121 opeq1 
 |-  ( c = C -> <. c , d >. = <. C , d >. )
122 121 opeq2d 
 |-  ( c = C -> <. <. A , B >. , <. c , d >. >. = <. <. A , B >. , <. C , d >. >. )
123 122 eqeq2d 
 |-  ( c = C -> ( <. <. A , B >. , <. C , D >. >. = <. <. A , B >. , <. c , d >. >. <-> <. <. A , B >. , <. C , D >. >. = <. <. A , B >. , <. C , d >. >. ) )
124 123 3 3anbi13d 
 |-  ( c = C -> ( ( <. <. 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 ) ) )
125 124 rexbidv 
 |-  ( c = C -> ( E. h e. Q ( <. <. A , B >. , <. C , D >. >. = <. <. A , B >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ch ) <-> E. h e. Q ( <. <. A , B >. , <. C , D >. >. = <. <. A , B >. , <. C , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ th ) ) )
126 125 2rexbidv 
 |-  ( c = C -> ( E. f e. Q E. g e. Q E. h e. Q ( <. <. A , B >. , <. C , D >. >. = <. <. A , B >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ch ) <-> E. f e. Q E. g e. Q E. h e. Q ( <. <. A , B >. , <. C , D >. >. = <. <. A , B >. , <. C , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ th ) ) )
127 126 2rexbidv 
 |-  ( c = C -> ( E. d e. Q E. e e. Q E. f e. Q E. g e. Q E. h e. Q ( <. <. A , B >. , <. C , D >. >. = <. <. A , B >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ch ) <-> E. d e. Q E. e e. Q E. f e. Q E. g e. Q E. h e. Q ( <. <. A , B >. , <. C , D >. >. = <. <. A , B >. , <. C , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ th ) ) )
128 113 120 127 rspc3ev 
 |-  ( ( ( A e. Q /\ B e. Q /\ C e. Q ) /\ E. d e. Q E. e e. Q E. f e. Q E. g e. Q E. h e. Q ( <. <. A , B >. , <. C , D >. >. = <. <. A , B >. , <. C , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ 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 E. g e. Q E. h e. Q ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ph ) )
129 69 70 71 106 128 syl31anc 
 |-  ( ( ( ( X e. S /\ A e. Q /\ B e. Q ) /\ ( C e. Q /\ D e. Q /\ E e. Q ) /\ ( F e. Q /\ G e. Q /\ H e. Q ) ) /\ rh ) -> E. a e. Q E. b e. Q E. c e. Q E. d e. Q E. e e. Q E. f e. Q E. g e. Q E. h e. Q ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ph ) )
130 9 rexeqdv 
 |-  ( x = X -> ( E. h e. P ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ph ) <-> E. h e. Q ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ph ) ) )
131 9 130 rexeqbidv 
 |-  ( x = X -> ( E. g e. P E. h e. P ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ph ) <-> E. g e. Q E. h e. Q ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ph ) ) )
132 9 131 rexeqbidv 
 |-  ( x = X -> ( 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 >. >. /\ ph ) <-> E. f e. Q E. g e. Q E. h e. Q ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ph ) ) )
133 9 132 rexeqbidv 
 |-  ( x = X -> ( 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 >. >. /\ ph ) <-> E. e e. Q E. f e. Q E. g e. Q E. h e. Q ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ph ) ) )
134 9 133 rexeqbidv 
 |-  ( x = X -> ( 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 >. >. /\ ph ) <-> E. d e. Q E. e e. Q E. f e. Q E. g e. Q E. h e. Q ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ph ) ) )
135 9 134 rexeqbidv 
 |-  ( x = X -> ( 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 >. >. /\ ph ) <-> E. c e. Q E. d e. Q E. e e. Q E. f e. Q E. g e. Q E. h e. Q ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ph ) ) )
136 9 135 rexeqbidv 
 |-  ( x = X -> ( 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 >. >. /\ ph ) <-> E. b e. Q E. c e. Q E. d e. Q E. e e. Q E. f e. Q E. g e. Q E. h e. Q ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ph ) ) )
137 9 136 rexeqbidv 
 |-  ( 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 E. g e. P E. h e. P ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ 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 E. g e. Q E. h e. Q ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ph ) ) )
138 137 rspcev 
 |-  ( ( 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 E. g e. Q E. h e. Q ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ 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 E. g e. P E. h e. P ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ph ) )
139 68 129 138 syl2anc 
 |-  ( ( ( ( X e. S /\ A e. Q /\ B e. Q ) /\ ( C e. Q /\ D e. Q /\ E e. Q ) /\ ( F e. Q /\ G e. Q /\ H e. Q ) ) /\ rh ) -> 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 E. g e. P E. h e. P ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ph ) )
140 139 ex 
 |-  ( ( ( X e. S /\ A e. Q /\ B e. Q ) /\ ( C e. Q /\ D e. Q /\ E e. Q ) /\ ( F e. Q /\ G e. Q /\ H e. Q ) ) -> ( rh -> 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 E. g e. P E. h e. P ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ph ) ) )
141 67 140 impbid 
 |-  ( ( ( X e. S /\ A e. Q /\ B e. Q ) /\ ( C e. Q /\ D e. Q /\ E e. Q ) /\ ( F e. Q /\ G e. Q /\ H 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 E. g e. P E. h e. P ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ph ) <-> rh ) )
142 27 141 bitrid 
 |-  ( ( ( X e. S /\ A e. Q /\ B e. Q ) /\ ( C e. Q /\ D e. Q /\ E e. Q ) /\ ( F e. Q /\ G e. Q /\ H e. Q ) ) -> ( <. <. A , B >. , <. C , D >. >. R <. <. E , F >. , <. G , H >. >. <-> rh ) )