Metamath Proof Explorer

Theorem fressupp

Description: The restriction of a function to its support. (Contributed by Thierry Arnoux, 25-Jun-2024)

Ref Expression
Assertion fressupp ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( 𝐹 ↾ ( 𝐹 supp 𝑍 ) ) = ( 𝐹 ∖ ( V × { 𝑍 } ) ) )

Proof

Step Hyp Ref Expression
1 funrel ⊢ ( Fun 𝐹 → Rel 𝐹 )
2 1 3ad2ant1 ⊢ ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → Rel 𝐹 )
3 suppssdm ⊢ ( 𝐹 supp 𝑍 ) ⊆ dom 𝐹
4 undif ⊢ ( ( 𝐹 supp 𝑍 ) ⊆ dom 𝐹 ↔ ( ( 𝐹 supp 𝑍 ) ∪ ( dom 𝐹 ∖ ( 𝐹 supp 𝑍 ) ) ) = dom 𝐹 )
5 4 biimpi ⊢ ( ( 𝐹 supp 𝑍 ) ⊆ dom 𝐹 → ( ( 𝐹 supp 𝑍 ) ∪ ( dom 𝐹 ∖ ( 𝐹 supp 𝑍 ) ) ) = dom 𝐹 )
6 5 eqcomd ⊢ ( ( 𝐹 supp 𝑍 ) ⊆ dom 𝐹 → dom 𝐹 = ( ( 𝐹 supp 𝑍 ) ∪ ( dom 𝐹 ∖ ( 𝐹 supp 𝑍 ) ) ) )
7 3 6 mp1i ⊢ ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → dom 𝐹 = ( ( 𝐹 supp 𝑍 ) ∪ ( dom 𝐹 ∖ ( 𝐹 supp 𝑍 ) ) ) )
8 reldmun ⊢ ( ( Rel 𝐹 ∧ dom 𝐹 = ( ( 𝐹 supp 𝑍 ) ∪ ( dom 𝐹 ∖ ( 𝐹 supp 𝑍 ) ) ) ) → 𝐹 = ( ( 𝐹 ↾ ( 𝐹 supp 𝑍 ) ) ∪ ( 𝐹 ↾ ( dom 𝐹 ∖ ( 𝐹 supp 𝑍 ) ) ) ) )
9 2 7 8 syl2anc ⊢ ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → 𝐹 = ( ( 𝐹 ↾ ( 𝐹 supp 𝑍 ) ) ∪ ( 𝐹 ↾ ( dom 𝐹 ∖ ( 𝐹 supp 𝑍 ) ) ) ) )
10 9 difeq1d ⊢ ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( 𝐹 ∖ ( 𝐹 ↾ ( dom 𝐹 ∖ ( 𝐹 supp 𝑍 ) ) ) ) = ( ( ( 𝐹 ↾ ( 𝐹 supp 𝑍 ) ) ∪ ( 𝐹 ↾ ( dom 𝐹 ∖ ( 𝐹 supp 𝑍 ) ) ) ) ∖ ( 𝐹 ↾ ( dom 𝐹 ∖ ( 𝐹 supp 𝑍 ) ) ) ) )
11 resss ⊢ ( 𝐹 ↾ ( dom 𝐹 ∖ ( 𝐹 supp 𝑍 ) ) ) ⊆ 𝐹
12 sseqin2 ⊢ ( ( 𝐹 ↾ ( dom 𝐹 ∖ ( 𝐹 supp 𝑍 ) ) ) ⊆ 𝐹 ↔ ( 𝐹 ∩ ( 𝐹 ↾ ( dom 𝐹 ∖ ( 𝐹 supp 𝑍 ) ) ) ) = ( 𝐹 ↾ ( dom 𝐹 ∖ ( 𝐹 supp 𝑍 ) ) ) )
13 11 12 mpbi ⊢ ( 𝐹 ∩ ( 𝐹 ↾ ( dom 𝐹 ∖ ( 𝐹 supp 𝑍 ) ) ) ) = ( 𝐹 ↾ ( dom 𝐹 ∖ ( 𝐹 supp 𝑍 ) ) )
14 suppiniseg ⊢ ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( dom 𝐹 ∖ ( 𝐹 supp 𝑍 ) ) = ( ◡ 𝐹 “ { 𝑍 } ) )
15 14 reseq2d ⊢ ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( 𝐹 ↾ ( dom 𝐹 ∖ ( 𝐹 supp 𝑍 ) ) ) = ( 𝐹 ↾ ( ◡ 𝐹 “ { 𝑍 } ) ) )
16 cnvrescnv ⊢ ◡ ( ◡ 𝐹 ↾ { 𝑍 } ) = ( 𝐹 ∩ ( V × { 𝑍 } ) )
17 funcnvres2 ⊢ ( Fun 𝐹 → ◡ ( ◡ 𝐹 ↾ { 𝑍 } ) = ( 𝐹 ↾ ( ◡ 𝐹 “ { 𝑍 } ) ) )
18 16 17 eqtr3id ⊢ ( Fun 𝐹 → ( 𝐹 ∩ ( V × { 𝑍 } ) ) = ( 𝐹 ↾ ( ◡ 𝐹 “ { 𝑍 } ) ) )
19 18 3ad2ant1 ⊢ ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( 𝐹 ∩ ( V × { 𝑍 } ) ) = ( 𝐹 ↾ ( ◡ 𝐹 “ { 𝑍 } ) ) )
20 15 19 eqtr4d ⊢ ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( 𝐹 ↾ ( dom 𝐹 ∖ ( 𝐹 supp 𝑍 ) ) ) = ( 𝐹 ∩ ( V × { 𝑍 } ) ) )
21 13 20 eqtrid ⊢ ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( 𝐹 ∩ ( 𝐹 ↾ ( dom 𝐹 ∖ ( 𝐹 supp 𝑍 ) ) ) ) = ( 𝐹 ∩ ( V × { 𝑍 } ) ) )
22 indifbi ⊢ ( ( 𝐹 ∩ ( 𝐹 ↾ ( dom 𝐹 ∖ ( 𝐹 supp 𝑍 ) ) ) ) = ( 𝐹 ∩ ( V × { 𝑍 } ) ) ↔ ( 𝐹 ∖ ( 𝐹 ↾ ( dom 𝐹 ∖ ( 𝐹 supp 𝑍 ) ) ) ) = ( 𝐹 ∖ ( V × { 𝑍 } ) ) )
23 21 22 sylib ⊢ ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( 𝐹 ∖ ( 𝐹 ↾ ( dom 𝐹 ∖ ( 𝐹 supp 𝑍 ) ) ) ) = ( 𝐹 ∖ ( V × { 𝑍 } ) ) )
24 disjdif ⊢ ( ( 𝐹 supp 𝑍 ) ∩ ( dom 𝐹 ∖ ( 𝐹 supp 𝑍 ) ) ) = ∅
25 24 reseq2i ⊢ ( 𝐹 ↾ ( ( 𝐹 supp 𝑍 ) ∩ ( dom 𝐹 ∖ ( 𝐹 supp 𝑍 ) ) ) ) = ( 𝐹 ↾ ∅ )
26 resindi ⊢ ( 𝐹 ↾ ( ( 𝐹 supp 𝑍 ) ∩ ( dom 𝐹 ∖ ( 𝐹 supp 𝑍 ) ) ) ) = ( ( 𝐹 ↾ ( 𝐹 supp 𝑍 ) ) ∩ ( 𝐹 ↾ ( dom 𝐹 ∖ ( 𝐹 supp 𝑍 ) ) ) )
27 res0 ⊢ ( 𝐹 ↾ ∅ ) = ∅
28 25 26 27 3eqtr3i ⊢ ( ( 𝐹 ↾ ( 𝐹 supp 𝑍 ) ) ∩ ( 𝐹 ↾ ( dom 𝐹 ∖ ( 𝐹 supp 𝑍 ) ) ) ) = ∅
29 undif5 ⊢ ( ( ( 𝐹 ↾ ( 𝐹 supp 𝑍 ) ) ∩ ( 𝐹 ↾ ( dom 𝐹 ∖ ( 𝐹 supp 𝑍 ) ) ) ) = ∅ → ( ( ( 𝐹 ↾ ( 𝐹 supp 𝑍 ) ) ∪ ( 𝐹 ↾ ( dom 𝐹 ∖ ( 𝐹 supp 𝑍 ) ) ) ) ∖ ( 𝐹 ↾ ( dom 𝐹 ∖ ( 𝐹 supp 𝑍 ) ) ) ) = ( 𝐹 ↾ ( 𝐹 supp 𝑍 ) ) )
30 28 29 mp1i ⊢ ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( ( ( 𝐹 ↾ ( 𝐹 supp 𝑍 ) ) ∪ ( 𝐹 ↾ ( dom 𝐹 ∖ ( 𝐹 supp 𝑍 ) ) ) ) ∖ ( 𝐹 ↾ ( dom 𝐹 ∖ ( 𝐹 supp 𝑍 ) ) ) ) = ( 𝐹 ↾ ( 𝐹 supp 𝑍 ) ) )
31 10 23 30 3eqtr3rd ⊢ ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( 𝐹 ↾ ( 𝐹 supp 𝑍 ) ) = ( 𝐹 ∖ ( V × { 𝑍 } ) ) )