Theorem th3q 6147

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 4319	. . . 4 ⊢ ((A ∈ 𝑆 ∧ B ∈ 𝑆) → ⟨A, B⟩ ∈ (𝑆 × 𝑆))
2		th3q.1	. . . . 5 ⊢ ∼ ∈ V
3	2	ecelqsi 6096	. . . 4 ⊢ (⟨A, B⟩ ∈ (𝑆 × 𝑆) → [⟨A, B⟩] ∼ ∈ ((𝑆 × 𝑆) / ∼ ))
4	1, 3	syl 14	. . 3 ⊢ ((A ∈ 𝑆 ∧ B ∈ 𝑆) → [⟨A, B⟩] ∼ ∈ ((𝑆 × 𝑆) / ∼ ))
5		opelxpi 4319	. . . 4 ⊢ ((𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆) → ⟨𝐶, 𝐷⟩ ∈ (𝑆 × 𝑆))
6	2	ecelqsi 6096	. . . 4 ⊢ (⟨𝐶, 𝐷⟩ ∈ (𝑆 × 𝑆) → [⟨𝐶, 𝐷⟩] ∼ ∈ ((𝑆 × 𝑆) / ∼ ))
7	5, 6	syl 14	. . 3 ⊢ ((𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆) → [⟨𝐶, 𝐷⟩] ∼ ∈ ((𝑆 × 𝑆) / ∼ ))
8	4, 7	anim12i 321	. 2 ⊢ (((A ∈ 𝑆 ∧ B ∈ 𝑆) ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) → ([⟨A, B⟩] ∼ ∈ ((𝑆 × 𝑆) / ∼ ) ∧ [⟨𝐶, 𝐷⟩] ∼ ∈ ((𝑆 × 𝑆) / ∼ )))
9		eqid 2037	. . . 4 ⊢ [⟨A, B⟩] ∼ = [⟨A, B⟩] ∼
10		eqid 2037	. . . 4 ⊢ [⟨𝐶, 𝐷⟩] ∼ = [⟨𝐶, 𝐷⟩] ∼
11	9, 10	pm3.2i 257	. . 3 ⊢ ([⟨A, B⟩] ∼ = [⟨A, B⟩] ∼ ∧ [⟨𝐶, 𝐷⟩] ∼ = [⟨𝐶, 𝐷⟩] ∼ )
12		eqid 2037	. . 3 ⊢ [(⟨A, B⟩ + ⟨𝐶, 𝐷⟩)] ∼ = [(⟨A, B⟩ + ⟨𝐶, 𝐷⟩)] ∼
13		opeq12 3542	. . . . . 6 ⊢ ((w = A ∧ v = B) → ⟨w, v⟩ = ⟨A, B⟩)
14		eceq1 6077	. . . . . . . . 9 ⊢ (⟨w, v⟩ = ⟨A, B⟩ → [⟨w, v⟩] ∼ = [⟨A, B⟩] ∼ )
15	14	eqeq2d 2048	. . . . . . . 8 ⊢ (⟨w, v⟩ = ⟨A, B⟩ → ([⟨A, B⟩] ∼ = [⟨w, v⟩] ∼ ↔ [⟨A, B⟩] ∼ = [⟨A, B⟩] ∼ ))
16	15	anbi1d 438	. . . . . . 7 ⊢ (⟨w, v⟩ = ⟨A, B⟩ → (([⟨A, B⟩] ∼ = [⟨w, v⟩] ∼ ∧ [⟨𝐶, 𝐷⟩] ∼ = [⟨𝐶, 𝐷⟩] ∼ ) ↔ ([⟨A, B⟩] ∼ = [⟨A, B⟩] ∼ ∧ [⟨𝐶, 𝐷⟩] ∼ = [⟨𝐶, 𝐷⟩] ∼ )))
17		oveq1 5462	. . . . . . . . 9 ⊢ (⟨w, v⟩ = ⟨A, B⟩ → (⟨w, v⟩ + ⟨𝐶, 𝐷⟩) = (⟨A, B⟩ + ⟨𝐶, 𝐷⟩))
18	17	eceq1d 6078	. . . . . . . 8 ⊢ (⟨w, v⟩ = ⟨A, B⟩ → [(⟨w, v⟩ + ⟨𝐶, 𝐷⟩)] ∼ = [(⟨A, B⟩ + ⟨𝐶, 𝐷⟩)] ∼ )
19	18	eqeq2d 2048	. . . . . . 7 ⊢ (⟨w, v⟩ = ⟨A, B⟩ → ([(⟨A, B⟩ + ⟨𝐶, 𝐷⟩)] ∼ = [(⟨w, v⟩ + ⟨𝐶, 𝐷⟩)] ∼ ↔ [(⟨A, B⟩ + ⟨𝐶, 𝐷⟩)] ∼ = [(⟨A, B⟩ + ⟨𝐶, 𝐷⟩)] ∼ ))
20	16, 19	anbi12d 442	. . . . . 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 2636	. . . 4 ⊢ ((A ∈ 𝑆 ∧ B ∈ 𝑆) → ((([⟨A, B⟩] ∼ = [⟨A, B⟩] ∼ ∧ [⟨𝐶, 𝐷⟩] ∼ = [⟨𝐶, 𝐷⟩] ∼ ) ∧ [(⟨A, B⟩ + ⟨𝐶, 𝐷⟩)] ∼ = [(⟨A, B⟩ + ⟨𝐶, 𝐷⟩)] ∼ ) → ∃w∃v(([⟨A, B⟩] ∼ = [⟨w, v⟩] ∼ ∧ [⟨𝐶, 𝐷⟩] ∼ = [⟨𝐶, 𝐷⟩] ∼ ) ∧ [(⟨A, B⟩ + ⟨𝐶, 𝐷⟩)] ∼ = [(⟨w, v⟩ + ⟨𝐶, 𝐷⟩)] ∼ )))
23		opeq12 3542	. . . . . . 7 ⊢ ((u = 𝐶 ∧ 𝑡 = 𝐷) → ⟨u, 𝑡⟩ = ⟨𝐶, 𝐷⟩)
24		eceq1 6077	. . . . . . . . . 10 ⊢ (⟨u, 𝑡⟩ = ⟨𝐶, 𝐷⟩ → [⟨u, 𝑡⟩] ∼ = [⟨𝐶, 𝐷⟩] ∼ )
25	24	eqeq2d 2048	. . . . . . . . 9 ⊢ (⟨u, 𝑡⟩ = ⟨𝐶, 𝐷⟩ → ([⟨𝐶, 𝐷⟩] ∼ = [⟨u, 𝑡⟩] ∼ ↔ [⟨𝐶, 𝐷⟩] ∼ = [⟨𝐶, 𝐷⟩] ∼ ))
26	25	anbi2d 437	. . . . . . . 8 ⊢ (⟨u, 𝑡⟩ = ⟨𝐶, 𝐷⟩ → (([⟨A, B⟩] ∼ = [⟨w, v⟩] ∼ ∧ [⟨𝐶, 𝐷⟩] ∼ = [⟨u, 𝑡⟩] ∼ ) ↔ ([⟨A, B⟩] ∼ = [⟨w, v⟩] ∼ ∧ [⟨𝐶, 𝐷⟩] ∼ = [⟨𝐶, 𝐷⟩] ∼ )))
27		oveq2 5463	. . . . . . . . . 10 ⊢ (⟨u, 𝑡⟩ = ⟨𝐶, 𝐷⟩ → (⟨w, v⟩ + ⟨u, 𝑡⟩) = (⟨w, v⟩ + ⟨𝐶, 𝐷⟩))
28	27	eceq1d 6078	. . . . . . . . 9 ⊢ (⟨u, 𝑡⟩ = ⟨𝐶, 𝐷⟩ → [(⟨w, v⟩ + ⟨u, 𝑡⟩)] ∼ = [(⟨w, v⟩ + ⟨𝐶, 𝐷⟩)] ∼ )
29	28	eqeq2d 2048	. . . . . . . 8 ⊢ (⟨u, 𝑡⟩ = ⟨𝐶, 𝐷⟩ → ([(⟨A, B⟩ + ⟨𝐶, 𝐷⟩)] ∼ = [(⟨w, v⟩ + ⟨u, 𝑡⟩)] ∼ ↔ [(⟨A, B⟩ + ⟨𝐶, 𝐷⟩)] ∼ = [(⟨w, v⟩ + ⟨𝐶, 𝐷⟩)] ∼ ))
30	26, 29	anbi12d 442	. . . . . . 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 2636	. . . . 5 ⊢ ((𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆) → ((([⟨A, B⟩] ∼ = [⟨w, v⟩] ∼ ∧ [⟨𝐶, 𝐷⟩] ∼ = [⟨𝐶, 𝐷⟩] ∼ ) ∧ [(⟨A, B⟩ + ⟨𝐶, 𝐷⟩)] ∼ = [(⟨w, v⟩ + ⟨𝐶, 𝐷⟩)] ∼ ) → ∃u∃𝑡(([⟨A, B⟩] ∼ = [⟨w, v⟩] ∼ ∧ [⟨𝐶, 𝐷⟩] ∼ = [⟨u, 𝑡⟩] ∼ ) ∧ [(⟨A, B⟩ + ⟨𝐶, 𝐷⟩)] ∼ = [(⟨w, v⟩ + ⟨u, 𝑡⟩)] ∼ )))
33	32	2eximdv 1759	. . . 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 389	. . 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 408	. 2 ⊢ (((A ∈ 𝑆 ∧ B ∈ 𝑆) ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) → ∃w∃v∃u∃𝑡(([⟨A, B⟩] ∼ = [⟨w, v⟩] ∼ ∧ [⟨𝐶, 𝐷⟩] ∼ = [⟨u, 𝑡⟩] ∼ ) ∧ [(⟨A, B⟩ + ⟨𝐶, 𝐷⟩)] ∼ = [(⟨w, v⟩ + ⟨u, 𝑡⟩)] ∼ ))
36		ecexg 6046	. . . 4 ⊢ ( ∼ ∈ V → [(⟨A, B⟩ + ⟨𝐶, 𝐷⟩)] ∼ ∈ V)
37	2, 36	ax-mp 7	. . 3 ⊢ [(⟨A, B⟩ + ⟨𝐶, 𝐷⟩)] ∼ ∈ V
38		eqeq1 2043	. . . . . . . 8 ⊢ (x = [⟨A, B⟩] ∼ → (x = [⟨w, v⟩] ∼ ↔ [⟨A, B⟩] ∼ = [⟨w, v⟩] ∼ ))
39		eqeq1 2043	. . . . . . . 8 ⊢ (y = [⟨𝐶, 𝐷⟩] ∼ → (y = [⟨u, 𝑡⟩] ∼ ↔ [⟨𝐶, 𝐷⟩] ∼ = [⟨u, 𝑡⟩] ∼ ))
40	38, 39	bi2anan9 538	. . . . . . 7 ⊢ ((x = [⟨A, B⟩] ∼ ∧ y = [⟨𝐶, 𝐷⟩] ∼ ) → ((x = [⟨w, v⟩] ∼ ∧ y = [⟨u, 𝑡⟩] ∼ ) ↔ ([⟨A, B⟩] ∼ = [⟨w, v⟩] ∼ ∧ [⟨𝐶, 𝐷⟩] ∼ = [⟨u, 𝑡⟩] ∼ )))
41		eqeq1 2043	. . . . . . 7 ⊢ (z = [(⟨A, B⟩ + ⟨𝐶, 𝐷⟩)] ∼ → (z = [(⟨w, v⟩ + ⟨u, 𝑡⟩)] ∼ ↔ [(⟨A, B⟩ + ⟨𝐶, 𝐷⟩)] ∼ = [(⟨w, v⟩ + ⟨u, 𝑡⟩)] ∼ ))
42	40, 41	bi2anan9 538	. . . . . 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 1098	. . . . 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 1747	. . . 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 6145	. . . 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 5564	. . 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 1220	. 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 884   = wceq 1242  ∃wex 1378   ∈ wcel 1390  Vcvv 2551  ⟨cop 3370   class class class wbr 3755   × cxp 4286  (class class class)co 5455  {coprab 5456   Er wer 6039  [cec 6040   / cqs 6041

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 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bnd 1396  ax-4 1397  ax-13 1401  ax-14 1402  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019  ax-sep 3866  ax-pow 3918  ax-pr 3935  ax-un 4136

This theorem depends on definitions:  df-bi 110  df-3an 886  df-tru 1245  df-nf 1347  df-sb 1643  df-eu 1900  df-mo 1901  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-ral 2305  df-rex 2306  df-v 2553  df-sbc 2759  df-un 2916  df-in 2918  df-ss 2925  df-pw 3353  df-sn 3373  df-pr 3374  df-op 3376  df-uni 3572  df-br 3756  df-opab 3810  df-id 4021  df-xp 4294  df-rel 4295  df-cnv 4296  df-co 4297  df-dm 4298  df-rn 4299  df-res 4300  df-ima 4301  df-iota 4810  df-fun 4847  df-fv 4853  df-ov 5458  df-oprab 5459  df-er 6042  df-ec 6044  df-qs 6048

This theorem is referenced by:  oviec  6148