brecop

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

	Ref	Expression
Hypotheses	brecop.1	$⊢ \underset{˙}{\sim} \in V$
	brecop.2	$⊢ \underset{˙}{\sim} Er (G \times G)$
	brecop.4	$⊢ H = (G \times G) / \underset{˙}{\sim}$
	brecop.5	$⊢ \underset{˙}{\leq} = \{⟨x, y⟩ \| ((x \in H \land y \in H) \land \exists z \exists w \exists v \exists u ((x = [⟨z, w⟩] \underset{˙}{\sim} \land y = [⟨v, u⟩] \underset{˙}{\sim}) \land φ))\}$
	brecop.6	$⊢ (((z \in G \land w \in G) \land (A \in G \land B \in G)) \land ((v \in G \land u \in G) \land (C \in G \land D \in G))) \to (([⟨z, w⟩] \underset{˙}{\sim} = [⟨A, B⟩] \underset{˙}{\sim} \land [⟨v, u⟩] \underset{˙}{\sim} = [⟨C, D⟩] \underset{˙}{\sim}) \to (φ \leftrightarrow ψ))$
Assertion	brecop	$⊢ ((A \in G \land B \in G) \land (C \in G \land D \in G)) \to ([⟨A, B⟩] \underset{˙}{\sim} \underset{˙}{\leq} [⟨C, D⟩] \underset{˙}{\sim} \leftrightarrow ψ)$

Proof

Step	Hyp	Ref	Expression
1		brecop.1	$⊢ \underset{˙}{\sim} \in V$
2		brecop.2	$⊢ \underset{˙}{\sim} Er (G \times G)$
3		brecop.4	$⊢ H = (G \times G) / \underset{˙}{\sim}$
4		brecop.5	$⊢ \underset{˙}{\leq} = \{⟨x, y⟩ \| ((x \in H \land y \in H) \land \exists z \exists w \exists v \exists u ((x = [⟨z, w⟩] \underset{˙}{\sim} \land y = [⟨v, u⟩] \underset{˙}{\sim}) \land φ))\}$
5		brecop.6	$⊢ (((z \in G \land w \in G) \land (A \in G \land B \in G)) \land ((v \in G \land u \in G) \land (C \in G \land D \in G))) \to (([⟨z, w⟩] \underset{˙}{\sim} = [⟨A, B⟩] \underset{˙}{\sim} \land [⟨v, u⟩] \underset{˙}{\sim} = [⟨C, D⟩] \underset{˙}{\sim}) \to (φ \leftrightarrow ψ))$
6	1 3	ecopqsi	$⊢ (A \in G \land B \in G) \to [⟨A, B⟩] \underset{˙}{\sim} \in H$
7	1 3	ecopqsi	$⊢ (C \in G \land D \in G) \to [⟨C, D⟩] \underset{˙}{\sim} \in H$
8		df-br	$⊢ [⟨A, B⟩] \underset{˙}{\sim} \underset{˙}{\leq} [⟨C, D⟩] \underset{˙}{\sim} \leftrightarrow ⟨[⟨A, B⟩] \underset{˙}{\sim}, [⟨C, D⟩] \underset{˙}{\sim}⟩ \in \underset{˙}{\leq}$
9	4	eleq2i	$⊢ ⟨[⟨A, B⟩] \underset{˙}{\sim}, [⟨C, D⟩] \underset{˙}{\sim}⟩ \in \underset{˙}{\leq} \leftrightarrow ⟨[⟨A, B⟩] \underset{˙}{\sim}, [⟨C, D⟩] \underset{˙}{\sim}⟩ \in \{⟨x, y⟩ \| ((x \in H \land y \in H) \land \exists z \exists w \exists v \exists u ((x = [⟨z, w⟩] \underset{˙}{\sim} \land y = [⟨v, u⟩] \underset{˙}{\sim}) \land φ))\}$
10	8 9	bitri	$⊢ [⟨A, B⟩] \underset{˙}{\sim} \underset{˙}{\leq} [⟨C, D⟩] \underset{˙}{\sim} \leftrightarrow ⟨[⟨A, B⟩] \underset{˙}{\sim}, [⟨C, D⟩] \underset{˙}{\sim}⟩ \in \{⟨x, y⟩ \| ((x \in H \land y \in H) \land \exists z \exists w \exists v \exists u ((x = [⟨z, w⟩] \underset{˙}{\sim} \land y = [⟨v, u⟩] \underset{˙}{\sim}) \land φ))\}$
11		eqeq1	$⊢ x = [⟨A, B⟩] \underset{˙}{\sim} \to (x = [⟨z, w⟩] \underset{˙}{\sim} \leftrightarrow [⟨A, B⟩] \underset{˙}{\sim} = [⟨z, w⟩] \underset{˙}{\sim})$
12	11	anbi1d	$⊢ x = [⟨A, B⟩] \underset{˙}{\sim} \to ((x = [⟨z, w⟩] \underset{˙}{\sim} \land y = [⟨v, u⟩] \underset{˙}{\sim}) \leftrightarrow ([⟨A, B⟩] \underset{˙}{\sim} = [⟨z, w⟩] \underset{˙}{\sim} \land y = [⟨v, u⟩] \underset{˙}{\sim}))$
13	12	anbi1d	$⊢ x = [⟨A, B⟩] \underset{˙}{\sim} \to (((x = [⟨z, w⟩] \underset{˙}{\sim} \land y = [⟨v, u⟩] \underset{˙}{\sim}) \land φ) \leftrightarrow (([⟨A, B⟩] \underset{˙}{\sim} = [⟨z, w⟩] \underset{˙}{\sim} \land y = [⟨v, u⟩] \underset{˙}{\sim}) \land φ))$
14	13	4exbidv	$⊢ x = [⟨A, B⟩] \underset{˙}{\sim} \to (\exists z \exists w \exists v \exists u ((x = [⟨z, w⟩] \underset{˙}{\sim} \land y = [⟨v, u⟩] \underset{˙}{\sim}) \land φ) \leftrightarrow \exists z \exists w \exists v \exists u (([⟨A, B⟩] \underset{˙}{\sim} = [⟨z, w⟩] \underset{˙}{\sim} \land y = [⟨v, u⟩] \underset{˙}{\sim}) \land φ))$
15		eqeq1	$⊢ y = [⟨C, D⟩] \underset{˙}{\sim} \to (y = [⟨v, u⟩] \underset{˙}{\sim} \leftrightarrow [⟨C, D⟩] \underset{˙}{\sim} = [⟨v, u⟩] \underset{˙}{\sim})$
16	15	anbi2d	$⊢ y = [⟨C, D⟩] \underset{˙}{\sim} \to (([⟨A, B⟩] \underset{˙}{\sim} = [⟨z, w⟩] \underset{˙}{\sim} \land y = [⟨v, u⟩] \underset{˙}{\sim}) \leftrightarrow ([⟨A, B⟩] \underset{˙}{\sim} = [⟨z, w⟩] \underset{˙}{\sim} \land [⟨C, D⟩] \underset{˙}{\sim} = [⟨v, u⟩] \underset{˙}{\sim}))$
17	16	anbi1d	$⊢ y = [⟨C, D⟩] \underset{˙}{\sim} \to ((([⟨A, B⟩] \underset{˙}{\sim} = [⟨z, w⟩] \underset{˙}{\sim} \land y = [⟨v, u⟩] \underset{˙}{\sim}) \land φ) \leftrightarrow (([⟨A, B⟩] \underset{˙}{\sim} = [⟨z, w⟩] \underset{˙}{\sim} \land [⟨C, D⟩] \underset{˙}{\sim} = [⟨v, u⟩] \underset{˙}{\sim}) \land φ))$
18	17	4exbidv	$⊢ y = [⟨C, D⟩] \underset{˙}{\sim} \to (\exists z \exists w \exists v \exists u (([⟨A, B⟩] \underset{˙}{\sim} = [⟨z, w⟩] \underset{˙}{\sim} \land y = [⟨v, u⟩] \underset{˙}{\sim}) \land φ) \leftrightarrow \exists z \exists w \exists v \exists u (([⟨A, B⟩] \underset{˙}{\sim} = [⟨z, w⟩] \underset{˙}{\sim} \land [⟨C, D⟩] \underset{˙}{\sim} = [⟨v, u⟩] \underset{˙}{\sim}) \land φ))$
19	14 18	opelopab2	$⊢ ([⟨A, B⟩] \underset{˙}{\sim} \in H \land [⟨C, D⟩] \underset{˙}{\sim} \in H) \to (⟨[⟨A, B⟩] \underset{˙}{\sim}, [⟨C, D⟩] \underset{˙}{\sim}⟩ \in \{⟨x, y⟩ \| ((x \in H \land y \in H) \land \exists z \exists w \exists v \exists u ((x = [⟨z, w⟩] \underset{˙}{\sim} \land y = [⟨v, u⟩] \underset{˙}{\sim}) \land φ))\} \leftrightarrow \exists z \exists w \exists v \exists u (([⟨A, B⟩] \underset{˙}{\sim} = [⟨z, w⟩] \underset{˙}{\sim} \land [⟨C, D⟩] \underset{˙}{\sim} = [⟨v, u⟩] \underset{˙}{\sim}) \land φ))$
20	10 19	bitrid	$⊢ ([⟨A, B⟩] \underset{˙}{\sim} \in H \land [⟨C, D⟩] \underset{˙}{\sim} \in H) \to ([⟨A, B⟩] \underset{˙}{\sim} \underset{˙}{\leq} [⟨C, D⟩] \underset{˙}{\sim} \leftrightarrow \exists z \exists w \exists v \exists u (([⟨A, B⟩] \underset{˙}{\sim} = [⟨z, w⟩] \underset{˙}{\sim} \land [⟨C, D⟩] \underset{˙}{\sim} = [⟨v, u⟩] \underset{˙}{\sim}) \land φ))$
21	6 7 20	syl2an	$⊢ ((A \in G \land B \in G) \land (C \in G \land D \in G)) \to ([⟨A, B⟩] \underset{˙}{\sim} \underset{˙}{\leq} [⟨C, D⟩] \underset{˙}{\sim} \leftrightarrow \exists z \exists w \exists v \exists u (([⟨A, B⟩] \underset{˙}{\sim} = [⟨z, w⟩] \underset{˙}{\sim} \land [⟨C, D⟩] \underset{˙}{\sim} = [⟨v, u⟩] \underset{˙}{\sim}) \land φ))$
22		opeq12	$⊢ (z = A \land w = B) \to ⟨z, w⟩ = ⟨A, B⟩$
23	22	eceq1d	$⊢ (z = A \land w = B) \to [⟨z, w⟩] \underset{˙}{\sim} = [⟨A, B⟩] \underset{˙}{\sim}$
24		opeq12	$⊢ (v = C \land u = D) \to ⟨v, u⟩ = ⟨C, D⟩$
25	24	eceq1d	$⊢ (v = C \land u = D) \to [⟨v, u⟩] \underset{˙}{\sim} = [⟨C, D⟩] \underset{˙}{\sim}$
26	23 25	anim12i	$⊢ ((z = A \land w = B) \land (v = C \land u = D)) \to ([⟨z, w⟩] \underset{˙}{\sim} = [⟨A, B⟩] \underset{˙}{\sim} \land [⟨v, u⟩] \underset{˙}{\sim} = [⟨C, D⟩] \underset{˙}{\sim})$
27		opelxpi	$⊢ (A \in G \land B \in G) \to ⟨A, B⟩ \in (G \times G)$
28		opelxp	$⊢ ⟨z, w⟩ \in (G \times G) \leftrightarrow (z \in G \land w \in G)$
29	2	a1i	$⊢ [⟨z, w⟩] \underset{˙}{\sim} = [⟨A, B⟩] \underset{˙}{\sim} \to \underset{˙}{\sim} Er (G \times G)$
30		id	$⊢ [⟨z, w⟩] \underset{˙}{\sim} = [⟨A, B⟩] \underset{˙}{\sim} \to [⟨z, w⟩] \underset{˙}{\sim} = [⟨A, B⟩] \underset{˙}{\sim}$
31	29 30	ereldm	$⊢ [⟨z, w⟩] \underset{˙}{\sim} = [⟨A, B⟩] \underset{˙}{\sim} \to (⟨z, w⟩ \in (G \times G) \leftrightarrow ⟨A, B⟩ \in (G \times G))$
32	28 31	bitr3id	$⊢ [⟨z, w⟩] \underset{˙}{\sim} = [⟨A, B⟩] \underset{˙}{\sim} \to ((z \in G \land w \in G) \leftrightarrow ⟨A, B⟩ \in (G \times G))$
33	27 32	syl5ibr	$⊢ [⟨z, w⟩] \underset{˙}{\sim} = [⟨A, B⟩] \underset{˙}{\sim} \to ((A \in G \land B \in G) \to (z \in G \land w \in G))$
34		opelxpi	$⊢ (C \in G \land D \in G) \to ⟨C, D⟩ \in (G \times G)$
35		opelxp	$⊢ ⟨v, u⟩ \in (G \times G) \leftrightarrow (v \in G \land u \in G)$
36	2	a1i	$⊢ [⟨v, u⟩] \underset{˙}{\sim} = [⟨C, D⟩] \underset{˙}{\sim} \to \underset{˙}{\sim} Er (G \times G)$
37		id	$⊢ [⟨v, u⟩] \underset{˙}{\sim} = [⟨C, D⟩] \underset{˙}{\sim} \to [⟨v, u⟩] \underset{˙}{\sim} = [⟨C, D⟩] \underset{˙}{\sim}$
38	36 37	ereldm	$⊢ [⟨v, u⟩] \underset{˙}{\sim} = [⟨C, D⟩] \underset{˙}{\sim} \to (⟨v, u⟩ \in (G \times G) \leftrightarrow ⟨C, D⟩ \in (G \times G))$
39	35 38	bitr3id	$⊢ [⟨v, u⟩] \underset{˙}{\sim} = [⟨C, D⟩] \underset{˙}{\sim} \to ((v \in G \land u \in G) \leftrightarrow ⟨C, D⟩ \in (G \times G))$
40	34 39	syl5ibr	$⊢ [⟨v, u⟩] \underset{˙}{\sim} = [⟨C, D⟩] \underset{˙}{\sim} \to ((C \in G \land D \in G) \to (v \in G \land u \in G))$
41	33 40	im2anan9	$⊢ ([⟨z, w⟩] \underset{˙}{\sim} = [⟨A, B⟩] \underset{˙}{\sim} \land [⟨v, u⟩] \underset{˙}{\sim} = [⟨C, D⟩] \underset{˙}{\sim}) \to (((A \in G \land B \in G) \land (C \in G \land D \in G)) \to ((z \in G \land w \in G) \land (v \in G \land u \in G)))$
42	5	an4s	$⊢ (((z \in G \land w \in G) \land (v \in G \land u \in G)) \land ((A \in G \land B \in G) \land (C \in G \land D \in G))) \to (([⟨z, w⟩] \underset{˙}{\sim} = [⟨A, B⟩] \underset{˙}{\sim} \land [⟨v, u⟩] \underset{˙}{\sim} = [⟨C, D⟩] \underset{˙}{\sim}) \to (φ \leftrightarrow ψ))$
43	42	ex	$⊢ ((z \in G \land w \in G) \land (v \in G \land u \in G)) \to (((A \in G \land B \in G) \land (C \in G \land D \in G)) \to (([⟨z, w⟩] \underset{˙}{\sim} = [⟨A, B⟩] \underset{˙}{\sim} \land [⟨v, u⟩] \underset{˙}{\sim} = [⟨C, D⟩] \underset{˙}{\sim}) \to (φ \leftrightarrow ψ)))$
44	43	com13	$⊢ ([⟨z, w⟩] \underset{˙}{\sim} = [⟨A, B⟩] \underset{˙}{\sim} \land [⟨v, u⟩] \underset{˙}{\sim} = [⟨C, D⟩] \underset{˙}{\sim}) \to (((A \in G \land B \in G) \land (C \in G \land D \in G)) \to (((z \in G \land w \in G) \land (v \in G \land u \in G)) \to (φ \leftrightarrow ψ)))$
45	41 44	mpdd	$⊢ ([⟨z, w⟩] \underset{˙}{\sim} = [⟨A, B⟩] \underset{˙}{\sim} \land [⟨v, u⟩] \underset{˙}{\sim} = [⟨C, D⟩] \underset{˙}{\sim}) \to (((A \in G \land B \in G) \land (C \in G \land D \in G)) \to (φ \leftrightarrow ψ))$
46	45	pm5.74d	$⊢ ([⟨z, w⟩] \underset{˙}{\sim} = [⟨A, B⟩] \underset{˙}{\sim} \land [⟨v, u⟩] \underset{˙}{\sim} = [⟨C, D⟩] \underset{˙}{\sim}) \to ((((A \in G \land B \in G) \land (C \in G \land D \in G)) \to φ) \leftrightarrow (((A \in G \land B \in G) \land (C \in G \land D \in G)) \to ψ))$
47	26 46	cgsex4g	$⊢ ((A \in G \land B \in G) \land (C \in G \land D \in G)) \to (\exists z \exists w \exists v \exists u (([⟨z, w⟩] \underset{˙}{\sim} = [⟨A, B⟩] \underset{˙}{\sim} \land [⟨v, u⟩] \underset{˙}{\sim} = [⟨C, D⟩] \underset{˙}{\sim}) \land (((A \in G \land B \in G) \land (C \in G \land D \in G)) \to φ)) \leftrightarrow (((A \in G \land B \in G) \land (C \in G \land D \in G)) \to ψ))$
48		eqcom	$⊢ [⟨A, B⟩] \underset{˙}{\sim} = [⟨z, w⟩] \underset{˙}{\sim} \leftrightarrow [⟨z, w⟩] \underset{˙}{\sim} = [⟨A, B⟩] \underset{˙}{\sim}$
49		eqcom	$⊢ [⟨C, D⟩] \underset{˙}{\sim} = [⟨v, u⟩] \underset{˙}{\sim} \leftrightarrow [⟨v, u⟩] \underset{˙}{\sim} = [⟨C, D⟩] \underset{˙}{\sim}$
50	48 49	anbi12i	$⊢ ([⟨A, B⟩] \underset{˙}{\sim} = [⟨z, w⟩] \underset{˙}{\sim} \land [⟨C, D⟩] \underset{˙}{\sim} = [⟨v, u⟩] \underset{˙}{\sim}) \leftrightarrow ([⟨z, w⟩] \underset{˙}{\sim} = [⟨A, B⟩] \underset{˙}{\sim} \land [⟨v, u⟩] \underset{˙}{\sim} = [⟨C, D⟩] \underset{˙}{\sim})$
51	50	a1i	$⊢ ((A \in G \land B \in G) \land (C \in G \land D \in G)) \to (([⟨A, B⟩] \underset{˙}{\sim} = [⟨z, w⟩] \underset{˙}{\sim} \land [⟨C, D⟩] \underset{˙}{\sim} = [⟨v, u⟩] \underset{˙}{\sim}) \leftrightarrow ([⟨z, w⟩] \underset{˙}{\sim} = [⟨A, B⟩] \underset{˙}{\sim} \land [⟨v, u⟩] \underset{˙}{\sim} = [⟨C, D⟩] \underset{˙}{\sim}))$
52		biimt	$⊢ ((A \in G \land B \in G) \land (C \in G \land D \in G)) \to (φ \leftrightarrow (((A \in G \land B \in G) \land (C \in G \land D \in G)) \to φ))$
53	51 52	anbi12d	$⊢ ((A \in G \land B \in G) \land (C \in G \land D \in G)) \to ((([⟨A, B⟩] \underset{˙}{\sim} = [⟨z, w⟩] \underset{˙}{\sim} \land [⟨C, D⟩] \underset{˙}{\sim} = [⟨v, u⟩] \underset{˙}{\sim}) \land φ) \leftrightarrow (([⟨z, w⟩] \underset{˙}{\sim} = [⟨A, B⟩] \underset{˙}{\sim} \land [⟨v, u⟩] \underset{˙}{\sim} = [⟨C, D⟩] \underset{˙}{\sim}) \land (((A \in G \land B \in G) \land (C \in G \land D \in G)) \to φ)))$
54	53	4exbidv	$⊢ ((A \in G \land B \in G) \land (C \in G \land D \in G)) \to (\exists z \exists w \exists v \exists u (([⟨A, B⟩] \underset{˙}{\sim} = [⟨z, w⟩] \underset{˙}{\sim} \land [⟨C, D⟩] \underset{˙}{\sim} = [⟨v, u⟩] \underset{˙}{\sim}) \land φ) \leftrightarrow \exists z \exists w \exists v \exists u (([⟨z, w⟩] \underset{˙}{\sim} = [⟨A, B⟩] \underset{˙}{\sim} \land [⟨v, u⟩] \underset{˙}{\sim} = [⟨C, D⟩] \underset{˙}{\sim}) \land (((A \in G \land B \in G) \land (C \in G \land D \in G)) \to φ)))$
55		biimt	$⊢ ((A \in G \land B \in G) \land (C \in G \land D \in G)) \to (ψ \leftrightarrow (((A \in G \land B \in G) \land (C \in G \land D \in G)) \to ψ))$
56	47 54 55	3bitr4d	$⊢ ((A \in G \land B \in G) \land (C \in G \land D \in G)) \to (\exists z \exists w \exists v \exists u (([⟨A, B⟩] \underset{˙}{\sim} = [⟨z, w⟩] \underset{˙}{\sim} \land [⟨C, D⟩] \underset{˙}{\sim} = [⟨v, u⟩] \underset{˙}{\sim}) \land φ) \leftrightarrow ψ)$
57	21 56	bitrd	$⊢ ((A \in G \land B \in G) \land (C \in G \land D \in G)) \to ([⟨A, B⟩] \underset{˙}{\sim} \underset{˙}{\leq} [⟨C, D⟩] \underset{˙}{\sim} \leftrightarrow ψ)$

Metamath Proof Explorer

Theorem brecop

Proof