This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fvmptt

Description: Closed theorem form of fvmpt . (Contributed by Scott Fenton, 21-Feb-2013) (Revised by Mario Carneiro, 11-Sep-2015)

Ref Expression
Assertion fvmptt ( ( ∀ 𝑥 ( 𝑥 = 𝐴 → 𝐵 = 𝐶 ) ∧ 𝐹 = ( 𝑥 ∈ 𝐷 ↦ 𝐵 ) ∧ ( 𝐴 ∈ 𝐷 ∧ 𝐶 ∈ 𝑉 ) ) → ( 𝐹 ‘ 𝐴 ) = 𝐶 )

Proof

Step Hyp Ref Expression
1 simp2 ⊢ ( ( ∀ 𝑥 ( 𝑥 = 𝐴 → 𝐵 = 𝐶 ) ∧ 𝐹 = ( 𝑥 ∈ 𝐷 ↦ 𝐵 ) ∧ ( 𝐴 ∈ 𝐷 ∧ 𝐶 ∈ 𝑉 ) ) → 𝐹 = ( 𝑥 ∈ 𝐷 ↦ 𝐵 ) )
2 1 fveq1d ⊢ ( ( ∀ 𝑥 ( 𝑥 = 𝐴 → 𝐵 = 𝐶 ) ∧ 𝐹 = ( 𝑥 ∈ 𝐷 ↦ 𝐵 ) ∧ ( 𝐴 ∈ 𝐷 ∧ 𝐶 ∈ 𝑉 ) ) → ( 𝐹 ‘ 𝐴 ) = ( ( 𝑥 ∈ 𝐷 ↦ 𝐵 ) ‘ 𝐴 ) )
3 risset ⊢ ( 𝐴 ∈ 𝐷 ↔ ∃ 𝑥 ∈ 𝐷 𝑥 = 𝐴 )
4 elex ⊢ ( 𝐶 ∈ 𝑉 → 𝐶 ∈ V )
5 nfa1 ⊢ Ⅎ 𝑥 ∀ 𝑥 ( 𝑥 = 𝐴 → 𝐵 = 𝐶 )
6 nfv ⊢ Ⅎ 𝑥 𝐶 ∈ V
7 nffvmpt1 ⊢ Ⅎ 𝑥 ( ( 𝑥 ∈ 𝐷 ↦ 𝐵 ) ‘ 𝐴 )
8 7 nfeq1 ⊢ Ⅎ 𝑥 ( ( 𝑥 ∈ 𝐷 ↦ 𝐵 ) ‘ 𝐴 ) = 𝐶
9 6 8 nfim ⊢ Ⅎ 𝑥 ( 𝐶 ∈ V → ( ( 𝑥 ∈ 𝐷 ↦ 𝐵 ) ‘ 𝐴 ) = 𝐶 )
10 simprl ⊢ ( ( ( 𝑥 = 𝐴 ∧ 𝐵 = 𝐶 ) ∧ ( 𝑥 ∈ 𝐷 ∧ 𝐶 ∈ V ) ) → 𝑥 ∈ 𝐷 )
11 simplr ⊢ ( ( ( 𝑥 = 𝐴 ∧ 𝐵 = 𝐶 ) ∧ ( 𝑥 ∈ 𝐷 ∧ 𝐶 ∈ V ) ) → 𝐵 = 𝐶 )
12 simprr ⊢ ( ( ( 𝑥 = 𝐴 ∧ 𝐵 = 𝐶 ) ∧ ( 𝑥 ∈ 𝐷 ∧ 𝐶 ∈ V ) ) → 𝐶 ∈ V )
13 11 12 eqeltrd ⊢ ( ( ( 𝑥 = 𝐴 ∧ 𝐵 = 𝐶 ) ∧ ( 𝑥 ∈ 𝐷 ∧ 𝐶 ∈ V ) ) → 𝐵 ∈ V )
14 eqid ⊢ ( 𝑥 ∈ 𝐷 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐷 ↦ 𝐵 )
15 14 fvmpt2 ⊢ ( ( 𝑥 ∈ 𝐷 ∧ 𝐵 ∈ V ) → ( ( 𝑥 ∈ 𝐷 ↦ 𝐵 ) ‘ 𝑥 ) = 𝐵 )
16 10 13 15 syl2anc ⊢ ( ( ( 𝑥 = 𝐴 ∧ 𝐵 = 𝐶 ) ∧ ( 𝑥 ∈ 𝐷 ∧ 𝐶 ∈ V ) ) → ( ( 𝑥 ∈ 𝐷 ↦ 𝐵 ) ‘ 𝑥 ) = 𝐵 )
17 simpll ⊢ ( ( ( 𝑥 = 𝐴 ∧ 𝐵 = 𝐶 ) ∧ ( 𝑥 ∈ 𝐷 ∧ 𝐶 ∈ V ) ) → 𝑥 = 𝐴 )
18 17 fveq2d ⊢ ( ( ( 𝑥 = 𝐴 ∧ 𝐵 = 𝐶 ) ∧ ( 𝑥 ∈ 𝐷 ∧ 𝐶 ∈ V ) ) → ( ( 𝑥 ∈ 𝐷 ↦ 𝐵 ) ‘ 𝑥 ) = ( ( 𝑥 ∈ 𝐷 ↦ 𝐵 ) ‘ 𝐴 ) )
19 16 18 11 3eqtr3d ⊢ ( ( ( 𝑥 = 𝐴 ∧ 𝐵 = 𝐶 ) ∧ ( 𝑥 ∈ 𝐷 ∧ 𝐶 ∈ V ) ) → ( ( 𝑥 ∈ 𝐷 ↦ 𝐵 ) ‘ 𝐴 ) = 𝐶 )
20 19 exp43 ⊢ ( 𝑥 = 𝐴 → ( 𝐵 = 𝐶 → ( 𝑥 ∈ 𝐷 → ( 𝐶 ∈ V → ( ( 𝑥 ∈ 𝐷 ↦ 𝐵 ) ‘ 𝐴 ) = 𝐶 ) ) ) )
21 20 a2i ⊢ ( ( 𝑥 = 𝐴 → 𝐵 = 𝐶 ) → ( 𝑥 = 𝐴 → ( 𝑥 ∈ 𝐷 → ( 𝐶 ∈ V → ( ( 𝑥 ∈ 𝐷 ↦ 𝐵 ) ‘ 𝐴 ) = 𝐶 ) ) ) )
22 21 com23 ⊢ ( ( 𝑥 = 𝐴 → 𝐵 = 𝐶 ) → ( 𝑥 ∈ 𝐷 → ( 𝑥 = 𝐴 → ( 𝐶 ∈ V → ( ( 𝑥 ∈ 𝐷 ↦ 𝐵 ) ‘ 𝐴 ) = 𝐶 ) ) ) )
23 22 sps ⊢ ( ∀ 𝑥 ( 𝑥 = 𝐴 → 𝐵 = 𝐶 ) → ( 𝑥 ∈ 𝐷 → ( 𝑥 = 𝐴 → ( 𝐶 ∈ V → ( ( 𝑥 ∈ 𝐷 ↦ 𝐵 ) ‘ 𝐴 ) = 𝐶 ) ) ) )
24 5 9 23 rexlimd ⊢ ( ∀ 𝑥 ( 𝑥 = 𝐴 → 𝐵 = 𝐶 ) → ( ∃ 𝑥 ∈ 𝐷 𝑥 = 𝐴 → ( 𝐶 ∈ V → ( ( 𝑥 ∈ 𝐷 ↦ 𝐵 ) ‘ 𝐴 ) = 𝐶 ) ) )
25 4 24 syl7 ⊢ ( ∀ 𝑥 ( 𝑥 = 𝐴 → 𝐵 = 𝐶 ) → ( ∃ 𝑥 ∈ 𝐷 𝑥 = 𝐴 → ( 𝐶 ∈ 𝑉 → ( ( 𝑥 ∈ 𝐷 ↦ 𝐵 ) ‘ 𝐴 ) = 𝐶 ) ) )
26 3 25 biimtrid ⊢ ( ∀ 𝑥 ( 𝑥 = 𝐴 → 𝐵 = 𝐶 ) → ( 𝐴 ∈ 𝐷 → ( 𝐶 ∈ 𝑉 → ( ( 𝑥 ∈ 𝐷 ↦ 𝐵 ) ‘ 𝐴 ) = 𝐶 ) ) )
27 26 imp32 ⊢ ( ( ∀ 𝑥 ( 𝑥 = 𝐴 → 𝐵 = 𝐶 ) ∧ ( 𝐴 ∈ 𝐷 ∧ 𝐶 ∈ 𝑉 ) ) → ( ( 𝑥 ∈ 𝐷 ↦ 𝐵 ) ‘ 𝐴 ) = 𝐶 )
28 27 3adant2 ⊢ ( ( ∀ 𝑥 ( 𝑥 = 𝐴 → 𝐵 = 𝐶 ) ∧ 𝐹 = ( 𝑥 ∈ 𝐷 ↦ 𝐵 ) ∧ ( 𝐴 ∈ 𝐷 ∧ 𝐶 ∈ 𝑉 ) ) → ( ( 𝑥 ∈ 𝐷 ↦ 𝐵 ) ‘ 𝐴 ) = 𝐶 )
29 2 28 eqtrd ⊢ ( ( ∀ 𝑥 ( 𝑥 = 𝐴 → 𝐵 = 𝐶 ) ∧ 𝐹 = ( 𝑥 ∈ 𝐷 ↦ 𝐵 ) ∧ ( 𝐴 ∈ 𝐷 ∧ 𝐶 ∈ 𝑉 ) ) → ( 𝐹 ‘ 𝐴 ) = 𝐶 )