This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( dom 𝐹 ∖ ( 𝐹 supp 𝑍 ) ) = ( ◡ 𝐹 “ { 𝑍 } ) )

Proof

Step Hyp Ref Expression
1 eldif ⊢ ( 𝑥 ∈ ( dom 𝐹 ∖ ( 𝐹 supp 𝑍 ) ) ↔ ( 𝑥 ∈ dom 𝐹 ∧ ¬ 𝑥 ∈ ( 𝐹 supp 𝑍 ) ) )
2 funfn ⊢ ( Fun 𝐹 ↔ 𝐹 Fn dom 𝐹 )
3 2 biimpi ⊢ ( Fun 𝐹 → 𝐹 Fn dom 𝐹 )
4 elsuppfng ⊢ ( ( 𝐹 Fn dom 𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( 𝑥 ∈ ( 𝐹 supp 𝑍 ) ↔ ( 𝑥 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑥 ) ≠ 𝑍 ) ) )
5 3 4 syl3an1 ⊢ ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( 𝑥 ∈ ( 𝐹 supp 𝑍 ) ↔ ( 𝑥 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑥 ) ≠ 𝑍 ) ) )
6 5 baibd ⊢ ( ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ 𝑥 ∈ dom 𝐹 ) → ( 𝑥 ∈ ( 𝐹 supp 𝑍 ) ↔ ( 𝐹 ‘ 𝑥 ) ≠ 𝑍 ) )
7 6 notbid ⊢ ( ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ 𝑥 ∈ dom 𝐹 ) → ( ¬ 𝑥 ∈ ( 𝐹 supp 𝑍 ) ↔ ¬ ( 𝐹 ‘ 𝑥 ) ≠ 𝑍 ) )
8 nne ⊢ ( ¬ ( 𝐹 ‘ 𝑥 ) ≠ 𝑍 ↔ ( 𝐹 ‘ 𝑥 ) = 𝑍 )
9 7 8 bitrdi ⊢ ( ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ 𝑥 ∈ dom 𝐹 ) → ( ¬ 𝑥 ∈ ( 𝐹 supp 𝑍 ) ↔ ( 𝐹 ‘ 𝑥 ) = 𝑍 ) )
10 fvex ⊢ ( 𝐹 ‘ 𝑥 ) ∈ V
11 10 elsn ⊢ ( ( 𝐹 ‘ 𝑥 ) ∈ { 𝑍 } ↔ ( 𝐹 ‘ 𝑥 ) = 𝑍 )
12 9 11 bitr4di ⊢ ( ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ 𝑥 ∈ dom 𝐹 ) → ( ¬ 𝑥 ∈ ( 𝐹 supp 𝑍 ) ↔ ( 𝐹 ‘ 𝑥 ) ∈ { 𝑍 } ) )
13 12 pm5.32da ⊢ ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( ( 𝑥 ∈ dom 𝐹 ∧ ¬ 𝑥 ∈ ( 𝐹 supp 𝑍 ) ) ↔ ( 𝑥 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑥 ) ∈ { 𝑍 } ) ) )
14 1 13 bitrid ⊢ ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( 𝑥 ∈ ( dom 𝐹 ∖ ( 𝐹 supp 𝑍 ) ) ↔ ( 𝑥 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑥 ) ∈ { 𝑍 } ) ) )
15 3 3ad2ant1 ⊢ ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → 𝐹 Fn dom 𝐹 )
16 elpreima ⊢ ( 𝐹 Fn dom 𝐹 → ( 𝑥 ∈ ( ◡ 𝐹 “ { 𝑍 } ) ↔ ( 𝑥 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑥 ) ∈ { 𝑍 } ) ) )
17 15 16 syl ⊢ ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( 𝑥 ∈ ( ◡ 𝐹 “ { 𝑍 } ) ↔ ( 𝑥 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑥 ) ∈ { 𝑍 } ) ) )
18 14 17 bitr4d ⊢ ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( 𝑥 ∈ ( dom 𝐹 ∖ ( 𝐹 supp 𝑍 ) ) ↔ 𝑥 ∈ ( ◡ 𝐹 “ { 𝑍 } ) ) )
19 18 eqrdv ⊢ ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( dom 𝐹 ∖ ( 𝐹 supp 𝑍 ) ) = ( ◡ 𝐹 “ { 𝑍 } ) )