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 ⊢ Ⅎ 𝑘 𝜑
suppss2f.a ⊢ Ⅎ 𝑘 𝐴
suppss2f.w ⊢ Ⅎ 𝑘 𝑊
suppss2f.n ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 ∖ 𝑊 ) ) → 𝐵 = 𝑍 )
suppss2f.v ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
Assertion suppss2f ( 𝜑 → ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) supp 𝑍 ) ⊆ 𝑊 )

Proof

Step Hyp Ref Expression
1 suppss2f.p ⊢ Ⅎ 𝑘 𝜑
2 suppss2f.a ⊢ Ⅎ 𝑘 𝐴
3 suppss2f.w ⊢ Ⅎ 𝑘 𝑊
4 suppss2f.n ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 ∖ 𝑊 ) ) → 𝐵 = 𝑍 )
5 suppss2f.v ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
6 nfcv ⊢ Ⅎ 𝑙 𝐴
7 nfcv ⊢ Ⅎ 𝑙 𝐵
8 nfcsb1v ⊢ Ⅎ 𝑘 ⦋ 𝑙 / 𝑘 ⦌ 𝐵
9 csbeq1a ⊢ ( 𝑘 = 𝑙 → 𝐵 = ⦋ 𝑙 / 𝑘 ⦌ 𝐵 )
10 2 6 7 8 9 cbvmptf ⊢ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑙 ∈ 𝐴 ↦ ⦋ 𝑙 / 𝑘 ⦌ 𝐵 )
11 10 oveq1i ⊢ ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) supp 𝑍 ) = ( ( 𝑙 ∈ 𝐴 ↦ ⦋ 𝑙 / 𝑘 ⦌ 𝐵 ) supp 𝑍 )
12 4 sbt ⊢ [ 𝑙 / 𝑘 ] ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 ∖ 𝑊 ) ) → 𝐵 = 𝑍 )
13 sbim ⊢ ( [ 𝑙 / 𝑘 ] ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 ∖ 𝑊 ) ) → 𝐵 = 𝑍 ) ↔ ( [ 𝑙 / 𝑘 ] ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 ∖ 𝑊 ) ) → [ 𝑙 / 𝑘 ] 𝐵 = 𝑍 ) )
14 sban ⊢ ( [ 𝑙 / 𝑘 ] ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 ∖ 𝑊 ) ) ↔ ( [ 𝑙 / 𝑘 ] 𝜑 ∧ [ 𝑙 / 𝑘 ] 𝑘 ∈ ( 𝐴 ∖ 𝑊 ) ) )
15 1 sbf ⊢ ( [ 𝑙 / 𝑘 ] 𝜑 ↔ 𝜑 )
16 2 3 nfdif ⊢ Ⅎ 𝑘 ( 𝐴 ∖ 𝑊 )
17 16 clelsb3fw ⊢ ( [ 𝑙 / 𝑘 ] 𝑘 ∈ ( 𝐴 ∖ 𝑊 ) ↔ 𝑙 ∈ ( 𝐴 ∖ 𝑊 ) )
18 15 17 anbi12i ⊢ ( ( [ 𝑙 / 𝑘 ] 𝜑 ∧ [ 𝑙 / 𝑘 ] 𝑘 ∈ ( 𝐴 ∖ 𝑊 ) ) ↔ ( 𝜑 ∧ 𝑙 ∈ ( 𝐴 ∖ 𝑊 ) ) )
19 14 18 bitri ⊢ ( [ 𝑙 / 𝑘 ] ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 ∖ 𝑊 ) ) ↔ ( 𝜑 ∧ 𝑙 ∈ ( 𝐴 ∖ 𝑊 ) ) )
20 sbsbc ⊢ ( [ 𝑙 / 𝑘 ] 𝐵 = 𝑍 ↔ [ 𝑙 / 𝑘 ] 𝐵 = 𝑍 )
21 sbceq1g ⊢ ( 𝑙 ∈ V → ( [ 𝑙 / 𝑘 ] 𝐵 = 𝑍 ↔ ⦋ 𝑙 / 𝑘 ⦌ 𝐵 = 𝑍 ) )
22 21 elv ⊢ ( [ 𝑙 / 𝑘 ] 𝐵 = 𝑍 ↔ ⦋ 𝑙 / 𝑘 ⦌ 𝐵 = 𝑍 )
23 20 22 bitri ⊢ ( [ 𝑙 / 𝑘 ] 𝐵 = 𝑍 ↔ ⦋ 𝑙 / 𝑘 ⦌ 𝐵 = 𝑍 )
24 19 23 imbi12i ⊢ ( ( [ 𝑙 / 𝑘 ] ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 ∖ 𝑊 ) ) → [ 𝑙 / 𝑘 ] 𝐵 = 𝑍 ) ↔ ( ( 𝜑 ∧ 𝑙 ∈ ( 𝐴 ∖ 𝑊 ) ) → ⦋ 𝑙 / 𝑘 ⦌ 𝐵 = 𝑍 ) )
25 13 24 bitri ⊢ ( [ 𝑙 / 𝑘 ] ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 ∖ 𝑊 ) ) → 𝐵 = 𝑍 ) ↔ ( ( 𝜑 ∧ 𝑙 ∈ ( 𝐴 ∖ 𝑊 ) ) → ⦋ 𝑙 / 𝑘 ⦌ 𝐵 = 𝑍 ) )
26 12 25 mpbi ⊢ ( ( 𝜑 ∧ 𝑙 ∈ ( 𝐴 ∖ 𝑊 ) ) → ⦋ 𝑙 / 𝑘 ⦌ 𝐵 = 𝑍 )
27 26 5 suppss2 ⊢ ( 𝜑 → ( ( 𝑙 ∈ 𝐴 ↦ ⦋ 𝑙 / 𝑘 ⦌ 𝐵 ) supp 𝑍 ) ⊆ 𝑊 )
28 11 27 eqsstrid ⊢ ( 𝜑 → ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) supp 𝑍 ) ⊆ 𝑊 )