Metamath Proof Explorer

Theorem frnsuppeq

Description: Two ways of writing the support of a function with known codomain. (Contributed by Stefan O'Rear, 9-Jul-2015) (Revised by AV, 7-Jul-2019)

Ref Expression
Assertion frnsuppeq ⊢ I ∈ V ∧ Z ∈ W → F : I ⟶ S → F supp Z = F -1 S ∖ Z

Proof

Step Hyp Ref Expression
1 fex ⊢ F : I ⟶ S ∧ I ∈ V → F ∈ V
2 1 expcom ⊢ I ∈ V → F : I ⟶ S → F ∈ V
3 2 adantr ⊢ I ∈ V ∧ Z ∈ W → F : I ⟶ S → F ∈ V
4 3 imp ⊢ I ∈ V ∧ Z ∈ W ∧ F : I ⟶ S → F ∈ V
5 simplr ⊢ I ∈ V ∧ Z ∈ W ∧ F : I ⟶ S → Z ∈ W
6 suppimacnv ⊢ F ∈ V ∧ Z ∈ W → F supp Z = F -1 V ∖ Z
7 4 5 6 syl2anc ⊢ I ∈ V ∧ Z ∈ W ∧ F : I ⟶ S → F supp Z = F -1 V ∖ Z
8 invdif ⊢ S ∩ V ∖ Z = S ∖ Z
9 8 imaeq2i ⊢ F -1 S ∩ V ∖ Z = F -1 S ∖ Z
10 ffun ⊢ F : I ⟶ S → Fun ⁡ F
11 inpreima ⊢ Fun ⁡ F → F -1 S ∩ V ∖ Z = F -1 S ∩ F -1 V ∖ Z
12 10 11 syl ⊢ F : I ⟶ S → F -1 S ∩ V ∖ Z = F -1 S ∩ F -1 V ∖ Z
13 cnvimass ⊢ F -1 V ∖ Z ⊆ dom ⁡ F
14 fdm ⊢ F : I ⟶ S → dom ⁡ F = I
15 fimacnv ⊢ F : I ⟶ S → F -1 S = I
16 14 15 eqtr4d ⊢ F : I ⟶ S → dom ⁡ F = F -1 S
17 13 16 sseqtrid ⊢ F : I ⟶ S → F -1 V ∖ Z ⊆ F -1 S
18 sseqin2 ⊢ F -1 V ∖ Z ⊆ F -1 S ↔ F -1 S ∩ F -1 V ∖ Z = F -1 V ∖ Z
19 17 18 sylib ⊢ F : I ⟶ S → F -1 S ∩ F -1 V ∖ Z = F -1 V ∖ Z
20 12 19 eqtrd ⊢ F : I ⟶ S → F -1 S ∩ V ∖ Z = F -1 V ∖ Z
21 9 20 syl5reqr ⊢ F : I ⟶ S → F -1 V ∖ Z = F -1 S ∖ Z
22 21 adantl ⊢ I ∈ V ∧ Z ∈ W ∧ F : I ⟶ S → F -1 V ∖ Z = F -1 S ∖ Z
23 7 22 eqtrd ⊢ I ∈ V ∧ Z ∈ W ∧ F : I ⟶ S → F supp Z = F -1 S ∖ Z
24 23 ex ⊢ I ∈ V ∧ Z ∈ W → F : I ⟶ S → F supp Z = F -1 S ∖ Z