Theorem th3q 6118

Description: Theorem 3Q of [Enderton] p. 60, extended to operations on ordered pairs. (Contributed by NM, 4-Aug-1995.) (Revised by Mario Carneiro, 19-Dec-2013.)

Hypotheses

Ref	Expression
th3q.1	⊢ ∼ ∈ V
th3q.2	⊢ ∼ Er (𝑆 × 𝑆)
th3q.4	⊢ ((((w ∈ 𝑆 ∧ v ∈ 𝑆) ∧ (u ∈ 𝑆 ∧ 𝑡 ∈ 𝑆)) ∧ ((𝑠 ∈ 𝑆 ∧ f ∈ 𝑆) ∧ (g ∈ 𝑆 ∧ ℎ ∈ 𝑆))) → ((⟨w, v⟩ ∼ ⟨u, 𝑡⟩ ∧ ⟨𝑠, f⟩ ∼ ⟨g, ℎ⟩) → (⟨w, v⟩ + ⟨𝑠, f⟩) ∼ (⟨u, 𝑡⟩ + ⟨g, ℎ⟩)))
th3q.5	⊢ 𝐺 = {⟨⟨x, y⟩, z⟩ ∣ ((x ∈ ((𝑆 × 𝑆) / ∼ ) ∧ y ∈ ((𝑆 × 𝑆) / ∼ )) ∧ ∃w∃v∃u∃𝑡((x = [⟨w, v⟩] ∼ ∧ y = [⟨u, 𝑡⟩] ∼ ) ∧ z = [(⟨w, v⟩ + ⟨u, 𝑡⟩)] ∼ ))}

Assertion

Ref	Expression
th3q	⊢ (((A ∈ 𝑆 ∧ B ∈ 𝑆) ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) → ([⟨A, B⟩] ∼ 𝐺[⟨𝐶, 𝐷⟩] ∼ ) = [(⟨A, B⟩ + ⟨𝐶, 𝐷⟩)] ∼ )

Distinct variable groups:   x,y,z,w,v,u,𝑡,𝑠,f,g,ℎ, ∼   x,𝑆,y,z,w,v,u,𝑡,𝑠,f,g,ℎ   x,A,y,z,w,v,u,𝑡,𝑠,f   x,B,y,z,w,v,u,𝑡,𝑠,f   x,𝐶,y,z,w,v,u,𝑡   x,𝐷,y,z,w,v,u,𝑡   x, + ,y,z,w,v,u,𝑡,𝑠,f,g,ℎ

Allowed substitution hints:   A(g,ℎ)   B(g,ℎ)   𝐶(f,g,ℎ,𝑠)   𝐷(f,g,ℎ,𝑠)   𝐺(x,y,z,w,v,u,𝑡,f,g,ℎ,𝑠)

Proof of Theorem th3q

Step	Hyp	Ref	Expression
1		opelxpi 4299	. . . 4 ⊢ ((A ∈ 𝑆 ∧ B ∈ 𝑆) → ⟨A, B⟩ ∈ (𝑆 × 𝑆))
2		th3q.1	. . . . 5 ⊢ ∼ ∈ V
3	2	ecelqsi 6067	. . . 4 ⊢ (⟨A, B⟩ ∈ (𝑆 × 𝑆) → [⟨A, B⟩] ∼ ∈ ((𝑆 × 𝑆) / ∼ ))
4	1, 3	syl 14	. . 3 ⊢ ((A ∈ 𝑆 ∧ B ∈ 𝑆) → [⟨A, B⟩] ∼ ∈ ((𝑆 × 𝑆) / ∼ ))
5		opelxpi 4299	. . . 4 ⊢ ((𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆) → ⟨𝐶, 𝐷⟩ ∈ (𝑆 × 𝑆))
6	2	ecelqsi 6067	. . . 4 ⊢ (⟨𝐶, 𝐷⟩ ∈ (𝑆 × 𝑆) → [⟨𝐶, 𝐷⟩] ∼ ∈ ((𝑆 × 𝑆) / ∼ ))
7	5, 6	syl 14	. . 3 ⊢ ((𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆) → [⟨𝐶, 𝐷⟩] ∼ ∈ ((𝑆 × 𝑆) / ∼ ))
8	4, 7	anim12i 321	. 2 ⊢ (((A ∈ 𝑆 ∧ B ∈ 𝑆) ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) → ([⟨A, B⟩] ∼ ∈ ((𝑆 × 𝑆) / ∼ ) ∧ [⟨𝐶, 𝐷⟩] ∼ ∈ ((𝑆 × 𝑆) / ∼ )))
9		eqid 2018	. . . 4 ⊢ [⟨A, B⟩] ∼ = [⟨A, B⟩] ∼
10		eqid 2018	. . . 4 ⊢ [⟨𝐶, 𝐷⟩] ∼ = [⟨𝐶, 𝐷⟩] ∼
11	9, 10	pm3.2i 257	. . 3 ⊢ ([⟨A, B⟩] ∼ = [⟨A, B⟩] ∼ ∧ [⟨𝐶, 𝐷⟩] ∼ = [⟨𝐶, 𝐷⟩] ∼ )
12		eqid 2018	. . 3 ⊢ [(⟨A, B⟩ + ⟨𝐶, 𝐷⟩)] ∼ = [(⟨A, B⟩ + ⟨𝐶, 𝐷⟩)] ∼
13		opeq12 3521	. . . . . 6 ⊢ ((w = A ∧ v = B) → ⟨w, v⟩ = ⟨A, B⟩)
14		eceq1 6048	. . . . . . . . 9 ⊢ (⟨w, v⟩ = ⟨A, B⟩ → [⟨w, v⟩] ∼ = [⟨A, B⟩] ∼ )
15	14	eqeq2d 2029	. . . . . . . 8 ⊢ (⟨w, v⟩ = ⟨A, B⟩ → ([⟨A, B⟩] ∼ = [⟨w, v⟩] ∼ ↔ [⟨A, B⟩] ∼ = [⟨A, B⟩] ∼ ))
16	15	anbi1d 441	. . . . . . 7 ⊢ (⟨w, v⟩ = ⟨A, B⟩ → (([⟨A, B⟩] ∼ = [⟨w, v⟩] ∼ ∧ [⟨𝐶, 𝐷⟩] ∼ = [⟨𝐶, 𝐷⟩] ∼ ) ↔ ([⟨A, B⟩] ∼ = [⟨A, B⟩] ∼ ∧ [⟨𝐶, 𝐷⟩] ∼ = [⟨𝐶, 𝐷⟩] ∼ )))
17		oveq1 5439	. . . . . . . . 9 ⊢ (⟨w, v⟩ = ⟨A, B⟩ → (⟨w, v⟩ + ⟨𝐶, 𝐷⟩) = (⟨A, B⟩ + ⟨𝐶, 𝐷⟩))
18	17	eceq1d 6049	. . . . . . . 8 ⊢ (⟨w, v⟩ = ⟨A, B⟩ → [(⟨w, v⟩ + ⟨𝐶, 𝐷⟩)] ∼ = [(⟨A, B⟩ + ⟨𝐶, 𝐷⟩)] ∼ )
19	18	eqeq2d 2029	. . . . . . 7 ⊢ (⟨w, v⟩ = ⟨A, B⟩ → ([(⟨A, B⟩ + ⟨𝐶, 𝐷⟩)] ∼ = [(⟨w, v⟩ + ⟨𝐶, 𝐷⟩)] ∼ ↔ [(⟨A, B⟩ + ⟨𝐶, 𝐷⟩)] ∼ = [(⟨A, B⟩ + ⟨𝐶, 𝐷⟩)] ∼ ))
20	16, 19	anbi12d 445	. . . . . 6 ⊢ (⟨w, v⟩ = ⟨A, B⟩ → ((([⟨A, B⟩] ∼ = [⟨w, v⟩] ∼ ∧ [⟨𝐶, 𝐷⟩] ∼ = [⟨𝐶, 𝐷⟩] ∼ ) ∧ [(⟨A, B⟩ + ⟨𝐶, 𝐷⟩)] ∼ = [(⟨w, v⟩ + ⟨𝐶, 𝐷⟩)] ∼ ) ↔ (([⟨A, B⟩] ∼ = [⟨A, B⟩] ∼ ∧ [⟨𝐶, 𝐷⟩] ∼ = [⟨𝐶, 𝐷⟩] ∼ ) ∧ [(⟨A, B⟩ + ⟨𝐶, 𝐷⟩)] ∼ = [(⟨A, B⟩ + ⟨𝐶, 𝐷⟩)] ∼ )))
21	13, 20	syl 14	. . . . 5 ⊢ ((w = A ∧ v = B) → ((([⟨A, B⟩] ∼ = [⟨w, v⟩] ∼ ∧ [⟨𝐶, 𝐷⟩] ∼ = [⟨𝐶, 𝐷⟩] ∼ ) ∧ [(⟨A, B⟩ + ⟨𝐶, 𝐷⟩)] ∼ = [(⟨w, v⟩ + ⟨𝐶, 𝐷⟩)] ∼ ) ↔ (([⟨A, B⟩] ∼ = [⟨A, B⟩] ∼ ∧ [⟨𝐶, 𝐷⟩] ∼ = [⟨𝐶, 𝐷⟩] ∼ ) ∧ [(⟨A, B⟩ + ⟨𝐶, 𝐷⟩)] ∼ = [(⟨A, B⟩ + ⟨𝐶, 𝐷⟩)] ∼ )))
22	21	spc2egv 2615	. . . 4 ⊢ ((A ∈ 𝑆 ∧ B ∈ 𝑆) → ((([⟨A, B⟩] ∼ = [⟨A, B⟩] ∼ ∧ [⟨𝐶, 𝐷⟩] ∼ = [⟨𝐶, 𝐷⟩] ∼ ) ∧ [(⟨A, B⟩ + ⟨𝐶, 𝐷⟩)] ∼ = [(⟨A, B⟩ + ⟨𝐶, 𝐷⟩)] ∼ ) → ∃w∃v(([⟨A, B⟩] ∼ = [⟨w, v⟩] ∼ ∧ [⟨𝐶, 𝐷⟩] ∼ = [⟨𝐶, 𝐷⟩] ∼ ) ∧ [(⟨A, B⟩ + ⟨𝐶, 𝐷⟩)] ∼ = [(⟨w, v⟩ + ⟨𝐶, 𝐷⟩)] ∼ )))
23		opeq12 3521	. . . . . . 7 ⊢ ((u = 𝐶 ∧ 𝑡 = 𝐷) → ⟨u, 𝑡⟩ = ⟨𝐶, 𝐷⟩)
24		eceq1 6048	. . . . . . . . . 10 ⊢ (⟨u, 𝑡⟩ = ⟨𝐶, 𝐷⟩ → [⟨u, 𝑡⟩] ∼ = [⟨𝐶, 𝐷⟩] ∼ )
25	24	eqeq2d 2029	. . . . . . . . 9 ⊢ (⟨u, 𝑡⟩ = ⟨𝐶, 𝐷⟩ → ([⟨𝐶, 𝐷⟩] ∼ = [⟨u, 𝑡⟩] ∼ ↔ [⟨𝐶, 𝐷⟩] ∼ = [⟨𝐶, 𝐷⟩] ∼ ))
26	25	anbi2d 440	. . . . . . . 8 ⊢ (⟨u, 𝑡⟩ = ⟨𝐶, 𝐷⟩ → (([⟨A, B⟩] ∼ = [⟨w, v⟩] ∼ ∧ [⟨𝐶, 𝐷⟩] ∼ = [⟨u, 𝑡⟩] ∼ ) ↔ ([⟨A, B⟩] ∼ = [⟨w, v⟩] ∼ ∧ [⟨𝐶, 𝐷⟩] ∼ = [⟨𝐶, 𝐷⟩] ∼ )))
27		oveq2 5440	. . . . . . . . . 10 ⊢ (⟨u, 𝑡⟩ = ⟨𝐶, 𝐷⟩ → (⟨w, v⟩ + ⟨u, 𝑡⟩) = (⟨w, v⟩ + ⟨𝐶, 𝐷⟩))
28	27	eceq1d 6049	. . . . . . . . 9 ⊢ (⟨u, 𝑡⟩ = ⟨𝐶, 𝐷⟩ → [(⟨w, v⟩ + ⟨u, 𝑡⟩)] ∼ = [(⟨w, v⟩ + ⟨𝐶, 𝐷⟩)] ∼ )
29	28	eqeq2d 2029	. . . . . . . 8 ⊢ (⟨u, 𝑡⟩ = ⟨𝐶, 𝐷⟩ → ([(⟨A, B⟩ + ⟨𝐶, 𝐷⟩)] ∼ = [(⟨w, v⟩ + ⟨u, 𝑡⟩)] ∼ ↔ [(⟨A, B⟩ + ⟨𝐶, 𝐷⟩)] ∼ = [(⟨w, v⟩ + ⟨𝐶, 𝐷⟩)] ∼ ))
30	26, 29	anbi12d 445	. . . . . . 7 ⊢ (⟨u, 𝑡⟩ = ⟨𝐶, 𝐷⟩ → ((([⟨A, B⟩] ∼ = [⟨w, v⟩] ∼ ∧ [⟨𝐶, 𝐷⟩] ∼ = [⟨u, 𝑡⟩] ∼ ) ∧ [(⟨A, B⟩ + ⟨𝐶, 𝐷⟩)] ∼ = [(⟨w, v⟩ + ⟨u, 𝑡⟩)] ∼ ) ↔ (([⟨A, B⟩] ∼ = [⟨w, v⟩] ∼ ∧ [⟨𝐶, 𝐷⟩] ∼ = [⟨𝐶, 𝐷⟩] ∼ ) ∧ [(⟨A, B⟩ + ⟨𝐶, 𝐷⟩)] ∼ = [(⟨w, v⟩ + ⟨𝐶, 𝐷⟩)] ∼ )))
31	23, 30	syl 14	. . . . . 6 ⊢ ((u = 𝐶 ∧ 𝑡 = 𝐷) → ((([⟨A, B⟩] ∼ = [⟨w, v⟩] ∼ ∧ [⟨𝐶, 𝐷⟩] ∼ = [⟨u, 𝑡⟩] ∼ ) ∧ [(⟨A, B⟩ + ⟨𝐶, 𝐷⟩)] ∼ = [(⟨w, v⟩ + ⟨u, 𝑡⟩)] ∼ ) ↔ (([⟨A, B⟩] ∼ = [⟨w, v⟩] ∼ ∧ [⟨𝐶, 𝐷⟩] ∼ = [⟨𝐶, 𝐷⟩] ∼ ) ∧ [(⟨A, B⟩ + ⟨𝐶, 𝐷⟩)] ∼ = [(⟨w, v⟩ + ⟨𝐶, 𝐷⟩)] ∼ )))
32	31	spc2egv 2615	. . . . 5 ⊢ ((𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆) → ((([⟨A, B⟩] ∼ = [⟨w, v⟩] ∼ ∧ [⟨𝐶, 𝐷⟩] ∼ = [⟨𝐶, 𝐷⟩] ∼ ) ∧ [(⟨A, B⟩ + ⟨𝐶, 𝐷⟩)] ∼ = [(⟨w, v⟩ + ⟨𝐶, 𝐷⟩)] ∼ ) → ∃u∃𝑡(([⟨A, B⟩] ∼ = [⟨w, v⟩] ∼ ∧ [⟨𝐶, 𝐷⟩] ∼ = [⟨u, 𝑡⟩] ∼ ) ∧ [(⟨A, B⟩ + ⟨𝐶, 𝐷⟩)] ∼ = [(⟨w, v⟩ + ⟨u, 𝑡⟩)] ∼ )))
33	32	2eximdv 1740	. . . 4 ⊢ ((𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆) → (∃w∃v(([⟨A, B⟩] ∼ = [⟨w, v⟩] ∼ ∧ [⟨𝐶, 𝐷⟩] ∼ = [⟨𝐶, 𝐷⟩] ∼ ) ∧ [(⟨A, B⟩ + ⟨𝐶, 𝐷⟩)] ∼ = [(⟨w, v⟩ + ⟨𝐶, 𝐷⟩)] ∼ ) → ∃w∃v∃u∃𝑡(([⟨A, B⟩] ∼ = [⟨w, v⟩] ∼ ∧ [⟨𝐶, 𝐷⟩] ∼ = [⟨u, 𝑡⟩] ∼ ) ∧ [(⟨A, B⟩ + ⟨𝐶, 𝐷⟩)] ∼ = [(⟨w, v⟩ + ⟨u, 𝑡⟩)] ∼ )))
34	22, 33	sylan9 391	. . 3 ⊢ (((A ∈ 𝑆 ∧ B ∈ 𝑆) ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) → ((([⟨A, B⟩] ∼ = [⟨A, B⟩] ∼ ∧ [⟨𝐶, 𝐷⟩] ∼ = [⟨𝐶, 𝐷⟩] ∼ ) ∧ [(⟨A, B⟩ + ⟨𝐶, 𝐷⟩)] ∼ = [(⟨A, B⟩ + ⟨𝐶, 𝐷⟩)] ∼ ) → ∃w∃v∃u∃𝑡(([⟨A, B⟩] ∼ = [⟨w, v⟩] ∼ ∧ [⟨𝐶, 𝐷⟩] ∼ = [⟨u, 𝑡⟩] ∼ ) ∧ [(⟨A, B⟩ + ⟨𝐶, 𝐷⟩)] ∼ = [(⟨w, v⟩ + ⟨u, 𝑡⟩)] ∼ )))
35	11, 12, 34	mp2ani 410	. 2 ⊢ (((A ∈ 𝑆 ∧ B ∈ 𝑆) ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) → ∃w∃v∃u∃𝑡(([⟨A, B⟩] ∼ = [⟨w, v⟩] ∼ ∧ [⟨𝐶, 𝐷⟩] ∼ = [⟨u, 𝑡⟩] ∼ ) ∧ [(⟨A, B⟩ + ⟨𝐶, 𝐷⟩)] ∼ = [(⟨w, v⟩ + ⟨u, 𝑡⟩)] ∼ ))
36		ecexg 6017	. . . 4 ⊢ ( ∼ ∈ V → [(⟨A, B⟩ + ⟨𝐶, 𝐷⟩)] ∼ ∈ V)
37	2, 36	ax-mp 7	. . 3 ⊢ [(⟨A, B⟩ + ⟨𝐶, 𝐷⟩)] ∼ ∈ V
38		eqeq1 2024	. . . . . . . 8 ⊢ (x = [⟨A, B⟩] ∼ → (x = [⟨w, v⟩] ∼ ↔ [⟨A, B⟩] ∼ = [⟨w, v⟩] ∼ ))
39		eqeq1 2024	. . . . . . . 8 ⊢ (y = [⟨𝐶, 𝐷⟩] ∼ → (y = [⟨u, 𝑡⟩] ∼ ↔ [⟨𝐶, 𝐷⟩] ∼ = [⟨u, 𝑡⟩] ∼ ))
40	38, 39	bi2anan9 526	. . . . . . 7 ⊢ ((x = [⟨A, B⟩] ∼ ∧ y = [⟨𝐶, 𝐷⟩] ∼ ) → ((x = [⟨w, v⟩] ∼ ∧ y = [⟨u, 𝑡⟩] ∼ ) ↔ ([⟨A, B⟩] ∼ = [⟨w, v⟩] ∼ ∧ [⟨𝐶, 𝐷⟩] ∼ = [⟨u, 𝑡⟩] ∼ )))
41		eqeq1 2024	. . . . . . 7 ⊢ (z = [(⟨A, B⟩ + ⟨𝐶, 𝐷⟩)] ∼ → (z = [(⟨w, v⟩ + ⟨u, 𝑡⟩)] ∼ ↔ [(⟨A, B⟩ + ⟨𝐶, 𝐷⟩)] ∼ = [(⟨w, v⟩ + ⟨u, 𝑡⟩)] ∼ ))
42	40, 41	bi2anan9 526	. . . . . 6 ⊢ (((x = [⟨A, B⟩] ∼ ∧ y = [⟨𝐶, 𝐷⟩] ∼ ) ∧ z = [(⟨A, B⟩ + ⟨𝐶, 𝐷⟩)] ∼ ) → (((x = [⟨w, v⟩] ∼ ∧ y = [⟨u, 𝑡⟩] ∼ ) ∧ z = [(⟨w, v⟩ + ⟨u, 𝑡⟩)] ∼ ) ↔ (([⟨A, B⟩] ∼ = [⟨w, v⟩] ∼ ∧ [⟨𝐶, 𝐷⟩] ∼ = [⟨u, 𝑡⟩] ∼ ) ∧ [(⟨A, B⟩ + ⟨𝐶, 𝐷⟩)] ∼ = [(⟨w, v⟩ + ⟨u, 𝑡⟩)] ∼ )))
43	42	3impa 1083	. . . . 5 ⊢ ((x = [⟨A, B⟩] ∼ ∧ y = [⟨𝐶, 𝐷⟩] ∼ ∧ z = [(⟨A, B⟩ + ⟨𝐶, 𝐷⟩)] ∼ ) → (((x = [⟨w, v⟩] ∼ ∧ y = [⟨u, 𝑡⟩] ∼ ) ∧ z = [(⟨w, v⟩ + ⟨u, 𝑡⟩)] ∼ ) ↔ (([⟨A, B⟩] ∼ = [⟨w, v⟩] ∼ ∧ [⟨𝐶, 𝐷⟩] ∼ = [⟨u, 𝑡⟩] ∼ ) ∧ [(⟨A, B⟩ + ⟨𝐶, 𝐷⟩)] ∼ = [(⟨w, v⟩ + ⟨u, 𝑡⟩)] ∼ )))
44	43	4exbidv 1728	. . . 4 ⊢ ((x = [⟨A, B⟩] ∼ ∧ y = [⟨𝐶, 𝐷⟩] ∼ ∧ z = [(⟨A, B⟩ + ⟨𝐶, 𝐷⟩)] ∼ ) → (∃w∃v∃u∃𝑡((x = [⟨w, v⟩] ∼ ∧ y = [⟨u, 𝑡⟩] ∼ ) ∧ z = [(⟨w, v⟩ + ⟨u, 𝑡⟩)] ∼ ) ↔ ∃w∃v∃u∃𝑡(([⟨A, B⟩] ∼ = [⟨w, v⟩] ∼ ∧ [⟨𝐶, 𝐷⟩] ∼ = [⟨u, 𝑡⟩] ∼ ) ∧ [(⟨A, B⟩ + ⟨𝐶, 𝐷⟩)] ∼ = [(⟨w, v⟩ + ⟨u, 𝑡⟩)] ∼ )))
45		th3q.2	. . . . 5 ⊢ ∼ Er (𝑆 × 𝑆)
46		th3q.4	. . . . 5 ⊢ ((((w ∈ 𝑆 ∧ v ∈ 𝑆) ∧ (u ∈ 𝑆 ∧ 𝑡 ∈ 𝑆)) ∧ ((𝑠 ∈ 𝑆 ∧ f ∈ 𝑆) ∧ (g ∈ 𝑆 ∧ ℎ ∈ 𝑆))) → ((⟨w, v⟩ ∼ ⟨u, 𝑡⟩ ∧ ⟨𝑠, f⟩ ∼ ⟨g, ℎ⟩) → (⟨w, v⟩ + ⟨𝑠, f⟩) ∼ (⟨u, 𝑡⟩ + ⟨g, ℎ⟩)))
47	2, 45, 46	th3qlem2 6116	. . . 4 ⊢ ((x ∈ ((𝑆 × 𝑆) / ∼ ) ∧ y ∈ ((𝑆 × 𝑆) / ∼ )) → ∃*z∃w∃v∃u∃𝑡((x = [⟨w, v⟩] ∼ ∧ y = [⟨u, 𝑡⟩] ∼ ) ∧ z = [(⟨w, v⟩ + ⟨u, 𝑡⟩)] ∼ ))
48		th3q.5	. . . 4 ⊢ 𝐺 = {⟨⟨x, y⟩, z⟩ ∣ ((x ∈ ((𝑆 × 𝑆) / ∼ ) ∧ y ∈ ((𝑆 × 𝑆) / ∼ )) ∧ ∃w∃v∃u∃𝑡((x = [⟨w, v⟩] ∼ ∧ y = [⟨u, 𝑡⟩] ∼ ) ∧ z = [(⟨w, v⟩ + ⟨u, 𝑡⟩)] ∼ ))}
49	44, 47, 48	ovig 5541	. . 3 ⊢ (([⟨A, B⟩] ∼ ∈ ((𝑆 × 𝑆) / ∼ ) ∧ [⟨𝐶, 𝐷⟩] ∼ ∈ ((𝑆 × 𝑆) / ∼ ) ∧ [(⟨A, B⟩ + ⟨𝐶, 𝐷⟩)] ∼ ∈ V) → (∃w∃v∃u∃𝑡(([⟨A, B⟩] ∼ = [⟨w, v⟩] ∼ ∧ [⟨𝐶, 𝐷⟩] ∼ = [⟨u, 𝑡⟩] ∼ ) ∧ [(⟨A, B⟩ + ⟨𝐶, 𝐷⟩)] ∼ = [(⟨w, v⟩ + ⟨u, 𝑡⟩)] ∼ ) → ([⟨A, B⟩] ∼ 𝐺[⟨𝐶, 𝐷⟩] ∼ ) = [(⟨A, B⟩ + ⟨𝐶, 𝐷⟩)] ∼ ))
50	37, 49	mp3an3 1204	. 2 ⊢ (([⟨A, B⟩] ∼ ∈ ((𝑆 × 𝑆) / ∼ ) ∧ [⟨𝐶, 𝐷⟩] ∼ ∈ ((𝑆 × 𝑆) / ∼ )) → (∃w∃v∃u∃𝑡(([⟨A, B⟩] ∼ = [⟨w, v⟩] ∼ ∧ [⟨𝐶, 𝐷⟩] ∼ = [⟨u, 𝑡⟩] ∼ ) ∧ [(⟨A, B⟩ + ⟨𝐶, 𝐷⟩)] ∼ = [(⟨w, v⟩ + ⟨u, 𝑡⟩)] ∼ ) → ([⟨A, B⟩] ∼ 𝐺[⟨𝐶, 𝐷⟩] ∼ ) = [(⟨A, B⟩ + ⟨𝐶, 𝐷⟩)] ∼ ))
51	8, 35, 50	sylc 56	1 ⊢ (((A ∈ 𝑆 ∧ B ∈ 𝑆) ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) → ([⟨A, B⟩] ∼ 𝐺[⟨𝐶, 𝐷⟩] ∼ ) = [(⟨A, B⟩ + ⟨𝐶, 𝐷⟩)] ∼ )

Syntax hints:   → wi 4   ∧ wa 97   ↔ wb 98   ∧ w3a 871   = wceq 1226  ∃wex 1358   ∈ wcel 1370  Vcvv 2531  ⟨cop 3349   class class class wbr 3734   × cxp 4266  (class class class)co 5432  {coprab 5433   Er wer 6010  [cec 6011   / cqs 6012

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 617  ax-5 1312  ax-7 1313  ax-gen 1314  ax-ie1 1359  ax-ie2 1360  ax-8 1372  ax-10 1373  ax-11 1374  ax-i12 1375  ax-bnd 1376  ax-4 1377  ax-13 1381  ax-14 1382  ax-17 1396  ax-i9 1400  ax-ial 1405  ax-i5r 1406  ax-ext 2000  ax-sep 3845  ax-pow 3897  ax-pr 3914  ax-un 4116

This theorem depends on definitions:  df-bi 110  df-3an 873  df-tru 1229  df-nf 1326  df-sb 1624  df-eu 1881  df-mo 1882  df-clab 2005  df-cleq 2011  df-clel 2014  df-nfc 2145  df-ral 2285  df-rex 2286  df-v 2533  df-sbc 2738  df-un 2895  df-in 2897  df-ss 2904  df-pw 3332  df-sn 3352  df-pr 3353  df-op 3355  df-uni 3551  df-br 3735  df-opab 3789  df-id 4000  df-xp 4274  df-rel 4275  df-cnv 4276  df-co 4277  df-dm 4278  df-rn 4279  df-res 4280  df-ima 4281  df-iota 4790  df-fun 4827  df-fv 4833  df-ov 5435  df-oprab 5436  df-er 6013  df-ec 6015  df-qs 6019

This theorem is referenced by:  oviec  6119