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 resres ⊢ ( ( 𝐹 ↾ 𝐴 ) ↾ ( V ∖ { 𝑋 } ) ) = ( 𝐹 ↾ ( 𝐴 ∩ ( V ∖ { 𝑋 } ) ) )
5 invdif ⊢ ( 𝐴 ∩ ( V ∖ { 𝑋 } ) ) = ( 𝐴 ∖ { 𝑋 } )
6 5 reseq2i ⊢ ( 𝐹 ↾ ( 𝐴 ∩ ( V ∖ { 𝑋 } ) ) ) = ( 𝐹 ↾ ( 𝐴 ∖ { 𝑋 } ) )
7 4 6 eqtri ⊢ ( ( 𝐹 ↾ 𝐴 ) ↾ ( V ∖ { 𝑋 } ) ) = ( 𝐹 ↾ ( 𝐴 ∖ { 𝑋 } ) )
8 ffn ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → 𝐹 Fn 𝐴 )
9 fnresdm ⊢ ( 𝐹 Fn 𝐴 → ( 𝐹 ↾ 𝐴 ) = 𝐹 )
10 8 9 syl ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( 𝐹 ↾ 𝐴 ) = 𝐹 )
11 10 reseq1d ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( ( 𝐹 ↾ 𝐴 ) ↾ ( V ∖ { 𝑋 } ) ) = ( 𝐹 ↾ ( V ∖ { 𝑋 } ) ) )
12 7 11 syl5reqr ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( 𝐹 ↾ ( 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 ⟨ 𝑋 , 𝑌 ⟩ ) : 𝐴 ⟶ 𝐵 )