Metamath Proof Explorer

Theorem suppiniseg

Description: Relation between the support ( F supp Z ) and the initial segment (`' F " { Z } ) ` . (Contributed by Thierry Arnoux, 25-Jun-2024)

Ref Expression
Assertion suppiniseg ⊢ Fun ⁡ F ∧ F ∈ V ∧ Z ∈ W → dom ⁡ F ∖ supp Z⁡ F = F -1 Z

Proof

Step Hyp Ref Expression
1 eldif ⊢ x ∈ dom ⁡ F ∖ supp Z⁡ F ↔ x ∈ dom ⁡ F ∧ ¬ x ∈ supp Z⁡ F
2 funfn ⊢ Fun ⁡ F ↔ F Fn dom ⁡ F
3 2 biimpi ⊢ Fun ⁡ F → F Fn dom ⁡ F
4 elsuppfng ⊢ F Fn dom ⁡ F ∧ F ∈ V ∧ Z ∈ W → x ∈ supp Z⁡ F ↔ x ∈ dom ⁡ F ∧ F ⁡ x ≠ Z
5 3 4 syl3an1 ⊢ Fun ⁡ F ∧ F ∈ V ∧ Z ∈ W → x ∈ supp Z⁡ F ↔ x ∈ dom ⁡ F ∧ F ⁡ x ≠ Z
6 5 baibd ⊢ Fun ⁡ F ∧ F ∈ V ∧ Z ∈ W ∧ x ∈ dom ⁡ F → x ∈ supp Z⁡ F ↔ F ⁡ x ≠ Z
7 6 notbid ⊢ Fun ⁡ F ∧ F ∈ V ∧ Z ∈ W ∧ x ∈ dom ⁡ F → ¬ x ∈ supp Z⁡ F ↔ ¬ F ⁡ x ≠ Z
8 nne ⊢ ¬ F ⁡ x ≠ Z ↔ F ⁡ x = Z
9 7 8 bitrdi ⊢ Fun ⁡ F ∧ F ∈ V ∧ Z ∈ W ∧ x ∈ dom ⁡ F → ¬ x ∈ supp Z⁡ F ↔ F ⁡ x = Z
10 fvex ⊢ F ⁡ x ∈ V
11 10 elsn ⊢ F ⁡ x ∈ Z ↔ F ⁡ x = Z
12 9 11 bitr4di ⊢ Fun ⁡ F ∧ F ∈ V ∧ Z ∈ W ∧ x ∈ dom ⁡ F → ¬ x ∈ supp Z⁡ F ↔ F ⁡ x ∈ Z
13 12 pm5.32da ⊢ Fun ⁡ F ∧ F ∈ V ∧ Z ∈ W → x ∈ dom ⁡ F ∧ ¬ x ∈ supp Z⁡ F ↔ x ∈ dom ⁡ F ∧ F ⁡ x ∈ Z
14 1 13 syl5bb ⊢ Fun ⁡ F ∧ F ∈ V ∧ Z ∈ W → x ∈ dom ⁡ F ∖ supp Z⁡ F ↔ x ∈ dom ⁡ F ∧ F ⁡ x ∈ Z
15 3 3ad2ant1 ⊢ Fun ⁡ F ∧ F ∈ V ∧ Z ∈ W → F Fn dom ⁡ F
16 elpreima ⊢ F Fn dom ⁡ F → x ∈ F -1 Z ↔ x ∈ dom ⁡ F ∧ F ⁡ x ∈ Z
17 15 16 syl ⊢ Fun ⁡ F ∧ F ∈ V ∧ Z ∈ W → x ∈ F -1 Z ↔ x ∈ dom ⁡ F ∧ F ⁡ x ∈ Z
18 14 17 bitr4d ⊢ Fun ⁡ F ∧ F ∈ V ∧ Z ∈ W → x ∈ dom ⁡ F ∖ supp Z⁡ F ↔ x ∈ F -1 Z
19 18 eqrdv ⊢ Fun ⁡ F ∧ F ∈ V ∧ Z ∈ W → dom ⁡ F ∖ supp Z⁡ F = F -1 Z