ovmpodf

Description: Alternate deduction version of ovmpo , suitable for iteration. (Contributed by Mario Carneiro, 7-Jan-2017)

	Ref	Expression
Hypotheses	ovmpodf.1	$⊢ φ \to A \in C$
	ovmpodf.2	$⊢ (φ \land x = A) \to B \in D$
	ovmpodf.3	$⊢ (φ \land (x = A \land y = B)) \to R \in V$
	ovmpodf.4	$⊢ (φ \land (x = A \land y = B)) \to (A F B = R \to ψ)$
	ovmpodf.5	$⊢ \underline{Ⅎ} x F$
	ovmpodf.6	$⊢ Ⅎ x ψ$
	ovmpodf.7	$⊢ \underline{Ⅎ} y F$
	ovmpodf.8	$⊢ Ⅎ y ψ$
Assertion	ovmpodf	$⊢ φ \to (F = (x \in C, y \in D ⟼ R) \to ψ)$

Proof

Step	Hyp	Ref	Expression
1		ovmpodf.1	$⊢ φ \to A \in C$
2		ovmpodf.2	$⊢ (φ \land x = A) \to B \in D$
3		ovmpodf.3	$⊢ (φ \land (x = A \land y = B)) \to R \in V$
4		ovmpodf.4	$⊢ (φ \land (x = A \land y = B)) \to (A F B = R \to ψ)$
5		ovmpodf.5	$⊢ \underline{Ⅎ} x F$
6		ovmpodf.6	$⊢ Ⅎ x ψ$
7		ovmpodf.7	$⊢ \underline{Ⅎ} y F$
8		ovmpodf.8	$⊢ Ⅎ y ψ$
9		nfv	$⊢ Ⅎ x φ$
10		nfmpo1	$⊢ \underline{Ⅎ} x (x \in C, y \in D ⟼ R)$
11	5 10	nfeq	$⊢ Ⅎ x F = (x \in C, y \in D ⟼ R)$
12	11 6	nfim	$⊢ Ⅎ x (F = (x \in C, y \in D ⟼ R) \to ψ)$
13	1	elexd	$⊢ φ \to A \in V$
14		isset	$⊢ A \in V \leftrightarrow \exists x x = A$
15	13 14	sylib	$⊢ φ \to \exists x x = A$
16		nfv	$⊢ Ⅎ y (φ \land x = A)$
17		nfmpo2	$⊢ \underline{Ⅎ} y (x \in C, y \in D ⟼ R)$
18	7 17	nfeq	$⊢ Ⅎ y F = (x \in C, y \in D ⟼ R)$
19	18 8	nfim	$⊢ Ⅎ y (F = (x \in C, y \in D ⟼ R) \to ψ)$
20	2	elexd	$⊢ (φ \land x = A) \to B \in V$
21		isset	$⊢ B \in V \leftrightarrow \exists y y = B$
22	20 21	sylib	$⊢ (φ \land x = A) \to \exists y y = B$
23		oveq	$⊢ F = (x \in C, y \in D ⟼ R) \to A F B = A (x \in C, y \in D ⟼ R) B$
24		simprl	$⊢ (φ \land (x = A \land y = B)) \to x = A$
25		simprr	$⊢ (φ \land (x = A \land y = B)) \to y = B$
26	24 25	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$
27	1	adantr	$⊢ (φ \land (x = A \land y = B)) \to A \in C$
28	24 27	eqeltrd	$⊢ (φ \land (x = A \land y = B)) \to x \in C$
29	2	adantrr	$⊢ (φ \land (x = A \land y = B)) \to B \in D$
30	25 29	eqeltrd	$⊢ (φ \land (x = A \land y = B)) \to y \in D$
31		eqid	$⊢ (x \in C, y \in D ⟼ R) = (x \in C, y \in D ⟼ R)$
32	31	ovmpt4g	$⊢ (x \in C \land y \in D \land R \in V) \to x (x \in C, y \in D ⟼ R) y = R$
33	28 30 3 32	syl3anc	$⊢ (φ \land (x = A \land y = B)) \to x (x \in C, y \in D ⟼ R) y = R$
34	26 33	eqtr3d	$⊢ (φ \land (x = A \land y = B)) \to A (x \in C, y \in D ⟼ R) B = R$
35	34	eqeq2d	$⊢ (φ \land (x = A \land y = B)) \to (A F B = A (x \in C, y \in D ⟼ R) B \leftrightarrow A F B = R)$
36	35 4	sylbid	$⊢ (φ \land (x = A \land y = B)) \to (A F B = A (x \in C, y \in D ⟼ R) B \to ψ)$
37	23 36	syl5	$⊢ (φ \land (x = A \land y = B)) \to (F = (x \in C, y \in D ⟼ R) \to ψ)$
38	37	expr	$⊢ (φ \land x = A) \to (y = B \to (F = (x \in C, y \in D ⟼ R) \to ψ))$
39	16 19 22 38	exlimimdd	$⊢ (φ \land x = A) \to (F = (x \in C, y \in D ⟼ R) \to ψ)$
40	9 12 15 39	exlimdd	$⊢ φ \to (F = (x \in C, y \in D ⟼ R) \to ψ)$

Metamath Proof Explorer

Theorem ovmpodf

Proof