ovmpodxf

Description: Value of an operation given by a maps-to rule, deduction form. (Contributed by Mario Carneiro, 29-Dec-2014)

	Ref	Expression
Hypotheses	ovmpodx.1	$⊢ φ \to F = (x \in C, y \in D ⟼ R)$
	ovmpodx.2	$⊢ (φ \land (x = A \land y = B)) \to R = S$
	ovmpodx.3	$⊢ (φ \land x = A) \to D = L$
	ovmpodx.4	$⊢ φ \to A \in C$
	ovmpodx.5	$⊢ φ \to B \in L$
	ovmpodx.6	$⊢ φ \to S \in X$
	ovmpodxf.px	$⊢ Ⅎ x φ$
	ovmpodxf.py	$⊢ Ⅎ y φ$
	ovmpodxf.ay	$⊢ \underline{Ⅎ} y A$
	ovmpodxf.bx	$⊢ \underline{Ⅎ} x B$
	ovmpodxf.sx	$⊢ \underline{Ⅎ} x S$
	ovmpodxf.sy	$⊢ \underline{Ⅎ} y S$
Assertion	ovmpodxf	$⊢ φ \to A F B = S$

Proof

Step	Hyp	Ref	Expression
1		ovmpodx.1	$⊢ φ \to F = (x \in C, y \in D ⟼ R)$
2		ovmpodx.2	$⊢ (φ \land (x = A \land y = B)) \to R = S$
3		ovmpodx.3	$⊢ (φ \land x = A) \to D = L$
4		ovmpodx.4	$⊢ φ \to A \in C$
5		ovmpodx.5	$⊢ φ \to B \in L$
6		ovmpodx.6	$⊢ φ \to S \in X$
7		ovmpodxf.px	$⊢ Ⅎ x φ$
8		ovmpodxf.py	$⊢ Ⅎ y φ$
9		ovmpodxf.ay	$⊢ \underline{Ⅎ} y A$
10		ovmpodxf.bx	$⊢ \underline{Ⅎ} x B$
11		ovmpodxf.sx	$⊢ \underline{Ⅎ} x S$
12		ovmpodxf.sy	$⊢ \underline{Ⅎ} y S$
13	1	oveqd	$⊢ φ \to A F B = A (x \in C, y \in D ⟼ R) B$
14		eqid	$⊢ (x \in C, y \in D ⟼ R) = (x \in C, y \in D ⟼ R)$
15	14	ovmpt4g	$⊢ (x \in C \land y \in D \land R \in V) \to x (x \in C, y \in D ⟼ R) y = R$
16	15	a1i	$⊢ φ \to ((x \in C \land y \in D \land R \in V) \to x (x \in C, y \in D ⟼ R) y = R)$
17	8 16	alrimi	$⊢ φ \to \forall y ((x \in C \land y \in D \land R \in V) \to x (x \in C, y \in D ⟼ R) y = R)$
18	5 17	spsbcd	$⊢ φ \to \underset{˙}{[} B / y \underset{˙}{]} ((x \in C \land y \in D \land R \in V) \to x (x \in C, y \in D ⟼ R) y = R)$
19	7 18	alrimi	$⊢ φ \to \forall x \underset{˙}{[} B / y \underset{˙}{]} ((x \in C \land y \in D \land R \in V) \to x (x \in C, y \in D ⟼ R) y = R)$
20	4 19	spsbcd	$⊢ φ \to \underset{˙}{[} A / x \underset{˙}{]} \underset{˙}{[} B / y \underset{˙}{]} ((x \in C \land y \in D \land R \in V) \to x (x \in C, y \in D ⟼ R) y = R)$
21	5	adantr	$⊢ (φ \land x = A) \to B \in L$
22		simplr	$⊢ ((φ \land x = A) \land y = B) \to x = A$
23	4	ad2antrr	$⊢ ((φ \land x = A) \land y = B) \to A \in C$
24	22 23	eqeltrd	$⊢ ((φ \land x = A) \land y = B) \to x \in C$
25	5	ad2antrr	$⊢ ((φ \land x = A) \land y = B) \to B \in L$
26		simpr	$⊢ ((φ \land x = A) \land y = B) \to y = B$
27	3	adantr	$⊢ ((φ \land x = A) \land y = B) \to D = L$
28	25 26 27	3eltr4d	$⊢ ((φ \land x = A) \land y = B) \to y \in D$
29	2	anassrs	$⊢ ((φ \land x = A) \land y = B) \to R = S$
30	6	elexd	$⊢ φ \to S \in V$
31	30	ad2antrr	$⊢ ((φ \land x = A) \land y = B) \to S \in V$
32	29 31	eqeltrd	$⊢ ((φ \land x = A) \land y = B) \to R \in V$
33		biimt	$⊢ (x \in C \land y \in D \land R \in V) \to (x (x \in C, y \in D ⟼ R) y = R \leftrightarrow ((x \in C \land y \in D \land R \in V) \to x (x \in C, y \in D ⟼ R) y = R))$
34	24 28 32 33	syl3anc	$⊢ ((φ \land x = A) \land y = B) \to (x (x \in C, y \in D ⟼ R) y = R \leftrightarrow ((x \in C \land y \in D \land R \in V) \to x (x \in C, y \in D ⟼ R) y = R))$
35	22 26	oveq12d	$⊢ ((φ \land x = A) \land y = B) \to x (x \in C, y \in D ⟼ R) y = A (x \in C, y \in D ⟼ R) B$
36	35 29	eqeq12d	$⊢ ((φ \land x = A) \land y = B) \to (x (x \in C, y \in D ⟼ R) y = R \leftrightarrow A (x \in C, y \in D ⟼ R) B = S)$
37	34 36	bitr3d	$⊢ ((φ \land x = A) \land y = B) \to (((x \in C \land y \in D \land R \in V) \to x (x \in C, y \in D ⟼ R) y = R) \leftrightarrow A (x \in C, y \in D ⟼ R) B = S)$
38	9	nfeq2	$⊢ Ⅎ y x = A$
39	8 38	nfan	$⊢ Ⅎ y (φ \land x = A)$
40		nfmpo2	$⊢ \underline{Ⅎ} y (x \in C, y \in D ⟼ R)$
41		nfcv	$⊢ \underline{Ⅎ} y B$
42	9 40 41	nfov	$⊢ \underline{Ⅎ} y (A (x \in C, y \in D ⟼ R) B)$
43	42 12	nfeq	$⊢ Ⅎ y A (x \in C, y \in D ⟼ R) B = S$
44	43	a1i	$⊢ (φ \land x = A) \to Ⅎ y A (x \in C, y \in D ⟼ R) B = S$
45	21 37 39 44	sbciedf	$⊢ (φ \land x = A) \to (\underset{˙}{[} B / y \underset{˙}{]} ((x \in C \land y \in D \land R \in V) \to x (x \in C, y \in D ⟼ R) y = R) \leftrightarrow A (x \in C, y \in D ⟼ R) B = S)$
46		nfcv	$⊢ \underline{Ⅎ} x A$
47		nfmpo1	$⊢ \underline{Ⅎ} x (x \in C, y \in D ⟼ R)$
48	46 47 10	nfov	$⊢ \underline{Ⅎ} x (A (x \in C, y \in D ⟼ R) B)$
49	48 11	nfeq	$⊢ Ⅎ x A (x \in C, y \in D ⟼ R) B = S$
50	49	a1i	$⊢ φ \to Ⅎ x A (x \in C, y \in D ⟼ R) B = S$
51	4 45 7 50	sbciedf	$⊢ φ \to (\underset{˙}{[} A / x \underset{˙}{]} \underset{˙}{[} B / y \underset{˙}{]} ((x \in C \land y \in D \land R \in V) \to x (x \in C, y \in D ⟼ R) y = R) \leftrightarrow A (x \in C, y \in D ⟼ R) B = S)$
52	20 51	mpbid	$⊢ φ \to A (x \in C, y \in D ⟼ R) B = S$
53	13 52	eqtrd	$⊢ φ \to A F B = S$

Metamath Proof Explorer

Theorem ovmpodxf

Proof