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 ⊢ ( 𝑎 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
br8.2 ⊢ ( 𝑏 = 𝐵 → ( 𝜓 ↔ 𝜒 ) )
br8.3 ⊢ ( 𝑐 = 𝐶 → ( 𝜒 ↔ 𝜃 ) )
br8.4 ⊢ ( 𝑑 = 𝐷 → ( 𝜃 ↔ 𝜏 ) )
br8.5 ⊢ ( 𝑒 = 𝐸 → ( 𝜏 ↔ 𝜂 ) )
br8.6 ⊢ ( 𝑓 = 𝐹 → ( 𝜂 ↔ 𝜁 ) )
br8.7 ⊢ ( 𝑔 = 𝐺 → ( 𝜁 ↔ 𝜎 ) )
br8.8 ⊢ ( ℎ = 𝐻 → ( 𝜎 ↔ 𝜌 ) )
br8.9 ⊢ ( 𝑥 = 𝑋 → 𝑃 = 𝑄 )
br8.10 ⊢ 𝑅 = { ⟨ 𝑝 , 𝑞 ⟩ ∣ ∃ 𝑥 ∈ 𝑆 ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ∃ 𝑐 ∈ 𝑃 ∃ 𝑑 ∈ 𝑃 ∃ 𝑒 ∈ 𝑃 ∃ 𝑓 ∈ 𝑃 ∃ 𝑔 ∈ 𝑃 ∃ ℎ ∈ 𝑃 ( 𝑝 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ 𝑞 = ⟨ ⟨ 𝑒 , 𝑓 ⟩ , ⟨ 𝑔 , ℎ ⟩ ⟩ ∧ 𝜑 ) }
Assertion br8 ( ( ( 𝑋 ∈ 𝑆 ∧ 𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄 ) ∧ ( 𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄 ∧ 𝐸 ∈ 𝑄 ) ∧ ( 𝐹 ∈ 𝑄 ∧ 𝐺 ∈ 𝑄 ∧ 𝐻 ∈ 𝑄 ) ) → ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ 𝑅 ⟨ ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , 𝐻 ⟩ ⟩ ↔ 𝜌 ) )

Proof

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