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	syl5ibr	⊢ ( [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ = [ ⟨ 𝐴 , 𝐵 ⟩ ] ∼ → ( ( 𝐴 ∈ 𝐺 ∧ 𝐵 ∈ 𝐺 ) → ( 𝑧 ∈ 𝐺 ∧ 𝑤 ∈ 𝐺 ) ) )
34		opelxpi	⊢ ( ( 𝐶 ∈ 𝐺 ∧ 𝐷 ∈ 𝐺 ) → ⟨ 𝐶 , 𝐷 ⟩ ∈ ( 𝐺 × 𝐺 ) )
35		opelxp	⊢ ( ⟨ 𝑣 , 𝑢 ⟩ ∈ ( 𝐺 × 𝐺 ) ↔ ( 𝑣 ∈ 𝐺 ∧ 𝑢 ∈ 𝐺 ) )
36	2	a1i	⊢ ( [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ = [ ⟨ 𝐶 , 𝐷 ⟩ ] ∼ → ∼ Er ( 𝐺 × 𝐺 ) )
37		id	⊢ ( [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ = [ ⟨ 𝐶 , 𝐷 ⟩ ] ∼ → [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ = [ ⟨ 𝐶 , 𝐷 ⟩ ] ∼ )
38	36 37	ereldm	⊢ ( [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ = [ ⟨ 𝐶 , 𝐷 ⟩ ] ∼ → ( ⟨ 𝑣 , 𝑢 ⟩ ∈ ( 𝐺 × 𝐺 ) ↔ ⟨ 𝐶 , 𝐷 ⟩ ∈ ( 𝐺 × 𝐺 ) ) )
39	35 38	bitr3id	⊢ ( [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ = [ ⟨ 𝐶 , 𝐷 ⟩ ] ∼ → ( ( 𝑣 ∈ 𝐺 ∧ 𝑢 ∈ 𝐺 ) ↔ ⟨ 𝐶 , 𝐷 ⟩ ∈ ( 𝐺 × 𝐺 ) ) )
40	34 39	syl5ibr	⊢ ( [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ = [ ⟨ 𝐶 , 𝐷 ⟩ ] ∼ → ( ( 𝐶 ∈ 𝐺 ∧ 𝐷 ∈ 𝐺 ) → ( 𝑣 ∈ 𝐺 ∧ 𝑢 ∈ 𝐺 ) ) )
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	⊢ ( ( ( 𝐴 ∈ 𝐺 ∧ 𝐵 ∈ 𝐺 ) ∧ ( 𝐶 ∈ 𝐺 ∧ 𝐷 ∈ 𝐺 ) ) → ( [ ⟨ 𝐴 , 𝐵 ⟩ ] ∼ ≤ [ ⟨ 𝐶 , 𝐷 ⟩ ] ∼ ↔ 𝜓 ) )

Metamath Proof Explorer

Theorem brecop

Proof