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 ( ( 𝐴𝐶𝐵𝐷 𝐴 / 𝑥 𝐵 / 𝑦 𝑅𝑉 ) → ( 𝐴 𝐹 𝐵 ) = 𝐴 / 𝑥 𝐵 / 𝑦 𝑅 )