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 = a b
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 = a b
3 fvmpopr2d.3 ⊢ φ ∧ a ∈ A ∧ b ∈ B → C ∈ V
4 df-ov ⊢ a a ∈ A , b ∈ B ⟼ C b = a ∈ A , b ∈ B ⟼ C ⁡ a b
5 1 3ad2ant1 ⊢ φ ∧ a ∈ A ∧ b ∈ B → F = a ∈ A , b ∈ B ⟼ C
6 2 3ad2ant1 ⊢ φ ∧ a ∈ A ∧ b ∈ B → P = a b
7 5 6 fveq12d ⊢ φ ∧ a ∈ A ∧ b ∈ B → F ⁡ P = a ∈ A , b ∈ B ⟼ C ⁡ a b
8 4 7 eqtr4id ⊢ φ ∧ a ∈ A ∧ b ∈ B → a a ∈ A , b ∈ B ⟼ C b = F ⁡ P
9 nfcv ⊢ Ⅎ _ c C
10 nfcv ⊢ Ⅎ _ d C
11 nfcv ⊢ Ⅎ _ a d
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 ⊢ a a ∈ A , b ∈ B ⟼ C b = a c ∈ A , d ∈ B ⟼ ⦋ d / b⦌ ⦋ c / a⦌ C b
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 → a c ∈ A , d ∈ B ⟼ ⦋ d / b⦌ ⦋ c / a⦌ C b = C
30 19 29 eqtrid ⊢ φ ∧ a ∈ A ∧ b ∈ B → a a ∈ A , b ∈ B ⟼ C b = C
31 8 30 eqtr3d ⊢ φ ∧ a ∈ A ∧ b ∈ B → F ⁡ P = C