Theorem brecop 3242

Description: Binary relation on a quotient set. Lemma for real number construction.

Hypotheses

Ref	Expression
brecop.1	⊢ S ∈ V
brecop.2	⊢ Er S
brecop.3	⊢ dom S = (G × G)
brecop.4	⊢ H = ((G × G) / S)
brecop.5	⊢ R = {⟨x, y⟩∣((x ∈ H ∧ y ∈ H) ∧ ∃z∃w∃v∃u((x = [⟨z, w⟩]S ∧ y = [⟨v, u⟩]S) ∧ φ))}
brecop.6	⊢ ((((z ∈ G ∧ w ∈ G) ∧ (A ∈ G ∧ B ∈ G)) ∧ ((v ∈ G ∧ u ∈ G) ∧ (C ∈ G ∧ D ∈ G))) → (([⟨z, w⟩]S = [⟨A, B⟩]S ∧ [⟨v, u⟩]S = [⟨C, D⟩]S) → (φ ↔ ψ)))

Assertion

Ref	Expression
brecop	⊢ (((A ∈ G ∧ B ∈ G) ∧ (C ∈ G ∧ D ∈ G)) → ([⟨A, B⟩]SR[⟨C, D⟩]S ↔ ψ))

Distinct variable group(s):   x,y,z,w,v,u,A   x,B,y,z,w,v,u   x,C,y,z,w,v,u   x,D,y,z,w,v,u   x,S,y,z,w,v,u   x,H,y   z,G,w,v,u   φ,x,y   ψ,z,w,v,u

Proof of Theorem brecop

Step	Hyp	Ref	Expression
1		eleq1 1149	. . . . . . . 8 ⊢ (x = [⟨A, B⟩]S → (x ∈ H ↔ [⟨A, B⟩]S ∈ H))
2	1	anbi1d 469	. . . . . . 7 ⊢ (x = [⟨A, B⟩]S → ((x ∈ H ∧ y ∈ H) ↔ ([⟨A, B⟩]S ∈ H ∧ y ∈ H)))
3		cleq1 1107	. . . . . . . . . 10 ⊢ (x = [⟨A, B⟩]S → (x = [⟨z, w⟩]S ↔ [⟨A, B⟩]S = [⟨z, w⟩]S))
4	3	anbi1d 469	. . . . . . . . 9 ⊢ (x = [⟨A, B⟩]S → ((x = [⟨z, w⟩]S ∧ y = [⟨v, u⟩]S) ↔ ([⟨A, B⟩]S = [⟨z, w⟩]S ∧ y = [⟨v, u⟩]S)))
5	4	anbi1d 469	. . . . . . . 8 ⊢ (x = [⟨A, B⟩]S → (((x = [⟨z, w⟩]S ∧ y = [⟨v, u⟩]S) ∧ φ) ↔ (([⟨A, B⟩]S = [⟨z, w⟩]S ∧ y = [⟨v, u⟩]S) ∧ φ)))
6	5	bi4exdv 940	. . . . . . 7 ⊢ (x = [⟨A, B⟩]S → (∃z∃w∃v∃u((x = [⟨z, w⟩]S ∧ y = [⟨v, u⟩]S) ∧ φ) ↔ ∃z∃w∃v∃u(([⟨A, B⟩]S = [⟨z, w⟩]S ∧ y = [⟨v, u⟩]S) ∧ φ)))
7	2, 6	anbi12d 476	. . . . . 6 ⊢ (x = [⟨A, B⟩]S → (((x ∈ H ∧ y ∈ H) ∧ ∃z∃w∃v∃u((x = [⟨z, w⟩]S ∧ y = [⟨v, u⟩]S) ∧ φ)) ↔ (([⟨A, B⟩]S ∈ H ∧ y ∈ H) ∧ ∃z∃w∃v∃u(([⟨A, B⟩]S = [⟨z, w⟩]S ∧ y = [⟨v, u⟩]S) ∧ φ))))
8		eleq1 1149	. . . . . . . 8 ⊢ (y = [⟨C, D⟩]S → (y ∈ H ↔ [⟨C, D⟩]S ∈ H))
9	8	anbi2d 468	. . . . . . 7 ⊢ (y = [⟨C, D⟩]S → (([⟨A, B⟩]S ∈ H ∧ y ∈ H) ↔ ([⟨A, B⟩]S ∈ H ∧ [⟨C, D⟩]S ∈ H)))
10		cleq1 1107	. . . . . . . . . 10 ⊢ (y = [⟨C, D⟩]S → (y = [⟨v, u⟩]S ↔ [⟨C, D⟩]S = [⟨v, u⟩]S))
11	10	anbi2d 468	. . . . . . . . 9 ⊢ (y = [⟨C, D⟩]S → (([⟨A, B⟩]S = [⟨z, w⟩]S ∧ y = [⟨v, u⟩]S) ↔ ([⟨A, B⟩]S = [⟨z, w⟩]S ∧ [⟨C, D⟩]S = [⟨v, u⟩]S)))
12	11	anbi1d 469	. . . . . . . 8 ⊢ (y = [⟨C, D⟩]S → ((([⟨A, B⟩]S = [⟨z, w⟩]S ∧ y = [⟨v, u⟩]S) ∧ φ) ↔ (([⟨A, B⟩]S = [⟨z, w⟩]S ∧ [⟨C, D⟩]S = [⟨v, u⟩]S) ∧ φ)))
13	12	bi4exdv 940	. . . . . . 7 ⊢ (y = [⟨C, D⟩]S → (∃z∃w∃v∃u(([⟨A, B⟩]S = [⟨z, w⟩]S ∧ y = [⟨v, u⟩]S) ∧ φ) ↔ ∃z∃w∃v∃u(([⟨A, B⟩]S = [⟨z, w⟩]S ∧ [⟨C, D⟩]S = [⟨v, u⟩]S) ∧ φ)))
14	9, 13	anbi12d 476	. . . . . 6 ⊢ (y = [⟨C, D⟩]S → ((([⟨A, B⟩]S ∈ H ∧ y ∈ H) ∧ ∃z∃w∃v∃u(([⟨A, B⟩]S = [⟨z, w⟩]S ∧ y = [⟨v, u⟩]S) ∧ φ)) ↔ (([⟨A, B⟩]S ∈ H ∧ [⟨C, D⟩]S ∈ H) ∧ ∃z∃w∃v∃u(([⟨A, B⟩]S = [⟨z, w⟩]S ∧ [⟨C, D⟩]S = [⟨v, u⟩]S) ∧ φ))))
15	7, 14	opelopabg 2115	. . . . 5 ⊢ (([⟨A, B⟩]S ∈ H ∧ [⟨C, D⟩]S ∈ H) → (⟨[⟨A, B⟩]S, [⟨C, D⟩]S⟩ ∈ {⟨x, y⟩∣((x ∈ H ∧ y ∈ H) ∧ ∃z∃w∃v∃u((x = [⟨z, w⟩]S ∧ y = [⟨v, u⟩]S) ∧ φ))} ↔ (([⟨A, B⟩]S ∈ H ∧ [⟨C, D⟩]S ∈ H) ∧ ∃z∃w∃v∃u(([⟨A, B⟩]S = [⟨z, w⟩]S ∧ [⟨C, D⟩]S = [⟨v, u⟩]S) ∧ φ))))
16		ibar 487	. . . . 5 ⊢ (([⟨A, B⟩]S ∈ H ∧ [⟨C, D⟩]S ∈ H) → (∃z∃w∃v∃u(([⟨A, B⟩]S = [⟨z, w⟩]S ∧ [⟨C, D⟩]S = [⟨v, u⟩]S) ∧ φ) ↔ (([⟨A, B⟩]S ∈ H ∧ [⟨C, D⟩]S ∈ H) ∧ ∃z∃w∃v∃u(([⟨A, B⟩]S = [⟨z, w⟩]S ∧ [⟨C, D⟩]S = [⟨v, u⟩]S) ∧ φ))))
17	15, 16	bitr4d 409	. . . 4 ⊢ (([⟨A, B⟩]S ∈ H ∧ [⟨C, D⟩]S ∈ H) → (⟨[⟨A, B⟩]S, [⟨C, D⟩]S⟩ ∈ {⟨x, y⟩∣((x ∈ H ∧ y ∈ H) ∧ ∃z∃w∃v∃u((x = [⟨z, w⟩]S ∧ y = [⟨v, u⟩]S) ∧ φ))} ↔ ∃z∃w∃v∃u(([⟨A, B⟩]S = [⟨z, w⟩]S ∧ [⟨C, D⟩]S = [⟨v, u⟩]S) ∧ φ)))
18		df-br 2063	. . . . 5 ⊢ ([⟨A, B⟩]SR[⟨C, D⟩]S ↔ ⟨[⟨A, B⟩]S, [⟨C, D⟩]S⟩ ∈ R)
19		brecop.5	. . . . . 6 ⊢ R = {⟨x, y⟩∣((x ∈ H ∧ y ∈ H) ∧ ∃z∃w∃v∃u((x = [⟨z, w⟩]S ∧ y = [⟨v, u⟩]S) ∧ φ))}
20	19	eleq2i 1153	. . . . 5 ⊢ (⟨[⟨A, B⟩]S, [⟨C, D⟩]S⟩ ∈ R ↔ ⟨[⟨A, B⟩]S, [⟨C, D⟩]S⟩ ∈ {⟨x, y⟩∣((x ∈ H ∧ y ∈ H) ∧ ∃z∃w∃v∃u((x = [⟨z, w⟩]S ∧ y = [⟨v, u⟩]S) ∧ φ))})
21	18, 20	bitr 151	. . . 4 ⊢ ([⟨A, B⟩]SR[⟨C, D⟩]S ↔ ⟨[⟨A, B⟩]S, [⟨C, D⟩]S⟩ ∈ {⟨x, y⟩∣((x ∈ H ∧ y ∈ H) ∧ ∃z∃w∃v∃u((x = [⟨z, w⟩]S ∧ y = [⟨v, u⟩]S) ∧ φ))})
22	17, 21	syl5bb 410	. . 3 ⊢ (([⟨A, B⟩]S ∈ H ∧ [⟨C, D⟩]S ∈ H) → ([⟨A, B⟩]SR[⟨C, D⟩]S ↔ ∃z∃w∃v∃u(([⟨A, B⟩]S = [⟨z, w⟩]S ∧ [⟨C, D⟩]S = [⟨v, u⟩]S) ∧ φ)))
23		brecop.1	. . . 4 ⊢ S ∈ V
24		brecop.4	. . . 4 ⊢ H = ((G × G) / S)
25	23, 24	ecopqsi 3230	. . 3 ⊢ ((A ∈ G ∧ B ∈ G) → [⟨A, B⟩]S ∈ H)
26	23, 24	ecopqsi 3230	. . 3 ⊢ ((C ∈ G ∧ D ∈ G) → [⟨C, D⟩]S ∈ H)
27	22, 25, 26	syl2an 349	. 2 ⊢ (((A ∈ G ∧ B ∈ G) ∧ (C ∈ G ∧ D ∈ G)) → ([⟨A, B⟩]SR[⟨C, D⟩]S ↔ ∃z∃w∃v∃u(([⟨A, B⟩]S = [⟨z, w⟩]S ∧ [⟨C, D⟩]S = [⟨v, u⟩]S) ∧ φ)))
28		opeq12 1878	. . . . . 6 ⊢ ((z = A ∧ w = B) → ⟨z, w⟩ = ⟨A, B⟩)
29		eceq2 3215	. . . . . 6 ⊢ (⟨z, w⟩ = ⟨A, B⟩ → [⟨z, w⟩]S = [⟨A, B⟩]S)
30	28, 29	syl 12	. . . . 5 ⊢ ((z = A ∧ w = B) → [⟨z, w⟩]S = [⟨A, B⟩]S)
31		opeq12 1878	. . . . . 6 ⊢ ((v = C ∧ u = D) → ⟨v, u⟩ = ⟨C, D⟩)
32		eceq2 3215	. . . . . 6 ⊢ (⟨v, u⟩ = ⟨C, D⟩ → [⟨v, u⟩]S = [⟨C, D⟩]S)
33	31, 32	syl 12	. . . . 5 ⊢ ((v = C ∧ u = D) → [⟨v, u⟩]S = [⟨C, D⟩]S)
34	30, 33	anim12i 268	. . . 4 ⊢ (((z = A ∧ w = B) ∧ (v = C ∧ u = D)) → ([⟨z, w⟩]S = [⟨A, B⟩]S ∧ [⟨v, u⟩]S = [⟨C, D⟩]S))
35		opex 1893	. . . . . . . . . 10 ⊢ ⟨z, w⟩ ∈ V
36		opex 1893	. . . . . . . . . 10 ⊢ ⟨A, B⟩ ∈ V
37		brecop.2	. . . . . . . . . 10 ⊢ Er S
38		brecop.3	. . . . . . . . . 10 ⊢ dom S = (G × G)
39	35, 36, 37, 38	ereldm 3222	. . . . . . . . 9 ⊢ ([⟨z, w⟩]S = [⟨A, B⟩]S → (⟨z, w⟩ ∈ (G × G) ↔ ⟨A, B⟩ ∈ (G × G)))
40		visset 1350	. . . . . . . . . 10 ⊢ w ∈ V
41	40	opelxp 2452	. . . . . . . . 9 ⊢ (⟨z, w⟩ ∈ (G × G) ↔ (z ∈ G ∧ w ∈ G))
42	39, 41	syl5bbr 412	. . . . . . . 8 ⊢ ([⟨z, w⟩]S = [⟨A, B⟩]S → ((z ∈ G ∧ w ∈ G) ↔ ⟨A, B⟩ ∈ (G × G)))
43		opelxpi 2455	. . . . . . . 8 ⊢ ((A ∈ G ∧ B ∈ G) → ⟨A, B⟩ ∈ (G × G))
44	42, 43	syl5bir 184	. . . . . . 7 ⊢ ([⟨z, w⟩]S = [⟨A, B⟩]S → ((A ∈ G ∧ B ∈ G) → (z ∈ G ∧ w ∈ G)))
45		opex 1893	. . . . . . . . . 10 ⊢ ⟨v, u⟩ ∈ V
46		opex 1893	. . . . . . . . . 10 ⊢ ⟨C, D⟩ ∈ V
47	45, 46, 37, 38	ereldm 3222	. . . . . . . . 9 ⊢ ([⟨v, u⟩]S = [⟨C, D⟩]S → (⟨v, u⟩ ∈ (G × G) ↔ ⟨C, D⟩ ∈ (G × G)))
48		visset 1350	. . . . . . . . . 10 ⊢ u ∈ V
49	48	opelxp 2452	. . . . . . . . 9 ⊢ (⟨v, u⟩ ∈ (G × G) ↔ (v ∈ G ∧ u ∈ G))
50	47, 49	syl5bbr 412	. . . . . . . 8 ⊢ ([⟨v, u⟩]S = [⟨C, D⟩]S → ((v ∈ G ∧ u ∈ G) ↔ ⟨C, D⟩ ∈ (G × G)))
51		opelxpi 2455	. . . . . . . 8 ⊢ ((C ∈ G ∧ D ∈ G) → ⟨C, D⟩ ∈ (G × G))
52	50, 51	syl5bir 184	. . . . . . 7 ⊢ ([⟨v, u⟩]S = [⟨C, D⟩]S → ((C ∈ G ∧ D ∈ G) → (v ∈ G ∧ u ∈ G)))
53	44, 52	im2anan9 434	. . . . . 6 ⊢ (([⟨z, w⟩]S = [⟨A, B⟩]S ∧ [⟨v, u⟩]S = [⟨C, D⟩]S) → (((A ∈ G ∧ B ∈ G) ∧ (C ∈ G ∧ D ∈ G)) → ((z ∈ G ∧ w ∈ G) ∧ (v ∈ G ∧ u ∈ G))))
54		brecop.6	. . . . . . . . 9 ⊢ ((((z ∈ G ∧ w ∈ G) ∧ (A ∈ G ∧ B ∈ G)) ∧ ((v ∈ G ∧ u ∈ G) ∧ (C ∈ G ∧ D ∈ G))) → (([⟨z, w⟩]S = [⟨A, B⟩]S ∧ [⟨v, u⟩]S = [⟨C, D⟩]S) → (φ ↔ ψ)))
55	54	an4s 390	. . . . . . . 8 ⊢ ((((z ∈ G ∧ w ∈ G) ∧ (v ∈ G ∧ u ∈ G)) ∧ ((A ∈ G ∧ B ∈ G) ∧ (C ∈ G ∧ D ∈ G))) → (([⟨z, w⟩]S = [⟨A, B⟩]S ∧ [⟨v, u⟩]S = [⟨C, D⟩]S) → (φ ↔ ψ)))
56	55	exp 291	. . . . . . 7 ⊢ (((z ∈ G ∧ w ∈ G) ∧ (v ∈ G ∧ u ∈ G)) → (((A ∈ G ∧ B ∈ G) ∧ (C ∈ G ∧ D ∈ G)) → (([⟨z, w⟩]S = [⟨A, B⟩]S ∧ [⟨v, u⟩]S = [⟨C, D⟩]S) → (φ ↔ ψ))))
57	56	com13 33	. . . . . 6 ⊢ (([⟨z, w⟩]S = [⟨A, B⟩]S ∧ [⟨v, u⟩]S = [⟨C, D⟩]S) → (((A ∈ G ∧ B ∈ G) ∧ (C ∈ G ∧ D ∈ G)) → (((z ∈ G ∧ w ∈ G) ∧ (v ∈ G ∧ u ∈ G)) → (φ ↔ ψ))))
58	53, 57	mpdd 47	. . . . 5 ⊢ (([⟨z, w⟩]S = [⟨A, B⟩]S ∧ [⟨v, u⟩]S = [⟨C, D⟩]S) → (((A ∈ G ∧ B ∈ G) ∧ (C ∈ G ∧ D ∈ G)) → (φ ↔ ψ)))
59	58	pm5.74d 444	. . . 4 ⊢ (([⟨z, w⟩]S = [⟨A, B⟩]S ∧ [⟨v, u⟩]S = [⟨C, D⟩]S) → ((((A ∈ G ∧ B ∈ G) ∧ (C ∈ G ∧ D ∈ G)) → φ) ↔ (((A ∈ G ∧ B ∈ G) ∧ (C ∈ G ∧ D ∈ G)) → ψ)))
60	34, 59	cgsex4g 1369	. . 3 ⊢ (((A ∈ G ∧ B ∈ G) ∧ (C ∈ G ∧ D ∈ G)) → (∃z∃w∃v∃u(([⟨z, w⟩]S = [⟨A, B⟩]S ∧ [⟨v, u⟩]S = [⟨C, D⟩]S) ∧ (((A ∈ G ∧ B ∈ G) ∧ (C ∈ G ∧ D ∈ G)) → φ)) ↔ (((A ∈ G ∧ B ∈ G) ∧ (C ∈ G ∧ D ∈ G)) → ψ)))
61		cleqcom 1103	. . . . . . 7 ⊢ ([⟨A, B⟩]S = [⟨z, w⟩]S ↔ [⟨z, w⟩]S = [⟨A, B⟩]S)
62		cleqcom 1103	. . . . . . 7 ⊢ ([⟨C, D⟩]S = [⟨v, u⟩]S ↔ [⟨v, u⟩]S = [⟨C, D⟩]S)
63	61, 62	anbi12i 369	. . . . . 6 ⊢ (([⟨A, B⟩]S = [⟨z, w⟩]S ∧ [⟨C, D⟩]S = [⟨v, u⟩]S) ↔ ([⟨z, w⟩]S = [⟨A, B⟩]S ∧ [⟨v, u⟩]S = [⟨C, D⟩]S))
64	63	a1i 7	. . . . 5 ⊢ (((A ∈ G ∧ B ∈ G) ∧ (C ∈ G ∧ D ∈ G)) → (([⟨A, B⟩]S = [⟨z, w⟩]S ∧ [⟨C, D⟩]S = [⟨v, u⟩]S) ↔ ([⟨z, w⟩]S = [⟨A, B⟩]S ∧ [⟨v, u⟩]S = [⟨C, D⟩]S)))
65		biimt 549	. . . . 5 ⊢ (((A ∈ G ∧ B ∈ G) ∧ (C ∈ G ∧ D ∈ G)) → (φ ↔ (((A ∈ G ∧ B ∈ G) ∧ (C ∈ G ∧ D ∈ G)) → φ)))
66	64, 65	anbi12d 476	. . . 4 ⊢ (((A ∈ G ∧ B ∈ G) ∧ (C ∈ G ∧ D ∈ G)) → ((([⟨A, B⟩]S = [⟨z, w⟩]S ∧ [⟨C, D⟩]S = [⟨v, u⟩]S) ∧ φ) ↔ (([⟨z, w⟩]S = [⟨A, B⟩]S ∧ [⟨v, u⟩]S = [⟨C, D⟩]S) ∧ (((A ∈ G ∧ B ∈ G) ∧ (C ∈ G ∧ D ∈ G)) → φ))))
67	66	bi4exdv 940	. . 3 ⊢ (((A ∈ G ∧ B ∈ G) ∧ (C ∈ G ∧ D ∈ G)) → (∃z∃w∃v∃u(([⟨A, B⟩]S = [⟨z, w⟩]S ∧ [⟨C, D⟩]S = [⟨v, u⟩]S) ∧ φ) ↔ ∃z∃w∃v∃u(([⟨z, w⟩]S = [⟨A, B⟩]S ∧ [⟨v, u⟩]S = [⟨C, D⟩]S) ∧ (((A ∈ G ∧ B ∈ G) ∧ (C ∈ G ∧ D ∈ G)) → φ))))
68		biimt 549	. . 3 ⊢ (((A ∈ G ∧ B ∈ G) ∧ (C ∈ G ∧ D ∈ G)) → (ψ ↔ (((A ∈ G ∧ B ∈ G) ∧ (C ∈ G ∧ D ∈ G)) → ψ)))
69	60, 67, 68	3bitr4d 424	. 2 ⊢ (((A ∈ G ∧ B ∈ G) ∧ (C ∈ G ∧ D ∈ G)) → (∃z∃w∃v∃u(([⟨A, B⟩]S = [⟨z, w⟩]S ∧ [⟨C, D⟩]S = [⟨v, u⟩]S) ∧ φ) ↔ ψ))
70	27, 69	bitrd 406	1 ⊢ (((A ∈ G ∧ B ∈ G) ∧ (C ∈ G ∧ D ∈ G)) → ([⟨A, B⟩]SR[⟨C, D⟩]S ↔ ψ))

Syntax hints:   → wi 2   ↔ wb 127   ∧ wa 196  ∃wex 678   = wceq 1091   ∈ wcel 1092  Vcvv 1348  ⟨cop 1810   class class class wbr 2054  {copab 2055   × cxp 2408  dom cdm 2410  Er wer 3197  [cec 3198   / cqs 3199

This theorem is referenced by:  ordpipq 3850  ltsrpr 3980

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-13 804  ax-14 805  ax-16 922  ax-17 925  ax-ext 1074  ax-rep 1075  ax-un 1076  ax-pow 1077

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-3an 583  df-ex 679  df-sb 853  df-clab 1093  df-cleq 1097  df-clel 1099  df-rex 1206  df-v 1349  df-dif 1489  df-un 1490  df-in 1491  df-ss 1492  df-nul 1708  df-pw 1799  df-sn 1811  df-pr 1812  df-op 1815  df-uni 1920  df-br 2063  df-opab 2098  df-xp 2424  df-cnv 2426  df-co 2427  df-dm 2428  df-rn 2429  df-res 2430  df-ima 2431  df-er 3200  df-ec 3202  df-qs 3205

metamath.org