Theorem ovi3 5579

Description: The value of an operation class abstraction. Special case. (Contributed by NM, 28-May-1995.) (Revised by Mario Carneiro, 29-Dec-2014.)

Hypotheses

Ref	Expression
ovi3.1	⊢ (((A ∈ 𝐻 ∧ B ∈ 𝐻) ∧ (𝐶 ∈ 𝐻 ∧ 𝐷 ∈ 𝐻)) → 𝑆 ∈ (𝐻 × 𝐻))
ovi3.2	⊢ (((w = A ∧ v = B) ∧ (u = 𝐶 ∧ f = 𝐷)) → 𝑅 = 𝑆)
ovi3.3	⊢ 𝐹 = {⟨⟨x, y⟩, z⟩ ∣ ((x ∈ (𝐻 × 𝐻) ∧ y ∈ (𝐻 × 𝐻)) ∧ ∃w∃v∃u∃f((x = ⟨w, v⟩ ∧ y = ⟨u, f⟩) ∧ z = 𝑅))}

Assertion

Ref	Expression
ovi3	⊢ (((A ∈ 𝐻 ∧ B ∈ 𝐻) ∧ (𝐶 ∈ 𝐻 ∧ 𝐷 ∈ 𝐻)) → (⟨A, B⟩𝐹⟨𝐶, 𝐷⟩) = 𝑆)

Distinct variable groups:   u,f,v,w,x,y,z,A   B,f,u,v,w,x,y,z   x,𝑅,y,z   𝐶,f,u,v,w,y,z   𝐷,f,u,v,w,y,z   f,𝐻,u,v,w,x,y,z   𝑆,f,u,v,w,z

Allowed substitution hints:   𝐶(x)   𝐷(x)   𝑅(w,v,u,f)   𝑆(x,y)   𝐹(x,y,z,w,v,u,f)

Proof of Theorem ovi3

Step	Hyp	Ref	Expression
1		ovi3.1	. . . 4 ⊢ (((A ∈ 𝐻 ∧ B ∈ 𝐻) ∧ (𝐶 ∈ 𝐻 ∧ 𝐷 ∈ 𝐻)) → 𝑆 ∈ (𝐻 × 𝐻))
2		elex 2560	. . . 4 ⊢ (𝑆 ∈ (𝐻 × 𝐻) → 𝑆 ∈ V)
3	1, 2	syl 14	. . 3 ⊢ (((A ∈ 𝐻 ∧ B ∈ 𝐻) ∧ (𝐶 ∈ 𝐻 ∧ 𝐷 ∈ 𝐻)) → 𝑆 ∈ V)
4		isset 2555	. . 3 ⊢ (𝑆 ∈ V ↔ ∃z z = 𝑆)
5	3, 4	sylib 127	. 2 ⊢ (((A ∈ 𝐻 ∧ B ∈ 𝐻) ∧ (𝐶 ∈ 𝐻 ∧ 𝐷 ∈ 𝐻)) → ∃z z = 𝑆)
6		nfv 1418	. . 3 ⊢ Ⅎz((A ∈ 𝐻 ∧ B ∈ 𝐻) ∧ (𝐶 ∈ 𝐻 ∧ 𝐷 ∈ 𝐻))
7		nfcv 2175	. . . . 5 ⊢ Ⅎz⟨A, B⟩
8		ovi3.3	. . . . . 6 ⊢ 𝐹 = {⟨⟨x, y⟩, z⟩ ∣ ((x ∈ (𝐻 × 𝐻) ∧ y ∈ (𝐻 × 𝐻)) ∧ ∃w∃v∃u∃f((x = ⟨w, v⟩ ∧ y = ⟨u, f⟩) ∧ z = 𝑅))}
9		nfoprab3 5498	. . . . . 6 ⊢ Ⅎz{⟨⟨x, y⟩, z⟩ ∣ ((x ∈ (𝐻 × 𝐻) ∧ y ∈ (𝐻 × 𝐻)) ∧ ∃w∃v∃u∃f((x = ⟨w, v⟩ ∧ y = ⟨u, f⟩) ∧ z = 𝑅))}
10	8, 9	nfcxfr 2172	. . . . 5 ⊢ Ⅎz𝐹
11		nfcv 2175	. . . . 5 ⊢ Ⅎz⟨𝐶, 𝐷⟩
12	7, 10, 11	nfov 5478	. . . 4 ⊢ Ⅎz(⟨A, B⟩𝐹⟨𝐶, 𝐷⟩)
13	12	nfeq1 2184	. . 3 ⊢ Ⅎz(⟨A, B⟩𝐹⟨𝐶, 𝐷⟩) = 𝑆
14		ovi3.2	. . . . . . 7 ⊢ (((w = A ∧ v = B) ∧ (u = 𝐶 ∧ f = 𝐷)) → 𝑅 = 𝑆)
15	14	eqeq2d 2048	. . . . . 6 ⊢ (((w = A ∧ v = B) ∧ (u = 𝐶 ∧ f = 𝐷)) → (z = 𝑅 ↔ z = 𝑆))
16	15	copsex4g 3975	. . . . 5 ⊢ (((A ∈ 𝐻 ∧ B ∈ 𝐻) ∧ (𝐶 ∈ 𝐻 ∧ 𝐷 ∈ 𝐻)) → (∃w∃v∃u∃f((⟨A, B⟩ = ⟨w, v⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨u, f⟩) ∧ z = 𝑅) ↔ z = 𝑆))
17		opelxpi 4319	. . . . . 6 ⊢ ((A ∈ 𝐻 ∧ B ∈ 𝐻) → ⟨A, B⟩ ∈ (𝐻 × 𝐻))
18		opelxpi 4319	. . . . . 6 ⊢ ((𝐶 ∈ 𝐻 ∧ 𝐷 ∈ 𝐻) → ⟨𝐶, 𝐷⟩ ∈ (𝐻 × 𝐻))
19		nfcv 2175	. . . . . . 7 ⊢ Ⅎx⟨A, B⟩
20		nfcv 2175	. . . . . . 7 ⊢ Ⅎy⟨A, B⟩
21		nfcv 2175	. . . . . . 7 ⊢ Ⅎy⟨𝐶, 𝐷⟩
22		nfv 1418	. . . . . . . 8 ⊢ Ⅎx∃w∃v∃u∃f((⟨A, B⟩ = ⟨w, v⟩ ∧ y = ⟨u, f⟩) ∧ z = 𝑅)
23		nfoprab1 5496	. . . . . . . . . . 11 ⊢ Ⅎx{⟨⟨x, y⟩, z⟩ ∣ ((x ∈ (𝐻 × 𝐻) ∧ y ∈ (𝐻 × 𝐻)) ∧ ∃w∃v∃u∃f((x = ⟨w, v⟩ ∧ y = ⟨u, f⟩) ∧ z = 𝑅))}
24	8, 23	nfcxfr 2172	. . . . . . . . . 10 ⊢ Ⅎx𝐹
25		nfcv 2175	. . . . . . . . . 10 ⊢ Ⅎxy
26	19, 24, 25	nfov 5478	. . . . . . . . 9 ⊢ Ⅎx(⟨A, B⟩𝐹y)
27	26	nfeq1 2184	. . . . . . . 8 ⊢ Ⅎx(⟨A, B⟩𝐹y) = z
28	22, 27	nfim 1461	. . . . . . 7 ⊢ Ⅎx(∃w∃v∃u∃f((⟨A, B⟩ = ⟨w, v⟩ ∧ y = ⟨u, f⟩) ∧ z = 𝑅) → (⟨A, B⟩𝐹y) = z)
29		nfv 1418	. . . . . . . 8 ⊢ Ⅎy∃w∃v∃u∃f((⟨A, B⟩ = ⟨w, v⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨u, f⟩) ∧ z = 𝑅)
30		nfoprab2 5497	. . . . . . . . . . 11 ⊢ Ⅎy{⟨⟨x, y⟩, z⟩ ∣ ((x ∈ (𝐻 × 𝐻) ∧ y ∈ (𝐻 × 𝐻)) ∧ ∃w∃v∃u∃f((x = ⟨w, v⟩ ∧ y = ⟨u, f⟩) ∧ z = 𝑅))}
31	8, 30	nfcxfr 2172	. . . . . . . . . 10 ⊢ Ⅎy𝐹
32	20, 31, 21	nfov 5478	. . . . . . . . 9 ⊢ Ⅎy(⟨A, B⟩𝐹⟨𝐶, 𝐷⟩)
33	32	nfeq1 2184	. . . . . . . 8 ⊢ Ⅎy(⟨A, B⟩𝐹⟨𝐶, 𝐷⟩) = z
34	29, 33	nfim 1461	. . . . . . 7 ⊢ Ⅎy(∃w∃v∃u∃f((⟨A, B⟩ = ⟨w, v⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨u, f⟩) ∧ z = 𝑅) → (⟨A, B⟩𝐹⟨𝐶, 𝐷⟩) = z)
35		eqeq1 2043	. . . . . . . . . . 11 ⊢ (x = ⟨A, B⟩ → (x = ⟨w, v⟩ ↔ ⟨A, B⟩ = ⟨w, v⟩))
36	35	anbi1d 438	. . . . . . . . . 10 ⊢ (x = ⟨A, B⟩ → ((x = ⟨w, v⟩ ∧ y = ⟨u, f⟩) ↔ (⟨A, B⟩ = ⟨w, v⟩ ∧ y = ⟨u, f⟩)))
37	36	anbi1d 438	. . . . . . . . 9 ⊢ (x = ⟨A, B⟩ → (((x = ⟨w, v⟩ ∧ y = ⟨u, f⟩) ∧ z = 𝑅) ↔ ((⟨A, B⟩ = ⟨w, v⟩ ∧ y = ⟨u, f⟩) ∧ z = 𝑅)))
38	37	4exbidv 1747	. . . . . . . 8 ⊢ (x = ⟨A, B⟩ → (∃w∃v∃u∃f((x = ⟨w, v⟩ ∧ y = ⟨u, f⟩) ∧ z = 𝑅) ↔ ∃w∃v∃u∃f((⟨A, B⟩ = ⟨w, v⟩ ∧ y = ⟨u, f⟩) ∧ z = 𝑅)))
39		oveq1 5462	. . . . . . . . 9 ⊢ (x = ⟨A, B⟩ → (x𝐹y) = (⟨A, B⟩𝐹y))
40	39	eqeq1d 2045	. . . . . . . 8 ⊢ (x = ⟨A, B⟩ → ((x𝐹y) = z ↔ (⟨A, B⟩𝐹y) = z))
41	38, 40	imbi12d 223	. . . . . . 7 ⊢ (x = ⟨A, B⟩ → ((∃w∃v∃u∃f((x = ⟨w, v⟩ ∧ y = ⟨u, f⟩) ∧ z = 𝑅) → (x𝐹y) = z) ↔ (∃w∃v∃u∃f((⟨A, B⟩ = ⟨w, v⟩ ∧ y = ⟨u, f⟩) ∧ z = 𝑅) → (⟨A, B⟩𝐹y) = z)))
42		eqeq1 2043	. . . . . . . . . . 11 ⊢ (y = ⟨𝐶, 𝐷⟩ → (y = ⟨u, f⟩ ↔ ⟨𝐶, 𝐷⟩ = ⟨u, f⟩))
43	42	anbi2d 437	. . . . . . . . . 10 ⊢ (y = ⟨𝐶, 𝐷⟩ → ((⟨A, B⟩ = ⟨w, v⟩ ∧ y = ⟨u, f⟩) ↔ (⟨A, B⟩ = ⟨w, v⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨u, f⟩)))
44	43	anbi1d 438	. . . . . . . . 9 ⊢ (y = ⟨𝐶, 𝐷⟩ → (((⟨A, B⟩ = ⟨w, v⟩ ∧ y = ⟨u, f⟩) ∧ z = 𝑅) ↔ ((⟨A, B⟩ = ⟨w, v⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨u, f⟩) ∧ z = 𝑅)))
45	44	4exbidv 1747	. . . . . . . 8 ⊢ (y = ⟨𝐶, 𝐷⟩ → (∃w∃v∃u∃f((⟨A, B⟩ = ⟨w, v⟩ ∧ y = ⟨u, f⟩) ∧ z = 𝑅) ↔ ∃w∃v∃u∃f((⟨A, B⟩ = ⟨w, v⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨u, f⟩) ∧ z = 𝑅)))
46		oveq2 5463	. . . . . . . . 9 ⊢ (y = ⟨𝐶, 𝐷⟩ → (⟨A, B⟩𝐹y) = (⟨A, B⟩𝐹⟨𝐶, 𝐷⟩))
47	46	eqeq1d 2045	. . . . . . . 8 ⊢ (y = ⟨𝐶, 𝐷⟩ → ((⟨A, B⟩𝐹y) = z ↔ (⟨A, B⟩𝐹⟨𝐶, 𝐷⟩) = z))
48	45, 47	imbi12d 223	. . . . . . 7 ⊢ (y = ⟨𝐶, 𝐷⟩ → ((∃w∃v∃u∃f((⟨A, B⟩ = ⟨w, v⟩ ∧ y = ⟨u, f⟩) ∧ z = 𝑅) → (⟨A, B⟩𝐹y) = z) ↔ (∃w∃v∃u∃f((⟨A, B⟩ = ⟨w, v⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨u, f⟩) ∧ z = 𝑅) → (⟨A, B⟩𝐹⟨𝐶, 𝐷⟩) = z)))
49		moeq 2710	. . . . . . . . . . . 12 ⊢ ∃*z z = 𝑅
50	49	mosubop 4349	. . . . . . . . . . 11 ⊢ ∃*z∃u∃f(y = ⟨u, f⟩ ∧ z = 𝑅)
51	50	mosubop 4349	. . . . . . . . . 10 ⊢ ∃*z∃w∃v(x = ⟨w, v⟩ ∧ ∃u∃f(y = ⟨u, f⟩ ∧ z = 𝑅))
52		anass 381	. . . . . . . . . . . . . 14 ⊢ (((x = ⟨w, v⟩ ∧ y = ⟨u, f⟩) ∧ z = 𝑅) ↔ (x = ⟨w, v⟩ ∧ (y = ⟨u, f⟩ ∧ z = 𝑅)))
53	52	2exbii 1494	. . . . . . . . . . . . 13 ⊢ (∃u∃f((x = ⟨w, v⟩ ∧ y = ⟨u, f⟩) ∧ z = 𝑅) ↔ ∃u∃f(x = ⟨w, v⟩ ∧ (y = ⟨u, f⟩ ∧ z = 𝑅)))
54		19.42vv 1785	. . . . . . . . . . . . 13 ⊢ (∃u∃f(x = ⟨w, v⟩ ∧ (y = ⟨u, f⟩ ∧ z = 𝑅)) ↔ (x = ⟨w, v⟩ ∧ ∃u∃f(y = ⟨u, f⟩ ∧ z = 𝑅)))
55	53, 54	bitri 173	. . . . . . . . . . . 12 ⊢ (∃u∃f((x = ⟨w, v⟩ ∧ y = ⟨u, f⟩) ∧ z = 𝑅) ↔ (x = ⟨w, v⟩ ∧ ∃u∃f(y = ⟨u, f⟩ ∧ z = 𝑅)))
56	55	2exbii 1494	. . . . . . . . . . 11 ⊢ (∃w∃v∃u∃f((x = ⟨w, v⟩ ∧ y = ⟨u, f⟩) ∧ z = 𝑅) ↔ ∃w∃v(x = ⟨w, v⟩ ∧ ∃u∃f(y = ⟨u, f⟩ ∧ z = 𝑅)))
57	56	mobii 1934	. . . . . . . . . 10 ⊢ (∃*z∃w∃v∃u∃f((x = ⟨w, v⟩ ∧ y = ⟨u, f⟩) ∧ z = 𝑅) ↔ ∃*z∃w∃v(x = ⟨w, v⟩ ∧ ∃u∃f(y = ⟨u, f⟩ ∧ z = 𝑅)))
58	51, 57	mpbir 134	. . . . . . . . 9 ⊢ ∃*z∃w∃v∃u∃f((x = ⟨w, v⟩ ∧ y = ⟨u, f⟩) ∧ z = 𝑅)
59	58	a1i 9	. . . . . . . 8 ⊢ ((x ∈ (𝐻 × 𝐻) ∧ y ∈ (𝐻 × 𝐻)) → ∃*z∃w∃v∃u∃f((x = ⟨w, v⟩ ∧ y = ⟨u, f⟩) ∧ z = 𝑅))
60	59, 8	ovidi 5561	. . . . . . 7 ⊢ ((x ∈ (𝐻 × 𝐻) ∧ y ∈ (𝐻 × 𝐻)) → (∃w∃v∃u∃f((x = ⟨w, v⟩ ∧ y = ⟨u, f⟩) ∧ z = 𝑅) → (x𝐹y) = z))
61	19, 20, 21, 28, 34, 41, 48, 60	vtocl2gaf 2614	. . . . . 6 ⊢ ((⟨A, B⟩ ∈ (𝐻 × 𝐻) ∧ ⟨𝐶, 𝐷⟩ ∈ (𝐻 × 𝐻)) → (∃w∃v∃u∃f((⟨A, B⟩ = ⟨w, v⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨u, f⟩) ∧ z = 𝑅) → (⟨A, B⟩𝐹⟨𝐶, 𝐷⟩) = z))
62	17, 18, 61	syl2an 273	. . . . 5 ⊢ (((A ∈ 𝐻 ∧ B ∈ 𝐻) ∧ (𝐶 ∈ 𝐻 ∧ 𝐷 ∈ 𝐻)) → (∃w∃v∃u∃f((⟨A, B⟩ = ⟨w, v⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨u, f⟩) ∧ z = 𝑅) → (⟨A, B⟩𝐹⟨𝐶, 𝐷⟩) = z))
63	16, 62	sylbird 159	. . . 4 ⊢ (((A ∈ 𝐻 ∧ B ∈ 𝐻) ∧ (𝐶 ∈ 𝐻 ∧ 𝐷 ∈ 𝐻)) → (z = 𝑆 → (⟨A, B⟩𝐹⟨𝐶, 𝐷⟩) = z))
64		eqeq2 2046	. . . 4 ⊢ (z = 𝑆 → ((⟨A, B⟩𝐹⟨𝐶, 𝐷⟩) = z ↔ (⟨A, B⟩𝐹⟨𝐶, 𝐷⟩) = 𝑆))
65	63, 64	mpbidi 140	. . 3 ⊢ (((A ∈ 𝐻 ∧ B ∈ 𝐻) ∧ (𝐶 ∈ 𝐻 ∧ 𝐷 ∈ 𝐻)) → (z = 𝑆 → (⟨A, B⟩𝐹⟨𝐶, 𝐷⟩) = 𝑆))
66	6, 13, 65	exlimd 1485	. 2 ⊢ (((A ∈ 𝐻 ∧ B ∈ 𝐻) ∧ (𝐶 ∈ 𝐻 ∧ 𝐷 ∈ 𝐻)) → (∃z z = 𝑆 → (⟨A, B⟩𝐹⟨𝐶, 𝐷⟩) = 𝑆))
67	5, 66	mpd 13	1 ⊢ (((A ∈ 𝐻 ∧ B ∈ 𝐻) ∧ (𝐶 ∈ 𝐻 ∧ 𝐷 ∈ 𝐻)) → (⟨A, B⟩𝐹⟨𝐶, 𝐷⟩) = 𝑆)

Syntax hints:   → wi 4   ∧ wa 97   = wceq 1242  ∃wex 1378   ∈ wcel 1390  ∃*wmo 1898  Vcvv 2551  ⟨cop 3370   × cxp 4286  (class class class)co 5455  {coprab 5456

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-in1 544  ax-in2 545  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-bndl 1396  ax-4 1397  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-setind 4220

This theorem depends on definitions:  df-bi 110  df-3an 886  df-tru 1245  df-fal 1248  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-ne 2203  df-ral 2305  df-rex 2306  df-v 2553  df-sbc 2759  df-dif 2914  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-iota 4810  df-fun 4847  df-fv 4853  df-ov 5458  df-oprab 5459

This theorem is referenced by:  oviec  6148  addcnsr  6731  mulcnsr  6732