Metamath Proof Explorer

Theorem fsets

Description: The structure replacement function is a function. (Contributed by SO, 12-Jul-2018)

Ref Expression
Assertion fsets ( ( ( 𝐹 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) → ( 𝐹 sSet ⟨ 𝑋 , 𝑌 ⟩ ) : 𝐴 ⟶ 𝐵 )

Proof

Step Hyp Ref Expression
1 difss ⊢ ( 𝐴 ∖ { 𝑋 } ) ⊆ 𝐴
2 fssres ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ( 𝐴 ∖ { 𝑋 } ) ⊆ 𝐴 ) → ( 𝐹 ↾ ( 𝐴 ∖ { 𝑋 } ) ) : ( 𝐴 ∖ { 𝑋 } ) ⟶ 𝐵 )
3 1 2 mpan2 ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( 𝐹 ↾ ( 𝐴 ∖ { 𝑋 } ) ) : ( 𝐴 ∖ { 𝑋 } ) ⟶ 𝐵 )
4 ffn ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → 𝐹 Fn 𝐴 )
5 fnresdm ⊢ ( 𝐹 Fn 𝐴 → ( 𝐹 ↾ 𝐴 ) = 𝐹 )
6 4 5 syl ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( 𝐹 ↾ 𝐴 ) = 𝐹 )
7 6 reseq1d ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( ( 𝐹 ↾ 𝐴 ) ↾ ( V ∖ { 𝑋 } ) ) = ( 𝐹 ↾ ( V ∖ { 𝑋 } ) ) )
8 resres ⊢ ( ( 𝐹 ↾ 𝐴 ) ↾ ( V ∖ { 𝑋 } ) ) = ( 𝐹 ↾ ( 𝐴 ∩ ( V ∖ { 𝑋 } ) ) )
9 invdif ⊢ ( 𝐴 ∩ ( V ∖ { 𝑋 } ) ) = ( 𝐴 ∖ { 𝑋 } )
10 9 reseq2i ⊢ ( 𝐹 ↾ ( 𝐴 ∩ ( V ∖ { 𝑋 } ) ) ) = ( 𝐹 ↾ ( 𝐴 ∖ { 𝑋 } ) )
11 8 10 eqtri ⊢ ( ( 𝐹 ↾ 𝐴 ) ↾ ( V ∖ { 𝑋 } ) ) = ( 𝐹 ↾ ( 𝐴 ∖ { 𝑋 } ) )
12 7 11 eqtr3di ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( 𝐹 ↾ ( V ∖ { 𝑋 } ) ) = ( 𝐹 ↾ ( 𝐴 ∖ { 𝑋 } ) ) )
13 12 feq1d ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( ( 𝐹 ↾ ( V ∖ { 𝑋 } ) ) : ( 𝐴 ∖ { 𝑋 } ) ⟶ 𝐵 ↔ ( 𝐹 ↾ ( 𝐴 ∖ { 𝑋 } ) ) : ( 𝐴 ∖ { 𝑋 } ) ⟶ 𝐵 ) )
14 3 13 mpbird ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( 𝐹 ↾ ( V ∖ { 𝑋 } ) ) : ( 𝐴 ∖ { 𝑋 } ) ⟶ 𝐵 )
15 14 adantl ⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → ( 𝐹 ↾ ( V ∖ { 𝑋 } ) ) : ( 𝐴 ∖ { 𝑋 } ) ⟶ 𝐵 )
16 fsnunf2 ⊢ ( ( ( 𝐹 ↾ ( V ∖ { 𝑋 } ) ) : ( 𝐴 ∖ { 𝑋 } ) ⟶ 𝐵 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝐹 ↾ ( V ∖ { 𝑋 } ) ) ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) : 𝐴 ⟶ 𝐵 )
17 15 16 syl3an1 ⊢ ( ( ( 𝐹 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝐹 ↾ ( V ∖ { 𝑋 } ) ) ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) : 𝐴 ⟶ 𝐵 )
18 simp1l ⊢ ( ( ( 𝐹 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) → 𝐹 ∈ 𝑉 )
19 simp3 ⊢ ( ( ( 𝐹 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) → 𝑌 ∈ 𝐵 )
20 setsval ⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝑌 ∈ 𝐵 ) → ( 𝐹 sSet ⟨ 𝑋 , 𝑌 ⟩ ) = ( ( 𝐹 ↾ ( V ∖ { 𝑋 } ) ) ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) )
21 20 feq1d ⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝐹 sSet ⟨ 𝑋 , 𝑌 ⟩ ) : 𝐴 ⟶ 𝐵 ↔ ( ( 𝐹 ↾ ( V ∖ { 𝑋 } ) ) ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) : 𝐴 ⟶ 𝐵 ) )
22 18 19 21 syl2anc ⊢ ( ( ( 𝐹 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝐹 sSet ⟨ 𝑋 , 𝑌 ⟩ ) : 𝐴 ⟶ 𝐵 ↔ ( ( 𝐹 ↾ ( V ∖ { 𝑋 } ) ) ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) : 𝐴 ⟶ 𝐵 ) )
23 17 22 mpbird ⊢ ( ( ( 𝐹 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) → ( 𝐹 sSet ⟨ 𝑋 , 𝑌 ⟩ ) : 𝐴 ⟶ 𝐵 )