ov6g

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

	Ref	Expression
Hypotheses	ov6g.1	$⊢ ⟨x, y⟩ = ⟨A, B⟩ \to R = S$
	ov6g.2	$⊢ F = \{⟨⟨x, y⟩, z⟩ \| (⟨x, y⟩ \in C \land z = R)\}$
Assertion	ov6g	$⊢ ((A \in G \land B \in H \land ⟨A, B⟩ \in C) \land S \in J) \to A F B = S$

Proof

Step	Hyp	Ref	Expression
1		ov6g.1	$⊢ ⟨x, y⟩ = ⟨A, B⟩ \to R = S$
2		ov6g.2	$⊢ F = \{⟨⟨x, y⟩, z⟩ \| (⟨x, y⟩ \in C \land z = R)\}$
3		df-ov	$⊢ A F B = F (⟨A, B⟩)$
4		eqid	$⊢ S = S$
5		biidd	$⊢ (x = A \land y = B) \to (S = S \leftrightarrow S = S)$
6	5	copsex2g	$⊢ (A \in G \land B \in H) \to (\exists x \exists y (⟨A, B⟩ = ⟨x, y⟩ \land S = S) \leftrightarrow S = S)$
7	4 6	mpbiri	$⊢ (A \in G \land B \in H) \to \exists x \exists y (⟨A, B⟩ = ⟨x, y⟩ \land S = S)$
8	7	3adant3	$⊢ (A \in G \land B \in H \land ⟨A, B⟩ \in C) \to \exists x \exists y (⟨A, B⟩ = ⟨x, y⟩ \land S = S)$
9	8	adantr	$⊢ ((A \in G \land B \in H \land ⟨A, B⟩ \in C) \land S \in J) \to \exists x \exists y (⟨A, B⟩ = ⟨x, y⟩ \land S = S)$
10		eqeq1	$⊢ w = ⟨A, B⟩ \to (w = ⟨x, y⟩ \leftrightarrow ⟨A, B⟩ = ⟨x, y⟩)$
11	10	anbi1d	$⊢ w = ⟨A, B⟩ \to ((w = ⟨x, y⟩ \land z = R) \leftrightarrow (⟨A, B⟩ = ⟨x, y⟩ \land z = R))$
12	1	eqeq2d	$⊢ ⟨x, y⟩ = ⟨A, B⟩ \to (z = R \leftrightarrow z = S)$
13	12	eqcoms	$⊢ ⟨A, B⟩ = ⟨x, y⟩ \to (z = R \leftrightarrow z = S)$
14	13	pm5.32i	$⊢ (⟨A, B⟩ = ⟨x, y⟩ \land z = R) \leftrightarrow (⟨A, B⟩ = ⟨x, y⟩ \land z = S)$
15	11 14	bitrdi	$⊢ w = ⟨A, B⟩ \to ((w = ⟨x, y⟩ \land z = R) \leftrightarrow (⟨A, B⟩ = ⟨x, y⟩ \land z = S))$
16	15	2exbidv	$⊢ w = ⟨A, B⟩ \to (\exists x \exists y (w = ⟨x, y⟩ \land z = R) \leftrightarrow \exists x \exists y (⟨A, B⟩ = ⟨x, y⟩ \land z = S))$
17		eqeq1	$⊢ z = S \to (z = S \leftrightarrow S = S)$
18	17	anbi2d	$⊢ z = S \to ((⟨A, B⟩ = ⟨x, y⟩ \land z = S) \leftrightarrow (⟨A, B⟩ = ⟨x, y⟩ \land S = S))$
19	18	2exbidv	$⊢ z = S \to (\exists x \exists y (⟨A, B⟩ = ⟨x, y⟩ \land z = S) \leftrightarrow \exists x \exists y (⟨A, B⟩ = ⟨x, y⟩ \land S = S))$
20		moeq	$⊢ \exists^{*} z z = R$
21	20	mosubop	$⊢ \exists^{*} z \exists x \exists y (w = ⟨x, y⟩ \land z = R)$
22	21	a1i	$⊢ w \in C \to \exists^{*} z \exists x \exists y (w = ⟨x, y⟩ \land z = R)$
23		dfoprab2	$⊢ \{⟨⟨x, y⟩, z⟩ \| (⟨x, y⟩ \in C \land z = R)\} = \{⟨w, z⟩ \| \exists x \exists y (w = ⟨x, y⟩ \land (⟨x, y⟩ \in C \land z = R))\}$
24		eleq1	$⊢ w = ⟨x, y⟩ \to (w \in C \leftrightarrow ⟨x, y⟩ \in C)$
25	24	anbi1d	$⊢ w = ⟨x, y⟩ \to ((w \in C \land z = R) \leftrightarrow (⟨x, y⟩ \in C \land z = R))$
26	25	pm5.32i	$⊢ (w = ⟨x, y⟩ \land (w \in C \land z = R)) \leftrightarrow (w = ⟨x, y⟩ \land (⟨x, y⟩ \in C \land z = R))$
27		an12	$⊢ (w = ⟨x, y⟩ \land (w \in C \land z = R)) \leftrightarrow (w \in C \land (w = ⟨x, y⟩ \land z = R))$
28	26 27	bitr3i	$⊢ (w = ⟨x, y⟩ \land (⟨x, y⟩ \in C \land z = R)) \leftrightarrow (w \in C \land (w = ⟨x, y⟩ \land z = R))$
29	28	2exbii	$⊢ \exists x \exists y (w = ⟨x, y⟩ \land (⟨x, y⟩ \in C \land z = R)) \leftrightarrow \exists x \exists y (w \in C \land (w = ⟨x, y⟩ \land z = R))$
30		19.42vv	$⊢ \exists x \exists y (w \in C \land (w = ⟨x, y⟩ \land z = R)) \leftrightarrow (w \in C \land \exists x \exists y (w = ⟨x, y⟩ \land z = R))$
31	29 30	bitri	$⊢ \exists x \exists y (w = ⟨x, y⟩ \land (⟨x, y⟩ \in C \land z = R)) \leftrightarrow (w \in C \land \exists x \exists y (w = ⟨x, y⟩ \land z = R))$
32	31	opabbii	$⊢ \{⟨w, z⟩ \| \exists x \exists y (w = ⟨x, y⟩ \land (⟨x, y⟩ \in C \land z = R))\} = \{⟨w, z⟩ \| (w \in C \land \exists x \exists y (w = ⟨x, y⟩ \land z = R))\}$
33	2 23 32	3eqtri	$⊢ F = \{⟨w, z⟩ \| (w \in C \land \exists x \exists y (w = ⟨x, y⟩ \land z = R))\}$
34	16 19 22 33	fvopab3ig	$⊢ (⟨A, B⟩ \in C \land S \in J) \to (\exists x \exists y (⟨A, B⟩ = ⟨x, y⟩ \land S = S) \to F (⟨A, B⟩) = S)$
35	34	3ad2antl3	$⊢ ((A \in G \land B \in H \land ⟨A, B⟩ \in C) \land S \in J) \to (\exists x \exists y (⟨A, B⟩ = ⟨x, y⟩ \land S = S) \to F (⟨A, B⟩) = S)$
36	9 35	mpd	$⊢ ((A \in G \land B \in H \land ⟨A, B⟩ \in C) \land S \in J) \to F (⟨A, B⟩) = S$
37	3 36	eqtrid	$⊢ ((A \in G \land B \in H \land ⟨A, B⟩ \in C) \land S \in J) \to A F B = S$

Metamath Proof Explorer

Theorem ov6g

Proof