Metamath Proof Explorer


Theorem suppssrg

Description: A function is zero outside its support. Version of suppssr avoiding ax-rep by assuming F is a set rather than its domain A . (Contributed by SN, 5-May-2024)

Ref Expression
Hypotheses suppssrg.f ( 𝜑𝐹 : 𝐴𝐵 )
suppssrg.n ( 𝜑 → ( 𝐹 supp 𝑍 ) ⊆ 𝑊 )
suppssrg.a ( 𝜑𝐹𝑉 )
suppssrg.z ( 𝜑𝑍𝑈 )
Assertion suppssrg ( ( 𝜑𝑋 ∈ ( 𝐴𝑊 ) ) → ( 𝐹𝑋 ) = 𝑍 )

Proof

Step Hyp Ref Expression
1 suppssrg.f ( 𝜑𝐹 : 𝐴𝐵 )
2 suppssrg.n ( 𝜑 → ( 𝐹 supp 𝑍 ) ⊆ 𝑊 )
3 suppssrg.a ( 𝜑𝐹𝑉 )
4 suppssrg.z ( 𝜑𝑍𝑈 )
5 eldif ( 𝑋 ∈ ( 𝐴𝑊 ) ↔ ( 𝑋𝐴 ∧ ¬ 𝑋𝑊 ) )
6 1 ffnd ( 𝜑𝐹 Fn 𝐴 )
7 elsuppfng ( ( 𝐹 Fn 𝐴𝐹𝑉𝑍𝑈 ) → ( 𝑋 ∈ ( 𝐹 supp 𝑍 ) ↔ ( 𝑋𝐴 ∧ ( 𝐹𝑋 ) ≠ 𝑍 ) ) )
8 6 3 4 7 syl3anc ( 𝜑 → ( 𝑋 ∈ ( 𝐹 supp 𝑍 ) ↔ ( 𝑋𝐴 ∧ ( 𝐹𝑋 ) ≠ 𝑍 ) ) )
9 2 sseld ( 𝜑 → ( 𝑋 ∈ ( 𝐹 supp 𝑍 ) → 𝑋𝑊 ) )
10 8 9 sylbird ( 𝜑 → ( ( 𝑋𝐴 ∧ ( 𝐹𝑋 ) ≠ 𝑍 ) → 𝑋𝑊 ) )
11 10 expdimp ( ( 𝜑𝑋𝐴 ) → ( ( 𝐹𝑋 ) ≠ 𝑍𝑋𝑊 ) )
12 11 necon1bd ( ( 𝜑𝑋𝐴 ) → ( ¬ 𝑋𝑊 → ( 𝐹𝑋 ) = 𝑍 ) )
13 12 impr ( ( 𝜑 ∧ ( 𝑋𝐴 ∧ ¬ 𝑋𝑊 ) ) → ( 𝐹𝑋 ) = 𝑍 )
14 5 13 sylan2b ( ( 𝜑𝑋 ∈ ( 𝐴𝑊 ) ) → ( 𝐹𝑋 ) = 𝑍 )