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

Metamath Proof Explorer

Theorem br4

Description: Substitution for a four-place predicate. (Contributed by Scott Fenton, 9-Oct-2013) (Revised by Mario Carneiro, 14-Oct-2013)

Ref Expression
Hypotheses br4.1 ⊢ ( 𝑎 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
br4.2 ⊢ ( 𝑏 = 𝐵 → ( 𝜓 ↔ 𝜒 ) )
br4.3 ⊢ ( 𝑐 = 𝐶 → ( 𝜒 ↔ 𝜃 ) )
br4.4 ⊢ ( 𝑑 = 𝐷 → ( 𝜃 ↔ 𝜏 ) )
br4.5 ⊢ ( 𝑥 = 𝑋 → 𝑃 = 𝑄 )
br4.6 ⊢ 𝑅 = { ⟨ 𝑝 , 𝑞 ⟩ ∣ ∃ 𝑥 ∈ 𝑆 ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ∃ 𝑐 ∈ 𝑃 ∃ 𝑑 ∈ 𝑃 ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑞 = ⟨ 𝑐 , 𝑑 ⟩ ∧ 𝜑 ) }
Assertion br4 ( ( 𝑋 ∈ 𝑆 ∧ ( 𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄 ) ∧ ( 𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄 ) ) → ( ⟨ 𝐴 , 𝐵 ⟩ 𝑅 ⟨ 𝐶 , 𝐷 ⟩ ↔ 𝜏 ) )

Proof

Step Hyp Ref Expression
1 br4.1 ⊢ ( 𝑎 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
2 br4.2 ⊢ ( 𝑏 = 𝐵 → ( 𝜓 ↔ 𝜒 ) )
3 br4.3 ⊢ ( 𝑐 = 𝐶 → ( 𝜒 ↔ 𝜃 ) )
4 br4.4 ⊢ ( 𝑑 = 𝐷 → ( 𝜃 ↔ 𝜏 ) )
5 br4.5 ⊢ ( 𝑥 = 𝑋 → 𝑃 = 𝑄 )
6 br4.6 ⊢ 𝑅 = { ⟨ 𝑝 , 𝑞 ⟩ ∣ ∃ 𝑥 ∈ 𝑆 ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ∃ 𝑐 ∈ 𝑃 ∃ 𝑑 ∈ 𝑃 ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑞 = ⟨ 𝑐 , 𝑑 ⟩ ∧ 𝜑 ) }
7 opex ⊢ ⟨ 𝐴 , 𝐵 ⟩ ∈ V
8 opex ⊢ ⟨ 𝐶 , 𝐷 ⟩ ∈ V
9 eqeq1 ⊢ ( 𝑝 = ⟨ 𝐴 , 𝐵 ⟩ → ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ ↔ ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ) )
10 9 3anbi1d ⊢ ( 𝑝 = ⟨ 𝐴 , 𝐵 ⟩ → ( ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑞 = ⟨ 𝑐 , 𝑑 ⟩ ∧ 𝜑 ) ↔ ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑞 = ⟨ 𝑐 , 𝑑 ⟩ ∧ 𝜑 ) ) )
11 10 rexbidv ⊢ ( 𝑝 = ⟨ 𝐴 , 𝐵 ⟩ → ( ∃ 𝑑 ∈ 𝑃 ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑞 = ⟨ 𝑐 , 𝑑 ⟩ ∧ 𝜑 ) ↔ ∃ 𝑑 ∈ 𝑃 ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑞 = ⟨ 𝑐 , 𝑑 ⟩ ∧ 𝜑 ) ) )
12 11 2rexbidv ⊢ ( 𝑝 = ⟨ 𝐴 , 𝐵 ⟩ → ( ∃ 𝑏 ∈ 𝑃 ∃ 𝑐 ∈ 𝑃 ∃ 𝑑 ∈ 𝑃 ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑞 = ⟨ 𝑐 , 𝑑 ⟩ ∧ 𝜑 ) ↔ ∃ 𝑏 ∈ 𝑃 ∃ 𝑐 ∈ 𝑃 ∃ 𝑑 ∈ 𝑃 ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑞 = ⟨ 𝑐 , 𝑑 ⟩ ∧ 𝜑 ) ) )
13 12 2rexbidv ⊢ ( 𝑝 = ⟨ 𝐴 , 𝐵 ⟩ → ( ∃ 𝑥 ∈ 𝑆 ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ∃ 𝑐 ∈ 𝑃 ∃ 𝑑 ∈ 𝑃 ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑞 = ⟨ 𝑐 , 𝑑 ⟩ ∧ 𝜑 ) ↔ ∃ 𝑥 ∈ 𝑆 ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ∃ 𝑐 ∈ 𝑃 ∃ 𝑑 ∈ 𝑃 ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑞 = ⟨ 𝑐 , 𝑑 ⟩ ∧ 𝜑 ) ) )
14 eqeq1 ⊢ ( 𝑞 = ⟨ 𝐶 , 𝐷 ⟩ → ( 𝑞 = ⟨ 𝑐 , 𝑑 ⟩ ↔ ⟨ 𝐶 , 𝐷 ⟩ = ⟨ 𝑐 , 𝑑 ⟩ ) )
15 14 3anbi2d ⊢ ( 𝑞 = ⟨ 𝐶 , 𝐷 ⟩ → ( ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑞 = ⟨ 𝑐 , 𝑑 ⟩ ∧ 𝜑 ) ↔ ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ = ⟨ 𝑐 , 𝑑 ⟩ ∧ 𝜑 ) ) )
16 15 rexbidv ⊢ ( 𝑞 = ⟨ 𝐶 , 𝐷 ⟩ → ( ∃ 𝑑 ∈ 𝑃 ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑞 = ⟨ 𝑐 , 𝑑 ⟩ ∧ 𝜑 ) ↔ ∃ 𝑑 ∈ 𝑃 ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ = ⟨ 𝑐 , 𝑑 ⟩ ∧ 𝜑 ) ) )
17 16 2rexbidv ⊢ ( 𝑞 = ⟨ 𝐶 , 𝐷 ⟩ → ( ∃ 𝑏 ∈ 𝑃 ∃ 𝑐 ∈ 𝑃 ∃ 𝑑 ∈ 𝑃 ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑞 = ⟨ 𝑐 , 𝑑 ⟩ ∧ 𝜑 ) ↔ ∃ 𝑏 ∈ 𝑃 ∃ 𝑐 ∈ 𝑃 ∃ 𝑑 ∈ 𝑃 ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ = ⟨ 𝑐 , 𝑑 ⟩ ∧ 𝜑 ) ) )
18 17 2rexbidv ⊢ ( 𝑞 = ⟨ 𝐶 , 𝐷 ⟩ → ( ∃ 𝑥 ∈ 𝑆 ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ∃ 𝑐 ∈ 𝑃 ∃ 𝑑 ∈ 𝑃 ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑞 = ⟨ 𝑐 , 𝑑 ⟩ ∧ 𝜑 ) ↔ ∃ 𝑥 ∈ 𝑆 ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ∃ 𝑐 ∈ 𝑃 ∃ 𝑑 ∈ 𝑃 ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ = ⟨ 𝑐 , 𝑑 ⟩ ∧ 𝜑 ) ) )
19 7 8 13 18 6 brab ⊢ ( ⟨ 𝐴 , 𝐵 ⟩ 𝑅 ⟨ 𝐶 , 𝐷 ⟩ ↔ ∃ 𝑥 ∈ 𝑆 ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ∃ 𝑐 ∈ 𝑃 ∃ 𝑑 ∈ 𝑃 ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ = ⟨ 𝑐 , 𝑑 ⟩ ∧ 𝜑 ) )
20 vex ⊢ 𝑎 ∈ V
21 vex ⊢ 𝑏 ∈ V
22 20 21 opth ⊢ ( ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ ↔ ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ) )
23 1 2 sylan9bb ⊢ ( ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ) → ( 𝜑 ↔ 𝜒 ) )
24 22 23 sylbi ⊢ ( ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ → ( 𝜑 ↔ 𝜒 ) )
25 24 eqcoms ⊢ ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ → ( 𝜑 ↔ 𝜒 ) )
26 vex ⊢ 𝑐 ∈ V
27 vex ⊢ 𝑑 ∈ V
28 26 27 opth ⊢ ( ⟨ 𝑐 , 𝑑 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ ↔ ( 𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ) )
29 3 4 sylan9bb ⊢ ( ( 𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ) → ( 𝜒 ↔ 𝜏 ) )
30 28 29 sylbi ⊢ ( ⟨ 𝑐 , 𝑑 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ → ( 𝜒 ↔ 𝜏 ) )
31 30 eqcoms ⊢ ( ⟨ 𝐶 , 𝐷 ⟩ = ⟨ 𝑐 , 𝑑 ⟩ → ( 𝜒 ↔ 𝜏 ) )
32 25 31 sylan9bb ⊢ ( ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ = ⟨ 𝑐 , 𝑑 ⟩ ) → ( 𝜑 ↔ 𝜏 ) )
33 32 biimp3a ⊢ ( ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ = ⟨ 𝑐 , 𝑑 ⟩ ∧ 𝜑 ) → 𝜏 )
34 33 a1i ⊢ ( ( ( ( ( 𝑋 ∈ 𝑆 ∧ ( 𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄 ) ∧ ( 𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄 ) ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑎 ∈ 𝑃 ) ) ∧ ( 𝑏 ∈ 𝑃 ∧ 𝑐 ∈ 𝑃 ) ) ∧ 𝑑 ∈ 𝑃 ) → ( ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ = ⟨ 𝑐 , 𝑑 ⟩ ∧ 𝜑 ) → 𝜏 ) )
35 34 rexlimdva ⊢ ( ( ( ( 𝑋 ∈ 𝑆 ∧ ( 𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄 ) ∧ ( 𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄 ) ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑎 ∈ 𝑃 ) ) ∧ ( 𝑏 ∈ 𝑃 ∧ 𝑐 ∈ 𝑃 ) ) → ( ∃ 𝑑 ∈ 𝑃 ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ = ⟨ 𝑐 , 𝑑 ⟩ ∧ 𝜑 ) → 𝜏 ) )
36 35 rexlimdvva ⊢ ( ( ( 𝑋 ∈ 𝑆 ∧ ( 𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄 ) ∧ ( 𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄 ) ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑎 ∈ 𝑃 ) ) → ( ∃ 𝑏 ∈ 𝑃 ∃ 𝑐 ∈ 𝑃 ∃ 𝑑 ∈ 𝑃 ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ = ⟨ 𝑐 , 𝑑 ⟩ ∧ 𝜑 ) → 𝜏 ) )
37 36 rexlimdvva ⊢ ( ( 𝑋 ∈ 𝑆 ∧ ( 𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄 ) ∧ ( 𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄 ) ) → ( ∃ 𝑥 ∈ 𝑆 ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ∃ 𝑐 ∈ 𝑃 ∃ 𝑑 ∈ 𝑃 ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ = ⟨ 𝑐 , 𝑑 ⟩ ∧ 𝜑 ) → 𝜏 ) )
38 simpl1 ⊢ ( ( ( 𝑋 ∈ 𝑆 ∧ ( 𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄 ) ∧ ( 𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄 ) ) ∧ 𝜏 ) → 𝑋 ∈ 𝑆 )
39 simpl2l ⊢ ( ( ( 𝑋 ∈ 𝑆 ∧ ( 𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄 ) ∧ ( 𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄 ) ) ∧ 𝜏 ) → 𝐴 ∈ 𝑄 )
40 simpl2r ⊢ ( ( ( 𝑋 ∈ 𝑆 ∧ ( 𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄 ) ∧ ( 𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄 ) ) ∧ 𝜏 ) → 𝐵 ∈ 𝑄 )
41 simpl3l ⊢ ( ( ( 𝑋 ∈ 𝑆 ∧ ( 𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄 ) ∧ ( 𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄 ) ) ∧ 𝜏 ) → 𝐶 ∈ 𝑄 )
42 simpl3r ⊢ ( ( ( 𝑋 ∈ 𝑆 ∧ ( 𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄 ) ∧ ( 𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄 ) ) ∧ 𝜏 ) → 𝐷 ∈ 𝑄 )
43 eqidd ⊢ ( ( ( 𝑋 ∈ 𝑆 ∧ ( 𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄 ) ∧ ( 𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄 ) ) ∧ 𝜏 ) → ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ )
44 eqidd ⊢ ( ( ( 𝑋 ∈ 𝑆 ∧ ( 𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄 ) ∧ ( 𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄 ) ) ∧ 𝜏 ) → ⟨ 𝐶 , 𝐷 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ )
45 simpr ⊢ ( ( ( 𝑋 ∈ 𝑆 ∧ ( 𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄 ) ∧ ( 𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄 ) ) ∧ 𝜏 ) → 𝜏 )
46 opeq1 ⊢ ( 𝑐 = 𝐶 → ⟨ 𝑐 , 𝑑 ⟩ = ⟨ 𝐶 , 𝑑 ⟩ )
47 46 eqeq2d ⊢ ( 𝑐 = 𝐶 → ( ⟨ 𝐶 , 𝐷 ⟩ = ⟨ 𝑐 , 𝑑 ⟩ ↔ ⟨ 𝐶 , 𝐷 ⟩ = ⟨ 𝐶 , 𝑑 ⟩ ) )
48 47 3 3anbi23d ⊢ ( 𝑐 = 𝐶 → ( ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ = ⟨ 𝑐 , 𝑑 ⟩ ∧ 𝜒 ) ↔ ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ = ⟨ 𝐶 , 𝑑 ⟩ ∧ 𝜃 ) ) )
49 opeq2 ⊢ ( 𝑑 = 𝐷 → ⟨ 𝐶 , 𝑑 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ )
50 49 eqeq2d ⊢ ( 𝑑 = 𝐷 → ( ⟨ 𝐶 , 𝐷 ⟩ = ⟨ 𝐶 , 𝑑 ⟩ ↔ ⟨ 𝐶 , 𝐷 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ ) )
51 50 4 3anbi23d ⊢ ( 𝑑 = 𝐷 → ( ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ = ⟨ 𝐶 , 𝑑 ⟩ ∧ 𝜃 ) ↔ ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ ∧ 𝜏 ) ) )
52 48 51 rspc2ev ⊢ ( ( 𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄 ∧ ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ ∧ 𝜏 ) ) → ∃ 𝑐 ∈ 𝑄 ∃ 𝑑 ∈ 𝑄 ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ = ⟨ 𝑐 , 𝑑 ⟩ ∧ 𝜒 ) )
53 41 42 43 44 45 52 syl113anc ⊢ ( ( ( 𝑋 ∈ 𝑆 ∧ ( 𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄 ) ∧ ( 𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄 ) ) ∧ 𝜏 ) → ∃ 𝑐 ∈ 𝑄 ∃ 𝑑 ∈ 𝑄 ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ = ⟨ 𝑐 , 𝑑 ⟩ ∧ 𝜒 ) )
54 opeq1 ⊢ ( 𝑎 = 𝐴 → ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝐴 , 𝑏 ⟩ )
55 54 eqeq2d ⊢ ( 𝑎 = 𝐴 → ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ↔ ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝐴 , 𝑏 ⟩ ) )
56 55 1 3anbi13d ⊢ ( 𝑎 = 𝐴 → ( ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ = ⟨ 𝑐 , 𝑑 ⟩ ∧ 𝜑 ) ↔ ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ = ⟨ 𝑐 , 𝑑 ⟩ ∧ 𝜓 ) ) )
57 56 2rexbidv ⊢ ( 𝑎 = 𝐴 → ( ∃ 𝑐 ∈ 𝑄 ∃ 𝑑 ∈ 𝑄 ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ = ⟨ 𝑐 , 𝑑 ⟩ ∧ 𝜑 ) ↔ ∃ 𝑐 ∈ 𝑄 ∃ 𝑑 ∈ 𝑄 ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ = ⟨ 𝑐 , 𝑑 ⟩ ∧ 𝜓 ) ) )
58 opeq2 ⊢ ( 𝑏 = 𝐵 → ⟨ 𝐴 , 𝑏 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ )
59 58 eqeq2d ⊢ ( 𝑏 = 𝐵 → ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝐴 , 𝑏 ⟩ ↔ ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ ) )
60 59 2 3anbi13d ⊢ ( 𝑏 = 𝐵 → ( ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ = ⟨ 𝑐 , 𝑑 ⟩ ∧ 𝜓 ) ↔ ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ = ⟨ 𝑐 , 𝑑 ⟩ ∧ 𝜒 ) ) )
61 60 2rexbidv ⊢ ( 𝑏 = 𝐵 → ( ∃ 𝑐 ∈ 𝑄 ∃ 𝑑 ∈ 𝑄 ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝐴 , 𝑏 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ = ⟨ 𝑐 , 𝑑 ⟩ ∧ 𝜓 ) ↔ ∃ 𝑐 ∈ 𝑄 ∃ 𝑑 ∈ 𝑄 ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ = ⟨ 𝑐 , 𝑑 ⟩ ∧ 𝜒 ) ) )
62 57 61 rspc2ev ⊢ ( ( 𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄 ∧ ∃ 𝑐 ∈ 𝑄 ∃ 𝑑 ∈ 𝑄 ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ = ⟨ 𝑐 , 𝑑 ⟩ ∧ 𝜒 ) ) → ∃ 𝑎 ∈ 𝑄 ∃ 𝑏 ∈ 𝑄 ∃ 𝑐 ∈ 𝑄 ∃ 𝑑 ∈ 𝑄 ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ = ⟨ 𝑐 , 𝑑 ⟩ ∧ 𝜑 ) )
63 39 40 53 62 syl3anc ⊢ ( ( ( 𝑋 ∈ 𝑆 ∧ ( 𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄 ) ∧ ( 𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄 ) ) ∧ 𝜏 ) → ∃ 𝑎 ∈ 𝑄 ∃ 𝑏 ∈ 𝑄 ∃ 𝑐 ∈ 𝑄 ∃ 𝑑 ∈ 𝑄 ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ = ⟨ 𝑐 , 𝑑 ⟩ ∧ 𝜑 ) )
64 5 rexeqdv ⊢ ( 𝑥 = 𝑋 → ( ∃ 𝑑 ∈ 𝑃 ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ = ⟨ 𝑐 , 𝑑 ⟩ ∧ 𝜑 ) ↔ ∃ 𝑑 ∈ 𝑄 ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ = ⟨ 𝑐 , 𝑑 ⟩ ∧ 𝜑 ) ) )
65 5 64 rexeqbidv ⊢ ( 𝑥 = 𝑋 → ( ∃ 𝑐 ∈ 𝑃 ∃ 𝑑 ∈ 𝑃 ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ = ⟨ 𝑐 , 𝑑 ⟩ ∧ 𝜑 ) ↔ ∃ 𝑐 ∈ 𝑄 ∃ 𝑑 ∈ 𝑄 ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ = ⟨ 𝑐 , 𝑑 ⟩ ∧ 𝜑 ) ) )
66 5 65 rexeqbidv ⊢ ( 𝑥 = 𝑋 → ( ∃ 𝑏 ∈ 𝑃 ∃ 𝑐 ∈ 𝑃 ∃ 𝑑 ∈ 𝑃 ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ = ⟨ 𝑐 , 𝑑 ⟩ ∧ 𝜑 ) ↔ ∃ 𝑏 ∈ 𝑄 ∃ 𝑐 ∈ 𝑄 ∃ 𝑑 ∈ 𝑄 ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ = ⟨ 𝑐 , 𝑑 ⟩ ∧ 𝜑 ) ) )
67 5 66 rexeqbidv ⊢ ( 𝑥 = 𝑋 → ( ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ∃ 𝑐 ∈ 𝑃 ∃ 𝑑 ∈ 𝑃 ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ = ⟨ 𝑐 , 𝑑 ⟩ ∧ 𝜑 ) ↔ ∃ 𝑎 ∈ 𝑄 ∃ 𝑏 ∈ 𝑄 ∃ 𝑐 ∈ 𝑄 ∃ 𝑑 ∈ 𝑄 ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ = ⟨ 𝑐 , 𝑑 ⟩ ∧ 𝜑 ) ) )
68 67 rspcev ⊢ ( ( 𝑋 ∈ 𝑆 ∧ ∃ 𝑎 ∈ 𝑄 ∃ 𝑏 ∈ 𝑄 ∃ 𝑐 ∈ 𝑄 ∃ 𝑑 ∈ 𝑄 ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ = ⟨ 𝑐 , 𝑑 ⟩ ∧ 𝜑 ) ) → ∃ 𝑥 ∈ 𝑆 ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ∃ 𝑐 ∈ 𝑃 ∃ 𝑑 ∈ 𝑃 ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ = ⟨ 𝑐 , 𝑑 ⟩ ∧ 𝜑 ) )
69 38 63 68 syl2anc ⊢ ( ( ( 𝑋 ∈ 𝑆 ∧ ( 𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄 ) ∧ ( 𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄 ) ) ∧ 𝜏 ) → ∃ 𝑥 ∈ 𝑆 ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ∃ 𝑐 ∈ 𝑃 ∃ 𝑑 ∈ 𝑃 ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ = ⟨ 𝑐 , 𝑑 ⟩ ∧ 𝜑 ) )
70 69 ex ⊢ ( ( 𝑋 ∈ 𝑆 ∧ ( 𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄 ) ∧ ( 𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄 ) ) → ( 𝜏 → ∃ 𝑥 ∈ 𝑆 ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ∃ 𝑐 ∈ 𝑃 ∃ 𝑑 ∈ 𝑃 ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ = ⟨ 𝑐 , 𝑑 ⟩ ∧ 𝜑 ) ) )
71 37 70 impbid ⊢ ( ( 𝑋 ∈ 𝑆 ∧ ( 𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄 ) ∧ ( 𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄 ) ) → ( ∃ 𝑥 ∈ 𝑆 ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ∃ 𝑐 ∈ 𝑃 ∃ 𝑑 ∈ 𝑃 ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ = ⟨ 𝑐 , 𝑑 ⟩ ∧ 𝜑 ) ↔ 𝜏 ) )
72 19 71 bitrid ⊢ ( ( 𝑋 ∈ 𝑆 ∧ ( 𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄 ) ∧ ( 𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄 ) ) → ( ⟨ 𝐴 , 𝐵 ⟩ 𝑅 ⟨ 𝐶 , 𝐷 ⟩ ↔ 𝜏 ) )