Theorem ovmpodf

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

	Ref	Expression
Hypotheses	ovmpodf.1	⊢ ( 𝜑 → 𝐴 ∈ 𝐶 )
	ovmpodf.2	⊢ ( ( 𝜑 ∧ 𝑥 = 𝐴 ) → 𝐵 ∈ 𝐷 )
	ovmpodf.3	⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ) → 𝑅 ∈ 𝑉 )
	ovmpodf.4	⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ) → ( ( 𝐴 𝐹 𝐵 ) = 𝑅 → 𝜓 ) )
	ovmpodf.5	⊢ Ⅎ 𝑥 𝐹
	ovmpodf.6	⊢ Ⅎ 𝑥 𝜓
	ovmpodf.7	⊢ Ⅎ 𝑦 𝐹
	ovmpodf.8	⊢ Ⅎ 𝑦 𝜓
Assertion	ovmpodf	⊢ ( 𝜑 → ( 𝐹 = ( 𝑥 ∈ 𝐶 , 𝑦 ∈ 𝐷 ↦ 𝑅 ) → 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		ovmpodf.1	⊢ ( 𝜑 → 𝐴 ∈ 𝐶 )
2		ovmpodf.2	⊢ ( ( 𝜑 ∧ 𝑥 = 𝐴 ) → 𝐵 ∈ 𝐷 )
3		ovmpodf.3	⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ) → 𝑅 ∈ 𝑉 )
4		ovmpodf.4	⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ) → ( ( 𝐴 𝐹 𝐵 ) = 𝑅 → 𝜓 ) )
5		ovmpodf.5	⊢ Ⅎ 𝑥 𝐹
6		ovmpodf.6	⊢ Ⅎ 𝑥 𝜓
7		ovmpodf.7	⊢ Ⅎ 𝑦 𝐹
8		ovmpodf.8	⊢ Ⅎ 𝑦 𝜓
9		nfv	⊢ Ⅎ 𝑥 𝜑
10		nfmpo1	⊢ Ⅎ 𝑥 ( 𝑥 ∈ 𝐶 , 𝑦 ∈ 𝐷 ↦ 𝑅 )
11	5 10	nfeq	⊢ Ⅎ 𝑥 𝐹 = ( 𝑥 ∈ 𝐶 , 𝑦 ∈ 𝐷 ↦ 𝑅 )
12	11 6	nfim	⊢ Ⅎ 𝑥 ( 𝐹 = ( 𝑥 ∈ 𝐶 , 𝑦 ∈ 𝐷 ↦ 𝑅 ) → 𝜓 )
13	1	elexd	⊢ ( 𝜑 → 𝐴 ∈ V )
14		isset	⊢ ( 𝐴 ∈ V ↔ ∃ 𝑥 𝑥 = 𝐴 )
15	13 14	sylib	⊢ ( 𝜑 → ∃ 𝑥 𝑥 = 𝐴 )
16		nfv	⊢ Ⅎ 𝑦 ( 𝜑 ∧ 𝑥 = 𝐴 )
17		nfmpo2	⊢ Ⅎ 𝑦 ( 𝑥 ∈ 𝐶 , 𝑦 ∈ 𝐷 ↦ 𝑅 )
18	7 17	nfeq	⊢ Ⅎ 𝑦 𝐹 = ( 𝑥 ∈ 𝐶 , 𝑦 ∈ 𝐷 ↦ 𝑅 )
19	18 8	nfim	⊢ Ⅎ 𝑦 ( 𝐹 = ( 𝑥 ∈ 𝐶 , 𝑦 ∈ 𝐷 ↦ 𝑅 ) → 𝜓 )
20	2	elexd	⊢ ( ( 𝜑 ∧ 𝑥 = 𝐴 ) → 𝐵 ∈ V )
21		isset	⊢ ( 𝐵 ∈ V ↔ ∃ 𝑦 𝑦 = 𝐵 )
22	20 21	sylib	⊢ ( ( 𝜑 ∧ 𝑥 = 𝐴 ) → ∃ 𝑦 𝑦 = 𝐵 )
23		oveq	⊢ ( 𝐹 = ( 𝑥 ∈ 𝐶 , 𝑦 ∈ 𝐷 ↦ 𝑅 ) → ( 𝐴 𝐹 𝐵 ) = ( 𝐴 ( 𝑥 ∈ 𝐶 , 𝑦 ∈ 𝐷 ↦ 𝑅 ) 𝐵 ) )
24		simprl	⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ) → 𝑥 = 𝐴 )
25		simprr	⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ) → 𝑦 = 𝐵 )
26	24 25	oveq12d	⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ) → ( 𝑥 ( 𝑥 ∈ 𝐶 , 𝑦 ∈ 𝐷 ↦ 𝑅 ) 𝑦 ) = ( 𝐴 ( 𝑥 ∈ 𝐶 , 𝑦 ∈ 𝐷 ↦ 𝑅 ) 𝐵 ) )
27	1	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ) → 𝐴 ∈ 𝐶 )
28	24 27	eqeltrd	⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ) → 𝑥 ∈ 𝐶 )
29	2	adantrr	⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ) → 𝐵 ∈ 𝐷 )
30	25 29	eqeltrd	⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ) → 𝑦 ∈ 𝐷 )
31		eqid	⊢ ( 𝑥 ∈ 𝐶 , 𝑦 ∈ 𝐷 ↦ 𝑅 ) = ( 𝑥 ∈ 𝐶 , 𝑦 ∈ 𝐷 ↦ 𝑅 )
32	31	ovmpt4g	⊢ ( ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ∧ 𝑅 ∈ 𝑉 ) → ( 𝑥 ( 𝑥 ∈ 𝐶 , 𝑦 ∈ 𝐷 ↦ 𝑅 ) 𝑦 ) = 𝑅 )
33	28 30 3 32	syl3anc	⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ) → ( 𝑥 ( 𝑥 ∈ 𝐶 , 𝑦 ∈ 𝐷 ↦ 𝑅 ) 𝑦 ) = 𝑅 )
34	26 33	eqtr3d	⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ) → ( 𝐴 ( 𝑥 ∈ 𝐶 , 𝑦 ∈ 𝐷 ↦ 𝑅 ) 𝐵 ) = 𝑅 )
35	34	eqeq2d	⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ) → ( ( 𝐴 𝐹 𝐵 ) = ( 𝐴 ( 𝑥 ∈ 𝐶 , 𝑦 ∈ 𝐷 ↦ 𝑅 ) 𝐵 ) ↔ ( 𝐴 𝐹 𝐵 ) = 𝑅 ) )
36	35 4	sylbid	⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ) → ( ( 𝐴 𝐹 𝐵 ) = ( 𝐴 ( 𝑥 ∈ 𝐶 , 𝑦 ∈ 𝐷 ↦ 𝑅 ) 𝐵 ) → 𝜓 ) )
37	23 36	syl5	⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ) → ( 𝐹 = ( 𝑥 ∈ 𝐶 , 𝑦 ∈ 𝐷 ↦ 𝑅 ) → 𝜓 ) )
38	37	expr	⊢ ( ( 𝜑 ∧ 𝑥 = 𝐴 ) → ( 𝑦 = 𝐵 → ( 𝐹 = ( 𝑥 ∈ 𝐶 , 𝑦 ∈ 𝐷 ↦ 𝑅 ) → 𝜓 ) ) )
39	16 19 22 38	exlimimdd	⊢ ( ( 𝜑 ∧ 𝑥 = 𝐴 ) → ( 𝐹 = ( 𝑥 ∈ 𝐶 , 𝑦 ∈ 𝐷 ↦ 𝑅 ) → 𝜓 ) )
40	9 12 15 39	exlimdd	⊢ ( 𝜑 → ( 𝐹 = ( 𝑥 ∈ 𝐶 , 𝑦 ∈ 𝐷 ↦ 𝑅 ) → 𝜓 ) )