ov3

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

	Ref	Expression
Hypotheses	ov3.1	$⊢ S \in V$
	ov3.2	$⊢ ((w = A \land v = B) \land (u = C \land f = D)) \to R = S$
	ov3.3	$⊢ F = \{⟨⟨x, y⟩, z⟩ \| ((x \in (H \times H) \land y \in (H \times H)) \land \exists w \exists v \exists u \exists f ((x = ⟨w, v⟩ \land y = ⟨u, f⟩) \land z = R))\}$
Assertion	ov3	$⊢ ((A \in H \land B \in H) \land (C \in H \land D \in H)) \to ⟨A, B⟩ F ⟨C, D⟩ = S$

Proof

Step	Hyp	Ref	Expression
1		ov3.1	$⊢ S \in V$
2		ov3.2	$⊢ ((w = A \land v = B) \land (u = C \land f = D)) \to R = S$
3		ov3.3	$⊢ F = \{⟨⟨x, y⟩, z⟩ \| ((x \in (H \times H) \land y \in (H \times H)) \land \exists w \exists v \exists u \exists f ((x = ⟨w, v⟩ \land y = ⟨u, f⟩) \land z = R))\}$
4	1	isseti	$⊢ \exists z z = S$
5		nfv	$⊢ Ⅎ z ((A \in H \land B \in H) \land (C \in H \land D \in H))$
6		nfcv	$⊢ \underline{Ⅎ} z ⟨A, B⟩$
7		nfoprab3	$⊢ \underline{Ⅎ} z \{⟨⟨x, y⟩, z⟩ \| ((x \in (H \times H) \land y \in (H \times H)) \land \exists w \exists v \exists u \exists f ((x = ⟨w, v⟩ \land y = ⟨u, f⟩) \land z = R))\}$
8	3 7	nfcxfr	$⊢ \underline{Ⅎ} z F$
9		nfcv	$⊢ \underline{Ⅎ} z ⟨C, D⟩$
10	6 8 9	nfov	$⊢ \underline{Ⅎ} z (⟨A, B⟩ F ⟨C, D⟩)$
11	10	nfeq1	$⊢ Ⅎ z ⟨A, B⟩ F ⟨C, D⟩ = S$
12	2	eqeq2d	$⊢ ((w = A \land v = B) \land (u = C \land f = D)) \to (z = R \leftrightarrow z = S)$
13	12	copsex4g	$⊢ ((A \in H \land B \in H) \land (C \in H \land D \in H)) \to (\exists w \exists v \exists u \exists f ((⟨A, B⟩ = ⟨w, v⟩ \land ⟨C, D⟩ = ⟨u, f⟩) \land z = R) \leftrightarrow z = S)$
14		opelxpi	$⊢ (A \in H \land B \in H) \to ⟨A, B⟩ \in (H \times H)$
15		opelxpi	$⊢ (C \in H \land D \in H) \to ⟨C, D⟩ \in (H \times H)$
16		nfcv	$⊢ \underline{Ⅎ} x ⟨A, B⟩$
17		nfcv	$⊢ \underline{Ⅎ} y ⟨A, B⟩$
18		nfcv	$⊢ \underline{Ⅎ} y ⟨C, D⟩$
19		nfv	$⊢ Ⅎ x \exists w \exists v \exists u \exists f ((⟨A, B⟩ = ⟨w, v⟩ \land y = ⟨u, f⟩) \land z = R)$
20		nfoprab1	$⊢ \underline{Ⅎ} x \{⟨⟨x, y⟩, z⟩ \| ((x \in (H \times H) \land y \in (H \times H)) \land \exists w \exists v \exists u \exists f ((x = ⟨w, v⟩ \land y = ⟨u, f⟩) \land z = R))\}$
21	3 20	nfcxfr	$⊢ \underline{Ⅎ} x F$
22		nfcv	$⊢ \underline{Ⅎ} x y$
23	16 21 22	nfov	$⊢ \underline{Ⅎ} x (⟨A, B⟩ F y)$
24	23	nfeq1	$⊢ Ⅎ x ⟨A, B⟩ F y = z$
25	19 24	nfim	$⊢ Ⅎ x (\exists w \exists v \exists u \exists f ((⟨A, B⟩ = ⟨w, v⟩ \land y = ⟨u, f⟩) \land z = R) \to ⟨A, B⟩ F y = z)$
26		nfv	$⊢ Ⅎ y \exists w \exists v \exists u \exists f ((⟨A, B⟩ = ⟨w, v⟩ \land ⟨C, D⟩ = ⟨u, f⟩) \land z = R)$
27		nfoprab2	$⊢ \underline{Ⅎ} y \{⟨⟨x, y⟩, z⟩ \| ((x \in (H \times H) \land y \in (H \times H)) \land \exists w \exists v \exists u \exists f ((x = ⟨w, v⟩ \land y = ⟨u, f⟩) \land z = R))\}$
28	3 27	nfcxfr	$⊢ \underline{Ⅎ} y F$
29	17 28 18	nfov	$⊢ \underline{Ⅎ} y (⟨A, B⟩ F ⟨C, D⟩)$
30	29	nfeq1	$⊢ Ⅎ y ⟨A, B⟩ F ⟨C, D⟩ = z$
31	26 30	nfim	$⊢ Ⅎ y (\exists w \exists v \exists u \exists f ((⟨A, B⟩ = ⟨w, v⟩ \land ⟨C, D⟩ = ⟨u, f⟩) \land z = R) \to ⟨A, B⟩ F ⟨C, D⟩ = z)$
32		eqeq1	$⊢ x = ⟨A, B⟩ \to (x = ⟨w, v⟩ \leftrightarrow ⟨A, B⟩ = ⟨w, v⟩)$
33	32	anbi1d	$⊢ x = ⟨A, B⟩ \to ((x = ⟨w, v⟩ \land y = ⟨u, f⟩) \leftrightarrow (⟨A, B⟩ = ⟨w, v⟩ \land y = ⟨u, f⟩))$
34	33	anbi1d	$⊢ x = ⟨A, B⟩ \to (((x = ⟨w, v⟩ \land y = ⟨u, f⟩) \land z = R) \leftrightarrow ((⟨A, B⟩ = ⟨w, v⟩ \land y = ⟨u, f⟩) \land z = R))$
35	34	4exbidv	$⊢ x = ⟨A, B⟩ \to (\exists w \exists v \exists u \exists f ((x = ⟨w, v⟩ \land y = ⟨u, f⟩) \land z = R) \leftrightarrow \exists w \exists v \exists u \exists f ((⟨A, B⟩ = ⟨w, v⟩ \land y = ⟨u, f⟩) \land z = R))$
36		oveq1	$⊢ x = ⟨A, B⟩ \to x F y = ⟨A, B⟩ F y$
37	36	eqeq1d	$⊢ x = ⟨A, B⟩ \to (x F y = z \leftrightarrow ⟨A, B⟩ F y = z)$
38	35 37	imbi12d	$⊢ x = ⟨A, B⟩ \to ((\exists w \exists v \exists u \exists f ((x = ⟨w, v⟩ \land y = ⟨u, f⟩) \land z = R) \to x F y = z) \leftrightarrow (\exists w \exists v \exists u \exists f ((⟨A, B⟩ = ⟨w, v⟩ \land y = ⟨u, f⟩) \land z = R) \to ⟨A, B⟩ F y = z))$
39		eqeq1	$⊢ y = ⟨C, D⟩ \to (y = ⟨u, f⟩ \leftrightarrow ⟨C, D⟩ = ⟨u, f⟩)$
40	39	anbi2d	$⊢ y = ⟨C, D⟩ \to ((⟨A, B⟩ = ⟨w, v⟩ \land y = ⟨u, f⟩) \leftrightarrow (⟨A, B⟩ = ⟨w, v⟩ \land ⟨C, D⟩ = ⟨u, f⟩))$
41	40	anbi1d	$⊢ y = ⟨C, D⟩ \to (((⟨A, B⟩ = ⟨w, v⟩ \land y = ⟨u, f⟩) \land z = R) \leftrightarrow ((⟨A, B⟩ = ⟨w, v⟩ \land ⟨C, D⟩ = ⟨u, f⟩) \land z = R))$
42	41	4exbidv	$⊢ y = ⟨C, D⟩ \to (\exists w \exists v \exists u \exists f ((⟨A, B⟩ = ⟨w, v⟩ \land y = ⟨u, f⟩) \land z = R) \leftrightarrow \exists w \exists v \exists u \exists f ((⟨A, B⟩ = ⟨w, v⟩ \land ⟨C, D⟩ = ⟨u, f⟩) \land z = R))$
43		oveq2	$⊢ y = ⟨C, D⟩ \to ⟨A, B⟩ F y = ⟨A, B⟩ F ⟨C, D⟩$
44	43	eqeq1d	$⊢ y = ⟨C, D⟩ \to (⟨A, B⟩ F y = z \leftrightarrow ⟨A, B⟩ F ⟨C, D⟩ = z)$
45	42 44	imbi12d	$⊢ y = ⟨C, D⟩ \to ((\exists w \exists v \exists u \exists f ((⟨A, B⟩ = ⟨w, v⟩ \land y = ⟨u, f⟩) \land z = R) \to ⟨A, B⟩ F y = z) \leftrightarrow (\exists w \exists v \exists u \exists f ((⟨A, B⟩ = ⟨w, v⟩ \land ⟨C, D⟩ = ⟨u, f⟩) \land z = R) \to ⟨A, B⟩ F ⟨C, D⟩ = z))$
46		moeq	$⊢ \exists^{*} z z = R$
47	46	mosubop	$⊢ \exists^{*} z \exists u \exists f (y = ⟨u, f⟩ \land z = R)$
48	47	mosubop	$⊢ \exists^{*} z \exists w \exists v (x = ⟨w, v⟩ \land \exists u \exists f (y = ⟨u, f⟩ \land z = R))$
49		anass	$⊢ ((x = ⟨w, v⟩ \land y = ⟨u, f⟩) \land z = R) \leftrightarrow (x = ⟨w, v⟩ \land (y = ⟨u, f⟩ \land z = R))$
50	49	2exbii	$⊢ \exists u \exists f ((x = ⟨w, v⟩ \land y = ⟨u, f⟩) \land z = R) \leftrightarrow \exists u \exists f (x = ⟨w, v⟩ \land (y = ⟨u, f⟩ \land z = R))$
51		19.42vv	$⊢ \exists u \exists f (x = ⟨w, v⟩ \land (y = ⟨u, f⟩ \land z = R)) \leftrightarrow (x = ⟨w, v⟩ \land \exists u \exists f (y = ⟨u, f⟩ \land z = R))$
52	50 51	bitri	$⊢ \exists u \exists f ((x = ⟨w, v⟩ \land y = ⟨u, f⟩) \land z = R) \leftrightarrow (x = ⟨w, v⟩ \land \exists u \exists f (y = ⟨u, f⟩ \land z = R))$
53	52	2exbii	$⊢ \exists w \exists v \exists u \exists f ((x = ⟨w, v⟩ \land y = ⟨u, f⟩) \land z = R) \leftrightarrow \exists w \exists v (x = ⟨w, v⟩ \land \exists u \exists f (y = ⟨u, f⟩ \land z = R))$
54	53	mobii	$⊢ \exists^{} z \exists w \exists v \exists u \exists f ((x = ⟨w, v⟩ \land y = ⟨u, f⟩) \land z = R) \leftrightarrow \exists^{} z \exists w \exists v (x = ⟨w, v⟩ \land \exists u \exists f (y = ⟨u, f⟩ \land z = R))$
55	48 54	mpbir	$⊢ \exists^{*} z \exists w \exists v \exists u \exists f ((x = ⟨w, v⟩ \land y = ⟨u, f⟩) \land z = R)$
56	55	a1i	$⊢ (x \in (H \times H) \land y \in (H \times H)) \to \exists^{*} z \exists w \exists v \exists u \exists f ((x = ⟨w, v⟩ \land y = ⟨u, f⟩) \land z = R)$
57	56 3	ovidi	$⊢ (x \in (H \times H) \land y \in (H \times H)) \to (\exists w \exists v \exists u \exists f ((x = ⟨w, v⟩ \land y = ⟨u, f⟩) \land z = R) \to x F y = z)$
58	16 17 18 25 31 38 45 57	vtocl2gaf	$⊢ (⟨A, B⟩ \in (H \times H) \land ⟨C, D⟩ \in (H \times H)) \to (\exists w \exists v \exists u \exists f ((⟨A, B⟩ = ⟨w, v⟩ \land ⟨C, D⟩ = ⟨u, f⟩) \land z = R) \to ⟨A, B⟩ F ⟨C, D⟩ = z)$
59	14 15 58	syl2an	$⊢ ((A \in H \land B \in H) \land (C \in H \land D \in H)) \to (\exists w \exists v \exists u \exists f ((⟨A, B⟩ = ⟨w, v⟩ \land ⟨C, D⟩ = ⟨u, f⟩) \land z = R) \to ⟨A, B⟩ F ⟨C, D⟩ = z)$
60	13 59	sylbird	$⊢ ((A \in H \land B \in H) \land (C \in H \land D \in H)) \to (z = S \to ⟨A, B⟩ F ⟨C, D⟩ = z)$
61		eqeq2	$⊢ z = S \to (⟨A, B⟩ F ⟨C, D⟩ = z \leftrightarrow ⟨A, B⟩ F ⟨C, D⟩ = S)$
62	60 61	mpbidi	$⊢ ((A \in H \land B \in H) \land (C \in H \land D \in H)) \to (z = S \to ⟨A, B⟩ F ⟨C, D⟩ = S)$
63	5 11 62	exlimd	$⊢ ((A \in H \land B \in H) \land (C \in H \land D \in H)) \to (\exists z z = S \to ⟨A, B⟩ F ⟨C, D⟩ = S)$
64	4 63	mpi	$⊢ ((A \in H \land B \in H) \land (C \in H \land D \in H)) \to ⟨A, B⟩ F ⟨C, D⟩ = S$

Metamath Proof Explorer

Theorem ov3

Proof