Metamath Proof Explorer

Theorem ovmpos

Description: Value of a function given by the maps-to notation, expressed using explicit substitution. (Contributed by Mario Carneiro, 30-Apr-2015)

Ref Expression
Hypothesis ovmpos.3 ⊢ 𝐹 = ( 𝑥 ∈ 𝐶 , 𝑦 ∈ 𝐷 ↦ 𝑅 )
Assertion ovmpos ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ ⦋ 𝐴 / 𝑥 ⦌ ⦋ 𝐵 / 𝑦 ⦌ 𝑅 ∈ 𝑉 ) → ( 𝐴 𝐹 𝐵 ) = ⦋ 𝐴 / 𝑥 ⦌ ⦋ 𝐵 / 𝑦 ⦌ 𝑅 )

Proof

Step Hyp Ref Expression
1 ovmpos.3 ⊢ 𝐹 = ( 𝑥 ∈ 𝐶 , 𝑦 ∈ 𝐷 ↦ 𝑅 )
2 elex ⊢ ( ⦋ 𝐴 / 𝑥 ⦌ ⦋ 𝐵 / 𝑦 ⦌ 𝑅 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ ⦋ 𝐵 / 𝑦 ⦌ 𝑅 ∈ V )
3 nfcv ⊢ Ⅎ 𝑥 𝐴
4 nfcv ⊢ Ⅎ 𝑦 𝐴
5 nfcv ⊢ Ⅎ 𝑦 𝐵
6 nfcsb1v ⊢ Ⅎ 𝑥 ⦋ 𝐴 / 𝑥 ⦌ 𝑅
7 6 nfel1 ⊢ Ⅎ 𝑥 ⦋ 𝐴 / 𝑥 ⦌ 𝑅 ∈ V
8 nfmpo1 ⊢ Ⅎ 𝑥 ( 𝑥 ∈ 𝐶 , 𝑦 ∈ 𝐷 ↦ 𝑅 )
9 1 8 nfcxfr ⊢ Ⅎ 𝑥 𝐹
10 nfcv ⊢ Ⅎ 𝑥 𝑦
11 3 9 10 nfov ⊢ Ⅎ 𝑥 ( 𝐴 𝐹 𝑦 )
12 11 6 nfeq ⊢ Ⅎ 𝑥 ( 𝐴 𝐹 𝑦 ) = ⦋ 𝐴 / 𝑥 ⦌ 𝑅
13 7 12 nfim ⊢ Ⅎ 𝑥 ( ⦋ 𝐴 / 𝑥 ⦌ 𝑅 ∈ V → ( 𝐴 𝐹 𝑦 ) = ⦋ 𝐴 / 𝑥 ⦌ 𝑅 )
14 nfcsb1v ⊢ Ⅎ 𝑦 ⦋ 𝐵 / 𝑦 ⦌ ⦋ 𝐴 / 𝑥 ⦌ 𝑅
15 14 nfel1 ⊢ Ⅎ 𝑦 ⦋ 𝐵 / 𝑦 ⦌ ⦋ 𝐴 / 𝑥 ⦌ 𝑅 ∈ V
16 nfmpo2 ⊢ Ⅎ 𝑦 ( 𝑥 ∈ 𝐶 , 𝑦 ∈ 𝐷 ↦ 𝑅 )
17 1 16 nfcxfr ⊢ Ⅎ 𝑦 𝐹
18 4 17 5 nfov ⊢ Ⅎ 𝑦 ( 𝐴 𝐹 𝐵 )
19 18 14 nfeq ⊢ Ⅎ 𝑦 ( 𝐴 𝐹 𝐵 ) = ⦋ 𝐵 / 𝑦 ⦌ ⦋ 𝐴 / 𝑥 ⦌ 𝑅
20 15 19 nfim ⊢ Ⅎ 𝑦 ( ⦋ 𝐵 / 𝑦 ⦌ ⦋ 𝐴 / 𝑥 ⦌ 𝑅 ∈ V → ( 𝐴 𝐹 𝐵 ) = ⦋ 𝐵 / 𝑦 ⦌ ⦋ 𝐴 / 𝑥 ⦌ 𝑅 )
21 csbeq1a ⊢ ( 𝑥 = 𝐴 → 𝑅 = ⦋ 𝐴 / 𝑥 ⦌ 𝑅 )
22 21 eleq1d ⊢ ( 𝑥 = 𝐴 → ( 𝑅 ∈ V ↔ ⦋ 𝐴 / 𝑥 ⦌ 𝑅 ∈ V ) )
23 oveq1 ⊢ ( 𝑥 = 𝐴 → ( 𝑥 𝐹 𝑦 ) = ( 𝐴 𝐹 𝑦 ) )
24 23 21 eqeq12d ⊢ ( 𝑥 = 𝐴 → ( ( 𝑥 𝐹 𝑦 ) = 𝑅 ↔ ( 𝐴 𝐹 𝑦 ) = ⦋ 𝐴 / 𝑥 ⦌ 𝑅 ) )
25 22 24 imbi12d ⊢ ( 𝑥 = 𝐴 → ( ( 𝑅 ∈ V → ( 𝑥 𝐹 𝑦 ) = 𝑅 ) ↔ ( ⦋ 𝐴 / 𝑥 ⦌ 𝑅 ∈ V → ( 𝐴 𝐹 𝑦 ) = ⦋ 𝐴 / 𝑥 ⦌ 𝑅 ) ) )
26 csbeq1a ⊢ ( 𝑦 = 𝐵 → ⦋ 𝐴 / 𝑥 ⦌ 𝑅 = ⦋ 𝐵 / 𝑦 ⦌ ⦋ 𝐴 / 𝑥 ⦌ 𝑅 )
27 26 eleq1d ⊢ ( 𝑦 = 𝐵 → ( ⦋ 𝐴 / 𝑥 ⦌ 𝑅 ∈ V ↔ ⦋ 𝐵 / 𝑦 ⦌ ⦋ 𝐴 / 𝑥 ⦌ 𝑅 ∈ V ) )
28 oveq2 ⊢ ( 𝑦 = 𝐵 → ( 𝐴 𝐹 𝑦 ) = ( 𝐴 𝐹 𝐵 ) )
29 28 26 eqeq12d ⊢ ( 𝑦 = 𝐵 → ( ( 𝐴 𝐹 𝑦 ) = ⦋ 𝐴 / 𝑥 ⦌ 𝑅 ↔ ( 𝐴 𝐹 𝐵 ) = ⦋ 𝐵 / 𝑦 ⦌ ⦋ 𝐴 / 𝑥 ⦌ 𝑅 ) )
30 27 29 imbi12d ⊢ ( 𝑦 = 𝐵 → ( ( ⦋ 𝐴 / 𝑥 ⦌ 𝑅 ∈ V → ( 𝐴 𝐹 𝑦 ) = ⦋ 𝐴 / 𝑥 ⦌ 𝑅 ) ↔ ( ⦋ 𝐵 / 𝑦 ⦌ ⦋ 𝐴 / 𝑥 ⦌ 𝑅 ∈ V → ( 𝐴 𝐹 𝐵 ) = ⦋ 𝐵 / 𝑦 ⦌ ⦋ 𝐴 / 𝑥 ⦌ 𝑅 ) ) )
31 1 ovmpt4g ⊢ ( ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ∧ 𝑅 ∈ V ) → ( 𝑥 𝐹 𝑦 ) = 𝑅 )
32 31 3expia ⊢ ( ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) → ( 𝑅 ∈ V → ( 𝑥 𝐹 𝑦 ) = 𝑅 ) )
33 3 4 5 13 20 25 30 32 vtocl2gaf ⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → ( ⦋ 𝐵 / 𝑦 ⦌ ⦋ 𝐴 / 𝑥 ⦌ 𝑅 ∈ V → ( 𝐴 𝐹 𝐵 ) = ⦋ 𝐵 / 𝑦 ⦌ ⦋ 𝐴 / 𝑥 ⦌ 𝑅 ) )
34 csbcom ⊢ ⦋ 𝐴 / 𝑥 ⦌ ⦋ 𝐵 / 𝑦 ⦌ 𝑅 = ⦋ 𝐵 / 𝑦 ⦌ ⦋ 𝐴 / 𝑥 ⦌ 𝑅
35 34 eleq1i ⊢ ( ⦋ 𝐴 / 𝑥 ⦌ ⦋ 𝐵 / 𝑦 ⦌ 𝑅 ∈ V ↔ ⦋ 𝐵 / 𝑦 ⦌ ⦋ 𝐴 / 𝑥 ⦌ 𝑅 ∈ V )
36 34 eqeq2i ⊢ ( ( 𝐴 𝐹 𝐵 ) = ⦋ 𝐴 / 𝑥 ⦌ ⦋ 𝐵 / 𝑦 ⦌ 𝑅 ↔ ( 𝐴 𝐹 𝐵 ) = ⦋ 𝐵 / 𝑦 ⦌ ⦋ 𝐴 / 𝑥 ⦌ 𝑅 )
37 33 35 36 3imtr4g ⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → ( ⦋ 𝐴 / 𝑥 ⦌ ⦋ 𝐵 / 𝑦 ⦌ 𝑅 ∈ V → ( 𝐴 𝐹 𝐵 ) = ⦋ 𝐴 / 𝑥 ⦌ ⦋ 𝐵 / 𝑦 ⦌ 𝑅 ) )
38 2 37 syl5 ⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → ( ⦋ 𝐴 / 𝑥 ⦌ ⦋ 𝐵 / 𝑦 ⦌ 𝑅 ∈ 𝑉 → ( 𝐴 𝐹 𝐵 ) = ⦋ 𝐴 / 𝑥 ⦌ ⦋ 𝐵 / 𝑦 ⦌ 𝑅 ) )
39 38 3impia ⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ ⦋ 𝐴 / 𝑥 ⦌ ⦋ 𝐵 / 𝑦 ⦌ 𝑅 ∈ 𝑉 ) → ( 𝐴 𝐹 𝐵 ) = ⦋ 𝐴 / 𝑥 ⦌ ⦋ 𝐵 / 𝑦 ⦌ 𝑅 )