Metamath Proof Explorer

Theorem fvmpti

Description: Value of a function given in maps-to notation. (Contributed by Mario Carneiro, 23-Apr-2014)

Ref Expression
Hypotheses fvmptg.1 ⊢ x = A → B = C
fvmptg.2 ⊢ F = x ∈ D ⟼ B
Assertion fvmpti ⊢ A ∈ D → F ⁡ A = I ⁡ C

Proof

Step Hyp Ref Expression
1 fvmptg.1 ⊢ x = A → B = C
2 fvmptg.2 ⊢ F = x ∈ D ⟼ B
3 1 2 fvmptg ⊢ A ∈ D ∧ C ∈ V → F ⁡ A = C
4 fvi ⊢ C ∈ V → I ⁡ C = C
5 4 adantl ⊢ A ∈ D ∧ C ∈ V → I ⁡ C = C
6 3 5 eqtr4d ⊢ A ∈ D ∧ C ∈ V → F ⁡ A = I ⁡ C
7 1 eleq1d ⊢ x = A → B ∈ V ↔ C ∈ V
8 2 dmmpt ⊢ dom ⁡ F = x ∈ D | B ∈ V
9 7 8 elrab2 ⊢ A ∈ dom ⁡ F ↔ A ∈ D ∧ C ∈ V
10 9 baib ⊢ A ∈ D → A ∈ dom ⁡ F ↔ C ∈ V
11 10 notbid ⊢ A ∈ D → ¬ A ∈ dom ⁡ F ↔ ¬ C ∈ V
12 ndmfv ⊢ ¬ A ∈ dom ⁡ F → F ⁡ A = ∅
13 11 12 syl6bir ⊢ A ∈ D → ¬ C ∈ V → F ⁡ A = ∅
14 13 imp ⊢ A ∈ D ∧ ¬ C ∈ V → F ⁡ A = ∅
15 fvprc ⊢ ¬ C ∈ V → I ⁡ C = ∅
16 15 adantl ⊢ A ∈ D ∧ ¬ C ∈ V → I ⁡ C = ∅
17 14 16 eqtr4d ⊢ A ∈ D ∧ ¬ C ∈ V → F ⁡ A = I ⁡ C
18 6 17 pm2.61dan ⊢ A ∈ D → F ⁡ A = I ⁡ C