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

Metamath Proof Explorer

Theorem brecop

Description: Binary relation on a quotient set. Lemma for real number construction. (Contributed by NM, 29-Jan-1996)

Ref Expression
Hypotheses brecop.1 ⊢ ∼ ∈ V
brecop.2 ⊢ ∼ Er ( 𝐺 × 𝐺 )
brecop.4 ⊢ 𝐻 = ( ( 𝐺 × 𝐺 ) / ∼ )
brecop.5 ⊢ ≤ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻 ) ∧ ∃ 𝑧 ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ( ( 𝑥 = [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ ∧ 𝑦 = [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ ) ∧ 𝜑 ) ) }
brecop.6 ⊢ ( ( ( ( 𝑧 ∈ 𝐺 ∧ 𝑤 ∈ 𝐺 ) ∧ ( 𝐴 ∈ 𝐺 ∧ 𝐵 ∈ 𝐺 ) ) ∧ ( ( 𝑣 ∈ 𝐺 ∧ 𝑢 ∈ 𝐺 ) ∧ ( 𝐶 ∈ 𝐺 ∧ 𝐷 ∈ 𝐺 ) ) ) → ( ( [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ = [ ⟨ 𝐴 , 𝐵 ⟩ ] ∼ ∧ [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ = [ ⟨ 𝐶 , 𝐷 ⟩ ] ∼ ) → ( 𝜑 ↔ 𝜓 ) ) )
Assertion brecop ( ( ( 𝐴 ∈ 𝐺 ∧ 𝐵 ∈ 𝐺 ) ∧ ( 𝐶 ∈ 𝐺 ∧ 𝐷 ∈ 𝐺 ) ) → ( [ ⟨ 𝐴 , 𝐵 ⟩ ] ∼ ≤ [ ⟨ 𝐶 , 𝐷 ⟩ ] ∼ ↔ 𝜓 ) )

Proof

Step Hyp Ref Expression
1 brecop.1 ⊢ ∼ ∈ V
2 brecop.2 ⊢ ∼ Er ( 𝐺 × 𝐺 )
3 brecop.4 ⊢ 𝐻 = ( ( 𝐺 × 𝐺 ) / ∼ )
4 brecop.5 ⊢ ≤ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻 ) ∧ ∃ 𝑧 ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ( ( 𝑥 = [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ ∧ 𝑦 = [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ ) ∧ 𝜑 ) ) }
5 brecop.6 ⊢ ( ( ( ( 𝑧 ∈ 𝐺 ∧ 𝑤 ∈ 𝐺 ) ∧ ( 𝐴 ∈ 𝐺 ∧ 𝐵 ∈ 𝐺 ) ) ∧ ( ( 𝑣 ∈ 𝐺 ∧ 𝑢 ∈ 𝐺 ) ∧ ( 𝐶 ∈ 𝐺 ∧ 𝐷 ∈ 𝐺 ) ) ) → ( ( [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ = [ ⟨ 𝐴 , 𝐵 ⟩ ] ∼ ∧ [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ = [ ⟨ 𝐶 , 𝐷 ⟩ ] ∼ ) → ( 𝜑 ↔ 𝜓 ) ) )
6 1 3 ecopqsi ⊢ ( ( 𝐴 ∈ 𝐺 ∧ 𝐵 ∈ 𝐺 ) → [ ⟨ 𝐴 , 𝐵 ⟩ ] ∼ ∈ 𝐻 )
7 1 3 ecopqsi ⊢ ( ( 𝐶 ∈ 𝐺 ∧ 𝐷 ∈ 𝐺 ) → [ ⟨ 𝐶 , 𝐷 ⟩ ] ∼ ∈ 𝐻 )
8 df-br ⊢ ( [ ⟨ 𝐴 , 𝐵 ⟩ ] ∼ ≤ [ ⟨ 𝐶 , 𝐷 ⟩ ] ∼ ↔ ⟨ [ ⟨ 𝐴 , 𝐵 ⟩ ] ∼ , [ ⟨ 𝐶 , 𝐷 ⟩ ] ∼ ⟩ ∈ ≤ )
9 4 eleq2i ⊢ ( ⟨ [ ⟨ 𝐴 , 𝐵 ⟩ ] ∼ , [ ⟨ 𝐶 , 𝐷 ⟩ ] ∼ ⟩ ∈ ≤ ↔ ⟨ [ ⟨ 𝐴 , 𝐵 ⟩ ] ∼ , [ ⟨ 𝐶 , 𝐷 ⟩ ] ∼ ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻 ) ∧ ∃ 𝑧 ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ( ( 𝑥 = [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ ∧ 𝑦 = [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ ) ∧ 𝜑 ) ) } )
10 8 9 bitri ⊢ ( [ ⟨ 𝐴 , 𝐵 ⟩ ] ∼ ≤ [ ⟨ 𝐶 , 𝐷 ⟩ ] ∼ ↔ ⟨ [ ⟨ 𝐴 , 𝐵 ⟩ ] ∼ , [ ⟨ 𝐶 , 𝐷 ⟩ ] ∼ ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻 ) ∧ ∃ 𝑧 ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ( ( 𝑥 = [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ ∧ 𝑦 = [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ ) ∧ 𝜑 ) ) } )
11 eqeq1 ⊢ ( 𝑥 = [ ⟨ 𝐴 , 𝐵 ⟩ ] ∼ → ( 𝑥 = [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ ↔ [ ⟨ 𝐴 , 𝐵 ⟩ ] ∼ = [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ ) )
12 11 anbi1d ⊢ ( 𝑥 = [ ⟨ 𝐴 , 𝐵 ⟩ ] ∼ → ( ( 𝑥 = [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ ∧ 𝑦 = [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ ) ↔ ( [ ⟨ 𝐴 , 𝐵 ⟩ ] ∼ = [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ ∧ 𝑦 = [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ ) ) )
13 12 anbi1d ⊢ ( 𝑥 = [ ⟨ 𝐴 , 𝐵 ⟩ ] ∼ → ( ( ( 𝑥 = [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ ∧ 𝑦 = [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ ) ∧ 𝜑 ) ↔ ( ( [ ⟨ 𝐴 , 𝐵 ⟩ ] ∼ = [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ ∧ 𝑦 = [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ ) ∧ 𝜑 ) ) )
14 13 4exbidv ⊢ ( 𝑥 = [ ⟨ 𝐴 , 𝐵 ⟩ ] ∼ → ( ∃ 𝑧 ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ( ( 𝑥 = [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ ∧ 𝑦 = [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ ) ∧ 𝜑 ) ↔ ∃ 𝑧 ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ( ( [ ⟨ 𝐴 , 𝐵 ⟩ ] ∼ = [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ ∧ 𝑦 = [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ ) ∧ 𝜑 ) ) )
15 eqeq1 ⊢ ( 𝑦 = [ ⟨ 𝐶 , 𝐷 ⟩ ] ∼ → ( 𝑦 = [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ ↔ [ ⟨ 𝐶 , 𝐷 ⟩ ] ∼ = [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ ) )
16 15 anbi2d ⊢ ( 𝑦 = [ ⟨ 𝐶 , 𝐷 ⟩ ] ∼ → ( ( [ ⟨ 𝐴 , 𝐵 ⟩ ] ∼ = [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ ∧ 𝑦 = [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ ) ↔ ( [ ⟨ 𝐴 , 𝐵 ⟩ ] ∼ = [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ ∧ [ ⟨ 𝐶 , 𝐷 ⟩ ] ∼ = [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ ) ) )
17 16 anbi1d ⊢ ( 𝑦 = [ ⟨ 𝐶 , 𝐷 ⟩ ] ∼ → ( ( ( [ ⟨ 𝐴 , 𝐵 ⟩ ] ∼ = [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ ∧ 𝑦 = [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ ) ∧ 𝜑 ) ↔ ( ( [ ⟨ 𝐴 , 𝐵 ⟩ ] ∼ = [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ ∧ [ ⟨ 𝐶 , 𝐷 ⟩ ] ∼ = [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ ) ∧ 𝜑 ) ) )
18 17 4exbidv ⊢ ( 𝑦 = [ ⟨ 𝐶 , 𝐷 ⟩ ] ∼ → ( ∃ 𝑧 ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ( ( [ ⟨ 𝐴 , 𝐵 ⟩ ] ∼ = [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ ∧ 𝑦 = [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ ) ∧ 𝜑 ) ↔ ∃ 𝑧 ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ( ( [ ⟨ 𝐴 , 𝐵 ⟩ ] ∼ = [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ ∧ [ ⟨ 𝐶 , 𝐷 ⟩ ] ∼ = [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ ) ∧ 𝜑 ) ) )
19 14 18 opelopab2 ⊢ ( ( [ ⟨ 𝐴 , 𝐵 ⟩ ] ∼ ∈ 𝐻 ∧ [ ⟨ 𝐶 , 𝐷 ⟩ ] ∼ ∈ 𝐻 ) → ( ⟨ [ ⟨ 𝐴 , 𝐵 ⟩ ] ∼ , [ ⟨ 𝐶 , 𝐷 ⟩ ] ∼ ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻 ) ∧ ∃ 𝑧 ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ( ( 𝑥 = [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ ∧ 𝑦 = [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ ) ∧ 𝜑 ) ) } ↔ ∃ 𝑧 ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ( ( [ ⟨ 𝐴 , 𝐵 ⟩ ] ∼ = [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ ∧ [ ⟨ 𝐶 , 𝐷 ⟩ ] ∼ = [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ ) ∧ 𝜑 ) ) )
20 10 19 bitrid ⊢ ( ( [ ⟨ 𝐴 , 𝐵 ⟩ ] ∼ ∈ 𝐻 ∧ [ ⟨ 𝐶 , 𝐷 ⟩ ] ∼ ∈ 𝐻 ) → ( [ ⟨ 𝐴 , 𝐵 ⟩ ] ∼ ≤ [ ⟨ 𝐶 , 𝐷 ⟩ ] ∼ ↔ ∃ 𝑧 ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ( ( [ ⟨ 𝐴 , 𝐵 ⟩ ] ∼ = [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ ∧ [ ⟨ 𝐶 , 𝐷 ⟩ ] ∼ = [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ ) ∧ 𝜑 ) ) )
21 6 7 20 syl2an ⊢ ( ( ( 𝐴 ∈ 𝐺 ∧ 𝐵 ∈ 𝐺 ) ∧ ( 𝐶 ∈ 𝐺 ∧ 𝐷 ∈ 𝐺 ) ) → ( [ ⟨ 𝐴 , 𝐵 ⟩ ] ∼ ≤ [ ⟨ 𝐶 , 𝐷 ⟩ ] ∼ ↔ ∃ 𝑧 ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ( ( [ ⟨ 𝐴 , 𝐵 ⟩ ] ∼ = [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ ∧ [ ⟨ 𝐶 , 𝐷 ⟩ ] ∼ = [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ ) ∧ 𝜑 ) ) )
22 opeq12 ⊢ ( ( 𝑧 = 𝐴 ∧ 𝑤 = 𝐵 ) → ⟨ 𝑧 , 𝑤 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ )
23 22 eceq1d ⊢ ( ( 𝑧 = 𝐴 ∧ 𝑤 = 𝐵 ) → [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ = [ ⟨ 𝐴 , 𝐵 ⟩ ] ∼ )
24 opeq12 ⊢ ( ( 𝑣 = 𝐶 ∧ 𝑢 = 𝐷 ) → ⟨ 𝑣 , 𝑢 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ )
25 24 eceq1d ⊢ ( ( 𝑣 = 𝐶 ∧ 𝑢 = 𝐷 ) → [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ = [ ⟨ 𝐶 , 𝐷 ⟩ ] ∼ )
26 23 25 anim12i ⊢ ( ( ( 𝑧 = 𝐴 ∧ 𝑤 = 𝐵 ) ∧ ( 𝑣 = 𝐶 ∧ 𝑢 = 𝐷 ) ) → ( [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ = [ ⟨ 𝐴 , 𝐵 ⟩ ] ∼ ∧ [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ = [ ⟨ 𝐶 , 𝐷 ⟩ ] ∼ ) )
27 opelxpi ⊢ ( ( 𝐴 ∈ 𝐺 ∧ 𝐵 ∈ 𝐺 ) → ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝐺 × 𝐺 ) )
28 opelxp ⊢ ( ⟨ 𝑧 , 𝑤 ⟩ ∈ ( 𝐺 × 𝐺 ) ↔ ( 𝑧 ∈ 𝐺 ∧ 𝑤 ∈ 𝐺 ) )
29 2 a1i ⊢ ( [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ = [ ⟨ 𝐴 , 𝐵 ⟩ ] ∼ → ∼ Er ( 𝐺 × 𝐺 ) )
30 id ⊢ ( [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ = [ ⟨ 𝐴 , 𝐵 ⟩ ] ∼ → [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ = [ ⟨ 𝐴 , 𝐵 ⟩ ] ∼ )
31 29 30 ereldm ⊢ ( [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ = [ ⟨ 𝐴 , 𝐵 ⟩ ] ∼ → ( ⟨ 𝑧 , 𝑤 ⟩ ∈ ( 𝐺 × 𝐺 ) ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝐺 × 𝐺 ) ) )
32 28 31 bitr3id ⊢ ( [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ = [ ⟨ 𝐴 , 𝐵 ⟩ ] ∼ → ( ( 𝑧 ∈ 𝐺 ∧ 𝑤 ∈ 𝐺 ) ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝐺 × 𝐺 ) ) )
33 27 32 imbitrrid ⊢ ( [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ = [ ⟨ 𝐴 , 𝐵 ⟩ ] ∼ → ( ( 𝐴 ∈ 𝐺 ∧ 𝐵 ∈ 𝐺 ) → ( 𝑧 ∈ 𝐺 ∧ 𝑤 ∈ 𝐺 ) ) )
34 opelxpi ⊢ ( ( 𝐶 ∈ 𝐺 ∧ 𝐷 ∈ 𝐺 ) → ⟨ 𝐶 , 𝐷 ⟩ ∈ ( 𝐺 × 𝐺 ) )
35 opelxp ⊢ ( ⟨ 𝑣 , 𝑢 ⟩ ∈ ( 𝐺 × 𝐺 ) ↔ ( 𝑣 ∈ 𝐺 ∧ 𝑢 ∈ 𝐺 ) )
36 2 a1i ⊢ ( [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ = [ ⟨ 𝐶 , 𝐷 ⟩ ] ∼ → ∼ Er ( 𝐺 × 𝐺 ) )
37 id ⊢ ( [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ = [ ⟨ 𝐶 , 𝐷 ⟩ ] ∼ → [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ = [ ⟨ 𝐶 , 𝐷 ⟩ ] ∼ )
38 36 37 ereldm ⊢ ( [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ = [ ⟨ 𝐶 , 𝐷 ⟩ ] ∼ → ( ⟨ 𝑣 , 𝑢 ⟩ ∈ ( 𝐺 × 𝐺 ) ↔ ⟨ 𝐶 , 𝐷 ⟩ ∈ ( 𝐺 × 𝐺 ) ) )
39 35 38 bitr3id ⊢ ( [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ = [ ⟨ 𝐶 , 𝐷 ⟩ ] ∼ → ( ( 𝑣 ∈ 𝐺 ∧ 𝑢 ∈ 𝐺 ) ↔ ⟨ 𝐶 , 𝐷 ⟩ ∈ ( 𝐺 × 𝐺 ) ) )
40 34 39 imbitrrid ⊢ ( [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ = [ ⟨ 𝐶 , 𝐷 ⟩ ] ∼ → ( ( 𝐶 ∈ 𝐺 ∧ 𝐷 ∈ 𝐺 ) → ( 𝑣 ∈ 𝐺 ∧ 𝑢 ∈ 𝐺 ) ) )
41 33 40 im2anan9 ⊢ ( ( [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ = [ ⟨ 𝐴 , 𝐵 ⟩ ] ∼ ∧ [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ = [ ⟨ 𝐶 , 𝐷 ⟩ ] ∼ ) → ( ( ( 𝐴 ∈ 𝐺 ∧ 𝐵 ∈ 𝐺 ) ∧ ( 𝐶 ∈ 𝐺 ∧ 𝐷 ∈ 𝐺 ) ) → ( ( 𝑧 ∈ 𝐺 ∧ 𝑤 ∈ 𝐺 ) ∧ ( 𝑣 ∈ 𝐺 ∧ 𝑢 ∈ 𝐺 ) ) ) )
42 5 an4s ⊢ ( ( ( ( 𝑧 ∈ 𝐺 ∧ 𝑤 ∈ 𝐺 ) ∧ ( 𝑣 ∈ 𝐺 ∧ 𝑢 ∈ 𝐺 ) ) ∧ ( ( 𝐴 ∈ 𝐺 ∧ 𝐵 ∈ 𝐺 ) ∧ ( 𝐶 ∈ 𝐺 ∧ 𝐷 ∈ 𝐺 ) ) ) → ( ( [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ = [ ⟨ 𝐴 , 𝐵 ⟩ ] ∼ ∧ [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ = [ ⟨ 𝐶 , 𝐷 ⟩ ] ∼ ) → ( 𝜑 ↔ 𝜓 ) ) )
43 42 ex ⊢ ( ( ( 𝑧 ∈ 𝐺 ∧ 𝑤 ∈ 𝐺 ) ∧ ( 𝑣 ∈ 𝐺 ∧ 𝑢 ∈ 𝐺 ) ) → ( ( ( 𝐴 ∈ 𝐺 ∧ 𝐵 ∈ 𝐺 ) ∧ ( 𝐶 ∈ 𝐺 ∧ 𝐷 ∈ 𝐺 ) ) → ( ( [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ = [ ⟨ 𝐴 , 𝐵 ⟩ ] ∼ ∧ [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ = [ ⟨ 𝐶 , 𝐷 ⟩ ] ∼ ) → ( 𝜑 ↔ 𝜓 ) ) ) )
44 43 com13 ⊢ ( ( [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ = [ ⟨ 𝐴 , 𝐵 ⟩ ] ∼ ∧ [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ = [ ⟨ 𝐶 , 𝐷 ⟩ ] ∼ ) → ( ( ( 𝐴 ∈ 𝐺 ∧ 𝐵 ∈ 𝐺 ) ∧ ( 𝐶 ∈ 𝐺 ∧ 𝐷 ∈ 𝐺 ) ) → ( ( ( 𝑧 ∈ 𝐺 ∧ 𝑤 ∈ 𝐺 ) ∧ ( 𝑣 ∈ 𝐺 ∧ 𝑢 ∈ 𝐺 ) ) → ( 𝜑 ↔ 𝜓 ) ) ) )
45 41 44 mpdd ⊢ ( ( [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ = [ ⟨ 𝐴 , 𝐵 ⟩ ] ∼ ∧ [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ = [ ⟨ 𝐶 , 𝐷 ⟩ ] ∼ ) → ( ( ( 𝐴 ∈ 𝐺 ∧ 𝐵 ∈ 𝐺 ) ∧ ( 𝐶 ∈ 𝐺 ∧ 𝐷 ∈ 𝐺 ) ) → ( 𝜑 ↔ 𝜓 ) ) )
46 45 pm5.74d ⊢ ( ( [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ = [ ⟨ 𝐴 , 𝐵 ⟩ ] ∼ ∧ [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ = [ ⟨ 𝐶 , 𝐷 ⟩ ] ∼ ) → ( ( ( ( 𝐴 ∈ 𝐺 ∧ 𝐵 ∈ 𝐺 ) ∧ ( 𝐶 ∈ 𝐺 ∧ 𝐷 ∈ 𝐺 ) ) → 𝜑 ) ↔ ( ( ( 𝐴 ∈ 𝐺 ∧ 𝐵 ∈ 𝐺 ) ∧ ( 𝐶 ∈ 𝐺 ∧ 𝐷 ∈ 𝐺 ) ) → 𝜓 ) ) )
47 26 46 cgsex4g ⊢ ( ( ( 𝐴 ∈ 𝐺 ∧ 𝐵 ∈ 𝐺 ) ∧ ( 𝐶 ∈ 𝐺 ∧ 𝐷 ∈ 𝐺 ) ) → ( ∃ 𝑧 ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ( ( [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ = [ ⟨ 𝐴 , 𝐵 ⟩ ] ∼ ∧ [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ = [ ⟨ 𝐶 , 𝐷 ⟩ ] ∼ ) ∧ ( ( ( 𝐴 ∈ 𝐺 ∧ 𝐵 ∈ 𝐺 ) ∧ ( 𝐶 ∈ 𝐺 ∧ 𝐷 ∈ 𝐺 ) ) → 𝜑 ) ) ↔ ( ( ( 𝐴 ∈ 𝐺 ∧ 𝐵 ∈ 𝐺 ) ∧ ( 𝐶 ∈ 𝐺 ∧ 𝐷 ∈ 𝐺 ) ) → 𝜓 ) ) )
48 eqcom ⊢ ( [ ⟨ 𝐴 , 𝐵 ⟩ ] ∼ = [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ ↔ [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ = [ ⟨ 𝐴 , 𝐵 ⟩ ] ∼ )
49 eqcom ⊢ ( [ ⟨ 𝐶 , 𝐷 ⟩ ] ∼ = [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ ↔ [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ = [ ⟨ 𝐶 , 𝐷 ⟩ ] ∼ )
50 48 49 anbi12i ⊢ ( ( [ ⟨ 𝐴 , 𝐵 ⟩ ] ∼ = [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ ∧ [ ⟨ 𝐶 , 𝐷 ⟩ ] ∼ = [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ ) ↔ ( [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ = [ ⟨ 𝐴 , 𝐵 ⟩ ] ∼ ∧ [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ = [ ⟨ 𝐶 , 𝐷 ⟩ ] ∼ ) )
51 50 a1i ⊢ ( ( ( 𝐴 ∈ 𝐺 ∧ 𝐵 ∈ 𝐺 ) ∧ ( 𝐶 ∈ 𝐺 ∧ 𝐷 ∈ 𝐺 ) ) → ( ( [ ⟨ 𝐴 , 𝐵 ⟩ ] ∼ = [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ ∧ [ ⟨ 𝐶 , 𝐷 ⟩ ] ∼ = [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ ) ↔ ( [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ = [ ⟨ 𝐴 , 𝐵 ⟩ ] ∼ ∧ [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ = [ ⟨ 𝐶 , 𝐷 ⟩ ] ∼ ) ) )
52 biimt ⊢ ( ( ( 𝐴 ∈ 𝐺 ∧ 𝐵 ∈ 𝐺 ) ∧ ( 𝐶 ∈ 𝐺 ∧ 𝐷 ∈ 𝐺 ) ) → ( 𝜑 ↔ ( ( ( 𝐴 ∈ 𝐺 ∧ 𝐵 ∈ 𝐺 ) ∧ ( 𝐶 ∈ 𝐺 ∧ 𝐷 ∈ 𝐺 ) ) → 𝜑 ) ) )
53 51 52 anbi12d ⊢ ( ( ( 𝐴 ∈ 𝐺 ∧ 𝐵 ∈ 𝐺 ) ∧ ( 𝐶 ∈ 𝐺 ∧ 𝐷 ∈ 𝐺 ) ) → ( ( ( [ ⟨ 𝐴 , 𝐵 ⟩ ] ∼ = [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ ∧ [ ⟨ 𝐶 , 𝐷 ⟩ ] ∼ = [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ ) ∧ 𝜑 ) ↔ ( ( [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ = [ ⟨ 𝐴 , 𝐵 ⟩ ] ∼ ∧ [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ = [ ⟨ 𝐶 , 𝐷 ⟩ ] ∼ ) ∧ ( ( ( 𝐴 ∈ 𝐺 ∧ 𝐵 ∈ 𝐺 ) ∧ ( 𝐶 ∈ 𝐺 ∧ 𝐷 ∈ 𝐺 ) ) → 𝜑 ) ) ) )
54 53 4exbidv ⊢ ( ( ( 𝐴 ∈ 𝐺 ∧ 𝐵 ∈ 𝐺 ) ∧ ( 𝐶 ∈ 𝐺 ∧ 𝐷 ∈ 𝐺 ) ) → ( ∃ 𝑧 ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ( ( [ ⟨ 𝐴 , 𝐵 ⟩ ] ∼ = [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ ∧ [ ⟨ 𝐶 , 𝐷 ⟩ ] ∼ = [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ ) ∧ 𝜑 ) ↔ ∃ 𝑧 ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ( ( [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ = [ ⟨ 𝐴 , 𝐵 ⟩ ] ∼ ∧ [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ = [ ⟨ 𝐶 , 𝐷 ⟩ ] ∼ ) ∧ ( ( ( 𝐴 ∈ 𝐺 ∧ 𝐵 ∈ 𝐺 ) ∧ ( 𝐶 ∈ 𝐺 ∧ 𝐷 ∈ 𝐺 ) ) → 𝜑 ) ) ) )
55 biimt ⊢ ( ( ( 𝐴 ∈ 𝐺 ∧ 𝐵 ∈ 𝐺 ) ∧ ( 𝐶 ∈ 𝐺 ∧ 𝐷 ∈ 𝐺 ) ) → ( 𝜓 ↔ ( ( ( 𝐴 ∈ 𝐺 ∧ 𝐵 ∈ 𝐺 ) ∧ ( 𝐶 ∈ 𝐺 ∧ 𝐷 ∈ 𝐺 ) ) → 𝜓 ) ) )
56 47 54 55 3bitr4d ⊢ ( ( ( 𝐴 ∈ 𝐺 ∧ 𝐵 ∈ 𝐺 ) ∧ ( 𝐶 ∈ 𝐺 ∧ 𝐷 ∈ 𝐺 ) ) → ( ∃ 𝑧 ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ( ( [ ⟨ 𝐴 , 𝐵 ⟩ ] ∼ = [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ ∧ [ ⟨ 𝐶 , 𝐷 ⟩ ] ∼ = [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ ) ∧ 𝜑 ) ↔ 𝜓 ) )
57 21 56 bitrd ⊢ ( ( ( 𝐴 ∈ 𝐺 ∧ 𝐵 ∈ 𝐺 ) ∧ ( 𝐶 ∈ 𝐺 ∧ 𝐷 ∈ 𝐺 ) ) → ( [ ⟨ 𝐴 , 𝐵 ⟩ ] ∼ ≤ [ ⟨ 𝐶 , 𝐷 ⟩ ] ∼ ↔ 𝜓 ) )