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

Metamath Proof Explorer

Theorem fvsetsid

Description: The value of the structure replacement function for its first argument is its second argument. (Contributed by SO, 12-Jul-2018)

Ref Expression
Assertion fvsetsid ( ( 𝐹 ∈ 𝑉 ∧ 𝑋 ∈ 𝑊 ∧ 𝑌 ∈ 𝑈 ) → ( ( 𝐹 sSet ⟨ 𝑋 , 𝑌 ⟩ ) ‘ 𝑋 ) = 𝑌 )

Proof

Step Hyp Ref Expression
1 setsval ⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝑌 ∈ 𝑈 ) → ( 𝐹 sSet ⟨ 𝑋 , 𝑌 ⟩ ) = ( ( 𝐹 ↾ ( V ∖ { 𝑋 } ) ) ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) )
2 1 3adant2 ⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝑋 ∈ 𝑊 ∧ 𝑌 ∈ 𝑈 ) → ( 𝐹 sSet ⟨ 𝑋 , 𝑌 ⟩ ) = ( ( 𝐹 ↾ ( V ∖ { 𝑋 } ) ) ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) )
3 2 fveq1d ⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝑋 ∈ 𝑊 ∧ 𝑌 ∈ 𝑈 ) → ( ( 𝐹 sSet ⟨ 𝑋 , 𝑌 ⟩ ) ‘ 𝑋 ) = ( ( ( 𝐹 ↾ ( V ∖ { 𝑋 } ) ) ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ‘ 𝑋 ) )
4 simp2 ⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝑋 ∈ 𝑊 ∧ 𝑌 ∈ 𝑈 ) → 𝑋 ∈ 𝑊 )
5 simp3 ⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝑋 ∈ 𝑊 ∧ 𝑌 ∈ 𝑈 ) → 𝑌 ∈ 𝑈 )
6 neldifsn ⊢ ¬ 𝑋 ∈ ( V ∖ { 𝑋 } )
7 dmres ⊢ dom ( 𝐹 ↾ ( V ∖ { 𝑋 } ) ) = ( ( V ∖ { 𝑋 } ) ∩ dom 𝐹 )
8 inss1 ⊢ ( ( V ∖ { 𝑋 } ) ∩ dom 𝐹 ) ⊆ ( V ∖ { 𝑋 } )
9 7 8 eqsstri ⊢ dom ( 𝐹 ↾ ( V ∖ { 𝑋 } ) ) ⊆ ( V ∖ { 𝑋 } )
10 9 sseli ⊢ ( 𝑋 ∈ dom ( 𝐹 ↾ ( V ∖ { 𝑋 } ) ) → 𝑋 ∈ ( V ∖ { 𝑋 } ) )
11 6 10 mto ⊢ ¬ 𝑋 ∈ dom ( 𝐹 ↾ ( V ∖ { 𝑋 } ) )
12 11 a1i ⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝑋 ∈ 𝑊 ∧ 𝑌 ∈ 𝑈 ) → ¬ 𝑋 ∈ dom ( 𝐹 ↾ ( V ∖ { 𝑋 } ) ) )
13 fsnunfv ⊢ ( ( 𝑋 ∈ 𝑊 ∧ 𝑌 ∈ 𝑈 ∧ ¬ 𝑋 ∈ dom ( 𝐹 ↾ ( V ∖ { 𝑋 } ) ) ) → ( ( ( 𝐹 ↾ ( V ∖ { 𝑋 } ) ) ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ‘ 𝑋 ) = 𝑌 )
14 4 5 12 13 syl3anc ⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝑋 ∈ 𝑊 ∧ 𝑌 ∈ 𝑈 ) → ( ( ( 𝐹 ↾ ( V ∖ { 𝑋 } ) ) ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ‘ 𝑋 ) = 𝑌 )
15 3 14 eqtrd ⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝑋 ∈ 𝑊 ∧ 𝑌 ∈ 𝑈 ) → ( ( 𝐹 sSet ⟨ 𝑋 , 𝑌 ⟩ ) ‘ 𝑋 ) = 𝑌 )