Metamath Proof Explorer

Theorem br8d

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)

Ref Expression
Hypotheses 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 br8d 
|- ( ph -> ( <. <. A , B >. , <. C , D >. >. R <. <. E , F >. , <. G , H >. >. <-> mu ) )

Proof

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