Metamath Proof Explorer

Theorem frnsuppeqg

Description: Version of frnsuppeq avoiding ax-rep by assuming F is a set rather than its domain I . (Contributed by SN, 30-Jul-2024)

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

Proof

Step Hyp Ref Expression
1 suppimacnv ⊢ F ∈ V ∧ Z ∈ W → F supp Z = F -1 V ∖ Z
2 ffun ⊢ F : I ⟶ S → Fun ⁡ F
3 inpreima ⊢ Fun ⁡ F → F -1 S ∩ V ∖ Z = F -1 S ∩ F -1 V ∖ Z
4 2 3 syl ⊢ F : I ⟶ S → F -1 S ∩ V ∖ Z = F -1 S ∩ F -1 V ∖ Z
5 cnvimass ⊢ F -1 V ∖ Z ⊆ dom ⁡ F
6 fdm ⊢ F : I ⟶ S → dom ⁡ F = I
7 fimacnv ⊢ F : I ⟶ S → F -1 S = I
8 6 7 eqtr4d ⊢ F : I ⟶ S → dom ⁡ F = F -1 S
9 5 8 sseqtrid ⊢ F : I ⟶ S → F -1 V ∖ Z ⊆ F -1 S
10 sseqin2 ⊢ F -1 V ∖ Z ⊆ F -1 S ↔ F -1 S ∩ F -1 V ∖ Z = F -1 V ∖ Z
11 9 10 sylib ⊢ F : I ⟶ S → F -1 S ∩ F -1 V ∖ Z = F -1 V ∖ Z
12 4 11 eqtrd ⊢ F : I ⟶ S → F -1 S ∩ V ∖ Z = F -1 V ∖ Z
13 invdif ⊢ S ∩ V ∖ Z = S ∖ Z
14 13 imaeq2i ⊢ F -1 S ∩ V ∖ Z = F -1 S ∖ Z
15 12 14 eqtr3di ⊢ F : I ⟶ S → F -1 V ∖ Z = F -1 S ∖ Z
16 1 15 sylan9eq ⊢ F ∈ V ∧ Z ∈ W ∧ F : I ⟶ S → F supp Z = F -1 S ∖ Z
17 16 ex ⊢ F ∈ V ∧ Z ∈ W → F : I ⟶ S → F supp Z = F -1 S ∖ Z