Metamath Proof Explorer

Theorem suppss2f

Description: Show that the support of a function is contained in a set. (Contributed by Thierry Arnoux, 22-Jun-2017) (Revised by AV, 1-Sep-2020)

Ref Expression
Hypotheses suppss2f.p ⊢ Ⅎ k φ
suppss2f.a ⊢ Ⅎ _ k A
suppss2f.w ⊢ Ⅎ _ k W
suppss2f.n ⊢ φ ∧ k ∈ A ∖ W → B = Z
suppss2f.v ⊢ φ → A ∈ V
Assertion suppss2f ⊢ φ → k ∈ A ⟼ B supp Z ⊆ W

Proof

Step Hyp Ref Expression
1 suppss2f.p ⊢ Ⅎ k φ
2 suppss2f.a ⊢ Ⅎ _ k A
3 suppss2f.w ⊢ Ⅎ _ k W
4 suppss2f.n ⊢ φ ∧ k ∈ A ∖ W → B = Z
5 suppss2f.v ⊢ φ → A ∈ V
6 nfcv ⊢ Ⅎ _ l A
7 nfcv ⊢ Ⅎ _ l B
8 nfcsb1v ⊢ Ⅎ _ k ⦋ l / k⦌ B
9 csbeq1a ⊢ k = l → B = ⦋ l / k⦌ B
10 2 6 7 8 9 cbvmptf ⊢ k ∈ A ⟼ B = l ∈ A ⟼ ⦋ l / k⦌ B
11 10 oveq1i ⊢ k ∈ A ⟼ B supp Z = l ∈ A ⟼ ⦋ l / k⦌ B supp Z
12 4 sbt ⊢ l k φ ∧ k ∈ A ∖ W → B = Z
13 sbim ⊢ l k φ ∧ k ∈ A ∖ W → B = Z ↔ l k φ ∧ k ∈ A ∖ W → l k B = Z
14 sban ⊢ l k φ ∧ k ∈ A ∖ W ↔ l k φ ∧ l k k ∈ A ∖ W
15 1 sbf ⊢ l k φ ↔ φ
16 2 3 nfdif ⊢ Ⅎ _ k A ∖ W
17 16 clelsb1fw ⊢ l k k ∈ A ∖ W ↔ l ∈ A ∖ W
18 15 17 anbi12i ⊢ l k φ ∧ l k k ∈ A ∖ W ↔ φ ∧ l ∈ A ∖ W
19 14 18 bitri ⊢ l k φ ∧ k ∈ A ∖ W ↔ φ ∧ l ∈ A ∖ W
20 sbsbc ⊢ l k B = Z ↔ [˙l / k]˙ B = Z
21 sbceq1g ⊢ l ∈ V → [˙l / k]˙ B = Z ↔ ⦋ l / k⦌ B = Z
22 21 elv ⊢ [˙l / k]˙ B = Z ↔ ⦋ l / k⦌ B = Z
23 20 22 bitri ⊢ l k B = Z ↔ ⦋ l / k⦌ B = Z
24 19 23 imbi12i ⊢ l k φ ∧ k ∈ A ∖ W → l k B = Z ↔ φ ∧ l ∈ A ∖ W → ⦋ l / k⦌ B = Z
25 13 24 bitri ⊢ l k φ ∧ k ∈ A ∖ W → B = Z ↔ φ ∧ l ∈ A ∖ W → ⦋ l / k⦌ B = Z
26 12 25 mpbi ⊢ φ ∧ l ∈ A ∖ W → ⦋ l / k⦌ B = Z
27 26 5 suppss2 ⊢ φ → l ∈ A ⟼ ⦋ l / k⦌ B supp Z ⊆ W
28 11 27 eqsstrid ⊢ φ → k ∈ A ⟼ B supp Z ⊆ W