Metamath Proof Explorer

Theorem ovmpodv2

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

Ref Expression
Hypotheses ovmpodv2.1 ⊢ ( 𝜑 → 𝐴 ∈ 𝐶 )
ovmpodv2.2 ⊢ ( ( 𝜑 ∧ 𝑥 = 𝐴 ) → 𝐵 ∈ 𝐷 )
ovmpodv2.3 ⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ) → 𝑅 ∈ 𝑉 )
ovmpodv2.4 ⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ) → 𝑅 = 𝑆 )
Assertion ovmpodv2 ( 𝜑 → ( 𝐹 = ( 𝑥 ∈ 𝐶 , 𝑦 ∈ 𝐷 ↦ 𝑅 ) → ( 𝐴 𝐹 𝐵 ) = 𝑆 ) )

Proof

Step Hyp Ref Expression
1 ovmpodv2.1 ⊢ ( 𝜑 → 𝐴 ∈ 𝐶 )
2 ovmpodv2.2 ⊢ ( ( 𝜑 ∧ 𝑥 = 𝐴 ) → 𝐵 ∈ 𝐷 )
3 ovmpodv2.3 ⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ) → 𝑅 ∈ 𝑉 )
4 ovmpodv2.4 ⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ) → 𝑅 = 𝑆 )
5 eqidd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐶 , 𝑦 ∈ 𝐷 ↦ 𝑅 ) = ( 𝑥 ∈ 𝐶 , 𝑦 ∈ 𝐷 ↦ 𝑅 ) )
6 4 eqeq2d ⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ) → ( ( 𝐴 ( 𝑥 ∈ 𝐶 , 𝑦 ∈ 𝐷 ↦ 𝑅 ) 𝐵 ) = 𝑅 ↔ ( 𝐴 ( 𝑥 ∈ 𝐶 , 𝑦 ∈ 𝐷 ↦ 𝑅 ) 𝐵 ) = 𝑆 ) )
7 6 biimpd ⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ) → ( ( 𝐴 ( 𝑥 ∈ 𝐶 , 𝑦 ∈ 𝐷 ↦ 𝑅 ) 𝐵 ) = 𝑅 → ( 𝐴 ( 𝑥 ∈ 𝐶 , 𝑦 ∈ 𝐷 ↦ 𝑅 ) 𝐵 ) = 𝑆 ) )
8 nfmpo1 ⊢ Ⅎ 𝑥 ( 𝑥 ∈ 𝐶 , 𝑦 ∈ 𝐷 ↦ 𝑅 )
9 nfcv ⊢ Ⅎ 𝑥 𝐴
10 nfcv ⊢ Ⅎ 𝑥 𝐵
11 9 8 10 nfov ⊢ Ⅎ 𝑥 ( 𝐴 ( 𝑥 ∈ 𝐶 , 𝑦 ∈ 𝐷 ↦ 𝑅 ) 𝐵 )
12 11 nfeq1 ⊢ Ⅎ 𝑥 ( 𝐴 ( 𝑥 ∈ 𝐶 , 𝑦 ∈ 𝐷 ↦ 𝑅 ) 𝐵 ) = 𝑆
13 nfmpo2 ⊢ Ⅎ 𝑦 ( 𝑥 ∈ 𝐶 , 𝑦 ∈ 𝐷 ↦ 𝑅 )
14 nfcv ⊢ Ⅎ 𝑦 𝐴
15 nfcv ⊢ Ⅎ 𝑦 𝐵
16 14 13 15 nfov ⊢ Ⅎ 𝑦 ( 𝐴 ( 𝑥 ∈ 𝐶 , 𝑦 ∈ 𝐷 ↦ 𝑅 ) 𝐵 )
17 16 nfeq1 ⊢ Ⅎ 𝑦 ( 𝐴 ( 𝑥 ∈ 𝐶 , 𝑦 ∈ 𝐷 ↦ 𝑅 ) 𝐵 ) = 𝑆
18 1 2 3 7 8 12 13 17 ovmpodf ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐶 , 𝑦 ∈ 𝐷 ↦ 𝑅 ) = ( 𝑥 ∈ 𝐶 , 𝑦 ∈ 𝐷 ↦ 𝑅 ) → ( 𝐴 ( 𝑥 ∈ 𝐶 , 𝑦 ∈ 𝐷 ↦ 𝑅 ) 𝐵 ) = 𝑆 ) )
19 5 18 mpd ⊢ ( 𝜑 → ( 𝐴 ( 𝑥 ∈ 𝐶 , 𝑦 ∈ 𝐷 ↦ 𝑅 ) 𝐵 ) = 𝑆 )
20 oveq ⊢ ( 𝐹 = ( 𝑥 ∈ 𝐶 , 𝑦 ∈ 𝐷 ↦ 𝑅 ) → ( 𝐴 𝐹 𝐵 ) = ( 𝐴 ( 𝑥 ∈ 𝐶 , 𝑦 ∈ 𝐷 ↦ 𝑅 ) 𝐵 ) )
21 20 eqeq1d ⊢ ( 𝐹 = ( 𝑥 ∈ 𝐶 , 𝑦 ∈ 𝐷 ↦ 𝑅 ) → ( ( 𝐴 𝐹 𝐵 ) = 𝑆 ↔ ( 𝐴 ( 𝑥 ∈ 𝐶 , 𝑦 ∈ 𝐷 ↦ 𝑅 ) 𝐵 ) = 𝑆 ) )
22 19 21 syl5ibrcom ⊢ ( 𝜑 → ( 𝐹 = ( 𝑥 ∈ 𝐶 , 𝑦 ∈ 𝐷 ↦ 𝑅 ) → ( 𝐴 𝐹 𝐵 ) = 𝑆 ) )