Theorem ov6g 5658

Description: The value of an operation class abstraction. Special case. (Contributed by NM, 13-Nov-2006.)

Hypotheses

Ref	Expression
ov6g.1	⊢ (⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝐵⟩ → 𝑅 = 𝑆)
ov6g.2	⊢ 𝐹 = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ (⟨𝑥, 𝑦⟩ ∈ 𝐶 ∧ 𝑧 = 𝑅)}

Assertion

Ref	Expression
ov6g	⊢ (((𝐴 ∈ 𝐺 ∧ 𝐵 ∈ 𝐻 ∧ ⟨𝐴, 𝐵⟩ ∈ 𝐶) ∧ 𝑆 ∈ 𝐽) → (𝐴𝐹𝐵) = 𝑆)

Distinct variable groups:   𝑥,𝑦,𝑧,𝐴   𝑥,𝐵,𝑦,𝑧   𝑥,𝐶,𝑦,𝑧   𝑧,𝑅   𝑥,𝑆,𝑦,𝑧

Allowed substitution hints:   𝑅(𝑥,𝑦)   𝐹(𝑥,𝑦,𝑧)   𝐺(𝑥,𝑦,𝑧)   𝐻(𝑥,𝑦,𝑧)   𝐽(𝑥,𝑦,𝑧)

Proof of Theorem ov6g

Dummy variable 𝑤 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-ov 5535	. 2 ⊢ (𝐴𝐹𝐵) = (𝐹‘⟨𝐴, 𝐵⟩)
2		eqid 2081	. . . . . 6 ⊢ 𝑆 = 𝑆
3		biidd 170	. . . . . . 7 ⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝑆 = 𝑆 ↔ 𝑆 = 𝑆))
4	3	copsex2g 4001	. . . . . 6 ⊢ ((𝐴 ∈ 𝐺 ∧ 𝐵 ∈ 𝐻) → (∃𝑥∃𝑦(⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝑆 = 𝑆) ↔ 𝑆 = 𝑆))
5	2, 4	mpbiri 166	. . . . 5 ⊢ ((𝐴 ∈ 𝐺 ∧ 𝐵 ∈ 𝐻) → ∃𝑥∃𝑦(⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝑆 = 𝑆))
6	5	3adant3 958	. . . 4 ⊢ ((𝐴 ∈ 𝐺 ∧ 𝐵 ∈ 𝐻 ∧ ⟨𝐴, 𝐵⟩ ∈ 𝐶) → ∃𝑥∃𝑦(⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝑆 = 𝑆))
7	6	adantr 270	. . 3 ⊢ (((𝐴 ∈ 𝐺 ∧ 𝐵 ∈ 𝐻 ∧ ⟨𝐴, 𝐵⟩ ∈ 𝐶) ∧ 𝑆 ∈ 𝐽) → ∃𝑥∃𝑦(⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝑆 = 𝑆))
8		eqeq1 2087	. . . . . . . 8 ⊢ (𝑤 = ⟨𝐴, 𝐵⟩ → (𝑤 = ⟨𝑥, 𝑦⟩ ↔ ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩))
9	8	anbi1d 452	. . . . . . 7 ⊢ (𝑤 = ⟨𝐴, 𝐵⟩ → ((𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝑧 = 𝑅) ↔ (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝑧 = 𝑅)))
10		ov6g.1	. . . . . . . . . 10 ⊢ (⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝐵⟩ → 𝑅 = 𝑆)
11	10	eqeq2d 2092	. . . . . . . . 9 ⊢ (⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝐵⟩ → (𝑧 = 𝑅 ↔ 𝑧 = 𝑆))
12	11	eqcoms 2084	. . . . . . . 8 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → (𝑧 = 𝑅 ↔ 𝑧 = 𝑆))
13	12	pm5.32i 441	. . . . . . 7 ⊢ ((⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝑧 = 𝑅) ↔ (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝑧 = 𝑆))
14	9, 13	syl6bb 194	. . . . . 6 ⊢ (𝑤 = ⟨𝐴, 𝐵⟩ → ((𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝑧 = 𝑅) ↔ (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝑧 = 𝑆)))
15	14	2exbidv 1789	. . . . 5 ⊢ (𝑤 = ⟨𝐴, 𝐵⟩ → (∃𝑥∃𝑦(𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝑧 = 𝑅) ↔ ∃𝑥∃𝑦(⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝑧 = 𝑆)))
16		eqeq1 2087	. . . . . . 7 ⊢ (𝑧 = 𝑆 → (𝑧 = 𝑆 ↔ 𝑆 = 𝑆))
17	16	anbi2d 451	. . . . . 6 ⊢ (𝑧 = 𝑆 → ((⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝑧 = 𝑆) ↔ (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝑆 = 𝑆)))
18	17	2exbidv 1789	. . . . 5 ⊢ (𝑧 = 𝑆 → (∃𝑥∃𝑦(⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝑧 = 𝑆) ↔ ∃𝑥∃𝑦(⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝑆 = 𝑆)))
19		moeq 2767	. . . . . . 7 ⊢ ∃*𝑧 𝑧 = 𝑅
20	19	mosubop 4424	. . . . . 6 ⊢ ∃*𝑧∃𝑥∃𝑦(𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝑧 = 𝑅)
21	20	a1i 9	. . . . 5 ⊢ (𝑤 ∈ 𝐶 → ∃*𝑧∃𝑥∃𝑦(𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝑧 = 𝑅))
22		ov6g.2	. . . . . 6 ⊢ 𝐹 = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ (⟨𝑥, 𝑦⟩ ∈ 𝐶 ∧ 𝑧 = 𝑅)}
23		dfoprab2 5572	. . . . . 6 ⊢ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ (⟨𝑥, 𝑦⟩ ∈ 𝐶 ∧ 𝑧 = 𝑅)} = {⟨𝑤, 𝑧⟩ ∣ ∃𝑥∃𝑦(𝑤 = ⟨𝑥, 𝑦⟩ ∧ (⟨𝑥, 𝑦⟩ ∈ 𝐶 ∧ 𝑧 = 𝑅))}
24		eleq1 2141	. . . . . . . . . . . 12 ⊢ (𝑤 = ⟨𝑥, 𝑦⟩ → (𝑤 ∈ 𝐶 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝐶))
25	24	anbi1d 452	. . . . . . . . . . 11 ⊢ (𝑤 = ⟨𝑥, 𝑦⟩ → ((𝑤 ∈ 𝐶 ∧ 𝑧 = 𝑅) ↔ (⟨𝑥, 𝑦⟩ ∈ 𝐶 ∧ 𝑧 = 𝑅)))
26	25	pm5.32i 441	. . . . . . . . . 10 ⊢ ((𝑤 = ⟨𝑥, 𝑦⟩ ∧ (𝑤 ∈ 𝐶 ∧ 𝑧 = 𝑅)) ↔ (𝑤 = ⟨𝑥, 𝑦⟩ ∧ (⟨𝑥, 𝑦⟩ ∈ 𝐶 ∧ 𝑧 = 𝑅)))
27		an12 525	. . . . . . . . . 10 ⊢ ((𝑤 = ⟨𝑥, 𝑦⟩ ∧ (𝑤 ∈ 𝐶 ∧ 𝑧 = 𝑅)) ↔ (𝑤 ∈ 𝐶 ∧ (𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝑧 = 𝑅)))
28	26, 27	bitr3i 184	. . . . . . . . 9 ⊢ ((𝑤 = ⟨𝑥, 𝑦⟩ ∧ (⟨𝑥, 𝑦⟩ ∈ 𝐶 ∧ 𝑧 = 𝑅)) ↔ (𝑤 ∈ 𝐶 ∧ (𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝑧 = 𝑅)))
29	28	2exbii 1537	. . . . . . . 8 ⊢ (∃𝑥∃𝑦(𝑤 = ⟨𝑥, 𝑦⟩ ∧ (⟨𝑥, 𝑦⟩ ∈ 𝐶 ∧ 𝑧 = 𝑅)) ↔ ∃𝑥∃𝑦(𝑤 ∈ 𝐶 ∧ (𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝑧 = 𝑅)))
30		19.42vv 1829	. . . . . . . 8 ⊢ (∃𝑥∃𝑦(𝑤 ∈ 𝐶 ∧ (𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝑧 = 𝑅)) ↔ (𝑤 ∈ 𝐶 ∧ ∃𝑥∃𝑦(𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝑧 = 𝑅)))
31	29, 30	bitri 182	. . . . . . 7 ⊢ (∃𝑥∃𝑦(𝑤 = ⟨𝑥, 𝑦⟩ ∧ (⟨𝑥, 𝑦⟩ ∈ 𝐶 ∧ 𝑧 = 𝑅)) ↔ (𝑤 ∈ 𝐶 ∧ ∃𝑥∃𝑦(𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝑧 = 𝑅)))
32	31	opabbii 3845	. . . . . 6 ⊢ {⟨𝑤, 𝑧⟩ ∣ ∃𝑥∃𝑦(𝑤 = ⟨𝑥, 𝑦⟩ ∧ (⟨𝑥, 𝑦⟩ ∈ 𝐶 ∧ 𝑧 = 𝑅))} = {⟨𝑤, 𝑧⟩ ∣ (𝑤 ∈ 𝐶 ∧ ∃𝑥∃𝑦(𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝑧 = 𝑅))}
33	22, 23, 32	3eqtri 2105	. . . . 5 ⊢ 𝐹 = {⟨𝑤, 𝑧⟩ ∣ (𝑤 ∈ 𝐶 ∧ ∃𝑥∃𝑦(𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝑧 = 𝑅))}
34	15, 18, 21, 33	fvopab3ig 5267	. . . 4 ⊢ ((⟨𝐴, 𝐵⟩ ∈ 𝐶 ∧ 𝑆 ∈ 𝐽) → (∃𝑥∃𝑦(⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝑆 = 𝑆) → (𝐹‘⟨𝐴, 𝐵⟩) = 𝑆))
35	34	3ad2antl3 1102	. . 3 ⊢ (((𝐴 ∈ 𝐺 ∧ 𝐵 ∈ 𝐻 ∧ ⟨𝐴, 𝐵⟩ ∈ 𝐶) ∧ 𝑆 ∈ 𝐽) → (∃𝑥∃𝑦(⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝑆 = 𝑆) → (𝐹‘⟨𝐴, 𝐵⟩) = 𝑆))
36	7, 35	mpd 13	. 2 ⊢ (((𝐴 ∈ 𝐺 ∧ 𝐵 ∈ 𝐻 ∧ ⟨𝐴, 𝐵⟩ ∈ 𝐶) ∧ 𝑆 ∈ 𝐽) → (𝐹‘⟨𝐴, 𝐵⟩) = 𝑆)
37	1, 36	syl5eq 2125	1 ⊢ (((𝐴 ∈ 𝐺 ∧ 𝐵 ∈ 𝐻 ∧ ⟨𝐴, 𝐵⟩ ∈ 𝐶) ∧ 𝑆 ∈ 𝐽) → (𝐴𝐹𝐵) = 𝑆)

Syntax hints:   → wi 4   ∧ wa 102   ↔ wb 103   ∧ w3a 919   = wceq 1284  ∃wex 1421   ∈ wcel 1433  ∃*wmo 1942  ⟨cop 3401  {copab 3838  ‘cfv 4922  (class class class)co 5532  {coprab 5533

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 662  ax-5 1376  ax-7 1377  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-8 1435  ax-10 1436  ax-11 1437  ax-i12 1438  ax-bndl 1439  ax-4 1440  ax-14 1445  ax-17 1459  ax-i9 1463  ax-ial 1467  ax-i5r 1468  ax-ext 2063  ax-sep 3896  ax-pow 3948  ax-pr 3964

This theorem depends on definitions:  df-bi 115  df-3an 921  df-tru 1287  df-nf 1390  df-sb 1686  df-eu 1944  df-mo 1945  df-clab 2068  df-cleq 2074  df-clel 2077  df-nfc 2208  df-ral 2353  df-rex 2354  df-v 2603  df-sbc 2816  df-un 2977  df-in 2979  df-ss 2986  df-pw 3384  df-sn 3404  df-pr 3405  df-op 3407  df-uni 3602  df-br 3786  df-opab 3840  df-id 4048  df-xp 4369  df-rel 4370  df-cnv 4371  df-co 4372  df-dm 4373  df-iota 4887  df-fun 4924  df-fv 4930  df-ov 5535  df-oprab 5536

This theorem is referenced by: (None)