Metamath Proof Explorer

Theorem ressuppss

Description: The support of the restriction of a function is a subset of the support of the function itself. (Contributed by AV, 22-Apr-2019)

Ref Expression
Assertion ressuppss ( ( 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( ( 𝐹 ↾ 𝐵 ) supp 𝑍 ) ⊆ ( 𝐹 supp 𝑍 ) )

Proof

Step Hyp Ref Expression
1 elinel2 ⊢ ( 𝑏 ∈ ( 𝐵 ∩ dom 𝐹 ) → 𝑏 ∈ dom 𝐹 )
2 dmres ⊢ dom ( 𝐹 ↾ 𝐵 ) = ( 𝐵 ∩ dom 𝐹 )
3 1 2 eleq2s ⊢ ( 𝑏 ∈ dom ( 𝐹 ↾ 𝐵 ) → 𝑏 ∈ dom 𝐹 )
4 3 ad2antrl ⊢ ( ( ( 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ ( 𝑏 ∈ dom ( 𝐹 ↾ 𝐵 ) ∧ ( ( 𝐹 ↾ 𝐵 ) “ { 𝑏 } ) ≠ { 𝑍 } ) ) → 𝑏 ∈ dom 𝐹 )
5 snssi ⊢ ( 𝑏 ∈ 𝐵 → { 𝑏 } ⊆ 𝐵 )
6 resima2 ⊢ ( { 𝑏 } ⊆ 𝐵 → ( ( 𝐹 ↾ 𝐵 ) “ { 𝑏 } ) = ( 𝐹 “ { 𝑏 } ) )
7 5 6 syl ⊢ ( 𝑏 ∈ 𝐵 → ( ( 𝐹 ↾ 𝐵 ) “ { 𝑏 } ) = ( 𝐹 “ { 𝑏 } ) )
8 7 neeq1d ⊢ ( 𝑏 ∈ 𝐵 → ( ( ( 𝐹 ↾ 𝐵 ) “ { 𝑏 } ) ≠ { 𝑍 } ↔ ( 𝐹 “ { 𝑏 } ) ≠ { 𝑍 } ) )
9 8 biimpd ⊢ ( 𝑏 ∈ 𝐵 → ( ( ( 𝐹 ↾ 𝐵 ) “ { 𝑏 } ) ≠ { 𝑍 } → ( 𝐹 “ { 𝑏 } ) ≠ { 𝑍 } ) )
10 9 adantld ⊢ ( 𝑏 ∈ 𝐵 → ( ( 𝑏 ∈ dom ( 𝐹 ↾ 𝐵 ) ∧ ( ( 𝐹 ↾ 𝐵 ) “ { 𝑏 } ) ≠ { 𝑍 } ) → ( 𝐹 “ { 𝑏 } ) ≠ { 𝑍 } ) )
11 10 adantld ⊢ ( 𝑏 ∈ 𝐵 → ( ( ( 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ ( 𝑏 ∈ dom ( 𝐹 ↾ 𝐵 ) ∧ ( ( 𝐹 ↾ 𝐵 ) “ { 𝑏 } ) ≠ { 𝑍 } ) ) → ( 𝐹 “ { 𝑏 } ) ≠ { 𝑍 } ) )
12 elin ⊢ ( 𝑏 ∈ ( 𝐵 ∩ dom 𝐹 ) ↔ ( 𝑏 ∈ 𝐵 ∧ 𝑏 ∈ dom 𝐹 ) )
13 pm2.24 ⊢ ( 𝑏 ∈ 𝐵 → ( ¬ 𝑏 ∈ 𝐵 → ( 𝐹 “ { 𝑏 } ) ≠ { 𝑍 } ) )
14 13 adantr ⊢ ( ( 𝑏 ∈ 𝐵 ∧ 𝑏 ∈ dom 𝐹 ) → ( ¬ 𝑏 ∈ 𝐵 → ( 𝐹 “ { 𝑏 } ) ≠ { 𝑍 } ) )
15 12 14 sylbi ⊢ ( 𝑏 ∈ ( 𝐵 ∩ dom 𝐹 ) → ( ¬ 𝑏 ∈ 𝐵 → ( 𝐹 “ { 𝑏 } ) ≠ { 𝑍 } ) )
16 15 2 eleq2s ⊢ ( 𝑏 ∈ dom ( 𝐹 ↾ 𝐵 ) → ( ¬ 𝑏 ∈ 𝐵 → ( 𝐹 “ { 𝑏 } ) ≠ { 𝑍 } ) )
17 16 ad2antrl ⊢ ( ( ( 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ ( 𝑏 ∈ dom ( 𝐹 ↾ 𝐵 ) ∧ ( ( 𝐹 ↾ 𝐵 ) “ { 𝑏 } ) ≠ { 𝑍 } ) ) → ( ¬ 𝑏 ∈ 𝐵 → ( 𝐹 “ { 𝑏 } ) ≠ { 𝑍 } ) )
18 17 com12 ⊢ ( ¬ 𝑏 ∈ 𝐵 → ( ( ( 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ ( 𝑏 ∈ dom ( 𝐹 ↾ 𝐵 ) ∧ ( ( 𝐹 ↾ 𝐵 ) “ { 𝑏 } ) ≠ { 𝑍 } ) ) → ( 𝐹 “ { 𝑏 } ) ≠ { 𝑍 } ) )
19 11 18 pm2.61i ⊢ ( ( ( 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ ( 𝑏 ∈ dom ( 𝐹 ↾ 𝐵 ) ∧ ( ( 𝐹 ↾ 𝐵 ) “ { 𝑏 } ) ≠ { 𝑍 } ) ) → ( 𝐹 “ { 𝑏 } ) ≠ { 𝑍 } )
20 4 19 jca ⊢ ( ( ( 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ ( 𝑏 ∈ dom ( 𝐹 ↾ 𝐵 ) ∧ ( ( 𝐹 ↾ 𝐵 ) “ { 𝑏 } ) ≠ { 𝑍 } ) ) → ( 𝑏 ∈ dom 𝐹 ∧ ( 𝐹 “ { 𝑏 } ) ≠ { 𝑍 } ) )
21 20 ex ⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( ( 𝑏 ∈ dom ( 𝐹 ↾ 𝐵 ) ∧ ( ( 𝐹 ↾ 𝐵 ) “ { 𝑏 } ) ≠ { 𝑍 } ) → ( 𝑏 ∈ dom 𝐹 ∧ ( 𝐹 “ { 𝑏 } ) ≠ { 𝑍 } ) ) )
22 21 ss2abdv ⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → { 𝑏 ∣ ( 𝑏 ∈ dom ( 𝐹 ↾ 𝐵 ) ∧ ( ( 𝐹 ↾ 𝐵 ) “ { 𝑏 } ) ≠ { 𝑍 } ) } ⊆ { 𝑏 ∣ ( 𝑏 ∈ dom 𝐹 ∧ ( 𝐹 “ { 𝑏 } ) ≠ { 𝑍 } ) } )
23 df-rab ⊢ { 𝑏 ∈ dom ( 𝐹 ↾ 𝐵 ) ∣ ( ( 𝐹 ↾ 𝐵 ) “ { 𝑏 } ) ≠ { 𝑍 } } = { 𝑏 ∣ ( 𝑏 ∈ dom ( 𝐹 ↾ 𝐵 ) ∧ ( ( 𝐹 ↾ 𝐵 ) “ { 𝑏 } ) ≠ { 𝑍 } ) }
24 df-rab ⊢ { 𝑏 ∈ dom 𝐹 ∣ ( 𝐹 “ { 𝑏 } ) ≠ { 𝑍 } } = { 𝑏 ∣ ( 𝑏 ∈ dom 𝐹 ∧ ( 𝐹 “ { 𝑏 } ) ≠ { 𝑍 } ) }
25 22 23 24 3sstr4g ⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → { 𝑏 ∈ dom ( 𝐹 ↾ 𝐵 ) ∣ ( ( 𝐹 ↾ 𝐵 ) “ { 𝑏 } ) ≠ { 𝑍 } } ⊆ { 𝑏 ∈ dom 𝐹 ∣ ( 𝐹 “ { 𝑏 } ) ≠ { 𝑍 } } )
26 resexg ⊢ ( 𝐹 ∈ 𝑉 → ( 𝐹 ↾ 𝐵 ) ∈ V )
27 suppval ⊢ ( ( ( 𝐹 ↾ 𝐵 ) ∈ V ∧ 𝑍 ∈ 𝑊 ) → ( ( 𝐹 ↾ 𝐵 ) supp 𝑍 ) = { 𝑏 ∈ dom ( 𝐹 ↾ 𝐵 ) ∣ ( ( 𝐹 ↾ 𝐵 ) “ { 𝑏 } ) ≠ { 𝑍 } } )
28 26 27 sylan ⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( ( 𝐹 ↾ 𝐵 ) supp 𝑍 ) = { 𝑏 ∈ dom ( 𝐹 ↾ 𝐵 ) ∣ ( ( 𝐹 ↾ 𝐵 ) “ { 𝑏 } ) ≠ { 𝑍 } } )
29 suppval ⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( 𝐹 supp 𝑍 ) = { 𝑏 ∈ dom 𝐹 ∣ ( 𝐹 “ { 𝑏 } ) ≠ { 𝑍 } } )
30 25 28 29 3sstr4d ⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( ( 𝐹 ↾ 𝐵 ) supp 𝑍 ) ⊆ ( 𝐹 supp 𝑍 ) )