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 disjdif ⊢ ( ( 𝐹 supp 𝑍 ) ∩ ( dom 𝐹 ∖ ( 𝐹 supp 𝑍 ) ) ) = ∅
9 8 a1i ⊢ ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( ( 𝐹 supp 𝑍 ) ∩ ( dom 𝐹 ∖ ( 𝐹 supp 𝑍 ) ) ) = ∅ )
10 reldisjun ⊢ ( ( Rel 𝐹 ∧ dom 𝐹 = ( ( 𝐹 supp 𝑍 ) ∪ ( dom 𝐹 ∖ ( 𝐹 supp 𝑍 ) ) ) ∧ ( ( 𝐹 supp 𝑍 ) ∩ ( dom 𝐹 ∖ ( 𝐹 supp 𝑍 ) ) ) = ∅ ) → 𝐹 = ( ( 𝐹 ↾ ( 𝐹 supp 𝑍 ) ) ∪ ( 𝐹 ↾ ( dom 𝐹 ∖ ( 𝐹 supp 𝑍 ) ) ) ) )
11 2 7 9 10 syl3anc ⊢ ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → 𝐹 = ( ( 𝐹 ↾ ( 𝐹 supp 𝑍 ) ) ∪ ( 𝐹 ↾ ( dom 𝐹 ∖ ( 𝐹 supp 𝑍 ) ) ) ) )
12 11 difeq1d ⊢ ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( 𝐹 ∖ ( 𝐹 ↾ ( dom 𝐹 ∖ ( 𝐹 supp 𝑍 ) ) ) ) = ( ( ( 𝐹 ↾ ( 𝐹 supp 𝑍 ) ) ∪ ( 𝐹 ↾ ( dom 𝐹 ∖ ( 𝐹 supp 𝑍 ) ) ) ) ∖ ( 𝐹 ↾ ( dom 𝐹 ∖ ( 𝐹 supp 𝑍 ) ) ) ) )
13 resss ⊢ ( 𝐹 ↾ ( dom 𝐹 ∖ ( 𝐹 supp 𝑍 ) ) ) ⊆ 𝐹
14 sseqin2 ⊢ ( ( 𝐹 ↾ ( dom 𝐹 ∖ ( 𝐹 supp 𝑍 ) ) ) ⊆ 𝐹 ↔ ( 𝐹 ∩ ( 𝐹 ↾ ( dom 𝐹 ∖ ( 𝐹 supp 𝑍 ) ) ) ) = ( 𝐹 ↾ ( dom 𝐹 ∖ ( 𝐹 supp 𝑍 ) ) ) )
15 13 14 mpbi ⊢ ( 𝐹 ∩ ( 𝐹 ↾ ( dom 𝐹 ∖ ( 𝐹 supp 𝑍 ) ) ) ) = ( 𝐹 ↾ ( dom 𝐹 ∖ ( 𝐹 supp 𝑍 ) ) )
16 suppiniseg ⊢ ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( dom 𝐹 ∖ ( 𝐹 supp 𝑍 ) ) = ( ◡ 𝐹 “ { 𝑍 } ) )
17 16 reseq2d ⊢ ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( 𝐹 ↾ ( dom 𝐹 ∖ ( 𝐹 supp 𝑍 ) ) ) = ( 𝐹 ↾ ( ◡ 𝐹 “ { 𝑍 } ) ) )
18 cnvrescnv ⊢ ◡ ( ◡ 𝐹 ↾ { 𝑍 } ) = ( 𝐹 ∩ ( V × { 𝑍 } ) )
19 funcnvres2 ⊢ ( Fun 𝐹 → ◡ ( ◡ 𝐹 ↾ { 𝑍 } ) = ( 𝐹 ↾ ( ◡ 𝐹 “ { 𝑍 } ) ) )
20 18 19 eqtr3id ⊢ ( Fun 𝐹 → ( 𝐹 ∩ ( V × { 𝑍 } ) ) = ( 𝐹 ↾ ( ◡ 𝐹 “ { 𝑍 } ) ) )
21 20 3ad2ant1 ⊢ ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( 𝐹 ∩ ( V × { 𝑍 } ) ) = ( 𝐹 ↾ ( ◡ 𝐹 “ { 𝑍 } ) ) )
22 17 21 eqtr4d ⊢ ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( 𝐹 ↾ ( dom 𝐹 ∖ ( 𝐹 supp 𝑍 ) ) ) = ( 𝐹 ∩ ( V × { 𝑍 } ) ) )
23 15 22 syl5eq ⊢ ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( 𝐹 ∩ ( 𝐹 ↾ ( dom 𝐹 ∖ ( 𝐹 supp 𝑍 ) ) ) ) = ( 𝐹 ∩ ( V × { 𝑍 } ) ) )
24 indifbi ⊢ ( ( 𝐹 ∩ ( 𝐹 ↾ ( dom 𝐹 ∖ ( 𝐹 supp 𝑍 ) ) ) ) = ( 𝐹 ∩ ( V × { 𝑍 } ) ) ↔ ( 𝐹 ∖ ( 𝐹 ↾ ( dom 𝐹 ∖ ( 𝐹 supp 𝑍 ) ) ) ) = ( 𝐹 ∖ ( V × { 𝑍 } ) ) )
25 23 24 sylib ⊢ ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( 𝐹 ∖ ( 𝐹 ↾ ( dom 𝐹 ∖ ( 𝐹 supp 𝑍 ) ) ) ) = ( 𝐹 ∖ ( V × { 𝑍 } ) ) )
26 8 reseq2i ⊢ ( 𝐹 ↾ ( ( 𝐹 supp 𝑍 ) ∩ ( dom 𝐹 ∖ ( 𝐹 supp 𝑍 ) ) ) ) = ( 𝐹 ↾ ∅ )
27 resindi ⊢ ( 𝐹 ↾ ( ( 𝐹 supp 𝑍 ) ∩ ( dom 𝐹 ∖ ( 𝐹 supp 𝑍 ) ) ) ) = ( ( 𝐹 ↾ ( 𝐹 supp 𝑍 ) ) ∩ ( 𝐹 ↾ ( dom 𝐹 ∖ ( 𝐹 supp 𝑍 ) ) ) )
28 res0 ⊢ ( 𝐹 ↾ ∅ ) = ∅
29 26 27 28 3eqtr3i ⊢ ( ( 𝐹 ↾ ( 𝐹 supp 𝑍 ) ) ∩ ( 𝐹 ↾ ( dom 𝐹 ∖ ( 𝐹 supp 𝑍 ) ) ) ) = ∅
30 undif5 ⊢ ( ( ( 𝐹 ↾ ( 𝐹 supp 𝑍 ) ) ∩ ( 𝐹 ↾ ( dom 𝐹 ∖ ( 𝐹 supp 𝑍 ) ) ) ) = ∅ → ( ( ( 𝐹 ↾ ( 𝐹 supp 𝑍 ) ) ∪ ( 𝐹 ↾ ( dom 𝐹 ∖ ( 𝐹 supp 𝑍 ) ) ) ) ∖ ( 𝐹 ↾ ( dom 𝐹 ∖ ( 𝐹 supp 𝑍 ) ) ) ) = ( 𝐹 ↾ ( 𝐹 supp 𝑍 ) ) )
31 29 30 mp1i ⊢ ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( ( ( 𝐹 ↾ ( 𝐹 supp 𝑍 ) ) ∪ ( 𝐹 ↾ ( dom 𝐹 ∖ ( 𝐹 supp 𝑍 ) ) ) ) ∖ ( 𝐹 ↾ ( dom 𝐹 ∖ ( 𝐹 supp 𝑍 ) ) ) ) = ( 𝐹 ↾ ( 𝐹 supp 𝑍 ) ) )
32 12 25 31 3eqtr3rd ⊢ ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( 𝐹 ↾ ( 𝐹 supp 𝑍 ) ) = ( 𝐹 ∖ ( V × { 𝑍 } ) ) )