Metamath Proof Explorer

Theorem suppss3

Description: Deduce a function's support's inclusion in another function's support. (Contributed by Thierry Arnoux, 7-Sep-2017) (Revised by Thierry Arnoux, 1-Sep-2019)

Ref Expression
Hypotheses suppss3.1 ⊢ G = x ∈ A ⟼ B
suppss3.a ⊢ φ → A ∈ V
suppss3.z ⊢ φ → Z ∈ W
suppss3.2 ⊢ φ → F Fn A
suppss3.3 ⊢ φ ∧ x ∈ A ∧ F ⁡ x = Z → B = Z
Assertion suppss3 ⊢ φ → G supp Z ⊆ F supp Z

Proof

Step Hyp Ref Expression
1 suppss3.1 ⊢ G = x ∈ A ⟼ B
2 suppss3.a ⊢ φ → A ∈ V
3 suppss3.z ⊢ φ → Z ∈ W
4 suppss3.2 ⊢ φ → F Fn A
5 suppss3.3 ⊢ φ ∧ x ∈ A ∧ F ⁡ x = Z → B = Z
6 1 oveq1i ⊢ G supp Z = x ∈ A ⟼ B supp Z
7 simpl ⊢ φ ∧ x ∈ A ∖ supp Z⁡ F → φ
8 eldifi ⊢ x ∈ A ∖ supp Z⁡ F → x ∈ A
9 8 adantl ⊢ φ ∧ x ∈ A ∖ supp Z⁡ F → x ∈ A
10 fnex ⊢ F Fn A ∧ A ∈ V → F ∈ V
11 4 2 10 syl2anc ⊢ φ → F ∈ V
12 suppimacnv ⊢ F ∈ V ∧ Z ∈ W → F supp Z = F -1 V ∖ Z
13 11 3 12 syl2anc ⊢ φ → F supp Z = F -1 V ∖ Z
14 13 eleq2d ⊢ φ → x ∈ supp Z⁡ F ↔ x ∈ F -1 V ∖ Z
15 elpreima ⊢ F Fn A → x ∈ F -1 V ∖ Z ↔ x ∈ A ∧ F ⁡ x ∈ V ∖ Z
16 4 15 syl ⊢ φ → x ∈ F -1 V ∖ Z ↔ x ∈ A ∧ F ⁡ x ∈ V ∖ Z
17 14 16 bitrd ⊢ φ → x ∈ supp Z⁡ F ↔ x ∈ A ∧ F ⁡ x ∈ V ∖ Z
18 17 baibd ⊢ φ ∧ x ∈ A → x ∈ supp Z⁡ F ↔ F ⁡ x ∈ V ∖ Z
19 18 notbid ⊢ φ ∧ x ∈ A → ¬ x ∈ supp Z⁡ F ↔ ¬ F ⁡ x ∈ V ∖ Z
20 19 biimpd ⊢ φ ∧ x ∈ A → ¬ x ∈ supp Z⁡ F → ¬ F ⁡ x ∈ V ∖ Z
21 20 expimpd ⊢ φ → x ∈ A ∧ ¬ x ∈ supp Z⁡ F → ¬ F ⁡ x ∈ V ∖ Z
22 eldif ⊢ x ∈ A ∖ supp Z⁡ F ↔ x ∈ A ∧ ¬ x ∈ supp Z⁡ F
23 fvex ⊢ F ⁡ x ∈ V
24 eldifsn ⊢ F ⁡ x ∈ V ∖ Z ↔ F ⁡ x ∈ V ∧ F ⁡ x ≠ Z
25 23 24 mpbiran ⊢ F ⁡ x ∈ V ∖ Z ↔ F ⁡ x ≠ Z
26 25 necon2bbii ⊢ F ⁡ x = Z ↔ ¬ F ⁡ x ∈ V ∖ Z
27 21 22 26 3imtr4g ⊢ φ → x ∈ A ∖ supp Z⁡ F → F ⁡ x = Z
28 27 imp ⊢ φ ∧ x ∈ A ∖ supp Z⁡ F → F ⁡ x = Z
29 7 9 28 5 syl3anc ⊢ φ ∧ x ∈ A ∖ supp Z⁡ F → B = Z
30 29 2 suppss2 ⊢ φ → x ∈ A ⟼ B supp Z ⊆ F supp Z
31 6 30 eqsstrid ⊢ φ → G supp Z ⊆ F supp Z