This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ( 𝑎 = 𝐴 → ( 𝜓 ↔ 𝜒 ) )
br8d.2 ⊢ ( 𝑏 = 𝐵 → ( 𝜒 ↔ 𝜃 ) )
br8d.3 ⊢ ( 𝑐 = 𝐶 → ( 𝜃 ↔ 𝜏 ) )
br8d.4 ⊢ ( 𝑑 = 𝐷 → ( 𝜏 ↔ 𝜂 ) )
br8d.5 ⊢ ( 𝑒 = 𝐸 → ( 𝜂 ↔ 𝜁 ) )
br8d.6 ⊢ ( 𝑓 = 𝐹 → ( 𝜁 ↔ 𝜎 ) )
br8d.7 ⊢ ( 𝑔 = 𝐺 → ( 𝜎 ↔ 𝜌 ) )
br8d.8 ⊢ ( ℎ = 𝐻 → ( 𝜌 ↔ 𝜇 ) )
br8d.10 ⊢ ( 𝜑 → 𝑅 = { ⟨ 𝑝 , 𝑞 ⟩ ∣ ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ∃ 𝑐 ∈ 𝑃 ∃ 𝑑 ∈ 𝑃 ∃ 𝑒 ∈ 𝑃 ∃ 𝑓 ∈ 𝑃 ∃ 𝑔 ∈ 𝑃 ∃ ℎ ∈ 𝑃 ( 𝑝 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ 𝑞 = ⟨ ⟨ 𝑒 , 𝑓 ⟩ , ⟨ 𝑔 , ℎ ⟩ ⟩ ∧ 𝜓 ) } )
br8d.11 ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
br8d.12 ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
br8d.13 ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
br8d.14 ⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
br8d.15 ⊢ ( 𝜑 → 𝐸 ∈ 𝑃 )
br8d.16 ⊢ ( 𝜑 → 𝐹 ∈ 𝑃 )
br8d.17 ⊢ ( 𝜑 → 𝐺 ∈ 𝑃 )
br8d.18 ⊢ ( 𝜑 → 𝐻 ∈ 𝑃 )
Assertion br8d ( 𝜑 → ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ 𝑅 ⟨ ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , 𝐻 ⟩ ⟩ ↔ 𝜇 ) )

Proof

Step Hyp Ref Expression
1 br8d.1 ⊢ ( 𝑎 = 𝐴 → ( 𝜓 ↔ 𝜒 ) )
2 br8d.2 ⊢ ( 𝑏 = 𝐵 → ( 𝜒 ↔ 𝜃 ) )
3 br8d.3 ⊢ ( 𝑐 = 𝐶 → ( 𝜃 ↔ 𝜏 ) )
4 br8d.4 ⊢ ( 𝑑 = 𝐷 → ( 𝜏 ↔ 𝜂 ) )
5 br8d.5 ⊢ ( 𝑒 = 𝐸 → ( 𝜂 ↔ 𝜁 ) )
6 br8d.6 ⊢ ( 𝑓 = 𝐹 → ( 𝜁 ↔ 𝜎 ) )
7 br8d.7 ⊢ ( 𝑔 = 𝐺 → ( 𝜎 ↔ 𝜌 ) )
8 br8d.8 ⊢ ( ℎ = 𝐻 → ( 𝜌 ↔ 𝜇 ) )
9 br8d.10 ⊢ ( 𝜑 → 𝑅 = { ⟨ 𝑝 , 𝑞 ⟩ ∣ ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ∃ 𝑐 ∈ 𝑃 ∃ 𝑑 ∈ 𝑃 ∃ 𝑒 ∈ 𝑃 ∃ 𝑓 ∈ 𝑃 ∃ 𝑔 ∈ 𝑃 ∃ ℎ ∈ 𝑃 ( 𝑝 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ 𝑞 = ⟨ ⟨ 𝑒 , 𝑓 ⟩ , ⟨ 𝑔 , ℎ ⟩ ⟩ ∧ 𝜓 ) } )
10 br8d.11 ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
11 br8d.12 ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
12 br8d.13 ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
13 br8d.14 ⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
14 br8d.15 ⊢ ( 𝜑 → 𝐸 ∈ 𝑃 )
15 br8d.16 ⊢ ( 𝜑 → 𝐹 ∈ 𝑃 )
16 br8d.17 ⊢ ( 𝜑 → 𝐺 ∈ 𝑃 )
17 br8d.18 ⊢ ( 𝜑 → 𝐻 ∈ 𝑃 )
18 9 breqd ⊢ ( 𝜑 → ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ 𝑅 ⟨ ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , 𝐻 ⟩ ⟩ ↔ ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ { ⟨ 𝑝 , 𝑞 ⟩ ∣ ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ∃ 𝑐 ∈ 𝑃 ∃ 𝑑 ∈ 𝑃 ∃ 𝑒 ∈ 𝑃 ∃ 𝑓 ∈ 𝑃 ∃ 𝑔 ∈ 𝑃 ∃ ℎ ∈ 𝑃 ( 𝑝 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ 𝑞 = ⟨ ⟨ 𝑒 , 𝑓 ⟩ , ⟨ 𝑔 , ℎ ⟩ ⟩ ∧ 𝜓 ) } ⟨ ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , 𝐻 ⟩ ⟩ ) )
19 opex ⊢ ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ ∈ V
20 opex ⊢ ⟨ ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , 𝐻 ⟩ ⟩ ∈ V
21 eqeq1 ⊢ ( 𝑝 = ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ → ( 𝑝 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ↔ ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ) )
22 21 3anbi1d ⊢ ( 𝑝 = ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ → ( ( 𝑝 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ 𝑞 = ⟨ ⟨ 𝑒 , 𝑓 ⟩ , ⟨ 𝑔 , ℎ ⟩ ⟩ ∧ 𝜓 ) ↔ ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ 𝑞 = ⟨ ⟨ 𝑒 , 𝑓 ⟩ , ⟨ 𝑔 , ℎ ⟩ ⟩ ∧ 𝜓 ) ) )
23 22 rexbidv ⊢ ( 𝑝 = ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ → ( ∃ ℎ ∈ 𝑃 ( 𝑝 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ 𝑞 = ⟨ ⟨ 𝑒 , 𝑓 ⟩ , ⟨ 𝑔 , ℎ ⟩ ⟩ ∧ 𝜓 ) ↔ ∃ ℎ ∈ 𝑃 ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ 𝑞 = ⟨ ⟨ 𝑒 , 𝑓 ⟩ , ⟨ 𝑔 , ℎ ⟩ ⟩ ∧ 𝜓 ) ) )
24 23 2rexbidv ⊢ ( 𝑝 = ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ → ( ∃ 𝑓 ∈ 𝑃 ∃ 𝑔 ∈ 𝑃 ∃ ℎ ∈ 𝑃 ( 𝑝 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ 𝑞 = ⟨ ⟨ 𝑒 , 𝑓 ⟩ , ⟨ 𝑔 , ℎ ⟩ ⟩ ∧ 𝜓 ) ↔ ∃ 𝑓 ∈ 𝑃 ∃ 𝑔 ∈ 𝑃 ∃ ℎ ∈ 𝑃 ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ 𝑞 = ⟨ ⟨ 𝑒 , 𝑓 ⟩ , ⟨ 𝑔 , ℎ ⟩ ⟩ ∧ 𝜓 ) ) )
25 24 2rexbidv ⊢ ( 𝑝 = ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ → ( ∃ 𝑑 ∈ 𝑃 ∃ 𝑒 ∈ 𝑃 ∃ 𝑓 ∈ 𝑃 ∃ 𝑔 ∈ 𝑃 ∃ ℎ ∈ 𝑃 ( 𝑝 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ 𝑞 = ⟨ ⟨ 𝑒 , 𝑓 ⟩ , ⟨ 𝑔 , ℎ ⟩ ⟩ ∧ 𝜓 ) ↔ ∃ 𝑑 ∈ 𝑃 ∃ 𝑒 ∈ 𝑃 ∃ 𝑓 ∈ 𝑃 ∃ 𝑔 ∈ 𝑃 ∃ ℎ ∈ 𝑃 ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ 𝑞 = ⟨ ⟨ 𝑒 , 𝑓 ⟩ , ⟨ 𝑔 , ℎ ⟩ ⟩ ∧ 𝜓 ) ) )
26 25 2rexbidv ⊢ ( 𝑝 = ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ → ( ∃ 𝑏 ∈ 𝑃 ∃ 𝑐 ∈ 𝑃 ∃ 𝑑 ∈ 𝑃 ∃ 𝑒 ∈ 𝑃 ∃ 𝑓 ∈ 𝑃 ∃ 𝑔 ∈ 𝑃 ∃ ℎ ∈ 𝑃 ( 𝑝 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ 𝑞 = ⟨ ⟨ 𝑒 , 𝑓 ⟩ , ⟨ 𝑔 , ℎ ⟩ ⟩ ∧ 𝜓 ) ↔ ∃ 𝑏 ∈ 𝑃 ∃ 𝑐 ∈ 𝑃 ∃ 𝑑 ∈ 𝑃 ∃ 𝑒 ∈ 𝑃 ∃ 𝑓 ∈ 𝑃 ∃ 𝑔 ∈ 𝑃 ∃ ℎ ∈ 𝑃 ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ 𝑞 = ⟨ ⟨ 𝑒 , 𝑓 ⟩ , ⟨ 𝑔 , ℎ ⟩ ⟩ ∧ 𝜓 ) ) )
27 26 rexbidv ⊢ ( 𝑝 = ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ → ( ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ∃ 𝑐 ∈ 𝑃 ∃ 𝑑 ∈ 𝑃 ∃ 𝑒 ∈ 𝑃 ∃ 𝑓 ∈ 𝑃 ∃ 𝑔 ∈ 𝑃 ∃ ℎ ∈ 𝑃 ( 𝑝 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ 𝑞 = ⟨ ⟨ 𝑒 , 𝑓 ⟩ , ⟨ 𝑔 , ℎ ⟩ ⟩ ∧ 𝜓 ) ↔ ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ∃ 𝑐 ∈ 𝑃 ∃ 𝑑 ∈ 𝑃 ∃ 𝑒 ∈ 𝑃 ∃ 𝑓 ∈ 𝑃 ∃ 𝑔 ∈ 𝑃 ∃ ℎ ∈ 𝑃 ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ 𝑞 = ⟨ ⟨ 𝑒 , 𝑓 ⟩ , ⟨ 𝑔 , ℎ ⟩ ⟩ ∧ 𝜓 ) ) )
28 eqeq1 ⊢ ( 𝑞 = ⟨ ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , 𝐻 ⟩ ⟩ → ( 𝑞 = ⟨ ⟨ 𝑒 , 𝑓 ⟩ , ⟨ 𝑔 , ℎ ⟩ ⟩ ↔ ⟨ ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , 𝐻 ⟩ ⟩ = ⟨ ⟨ 𝑒 , 𝑓 ⟩ , ⟨ 𝑔 , ℎ ⟩ ⟩ ) )
29 28 3anbi2d ⊢ ( 𝑞 = ⟨ ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , 𝐻 ⟩ ⟩ → ( ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ 𝑞 = ⟨ ⟨ 𝑒 , 𝑓 ⟩ , ⟨ 𝑔 , ℎ ⟩ ⟩ ∧ 𝜓 ) ↔ ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ ⟨ ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , 𝐻 ⟩ ⟩ = ⟨ ⟨ 𝑒 , 𝑓 ⟩ , ⟨ 𝑔 , ℎ ⟩ ⟩ ∧ 𝜓 ) ) )
30 29 rexbidv ⊢ ( 𝑞 = ⟨ ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , 𝐻 ⟩ ⟩ → ( ∃ ℎ ∈ 𝑃 ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ 𝑞 = ⟨ ⟨ 𝑒 , 𝑓 ⟩ , ⟨ 𝑔 , ℎ ⟩ ⟩ ∧ 𝜓 ) ↔ ∃ ℎ ∈ 𝑃 ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ ⟨ ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , 𝐻 ⟩ ⟩ = ⟨ ⟨ 𝑒 , 𝑓 ⟩ , ⟨ 𝑔 , ℎ ⟩ ⟩ ∧ 𝜓 ) ) )
31 30 2rexbidv ⊢ ( 𝑞 = ⟨ ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , 𝐻 ⟩ ⟩ → ( ∃ 𝑓 ∈ 𝑃 ∃ 𝑔 ∈ 𝑃 ∃ ℎ ∈ 𝑃 ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ 𝑞 = ⟨ ⟨ 𝑒 , 𝑓 ⟩ , ⟨ 𝑔 , ℎ ⟩ ⟩ ∧ 𝜓 ) ↔ ∃ 𝑓 ∈ 𝑃 ∃ 𝑔 ∈ 𝑃 ∃ ℎ ∈ 𝑃 ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ ⟨ ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , 𝐻 ⟩ ⟩ = ⟨ ⟨ 𝑒 , 𝑓 ⟩ , ⟨ 𝑔 , ℎ ⟩ ⟩ ∧ 𝜓 ) ) )
32 31 2rexbidv ⊢ ( 𝑞 = ⟨ ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , 𝐻 ⟩ ⟩ → ( ∃ 𝑑 ∈ 𝑃 ∃ 𝑒 ∈ 𝑃 ∃ 𝑓 ∈ 𝑃 ∃ 𝑔 ∈ 𝑃 ∃ ℎ ∈ 𝑃 ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ 𝑞 = ⟨ ⟨ 𝑒 , 𝑓 ⟩ , ⟨ 𝑔 , ℎ ⟩ ⟩ ∧ 𝜓 ) ↔ ∃ 𝑑 ∈ 𝑃 ∃ 𝑒 ∈ 𝑃 ∃ 𝑓 ∈ 𝑃 ∃ 𝑔 ∈ 𝑃 ∃ ℎ ∈ 𝑃 ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ ⟨ ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , 𝐻 ⟩ ⟩ = ⟨ ⟨ 𝑒 , 𝑓 ⟩ , ⟨ 𝑔 , ℎ ⟩ ⟩ ∧ 𝜓 ) ) )
33 32 2rexbidv ⊢ ( 𝑞 = ⟨ ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , 𝐻 ⟩ ⟩ → ( ∃ 𝑏 ∈ 𝑃 ∃ 𝑐 ∈ 𝑃 ∃ 𝑑 ∈ 𝑃 ∃ 𝑒 ∈ 𝑃 ∃ 𝑓 ∈ 𝑃 ∃ 𝑔 ∈ 𝑃 ∃ ℎ ∈ 𝑃 ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ 𝑞 = ⟨ ⟨ 𝑒 , 𝑓 ⟩ , ⟨ 𝑔 , ℎ ⟩ ⟩ ∧ 𝜓 ) ↔ ∃ 𝑏 ∈ 𝑃 ∃ 𝑐 ∈ 𝑃 ∃ 𝑑 ∈ 𝑃 ∃ 𝑒 ∈ 𝑃 ∃ 𝑓 ∈ 𝑃 ∃ 𝑔 ∈ 𝑃 ∃ ℎ ∈ 𝑃 ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ ⟨ ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , 𝐻 ⟩ ⟩ = ⟨ ⟨ 𝑒 , 𝑓 ⟩ , ⟨ 𝑔 , ℎ ⟩ ⟩ ∧ 𝜓 ) ) )
34 33 rexbidv ⊢ ( 𝑞 = ⟨ ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , 𝐻 ⟩ ⟩ → ( ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ∃ 𝑐 ∈ 𝑃 ∃ 𝑑 ∈ 𝑃 ∃ 𝑒 ∈ 𝑃 ∃ 𝑓 ∈ 𝑃 ∃ 𝑔 ∈ 𝑃 ∃ ℎ ∈ 𝑃 ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ 𝑞 = ⟨ ⟨ 𝑒 , 𝑓 ⟩ , ⟨ 𝑔 , ℎ ⟩ ⟩ ∧ 𝜓 ) ↔ ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ∃ 𝑐 ∈ 𝑃 ∃ 𝑑 ∈ 𝑃 ∃ 𝑒 ∈ 𝑃 ∃ 𝑓 ∈ 𝑃 ∃ 𝑔 ∈ 𝑃 ∃ ℎ ∈ 𝑃 ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ ⟨ ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , 𝐻 ⟩ ⟩ = ⟨ ⟨ 𝑒 , 𝑓 ⟩ , ⟨ 𝑔 , ℎ ⟩ ⟩ ∧ 𝜓 ) ) )
35 eqid ⊢ { ⟨ 𝑝 , 𝑞 ⟩ ∣ ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ∃ 𝑐 ∈ 𝑃 ∃ 𝑑 ∈ 𝑃 ∃ 𝑒 ∈ 𝑃 ∃ 𝑓 ∈ 𝑃 ∃ 𝑔 ∈ 𝑃 ∃ ℎ ∈ 𝑃 ( 𝑝 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ 𝑞 = ⟨ ⟨ 𝑒 , 𝑓 ⟩ , ⟨ 𝑔 , ℎ ⟩ ⟩ ∧ 𝜓 ) } = { ⟨ 𝑝 , 𝑞 ⟩ ∣ ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ∃ 𝑐 ∈ 𝑃 ∃ 𝑑 ∈ 𝑃 ∃ 𝑒 ∈ 𝑃 ∃ 𝑓 ∈ 𝑃 ∃ 𝑔 ∈ 𝑃 ∃ ℎ ∈ 𝑃 ( 𝑝 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ 𝑞 = ⟨ ⟨ 𝑒 , 𝑓 ⟩ , ⟨ 𝑔 , ℎ ⟩ ⟩ ∧ 𝜓 ) }
36 19 20 27 34 35 brab ⊢ ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ { ⟨ 𝑝 , 𝑞 ⟩ ∣ ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ∃ 𝑐 ∈ 𝑃 ∃ 𝑑 ∈ 𝑃 ∃ 𝑒 ∈ 𝑃 ∃ 𝑓 ∈ 𝑃 ∃ 𝑔 ∈ 𝑃 ∃ ℎ ∈ 𝑃 ( 𝑝 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ 𝑞 = ⟨ ⟨ 𝑒 , 𝑓 ⟩ , ⟨ 𝑔 , ℎ ⟩ ⟩ ∧ 𝜓 ) } ⟨ ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , 𝐻 ⟩ ⟩ ↔ ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ∃ 𝑐 ∈ 𝑃 ∃ 𝑑 ∈ 𝑃 ∃ 𝑒 ∈ 𝑃 ∃ 𝑓 ∈ 𝑃 ∃ 𝑔 ∈ 𝑃 ∃ ℎ ∈ 𝑃 ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ ⟨ ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , 𝐻 ⟩ ⟩ = ⟨ ⟨ 𝑒 , 𝑓 ⟩ , ⟨ 𝑔 , ℎ ⟩ ⟩ ∧ 𝜓 ) )
37 18 36 bitrdi ⊢ ( 𝜑 → ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ 𝑅 ⟨ ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , 𝐻 ⟩ ⟩ ↔ ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ∃ 𝑐 ∈ 𝑃 ∃ 𝑑 ∈ 𝑃 ∃ 𝑒 ∈ 𝑃 ∃ 𝑓 ∈ 𝑃 ∃ 𝑔 ∈ 𝑃 ∃ ℎ ∈ 𝑃 ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ ⟨ ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , 𝐻 ⟩ ⟩ = ⟨ ⟨ 𝑒 , 𝑓 ⟩ , ⟨ 𝑔 , ℎ ⟩ ⟩ ∧ 𝜓 ) ) )
38 opex ⊢ ⟨ 𝑎 , 𝑏 ⟩ ∈ V
39 opex ⊢ ⟨ 𝑐 , 𝑑 ⟩ ∈ V
40 38 39 opth ⊢ ( ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ = ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ ↔ ( ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝑐 , 𝑑 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ ) )
41 vex ⊢ 𝑎 ∈ V
42 vex ⊢ 𝑏 ∈ V
43 41 42 opth ⊢ ( ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ ↔ ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ) )
44 1 2 sylan9bb ⊢ ( ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ) → ( 𝜓 ↔ 𝜃 ) )
45 43 44 sylbi ⊢ ( ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ → ( 𝜓 ↔ 𝜃 ) )
46 vex ⊢ 𝑐 ∈ V
47 vex ⊢ 𝑑 ∈ V
48 46 47 opth ⊢ ( ⟨ 𝑐 , 𝑑 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ ↔ ( 𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ) )
49 3 4 sylan9bb ⊢ ( ( 𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ) → ( 𝜃 ↔ 𝜂 ) )
50 48 49 sylbi ⊢ ( ⟨ 𝑐 , 𝑑 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ → ( 𝜃 ↔ 𝜂 ) )
51 45 50 sylan9bb ⊢ ( ( ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝑐 , 𝑑 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ ) → ( 𝜓 ↔ 𝜂 ) )
52 40 51 sylbi ⊢ ( ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ = ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ → ( 𝜓 ↔ 𝜂 ) )
53 52 eqcoms ⊢ ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ → ( 𝜓 ↔ 𝜂 ) )
54 opex ⊢ ⟨ 𝑒 , 𝑓 ⟩ ∈ V
55 opex ⊢ ⟨ 𝑔 , ℎ ⟩ ∈ V
56 54 55 opth ⊢ ( ⟨ ⟨ 𝑒 , 𝑓 ⟩ , ⟨ 𝑔 , ℎ ⟩ ⟩ = ⟨ ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , 𝐻 ⟩ ⟩ ↔ ( ⟨ 𝑒 , 𝑓 ⟩ = ⟨ 𝐸 , 𝐹 ⟩ ∧ ⟨ 𝑔 , ℎ ⟩ = ⟨ 𝐺 , 𝐻 ⟩ ) )
57 vex ⊢ 𝑒 ∈ V
58 vex ⊢ 𝑓 ∈ V
59 57 58 opth ⊢ ( ⟨ 𝑒 , 𝑓 ⟩ = ⟨ 𝐸 , 𝐹 ⟩ ↔ ( 𝑒 = 𝐸 ∧ 𝑓 = 𝐹 ) )
60 5 6 sylan9bb ⊢ ( ( 𝑒 = 𝐸 ∧ 𝑓 = 𝐹 ) → ( 𝜂 ↔ 𝜎 ) )
61 59 60 sylbi ⊢ ( ⟨ 𝑒 , 𝑓 ⟩ = ⟨ 𝐸 , 𝐹 ⟩ → ( 𝜂 ↔ 𝜎 ) )
62 vex ⊢ 𝑔 ∈ V
63 vex ⊢ ℎ ∈ V
64 62 63 opth ⊢ ( ⟨ 𝑔 , ℎ ⟩ = ⟨ 𝐺 , 𝐻 ⟩ ↔ ( 𝑔 = 𝐺 ∧ ℎ = 𝐻 ) )
65 7 8 sylan9bb ⊢ ( ( 𝑔 = 𝐺 ∧ ℎ = 𝐻 ) → ( 𝜎 ↔ 𝜇 ) )
66 64 65 sylbi ⊢ ( ⟨ 𝑔 , ℎ ⟩ = ⟨ 𝐺 , 𝐻 ⟩ → ( 𝜎 ↔ 𝜇 ) )
67 61 66 sylan9bb ⊢ ( ( ⟨ 𝑒 , 𝑓 ⟩ = ⟨ 𝐸 , 𝐹 ⟩ ∧ ⟨ 𝑔 , ℎ ⟩ = ⟨ 𝐺 , 𝐻 ⟩ ) → ( 𝜂 ↔ 𝜇 ) )
68 56 67 sylbi ⊢ ( ⟨ ⟨ 𝑒 , 𝑓 ⟩ , ⟨ 𝑔 , ℎ ⟩ ⟩ = ⟨ ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , 𝐻 ⟩ ⟩ → ( 𝜂 ↔ 𝜇 ) )
69 68 eqcoms ⊢ ( ⟨ ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , 𝐻 ⟩ ⟩ = ⟨ ⟨ 𝑒 , 𝑓 ⟩ , ⟨ 𝑔 , ℎ ⟩ ⟩ → ( 𝜂 ↔ 𝜇 ) )
70 53 69 sylan9bb ⊢ ( ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ ⟨ ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , 𝐻 ⟩ ⟩ = ⟨ ⟨ 𝑒 , 𝑓 ⟩ , ⟨ 𝑔 , ℎ ⟩ ⟩ ) → ( 𝜓 ↔ 𝜇 ) )
71 70 biimp3a ⊢ ( ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ ⟨ ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , 𝐻 ⟩ ⟩ = ⟨ ⟨ 𝑒 , 𝑓 ⟩ , ⟨ 𝑔 , ℎ ⟩ ⟩ ∧ 𝜓 ) → 𝜇 )
72 71 a1i ⊢ ( ( ( ( ( ( ( ( 𝐴 ∈ 𝑃 ∧ 𝐵 ∈ 𝑃 ) ∧ ( 𝐶 ∈ 𝑃 ∧ 𝐷 ∈ 𝑃 ∧ 𝐸 ∈ 𝑃 ) ∧ ( 𝐹 ∈ 𝑃 ∧ 𝐺 ∈ 𝑃 ∧ 𝐻 ∈ 𝑃 ) ) ∧ 𝑎 ∈ 𝑃 ) ∧ ( 𝑏 ∈ 𝑃 ∧ 𝑐 ∈ 𝑃 ) ) ∧ ( 𝑑 ∈ 𝑃 ∧ 𝑒 ∈ 𝑃 ) ) ∧ ( 𝑓 ∈ 𝑃 ∧ 𝑔 ∈ 𝑃 ) ) ∧ ℎ ∈ 𝑃 ) → ( ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ ⟨ ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , 𝐻 ⟩ ⟩ = ⟨ ⟨ 𝑒 , 𝑓 ⟩ , ⟨ 𝑔 , ℎ ⟩ ⟩ ∧ 𝜓 ) → 𝜇 ) )
73 72 rexlimdva ⊢ ( ( ( ( ( ( ( 𝐴 ∈ 𝑃 ∧ 𝐵 ∈ 𝑃 ) ∧ ( 𝐶 ∈ 𝑃 ∧ 𝐷 ∈ 𝑃 ∧ 𝐸 ∈ 𝑃 ) ∧ ( 𝐹 ∈ 𝑃 ∧ 𝐺 ∈ 𝑃 ∧ 𝐻 ∈ 𝑃 ) ) ∧ 𝑎 ∈ 𝑃 ) ∧ ( 𝑏 ∈ 𝑃 ∧ 𝑐 ∈ 𝑃 ) ) ∧ ( 𝑑 ∈ 𝑃 ∧ 𝑒 ∈ 𝑃 ) ) ∧ ( 𝑓 ∈ 𝑃 ∧ 𝑔 ∈ 𝑃 ) ) → ( ∃ ℎ ∈ 𝑃 ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ ⟨ ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , 𝐻 ⟩ ⟩ = ⟨ ⟨ 𝑒 , 𝑓 ⟩ , ⟨ 𝑔 , ℎ ⟩ ⟩ ∧ 𝜓 ) → 𝜇 ) )
74 73 rexlimdvva ⊢ ( ( ( ( ( ( 𝐴 ∈ 𝑃 ∧ 𝐵 ∈ 𝑃 ) ∧ ( 𝐶 ∈ 𝑃 ∧ 𝐷 ∈ 𝑃 ∧ 𝐸 ∈ 𝑃 ) ∧ ( 𝐹 ∈ 𝑃 ∧ 𝐺 ∈ 𝑃 ∧ 𝐻 ∈ 𝑃 ) ) ∧ 𝑎 ∈ 𝑃 ) ∧ ( 𝑏 ∈ 𝑃 ∧ 𝑐 ∈ 𝑃 ) ) ∧ ( 𝑑 ∈ 𝑃 ∧ 𝑒 ∈ 𝑃 ) ) → ( ∃ 𝑓 ∈ 𝑃 ∃ 𝑔 ∈ 𝑃 ∃ ℎ ∈ 𝑃 ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ ⟨ ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , 𝐻 ⟩ ⟩ = ⟨ ⟨ 𝑒 , 𝑓 ⟩ , ⟨ 𝑔 , ℎ ⟩ ⟩ ∧ 𝜓 ) → 𝜇 ) )
75 74 rexlimdvva ⊢ ( ( ( ( ( 𝐴 ∈ 𝑃 ∧ 𝐵 ∈ 𝑃 ) ∧ ( 𝐶 ∈ 𝑃 ∧ 𝐷 ∈ 𝑃 ∧ 𝐸 ∈ 𝑃 ) ∧ ( 𝐹 ∈ 𝑃 ∧ 𝐺 ∈ 𝑃 ∧ 𝐻 ∈ 𝑃 ) ) ∧ 𝑎 ∈ 𝑃 ) ∧ ( 𝑏 ∈ 𝑃 ∧ 𝑐 ∈ 𝑃 ) ) → ( ∃ 𝑑 ∈ 𝑃 ∃ 𝑒 ∈ 𝑃 ∃ 𝑓 ∈ 𝑃 ∃ 𝑔 ∈ 𝑃 ∃ ℎ ∈ 𝑃 ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ ⟨ ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , 𝐻 ⟩ ⟩ = ⟨ ⟨ 𝑒 , 𝑓 ⟩ , ⟨ 𝑔 , ℎ ⟩ ⟩ ∧ 𝜓 ) → 𝜇 ) )
76 75 rexlimdvva ⊢ ( ( ( ( 𝐴 ∈ 𝑃 ∧ 𝐵 ∈ 𝑃 ) ∧ ( 𝐶 ∈ 𝑃 ∧ 𝐷 ∈ 𝑃 ∧ 𝐸 ∈ 𝑃 ) ∧ ( 𝐹 ∈ 𝑃 ∧ 𝐺 ∈ 𝑃 ∧ 𝐻 ∈ 𝑃 ) ) ∧ 𝑎 ∈ 𝑃 ) → ( ∃ 𝑏 ∈ 𝑃 ∃ 𝑐 ∈ 𝑃 ∃ 𝑑 ∈ 𝑃 ∃ 𝑒 ∈ 𝑃 ∃ 𝑓 ∈ 𝑃 ∃ 𝑔 ∈ 𝑃 ∃ ℎ ∈ 𝑃 ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ ⟨ ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , 𝐻 ⟩ ⟩ = ⟨ ⟨ 𝑒 , 𝑓 ⟩ , ⟨ 𝑔 , ℎ ⟩ ⟩ ∧ 𝜓 ) → 𝜇 ) )
77 76 rexlimdva ⊢ ( ( ( 𝐴 ∈ 𝑃 ∧ 𝐵 ∈ 𝑃 ) ∧ ( 𝐶 ∈ 𝑃 ∧ 𝐷 ∈ 𝑃 ∧ 𝐸 ∈ 𝑃 ) ∧ ( 𝐹 ∈ 𝑃 ∧ 𝐺 ∈ 𝑃 ∧ 𝐻 ∈ 𝑃 ) ) → ( ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ∃ 𝑐 ∈ 𝑃 ∃ 𝑑 ∈ 𝑃 ∃ 𝑒 ∈ 𝑃 ∃ 𝑓 ∈ 𝑃 ∃ 𝑔 ∈ 𝑃 ∃ ℎ ∈ 𝑃 ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ ⟨ ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , 𝐻 ⟩ ⟩ = ⟨ ⟨ 𝑒 , 𝑓 ⟩ , ⟨ 𝑔 , ℎ ⟩ ⟩ ∧ 𝜓 ) → 𝜇 ) )
78 simpl1l ⊢ ( ( ( ( 𝐴 ∈ 𝑃 ∧ 𝐵 ∈ 𝑃 ) ∧ ( 𝐶 ∈ 𝑃 ∧ 𝐷 ∈ 𝑃 ∧ 𝐸 ∈ 𝑃 ) ∧ ( 𝐹 ∈ 𝑃 ∧ 𝐺 ∈ 𝑃 ∧ 𝐻 ∈ 𝑃 ) ) ∧ 𝜇 ) → 𝐴 ∈ 𝑃 )
79 simpl1r ⊢ ( ( ( ( 𝐴 ∈ 𝑃 ∧ 𝐵 ∈ 𝑃 ) ∧ ( 𝐶 ∈ 𝑃 ∧ 𝐷 ∈ 𝑃 ∧ 𝐸 ∈ 𝑃 ) ∧ ( 𝐹 ∈ 𝑃 ∧ 𝐺 ∈ 𝑃 ∧ 𝐻 ∈ 𝑃 ) ) ∧ 𝜇 ) → 𝐵 ∈ 𝑃 )
80 simpl21 ⊢ ( ( ( ( 𝐴 ∈ 𝑃 ∧ 𝐵 ∈ 𝑃 ) ∧ ( 𝐶 ∈ 𝑃 ∧ 𝐷 ∈ 𝑃 ∧ 𝐸 ∈ 𝑃 ) ∧ ( 𝐹 ∈ 𝑃 ∧ 𝐺 ∈ 𝑃 ∧ 𝐻 ∈ 𝑃 ) ) ∧ 𝜇 ) → 𝐶 ∈ 𝑃 )
81 simpl22 ⊢ ( ( ( ( 𝐴 ∈ 𝑃 ∧ 𝐵 ∈ 𝑃 ) ∧ ( 𝐶 ∈ 𝑃 ∧ 𝐷 ∈ 𝑃 ∧ 𝐸 ∈ 𝑃 ) ∧ ( 𝐹 ∈ 𝑃 ∧ 𝐺 ∈ 𝑃 ∧ 𝐻 ∈ 𝑃 ) ) ∧ 𝜇 ) → 𝐷 ∈ 𝑃 )
82 simpl23 ⊢ ( ( ( ( 𝐴 ∈ 𝑃 ∧ 𝐵 ∈ 𝑃 ) ∧ ( 𝐶 ∈ 𝑃 ∧ 𝐷 ∈ 𝑃 ∧ 𝐸 ∈ 𝑃 ) ∧ ( 𝐹 ∈ 𝑃 ∧ 𝐺 ∈ 𝑃 ∧ 𝐻 ∈ 𝑃 ) ) ∧ 𝜇 ) → 𝐸 ∈ 𝑃 )
83 simpl31 ⊢ ( ( ( ( 𝐴 ∈ 𝑃 ∧ 𝐵 ∈ 𝑃 ) ∧ ( 𝐶 ∈ 𝑃 ∧ 𝐷 ∈ 𝑃 ∧ 𝐸 ∈ 𝑃 ) ∧ ( 𝐹 ∈ 𝑃 ∧ 𝐺 ∈ 𝑃 ∧ 𝐻 ∈ 𝑃 ) ) ∧ 𝜇 ) → 𝐹 ∈ 𝑃 )
84 simpl32 ⊢ ( ( ( ( 𝐴 ∈ 𝑃 ∧ 𝐵 ∈ 𝑃 ) ∧ ( 𝐶 ∈ 𝑃 ∧ 𝐷 ∈ 𝑃 ∧ 𝐸 ∈ 𝑃 ) ∧ ( 𝐹 ∈ 𝑃 ∧ 𝐺 ∈ 𝑃 ∧ 𝐻 ∈ 𝑃 ) ) ∧ 𝜇 ) → 𝐺 ∈ 𝑃 )
85 simpl33 ⊢ ( ( ( ( 𝐴 ∈ 𝑃 ∧ 𝐵 ∈ 𝑃 ) ∧ ( 𝐶 ∈ 𝑃 ∧ 𝐷 ∈ 𝑃 ∧ 𝐸 ∈ 𝑃 ) ∧ ( 𝐹 ∈ 𝑃 ∧ 𝐺 ∈ 𝑃 ∧ 𝐻 ∈ 𝑃 ) ) ∧ 𝜇 ) → 𝐻 ∈ 𝑃 )
86 eqidd ⊢ ( ( ( ( 𝐴 ∈ 𝑃 ∧ 𝐵 ∈ 𝑃 ) ∧ ( 𝐶 ∈ 𝑃 ∧ 𝐷 ∈ 𝑃 ∧ 𝐸 ∈ 𝑃 ) ∧ ( 𝐹 ∈ 𝑃 ∧ 𝐺 ∈ 𝑃 ∧ 𝐻 ∈ 𝑃 ) ) ∧ 𝜇 ) → ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ = ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ )
87 eqidd ⊢ ( ( ( ( 𝐴 ∈ 𝑃 ∧ 𝐵 ∈ 𝑃 ) ∧ ( 𝐶 ∈ 𝑃 ∧ 𝐷 ∈ 𝑃 ∧ 𝐸 ∈ 𝑃 ) ∧ ( 𝐹 ∈ 𝑃 ∧ 𝐺 ∈ 𝑃 ∧ 𝐻 ∈ 𝑃 ) ) ∧ 𝜇 ) → ⟨ ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , 𝐻 ⟩ ⟩ = ⟨ ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , 𝐻 ⟩ ⟩ )
88 simpr ⊢ ( ( ( ( 𝐴 ∈ 𝑃 ∧ 𝐵 ∈ 𝑃 ) ∧ ( 𝐶 ∈ 𝑃 ∧ 𝐷 ∈ 𝑃 ∧ 𝐸 ∈ 𝑃 ) ∧ ( 𝐹 ∈ 𝑃 ∧ 𝐺 ∈ 𝑃 ∧ 𝐻 ∈ 𝑃 ) ) ∧ 𝜇 ) → 𝜇 )
89 opeq1 ⊢ ( 𝑔 = 𝐺 → ⟨ 𝑔 , ℎ ⟩ = ⟨ 𝐺 , ℎ ⟩ )
90 89 opeq2d ⊢ ( 𝑔 = 𝐺 → ⟨ ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝑔 , ℎ ⟩ ⟩ = ⟨ ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , ℎ ⟩ ⟩ )
91 90 eqeq2d ⊢ ( 𝑔 = 𝐺 → ( ⟨ ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , 𝐻 ⟩ ⟩ = ⟨ ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝑔 , ℎ ⟩ ⟩ ↔ ⟨ ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , 𝐻 ⟩ ⟩ = ⟨ ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , ℎ ⟩ ⟩ ) )
92 91 7 3anbi23d ⊢ ( 𝑔 = 𝐺 → ( ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ = ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ ∧ ⟨ ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , 𝐻 ⟩ ⟩ = ⟨ ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝑔 , ℎ ⟩ ⟩ ∧ 𝜎 ) ↔ ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ = ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ ∧ ⟨ ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , 𝐻 ⟩ ⟩ = ⟨ ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , ℎ ⟩ ⟩ ∧ 𝜌 ) ) )
93 opeq2 ⊢ ( ℎ = 𝐻 → ⟨ 𝐺 , ℎ ⟩ = ⟨ 𝐺 , 𝐻 ⟩ )
94 93 opeq2d ⊢ ( ℎ = 𝐻 → ⟨ ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , ℎ ⟩ ⟩ = ⟨ ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , 𝐻 ⟩ ⟩ )
95 94 eqeq2d ⊢ ( ℎ = 𝐻 → ( ⟨ ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , 𝐻 ⟩ ⟩ = ⟨ ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , ℎ ⟩ ⟩ ↔ ⟨ ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , 𝐻 ⟩ ⟩ = ⟨ ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , 𝐻 ⟩ ⟩ ) )
96 95 8 3anbi23d ⊢ ( ℎ = 𝐻 → ( ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ = ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ ∧ ⟨ ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , 𝐻 ⟩ ⟩ = ⟨ ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , ℎ ⟩ ⟩ ∧ 𝜌 ) ↔ ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ = ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ ∧ ⟨ ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , 𝐻 ⟩ ⟩ = ⟨ ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , 𝐻 ⟩ ⟩ ∧ 𝜇 ) ) )
97 92 96 rspc2ev ⊢ ( ( 𝐺 ∈ 𝑃 ∧ 𝐻 ∈ 𝑃 ∧ ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ = ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ ∧ ⟨ ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , 𝐻 ⟩ ⟩ = ⟨ ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , 𝐻 ⟩ ⟩ ∧ 𝜇 ) ) → ∃ 𝑔 ∈ 𝑃 ∃ ℎ ∈ 𝑃 ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ = ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ ∧ ⟨ ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , 𝐻 ⟩ ⟩ = ⟨ ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝑔 , ℎ ⟩ ⟩ ∧ 𝜎 ) )
98 84 85 86 87 88 97 syl113anc ⊢ ( ( ( ( 𝐴 ∈ 𝑃 ∧ 𝐵 ∈ 𝑃 ) ∧ ( 𝐶 ∈ 𝑃 ∧ 𝐷 ∈ 𝑃 ∧ 𝐸 ∈ 𝑃 ) ∧ ( 𝐹 ∈ 𝑃 ∧ 𝐺 ∈ 𝑃 ∧ 𝐻 ∈ 𝑃 ) ) ∧ 𝜇 ) → ∃ 𝑔 ∈ 𝑃 ∃ ℎ ∈ 𝑃 ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ = ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ ∧ ⟨ ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , 𝐻 ⟩ ⟩ = ⟨ ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝑔 , ℎ ⟩ ⟩ ∧ 𝜎 ) )
99 opeq2 ⊢ ( 𝑑 = 𝐷 → ⟨ 𝐶 , 𝑑 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ )
100 99 opeq2d ⊢ ( 𝑑 = 𝐷 → ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝑑 ⟩ ⟩ = ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ )
101 100 eqeq2d ⊢ ( 𝑑 = 𝐷 → ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ = ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝑑 ⟩ ⟩ ↔ ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ = ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ ) )
102 101 4 3anbi13d ⊢ ( 𝑑 = 𝐷 → ( ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ = ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝑑 ⟩ ⟩ ∧ ⟨ ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , 𝐻 ⟩ ⟩ = ⟨ ⟨ 𝑒 , 𝑓 ⟩ , ⟨ 𝑔 , ℎ ⟩ ⟩ ∧ 𝜏 ) ↔ ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ = ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ ∧ ⟨ ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , 𝐻 ⟩ ⟩ = ⟨ ⟨ 𝑒 , 𝑓 ⟩ , ⟨ 𝑔 , ℎ ⟩ ⟩ ∧ 𝜂 ) ) )
103 102 2rexbidv ⊢ ( 𝑑 = 𝐷 → ( ∃ 𝑔 ∈ 𝑃 ∃ ℎ ∈ 𝑃 ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ = ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝑑 ⟩ ⟩ ∧ ⟨ ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , 𝐻 ⟩ ⟩ = ⟨ ⟨ 𝑒 , 𝑓 ⟩ , ⟨ 𝑔 , ℎ ⟩ ⟩ ∧ 𝜏 ) ↔ ∃ 𝑔 ∈ 𝑃 ∃ ℎ ∈ 𝑃 ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ = ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ ∧ ⟨ ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , 𝐻 ⟩ ⟩ = ⟨ ⟨ 𝑒 , 𝑓 ⟩ , ⟨ 𝑔 , ℎ ⟩ ⟩ ∧ 𝜂 ) ) )
104 opeq1 ⊢ ( 𝑒 = 𝐸 → ⟨ 𝑒 , 𝑓 ⟩ = ⟨ 𝐸 , 𝑓 ⟩ )
105 104 opeq1d ⊢ ( 𝑒 = 𝐸 → ⟨ ⟨ 𝑒 , 𝑓 ⟩ , ⟨ 𝑔 , ℎ ⟩ ⟩ = ⟨ ⟨ 𝐸 , 𝑓 ⟩ , ⟨ 𝑔 , ℎ ⟩ ⟩ )
106 105 eqeq2d ⊢ ( 𝑒 = 𝐸 → ( ⟨ ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , 𝐻 ⟩ ⟩ = ⟨ ⟨ 𝑒 , 𝑓 ⟩ , ⟨ 𝑔 , ℎ ⟩ ⟩ ↔ ⟨ ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , 𝐻 ⟩ ⟩ = ⟨ ⟨ 𝐸 , 𝑓 ⟩ , ⟨ 𝑔 , ℎ ⟩ ⟩ ) )
107 106 5 3anbi23d ⊢ ( 𝑒 = 𝐸 → ( ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ = ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ ∧ ⟨ ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , 𝐻 ⟩ ⟩ = ⟨ ⟨ 𝑒 , 𝑓 ⟩ , ⟨ 𝑔 , ℎ ⟩ ⟩ ∧ 𝜂 ) ↔ ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ = ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ ∧ ⟨ ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , 𝐻 ⟩ ⟩ = ⟨ ⟨ 𝐸 , 𝑓 ⟩ , ⟨ 𝑔 , ℎ ⟩ ⟩ ∧ 𝜁 ) ) )
108 107 2rexbidv ⊢ ( 𝑒 = 𝐸 → ( ∃ 𝑔 ∈ 𝑃 ∃ ℎ ∈ 𝑃 ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ = ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ ∧ ⟨ ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , 𝐻 ⟩ ⟩ = ⟨ ⟨ 𝑒 , 𝑓 ⟩ , ⟨ 𝑔 , ℎ ⟩ ⟩ ∧ 𝜂 ) ↔ ∃ 𝑔 ∈ 𝑃 ∃ ℎ ∈ 𝑃 ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ = ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ ∧ ⟨ ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , 𝐻 ⟩ ⟩ = ⟨ ⟨ 𝐸 , 𝑓 ⟩ , ⟨ 𝑔 , ℎ ⟩ ⟩ ∧ 𝜁 ) ) )
109 opeq2 ⊢ ( 𝑓 = 𝐹 → ⟨ 𝐸 , 𝑓 ⟩ = ⟨ 𝐸 , 𝐹 ⟩ )
110 109 opeq1d ⊢ ( 𝑓 = 𝐹 → ⟨ ⟨ 𝐸 , 𝑓 ⟩ , ⟨ 𝑔 , ℎ ⟩ ⟩ = ⟨ ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝑔 , ℎ ⟩ ⟩ )
111 110 eqeq2d ⊢ ( 𝑓 = 𝐹 → ( ⟨ ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , 𝐻 ⟩ ⟩ = ⟨ ⟨ 𝐸 , 𝑓 ⟩ , ⟨ 𝑔 , ℎ ⟩ ⟩ ↔ ⟨ ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , 𝐻 ⟩ ⟩ = ⟨ ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝑔 , ℎ ⟩ ⟩ ) )
112 111 6 3anbi23d ⊢ ( 𝑓 = 𝐹 → ( ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ = ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ ∧ ⟨ ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , 𝐻 ⟩ ⟩ = ⟨ ⟨ 𝐸 , 𝑓 ⟩ , ⟨ 𝑔 , ℎ ⟩ ⟩ ∧ 𝜁 ) ↔ ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ = ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ ∧ ⟨ ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , 𝐻 ⟩ ⟩ = ⟨ ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝑔 , ℎ ⟩ ⟩ ∧ 𝜎 ) ) )
113 112 2rexbidv ⊢ ( 𝑓 = 𝐹 → ( ∃ 𝑔 ∈ 𝑃 ∃ ℎ ∈ 𝑃 ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ = ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ ∧ ⟨ ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , 𝐻 ⟩ ⟩ = ⟨ ⟨ 𝐸 , 𝑓 ⟩ , ⟨ 𝑔 , ℎ ⟩ ⟩ ∧ 𝜁 ) ↔ ∃ 𝑔 ∈ 𝑃 ∃ ℎ ∈ 𝑃 ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ = ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ ∧ ⟨ ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , 𝐻 ⟩ ⟩ = ⟨ ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝑔 , ℎ ⟩ ⟩ ∧ 𝜎 ) ) )
114 103 108 113 rspc3ev ⊢ ( ( ( 𝐷 ∈ 𝑃 ∧ 𝐸 ∈ 𝑃 ∧ 𝐹 ∈ 𝑃 ) ∧ ∃ 𝑔 ∈ 𝑃 ∃ ℎ ∈ 𝑃 ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ = ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ ∧ ⟨ ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , 𝐻 ⟩ ⟩ = ⟨ ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝑔 , ℎ ⟩ ⟩ ∧ 𝜎 ) ) → ∃ 𝑑 ∈ 𝑃 ∃ 𝑒 ∈ 𝑃 ∃ 𝑓 ∈ 𝑃 ∃ 𝑔 ∈ 𝑃 ∃ ℎ ∈ 𝑃 ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ = ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝑑 ⟩ ⟩ ∧ ⟨ ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , 𝐻 ⟩ ⟩ = ⟨ ⟨ 𝑒 , 𝑓 ⟩ , ⟨ 𝑔 , ℎ ⟩ ⟩ ∧ 𝜏 ) )
115 81 82 83 98 114 syl31anc ⊢ ( ( ( ( 𝐴 ∈ 𝑃 ∧ 𝐵 ∈ 𝑃 ) ∧ ( 𝐶 ∈ 𝑃 ∧ 𝐷 ∈ 𝑃 ∧ 𝐸 ∈ 𝑃 ) ∧ ( 𝐹 ∈ 𝑃 ∧ 𝐺 ∈ 𝑃 ∧ 𝐻 ∈ 𝑃 ) ) ∧ 𝜇 ) → ∃ 𝑑 ∈ 𝑃 ∃ 𝑒 ∈ 𝑃 ∃ 𝑓 ∈ 𝑃 ∃ 𝑔 ∈ 𝑃 ∃ ℎ ∈ 𝑃 ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ = ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝑑 ⟩ ⟩ ∧ ⟨ ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , 𝐻 ⟩ ⟩ = ⟨ ⟨ 𝑒 , 𝑓 ⟩ , ⟨ 𝑔 , ℎ ⟩ ⟩ ∧ 𝜏 ) )
116 opeq1 ⊢ ( 𝑎 = 𝐴 → ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝐴 , 𝑏 ⟩ )
117 116 opeq1d ⊢ ( 𝑎 = 𝐴 → ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ = ⟨ ⟨ 𝐴 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ )
118 117 eqeq2d ⊢ ( 𝑎 = 𝐴 → ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ↔ ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ = ⟨ ⟨ 𝐴 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ) )
119 118 1 3anbi13d ⊢ ( 𝑎 = 𝐴 → ( ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ ⟨ ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , 𝐻 ⟩ ⟩ = ⟨ ⟨ 𝑒 , 𝑓 ⟩ , ⟨ 𝑔 , ℎ ⟩ ⟩ ∧ 𝜓 ) ↔ ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ = ⟨ ⟨ 𝐴 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ ⟨ ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , 𝐻 ⟩ ⟩ = ⟨ ⟨ 𝑒 , 𝑓 ⟩ , ⟨ 𝑔 , ℎ ⟩ ⟩ ∧ 𝜒 ) ) )
120 119 rexbidv ⊢ ( 𝑎 = 𝐴 → ( ∃ ℎ ∈ 𝑃 ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ ⟨ ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , 𝐻 ⟩ ⟩ = ⟨ ⟨ 𝑒 , 𝑓 ⟩ , ⟨ 𝑔 , ℎ ⟩ ⟩ ∧ 𝜓 ) ↔ ∃ ℎ ∈ 𝑃 ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ = ⟨ ⟨ 𝐴 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ ⟨ ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , 𝐻 ⟩ ⟩ = ⟨ ⟨ 𝑒 , 𝑓 ⟩ , ⟨ 𝑔 , ℎ ⟩ ⟩ ∧ 𝜒 ) ) )
121 120 2rexbidv ⊢ ( 𝑎 = 𝐴 → ( ∃ 𝑓 ∈ 𝑃 ∃ 𝑔 ∈ 𝑃 ∃ ℎ ∈ 𝑃 ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ ⟨ ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , 𝐻 ⟩ ⟩ = ⟨ ⟨ 𝑒 , 𝑓 ⟩ , ⟨ 𝑔 , ℎ ⟩ ⟩ ∧ 𝜓 ) ↔ ∃ 𝑓 ∈ 𝑃 ∃ 𝑔 ∈ 𝑃 ∃ ℎ ∈ 𝑃 ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ = ⟨ ⟨ 𝐴 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ ⟨ ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , 𝐻 ⟩ ⟩ = ⟨ ⟨ 𝑒 , 𝑓 ⟩ , ⟨ 𝑔 , ℎ ⟩ ⟩ ∧ 𝜒 ) ) )
122 121 2rexbidv ⊢ ( 𝑎 = 𝐴 → ( ∃ 𝑑 ∈ 𝑃 ∃ 𝑒 ∈ 𝑃 ∃ 𝑓 ∈ 𝑃 ∃ 𝑔 ∈ 𝑃 ∃ ℎ ∈ 𝑃 ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ ⟨ ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , 𝐻 ⟩ ⟩ = ⟨ ⟨ 𝑒 , 𝑓 ⟩ , ⟨ 𝑔 , ℎ ⟩ ⟩ ∧ 𝜓 ) ↔ ∃ 𝑑 ∈ 𝑃 ∃ 𝑒 ∈ 𝑃 ∃ 𝑓 ∈ 𝑃 ∃ 𝑔 ∈ 𝑃 ∃ ℎ ∈ 𝑃 ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ = ⟨ ⟨ 𝐴 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ ⟨ ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , 𝐻 ⟩ ⟩ = ⟨ ⟨ 𝑒 , 𝑓 ⟩ , ⟨ 𝑔 , ℎ ⟩ ⟩ ∧ 𝜒 ) ) )
123 opeq2 ⊢ ( 𝑏 = 𝐵 → ⟨ 𝐴 , 𝑏 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ )
124 123 opeq1d ⊢ ( 𝑏 = 𝐵 → ⟨ ⟨ 𝐴 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ = ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ )
125 124 eqeq2d ⊢ ( 𝑏 = 𝐵 → ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ = ⟨ ⟨ 𝐴 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ↔ ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ = ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ) )
126 125 2 3anbi13d ⊢ ( 𝑏 = 𝐵 → ( ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ = ⟨ ⟨ 𝐴 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ ⟨ ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , 𝐻 ⟩ ⟩ = ⟨ ⟨ 𝑒 , 𝑓 ⟩ , ⟨ 𝑔 , ℎ ⟩ ⟩ ∧ 𝜒 ) ↔ ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ = ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ ⟨ ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , 𝐻 ⟩ ⟩ = ⟨ ⟨ 𝑒 , 𝑓 ⟩ , ⟨ 𝑔 , ℎ ⟩ ⟩ ∧ 𝜃 ) ) )
127 126 rexbidv ⊢ ( 𝑏 = 𝐵 → ( ∃ ℎ ∈ 𝑃 ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ = ⟨ ⟨ 𝐴 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ ⟨ ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , 𝐻 ⟩ ⟩ = ⟨ ⟨ 𝑒 , 𝑓 ⟩ , ⟨ 𝑔 , ℎ ⟩ ⟩ ∧ 𝜒 ) ↔ ∃ ℎ ∈ 𝑃 ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ = ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ ⟨ ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , 𝐻 ⟩ ⟩ = ⟨ ⟨ 𝑒 , 𝑓 ⟩ , ⟨ 𝑔 , ℎ ⟩ ⟩ ∧ 𝜃 ) ) )
128 127 2rexbidv ⊢ ( 𝑏 = 𝐵 → ( ∃ 𝑓 ∈ 𝑃 ∃ 𝑔 ∈ 𝑃 ∃ ℎ ∈ 𝑃 ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ = ⟨ ⟨ 𝐴 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ ⟨ ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , 𝐻 ⟩ ⟩ = ⟨ ⟨ 𝑒 , 𝑓 ⟩ , ⟨ 𝑔 , ℎ ⟩ ⟩ ∧ 𝜒 ) ↔ ∃ 𝑓 ∈ 𝑃 ∃ 𝑔 ∈ 𝑃 ∃ ℎ ∈ 𝑃 ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ = ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ ⟨ ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , 𝐻 ⟩ ⟩ = ⟨ ⟨ 𝑒 , 𝑓 ⟩ , ⟨ 𝑔 , ℎ ⟩ ⟩ ∧ 𝜃 ) ) )
129 128 2rexbidv ⊢ ( 𝑏 = 𝐵 → ( ∃ 𝑑 ∈ 𝑃 ∃ 𝑒 ∈ 𝑃 ∃ 𝑓 ∈ 𝑃 ∃ 𝑔 ∈ 𝑃 ∃ ℎ ∈ 𝑃 ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ = ⟨ ⟨ 𝐴 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ ⟨ ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , 𝐻 ⟩ ⟩ = ⟨ ⟨ 𝑒 , 𝑓 ⟩ , ⟨ 𝑔 , ℎ ⟩ ⟩ ∧ 𝜒 ) ↔ ∃ 𝑑 ∈ 𝑃 ∃ 𝑒 ∈ 𝑃 ∃ 𝑓 ∈ 𝑃 ∃ 𝑔 ∈ 𝑃 ∃ ℎ ∈ 𝑃 ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ = ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ ⟨ ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , 𝐻 ⟩ ⟩ = ⟨ ⟨ 𝑒 , 𝑓 ⟩ , ⟨ 𝑔 , ℎ ⟩ ⟩ ∧ 𝜃 ) ) )
130 opeq1 ⊢ ( 𝑐 = 𝐶 → ⟨ 𝑐 , 𝑑 ⟩ = ⟨ 𝐶 , 𝑑 ⟩ )
131 130 opeq2d ⊢ ( 𝑐 = 𝐶 → ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ = ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝑑 ⟩ ⟩ )
132 131 eqeq2d ⊢ ( 𝑐 = 𝐶 → ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ = ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ↔ ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ = ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝑑 ⟩ ⟩ ) )
133 132 3 3anbi13d ⊢ ( 𝑐 = 𝐶 → ( ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ = ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ ⟨ ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , 𝐻 ⟩ ⟩ = ⟨ ⟨ 𝑒 , 𝑓 ⟩ , ⟨ 𝑔 , ℎ ⟩ ⟩ ∧ 𝜃 ) ↔ ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ = ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝑑 ⟩ ⟩ ∧ ⟨ ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , 𝐻 ⟩ ⟩ = ⟨ ⟨ 𝑒 , 𝑓 ⟩ , ⟨ 𝑔 , ℎ ⟩ ⟩ ∧ 𝜏 ) ) )
134 133 rexbidv ⊢ ( 𝑐 = 𝐶 → ( ∃ ℎ ∈ 𝑃 ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ = ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ ⟨ ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , 𝐻 ⟩ ⟩ = ⟨ ⟨ 𝑒 , 𝑓 ⟩ , ⟨ 𝑔 , ℎ ⟩ ⟩ ∧ 𝜃 ) ↔ ∃ ℎ ∈ 𝑃 ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ = ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝑑 ⟩ ⟩ ∧ ⟨ ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , 𝐻 ⟩ ⟩ = ⟨ ⟨ 𝑒 , 𝑓 ⟩ , ⟨ 𝑔 , ℎ ⟩ ⟩ ∧ 𝜏 ) ) )
135 134 2rexbidv ⊢ ( 𝑐 = 𝐶 → ( ∃ 𝑓 ∈ 𝑃 ∃ 𝑔 ∈ 𝑃 ∃ ℎ ∈ 𝑃 ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ = ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ ⟨ ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , 𝐻 ⟩ ⟩ = ⟨ ⟨ 𝑒 , 𝑓 ⟩ , ⟨ 𝑔 , ℎ ⟩ ⟩ ∧ 𝜃 ) ↔ ∃ 𝑓 ∈ 𝑃 ∃ 𝑔 ∈ 𝑃 ∃ ℎ ∈ 𝑃 ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ = ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝑑 ⟩ ⟩ ∧ ⟨ ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , 𝐻 ⟩ ⟩ = ⟨ ⟨ 𝑒 , 𝑓 ⟩ , ⟨ 𝑔 , ℎ ⟩ ⟩ ∧ 𝜏 ) ) )
136 135 2rexbidv ⊢ ( 𝑐 = 𝐶 → ( ∃ 𝑑 ∈ 𝑃 ∃ 𝑒 ∈ 𝑃 ∃ 𝑓 ∈ 𝑃 ∃ 𝑔 ∈ 𝑃 ∃ ℎ ∈ 𝑃 ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ = ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ ⟨ ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , 𝐻 ⟩ ⟩ = ⟨ ⟨ 𝑒 , 𝑓 ⟩ , ⟨ 𝑔 , ℎ ⟩ ⟩ ∧ 𝜃 ) ↔ ∃ 𝑑 ∈ 𝑃 ∃ 𝑒 ∈ 𝑃 ∃ 𝑓 ∈ 𝑃 ∃ 𝑔 ∈ 𝑃 ∃ ℎ ∈ 𝑃 ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ = ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝑑 ⟩ ⟩ ∧ ⟨ ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , 𝐻 ⟩ ⟩ = ⟨ ⟨ 𝑒 , 𝑓 ⟩ , ⟨ 𝑔 , ℎ ⟩ ⟩ ∧ 𝜏 ) ) )
137 122 129 136 rspc3ev ⊢ ( ( ( 𝐴 ∈ 𝑃 ∧ 𝐵 ∈ 𝑃 ∧ 𝐶 ∈ 𝑃 ) ∧ ∃ 𝑑 ∈ 𝑃 ∃ 𝑒 ∈ 𝑃 ∃ 𝑓 ∈ 𝑃 ∃ 𝑔 ∈ 𝑃 ∃ ℎ ∈ 𝑃 ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ = ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝑑 ⟩ ⟩ ∧ ⟨ ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , 𝐻 ⟩ ⟩ = ⟨ ⟨ 𝑒 , 𝑓 ⟩ , ⟨ 𝑔 , ℎ ⟩ ⟩ ∧ 𝜏 ) ) → ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ∃ 𝑐 ∈ 𝑃 ∃ 𝑑 ∈ 𝑃 ∃ 𝑒 ∈ 𝑃 ∃ 𝑓 ∈ 𝑃 ∃ 𝑔 ∈ 𝑃 ∃ ℎ ∈ 𝑃 ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ ⟨ ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , 𝐻 ⟩ ⟩ = ⟨ ⟨ 𝑒 , 𝑓 ⟩ , ⟨ 𝑔 , ℎ ⟩ ⟩ ∧ 𝜓 ) )
138 78 79 80 115 137 syl31anc ⊢ ( ( ( ( 𝐴 ∈ 𝑃 ∧ 𝐵 ∈ 𝑃 ) ∧ ( 𝐶 ∈ 𝑃 ∧ 𝐷 ∈ 𝑃 ∧ 𝐸 ∈ 𝑃 ) ∧ ( 𝐹 ∈ 𝑃 ∧ 𝐺 ∈ 𝑃 ∧ 𝐻 ∈ 𝑃 ) ) ∧ 𝜇 ) → ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ∃ 𝑐 ∈ 𝑃 ∃ 𝑑 ∈ 𝑃 ∃ 𝑒 ∈ 𝑃 ∃ 𝑓 ∈ 𝑃 ∃ 𝑔 ∈ 𝑃 ∃ ℎ ∈ 𝑃 ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ ⟨ ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , 𝐻 ⟩ ⟩ = ⟨ ⟨ 𝑒 , 𝑓 ⟩ , ⟨ 𝑔 , ℎ ⟩ ⟩ ∧ 𝜓 ) )
139 138 ex ⊢ ( ( ( 𝐴 ∈ 𝑃 ∧ 𝐵 ∈ 𝑃 ) ∧ ( 𝐶 ∈ 𝑃 ∧ 𝐷 ∈ 𝑃 ∧ 𝐸 ∈ 𝑃 ) ∧ ( 𝐹 ∈ 𝑃 ∧ 𝐺 ∈ 𝑃 ∧ 𝐻 ∈ 𝑃 ) ) → ( 𝜇 → ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ∃ 𝑐 ∈ 𝑃 ∃ 𝑑 ∈ 𝑃 ∃ 𝑒 ∈ 𝑃 ∃ 𝑓 ∈ 𝑃 ∃ 𝑔 ∈ 𝑃 ∃ ℎ ∈ 𝑃 ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ ⟨ ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , 𝐻 ⟩ ⟩ = ⟨ ⟨ 𝑒 , 𝑓 ⟩ , ⟨ 𝑔 , ℎ ⟩ ⟩ ∧ 𝜓 ) ) )
140 77 139 impbid ⊢ ( ( ( 𝐴 ∈ 𝑃 ∧ 𝐵 ∈ 𝑃 ) ∧ ( 𝐶 ∈ 𝑃 ∧ 𝐷 ∈ 𝑃 ∧ 𝐸 ∈ 𝑃 ) ∧ ( 𝐹 ∈ 𝑃 ∧ 𝐺 ∈ 𝑃 ∧ 𝐻 ∈ 𝑃 ) ) → ( ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ∃ 𝑐 ∈ 𝑃 ∃ 𝑑 ∈ 𝑃 ∃ 𝑒 ∈ 𝑃 ∃ 𝑓 ∈ 𝑃 ∃ 𝑔 ∈ 𝑃 ∃ ℎ ∈ 𝑃 ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ ⟨ ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , 𝐻 ⟩ ⟩ = ⟨ ⟨ 𝑒 , 𝑓 ⟩ , ⟨ 𝑔 , ℎ ⟩ ⟩ ∧ 𝜓 ) ↔ 𝜇 ) )
141 10 11 12 13 14 15 16 17 140 syl233anc ⊢ ( 𝜑 → ( ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ∃ 𝑐 ∈ 𝑃 ∃ 𝑑 ∈ 𝑃 ∃ 𝑒 ∈ 𝑃 ∃ 𝑓 ∈ 𝑃 ∃ 𝑔 ∈ 𝑃 ∃ ℎ ∈ 𝑃 ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ ⟨ ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , 𝐻 ⟩ ⟩ = ⟨ ⟨ 𝑒 , 𝑓 ⟩ , ⟨ 𝑔 , ℎ ⟩ ⟩ ∧ 𝜓 ) ↔ 𝜇 ) )
142 37 141 bitrd ⊢ ( 𝜑 → ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ 𝑅 ⟨ ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , 𝐻 ⟩ ⟩ ↔ 𝜇 ) )