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 φ ψ
br8.2 b = B ψ χ
br8.3 c = C χ θ
br8.4 d = D θ τ
br8.5 e = E τ η
br8.6 f = F η ζ
br8.7 g = G ζ σ
br8.8 h = H σ ρ
br8.9 x = X P = Q
br8.10 R = p q | x S a P b P c P d P e P f P g P h P p = a b c d q = e f g h φ
Assertion br8 X S A Q B Q C Q D Q E Q F Q G Q H Q A B C D R E F G H ρ

Proof

Step Hyp Ref Expression
1 br8.1 a = A φ ψ
2 br8.2 b = B ψ χ
3 br8.3 c = C χ θ
4 br8.4 d = D θ τ
5 br8.5 e = E τ η
6 br8.6 f = F η ζ
7 br8.7 g = G ζ σ
8 br8.8 h = H σ ρ
9 br8.9 x = X P = Q
10 br8.10 R = p q | x S a P b P c P d P e P f P g P h P p = a b c d q = e f g h φ
11 opex A B C D V
12 opex E F G H 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 φ A B C D = a b c d q = e f g h φ
15 14 rexbidv p = A B C D h P p = a b c d q = e f g h φ h P A B C D = a b c d q = e f g h φ
16 15 2rexbidv p = A B C D f P g P h P p = a b c d q = e f g h φ f P g P h P A B C D = a b c d q = e f g h φ
17 16 2rexbidv p = A B C D d P e P f P g P h P p = a b c d q = e f g h φ d P e P f P g P h P A B C D = a b c d q = e f g h φ
18 17 2rexbidv p = A B C D b P c P d P e P f P g P h P p = a b c d q = e f g h φ b P c P d P e P f P g P h P A B C D = a b c d q = e f g h φ
19 18 2rexbidv p = A B C D x S a P b P c P d P e P f P g P h P p = a b c d q = e f g h φ x S a P b P c P d P e P f P g P h P A B C D = a b c d q = e f g h φ
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 φ A B C D = a b c d E F G H = e f g h φ
22 21 rexbidv q = E F G H h P A B C D = a b c d q = e f g h φ h P A B C D = a b c d E F G H = e f g h φ
23 22 2rexbidv q = E F G H f P g P h P A B C D = a b c d q = e f g h φ f P g P h P A B C D = a b c d E F G H = e f g h φ
24 23 2rexbidv q = E F G H d P e P f P g P h P A B C D = a b c d q = e f g h φ d P e P f P g P h P A B C D = a b c d E F G H = e f g h φ
25 24 2rexbidv q = E F G H b P c P d P e P f P g P h P A B C D = a b c d q = e f g h φ b P c P d P e P f P g P h P A B C D = a b c d E F G H = e f g h φ
26 25 2rexbidv q = E F G H x S a P b P c P d P e P f P g P h P A B C D = a b c d q = e f g h φ x S a P b P c P d P e P f P g P h P A B C D = a b c d E F G H = e f g h φ
27 11 12 19 26 10 brab A B C D R E F G H x S a P b P c P d P e P f P g P h P A B C D = a b c d E F G H = e f g h φ
28 opex a b V
29 opex c d V
30 28 29 opth a b c d = A B C D a b = A B c d = C D
31 vex a V
32 vex b V
33 31 32 opth a b = A B a = A b = B
34 1 2 sylan9bb a = A b = B φ χ
35 33 34 sylbi a b = A B φ χ
36 vex c V
37 vex d V
38 36 37 opth c d = C D c = C d = D
39 3 4 sylan9bb c = C d = D χ τ
40 38 39 sylbi c d = C D χ τ
41 35 40 sylan9bb a b = A B c d = C D φ τ
42 30 41 sylbi a b c d = A B C D φ τ
43 42 eqcoms A B C D = a b c d φ τ
44 opex e f V
45 opex g h V
46 44 45 opth e f g h = E F G H e f = E F g h = G H
47 vex e V
48 vex f V
49 47 48 opth e f = E F e = E f = F
50 5 6 sylan9bb e = E f = F τ ζ
51 49 50 sylbi e f = E F τ ζ
52 vex g V
53 vex h V
54 52 53 opth g h = G H g = G h = H
55 7 8 sylan9bb g = G h = H ζ ρ
56 54 55 sylbi g h = G H ζ ρ
57 51 56 sylan9bb e f = E F g h = G H τ ρ
58 46 57 sylbi e f g h = E F G H τ ρ
59 58 eqcoms E F G H = e f g h τ ρ
60 43 59 sylan9bb A B C D = a b c d E F G H = e f g h φ ρ
61 60 biimp3a A B C D = a b c d E F G H = e f g h φ ρ
62 61 a1i X S A Q B Q C Q D Q E Q F Q G Q H Q x S a P b P c P d P e P f P g P h P A B C D = a b c d E F G H = e f g h φ ρ
63 62 rexlimdva X S A Q B Q C Q D Q E Q F Q G Q H Q x S a P b P c P d P e P f P g P h P A B C D = a b c d E F G H = e f g h φ ρ
64 63 rexlimdvva X S A Q B Q C Q D Q E Q F Q G Q H Q x S a P b P c P d P e P f P g P h P A B C D = a b c d E F G H = e f g h φ ρ
65 64 rexlimdvva X S A Q B Q C Q D Q E Q F Q G Q H Q x S a P b P c P d P e P f P g P h P A B C D = a b c d E F G H = e f g h φ ρ
66 65 rexlimdvva X S A Q B Q C Q D Q E Q F Q G Q H Q x S a P b P c P d P e P f P g P h P A B C D = a b c d E F G H = e f g h φ ρ
67 66 rexlimdvva X S A Q B Q C Q D Q E Q F Q G Q H Q x S a P b P c P d P e P f P g P h P A B C D = a b c d E F G H = e f g h φ ρ
68 simpl11 X S A Q B Q C Q D Q E Q F Q G Q H Q ρ X S
69 simpl12 X S A Q B Q C Q D Q E Q F Q G Q H Q ρ A Q
70 simpl13 X S A Q B Q C Q D Q E Q F Q G Q H Q ρ B Q
71 simpl21 X S A Q B Q C Q D Q E Q F Q G Q H Q ρ C Q
72 simpl22 X S A Q B Q C Q D Q E Q F Q G Q H Q ρ D Q
73 simpl23 X S A Q B Q C Q D Q E Q F Q G Q H Q ρ E Q
74 simpl31 X S A Q B Q C Q D Q E Q F Q G Q H Q ρ F Q
75 simpl32 X S A Q B Q C Q D Q E Q F Q G Q H Q ρ G Q
76 simpl33 X S A Q B Q C Q D Q E Q F Q G Q H Q ρ H Q
77 eqidd X S A Q B Q C Q D Q E Q F Q G Q H Q ρ A B C D = A B C D
78 eqidd X S A Q B Q C Q D Q E Q F Q G Q H Q ρ E F G H = E F G H
79 simpr X S A Q B Q C Q D Q E Q F Q G Q H Q ρ ρ
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 ζ A B C D = A B C D E F G H = E F G h σ
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 σ A B C D = A B C D E F G H = E F G H ρ
88 83 87 rspc2ev G Q H Q A B C D = A B C D E F G H = E F G H ρ g Q h Q A B C D = A B C D E F G H = E F g h ζ
89 75 76 77 78 79 88 syl113anc X S A Q B Q C Q D Q E Q F Q G Q H Q ρ g Q h Q A B C D = A B C D E F G H = E F g h ζ
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 θ A B C D = A B C D E F G H = e f g h τ
94 93 2rexbidv d = D g Q h Q A B C D = A B C d E F G H = e f g h θ g Q h Q A B C D = A B C D E F G H = e f g h τ
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 τ A B C D = A B C D E F G H = E f g h η
99 98 2rexbidv e = E g Q h Q A B C D = A B C D E F G H = e f g h τ g Q h Q A B C D = A B C D E F G H = E f g h η
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 η A B C D = A B C D E F G H = E F g h ζ
104 103 2rexbidv f = F g Q h Q A B C D = A B C D E F G H = E f g h η g Q h Q A B C D = A B C D E F G H = E F g h ζ
105 94 99 104 rspc3ev D Q E Q F Q g Q h Q A B C D = A B C D E F G H = E F g h ζ d Q e Q f Q g Q h Q A B C D = A B C d E F G H = e f g h θ
106 72 73 74 89 105 syl31anc X S A Q B Q C Q D Q E Q F Q G Q H Q ρ d Q e Q f Q g Q h Q A B C D = A B C d E F G H = e f g h θ
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 φ A B C D = A b c d E F G H = e f g h ψ
111 110 rexbidv a = A h Q A B C D = a b c d E F G H = e f g h φ h Q A B C D = A b c d E F G H = e f g h ψ
112 111 2rexbidv a = A f Q g Q h Q A B C D = a b c d E F G H = e f g h φ f Q g Q h Q A B C D = A b c d E F G H = e f g h ψ
113 112 2rexbidv a = A d Q e Q f Q g Q h Q A B C D = a b c d E F G H = e f g h φ d Q e Q f Q g Q h Q A B C D = A b c d E F G H = e f g h ψ
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 ψ A B C D = A B c d E F G H = e f g h χ
118 117 rexbidv b = B h Q A B C D = A b c d E F G H = e f g h ψ h Q A B C D = A B c d E F G H = e f g h χ
119 118 2rexbidv b = B f Q g Q h Q A B C D = A b c d E F G H = e f g h ψ f Q g Q h Q A B C D = A B c d E F G H = e f g h χ
120 119 2rexbidv b = B d Q e Q f Q g Q h Q A B C D = A b c d E F G H = e f g h ψ d Q e Q f Q g Q h Q A B C D = A B c d E F G H = e f g h χ
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 χ A B C D = A B C d E F G H = e f g h θ
125 124 rexbidv c = C h Q A B C D = A B c d E F G H = e f g h χ h Q A B C D = A B C d E F G H = e f g h θ
126 125 2rexbidv c = C f Q g Q h Q A B C D = A B c d E F G H = e f g h χ f Q g Q h Q A B C D = A B C d E F G H = e f g h θ
127 126 2rexbidv c = C d Q e Q f Q g Q h Q A B C D = A B c d E F G H = e f g h χ d Q e Q f Q g Q h Q A B C D = A B C d E F G H = e f g h θ
128 113 120 127 rspc3ev A Q B Q C Q d Q e Q f Q g Q h Q A B C D = A B C d E F G H = e f g h θ a Q b Q c Q d Q e Q f Q g Q h Q A B C D = a b c d E F G H = e f g h φ
129 69 70 71 106 128 syl31anc X S A Q B Q C Q D Q E Q F Q G Q H Q ρ a Q b Q c Q d Q e Q f Q g Q h Q A B C D = a b c d E F G H = e f g h φ
130 9 rexeqdv x = X h P A B C D = a b c d E F G H = e f g h φ h Q A B C D = a b c d E F G H = e f g h φ
131 9 130 rexeqbidv x = X g P h P A B C D = a b c d E F G H = e f g h φ g Q h Q A B C D = a b c d E F G H = e f g h φ
132 9 131 rexeqbidv x = X f P g P h P A B C D = a b c d E F G H = e f g h φ f Q g Q h Q A B C D = a b c d E F G H = e f g h φ
133 9 132 rexeqbidv x = X e P f P g P h P A B C D = a b c d E F G H = e f g h φ e Q f Q g Q h Q A B C D = a b c d E F G H = e f g h φ
134 9 133 rexeqbidv x = X d P e P f P g P h P A B C D = a b c d E F G H = e f g h φ d Q e Q f Q g Q h Q A B C D = a b c d E F G H = e f g h φ
135 9 134 rexeqbidv x = X c P d P e P f P g P h P A B C D = a b c d E F G H = e f g h φ c Q d Q e Q f Q g Q h Q A B C D = a b c d E F G H = e f g h φ
136 9 135 rexeqbidv x = X b P c P d P e P f P g P h P A B C D = a b c d E F G H = e f g h φ b Q c Q d Q e Q f Q g Q h Q A B C D = a b c d E F G H = e f g h φ
137 9 136 rexeqbidv x = X a P b P c P d P e P f P g P h P A B C D = a b c d E F G H = e f g h φ a Q b Q c Q d Q e Q f Q g Q h Q A B C D = a b c d E F G H = e f g h φ
138 137 rspcev X S a Q b Q c Q d Q e Q f Q g Q h Q A B C D = a b c d E F G H = e f g h φ x S a P b P c P d P e P f P g P h P A B C D = a b c d E F G H = e f g h φ
139 68 129 138 syl2anc X S A Q B Q C Q D Q E Q F Q G Q H Q ρ x S a P b P c P d P e P f P g P h P A B C D = a b c d E F G H = e f g h φ
140 139 ex X S A Q B Q C Q D Q E Q F Q G Q H Q ρ x S a P b P c P d P e P f P g P h P A B C D = a b c d E F G H = e f g h φ
141 67 140 impbid X S A Q B Q C Q D Q E Q F Q G Q H Q x S a P b P c P d P e P f P g P h P A B C D = a b c d E F G H = e f g h φ ρ
142 27 141 syl5bb X S A Q B Q C Q D Q E Q F Q G Q H Q A B C D R E F G H ρ