Metamath Proof Explorer


Theorem fnsuppeq0

Description: The support of a function is empty iff it is identically zero. (Contributed by Stefan O'Rear, 22-Mar-2015) (Revised by AV, 28-May-2019)

Ref Expression
Assertion fnsuppeq0 F Fn A A W Z V F supp Z = F = A × Z

Proof

Step Hyp Ref Expression
1 ss0b F supp Z F supp Z =
2 un0 A = A
3 uncom A = A
4 2 3 eqtr3i A = A
5 4 fneq2i F Fn A F Fn A
6 5 biimpi F Fn A F Fn A
7 6 3ad2ant1 F Fn A A W Z V F Fn A
8 fnex F Fn A A W F V
9 8 3adant3 F Fn A A W Z V F V
10 simp3 F Fn A A W Z V Z V
11 0in A =
12 11 a1i F Fn A A W Z V A =
13 fnsuppres F Fn A F V Z V A = F supp Z F A = A × Z
14 7 9 10 12 13 syl121anc F Fn A A W Z V F supp Z F A = A × Z
15 1 14 syl5bbr F Fn A A W Z V F supp Z = F A = A × Z
16 fnresdm F Fn A F A = F
17 16 3ad2ant1 F Fn A A W Z V F A = F
18 17 eqeq1d F Fn A A W Z V F A = A × Z F = A × Z
19 15 18 bitrd F Fn A A W Z V F supp Z = F = A × Z