Metamath Proof Explorer

Theorem fvmpopr2d

Description: Value of an operation given by maps-to notation. (Contributed by Rohan Ridenour, 14-May-2024)

Ref Expression
Hypotheses fvmpopr2d.1 ⊢φ→F=a∈A,b∈B⟼C
fvmpopr2d.2 ⊢φ→P=ab
fvmpopr2d.3 ⊢φ∧a∈A∧b∈B→C∈V
Assertion fvmpopr2d ⊢φ∧a∈A∧b∈B→F⁡P=C

Proof

Step Hyp Ref Expression
1 fvmpopr2d.1 ⊢φ→F=a∈A,b∈B⟼C
2 fvmpopr2d.2 ⊢φ→P=ab
3 fvmpopr2d.3 ⊢φ∧a∈A∧b∈B→C∈V
4 df-ov ⊢aa∈A,b∈B⟼Cb=a∈A,b∈B⟼C⁡ab
5 1 3ad2ant1 ⊢φ∧a∈A∧b∈B→F=a∈A,b∈B⟼C
6 2 3ad2ant1 ⊢φ∧a∈A∧b∈B→P=ab
7 5 6 fveq12d ⊢φ∧a∈A∧b∈B→F⁡P=a∈A,b∈B⟼C⁡ab
8 4 7 eqtr4id ⊢φ∧a∈A∧b∈B→aa∈A,b∈B⟼Cb=F⁡P
9 nfcv ⊢Ⅎ_cC
10 nfcv ⊢Ⅎ_dC
11 nfcv ⊢Ⅎ_ad
12 nfcsb1v ⊢Ⅎ_a⦋c/a⦌C
13 11 12 nfcsbw ⊢Ⅎ_a⦋d/b⦌⦋c/a⦌C
14 nfcsb1v ⊢Ⅎ_b⦋d/b⦌⦋c/a⦌C
15 csbeq1a ⊢a=c→C=⦋c/a⦌C
16 csbeq1a ⊢b=d→⦋c/a⦌C=⦋d/b⦌⦋c/a⦌C
17 15 16 sylan9eq ⊢a=c∧b=d→C=⦋d/b⦌⦋c/a⦌C
18 9 10 13 14 17 cbvmpo ⊢a∈A,b∈B⟼C=c∈A,d∈B⟼⦋d/b⦌⦋c/a⦌C
19 18 oveqi ⊢aa∈A,b∈B⟼Cb=ac∈A,d∈B⟼⦋d/b⦌⦋c/a⦌Cb
20 eqidd ⊢φ∧a∈A∧b∈B→c∈A,d∈B⟼⦋d/b⦌⦋c/a⦌C=c∈A,d∈B⟼⦋d/b⦌⦋c/a⦌C
21 equcom ⊢a=c↔c=a
22 equcom ⊢b=d↔d=b
23 21 22 anbi12i ⊢a=c∧b=d↔c=a∧d=b
24 23 17 sylbir ⊢c=a∧d=b→C=⦋d/b⦌⦋c/a⦌C
25 24 eqcomd ⊢c=a∧d=b→⦋d/b⦌⦋c/a⦌C=C
26 25 adantl ⊢φ∧a∈A∧b∈B∧c=a∧d=b→⦋d/b⦌⦋c/a⦌C=C
27 simp2 ⊢φ∧a∈A∧b∈B→a∈A
28 simp3 ⊢φ∧a∈A∧b∈B→b∈B
29 20 26 27 28 3 ovmpod ⊢φ∧a∈A∧b∈B→ac∈A,d∈B⟼⦋d/b⦌⦋c/a⦌Cb=C
30 19 29 eqtrid ⊢φ∧a∈A∧b∈B→aa∈A,b∈B⟼Cb=C
31 8 30 eqtr3d ⊢φ∧a∈A∧b∈B→F⁡P=C