This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝜑 → ( 𝐹 = ( 𝑥 ∈ 𝐶 , 𝑦 ∈ 𝐷 ↦ 𝑅 ) → 𝜓 ) )