Metamath Proof Explorer

Theorem ressuppssdif

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 ressuppssdif ( ( 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( 𝐹 supp 𝑍 ) ⊆ ( ( ( 𝐹 ↾ 𝐵 ) supp 𝑍 ) ∪ ( dom 𝐹 ∖ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 eldif ⊢ ( 𝑥 ∈ ( { 𝑧 ∈ dom 𝐹 ∣ ( 𝐹 “ { 𝑧 } ) ≠ { 𝑍 } } ∖ { 𝑧 ∈ dom ( 𝐹 ↾ 𝐵 ) ∣ ( ( 𝐹 ↾ 𝐵 ) “ { 𝑧 } ) ≠ { 𝑍 } } ) ↔ ( 𝑥 ∈ { 𝑧 ∈ dom 𝐹 ∣ ( 𝐹 “ { 𝑧 } ) ≠ { 𝑍 } } ∧ ¬ 𝑥 ∈ { 𝑧 ∈ dom ( 𝐹 ↾ 𝐵 ) ∣ ( ( 𝐹 ↾ 𝐵 ) “ { 𝑧 } ) ≠ { 𝑍 } } ) )
2 sneq ⊢ ( 𝑧 = 𝑥 → { 𝑧 } = { 𝑥 } )
3 2 imaeq2d ⊢ ( 𝑧 = 𝑥 → ( 𝐹 “ { 𝑧 } ) = ( 𝐹 “ { 𝑥 } ) )
4 3 neeq1d ⊢ ( 𝑧 = 𝑥 → ( ( 𝐹 “ { 𝑧 } ) ≠ { 𝑍 } ↔ ( 𝐹 “ { 𝑥 } ) ≠ { 𝑍 } ) )
5 4 elrab ⊢ ( 𝑥 ∈ { 𝑧 ∈ dom 𝐹 ∣ ( 𝐹 “ { 𝑧 } ) ≠ { 𝑍 } } ↔ ( 𝑥 ∈ dom 𝐹 ∧ ( 𝐹 “ { 𝑥 } ) ≠ { 𝑍 } ) )
6 ianor ⊢ ( ¬ ( 𝑥 ∈ dom ( 𝐹 ↾ 𝐵 ) ∧ ( ( 𝐹 ↾ 𝐵 ) “ { 𝑥 } ) ≠ { 𝑍 } ) ↔ ( ¬ 𝑥 ∈ dom ( 𝐹 ↾ 𝐵 ) ∨ ¬ ( ( 𝐹 ↾ 𝐵 ) “ { 𝑥 } ) ≠ { 𝑍 } ) )
7 2 imaeq2d ⊢ ( 𝑧 = 𝑥 → ( ( 𝐹 ↾ 𝐵 ) “ { 𝑧 } ) = ( ( 𝐹 ↾ 𝐵 ) “ { 𝑥 } ) )
8 7 neeq1d ⊢ ( 𝑧 = 𝑥 → ( ( ( 𝐹 ↾ 𝐵 ) “ { 𝑧 } ) ≠ { 𝑍 } ↔ ( ( 𝐹 ↾ 𝐵 ) “ { 𝑥 } ) ≠ { 𝑍 } ) )
9 8 elrab ⊢ ( 𝑥 ∈ { 𝑧 ∈ dom ( 𝐹 ↾ 𝐵 ) ∣ ( ( 𝐹 ↾ 𝐵 ) “ { 𝑧 } ) ≠ { 𝑍 } } ↔ ( 𝑥 ∈ dom ( 𝐹 ↾ 𝐵 ) ∧ ( ( 𝐹 ↾ 𝐵 ) “ { 𝑥 } ) ≠ { 𝑍 } ) )
10 6 9 xchnxbir ⊢ ( ¬ 𝑥 ∈ { 𝑧 ∈ dom ( 𝐹 ↾ 𝐵 ) ∣ ( ( 𝐹 ↾ 𝐵 ) “ { 𝑧 } ) ≠ { 𝑍 } } ↔ ( ¬ 𝑥 ∈ dom ( 𝐹 ↾ 𝐵 ) ∨ ¬ ( ( 𝐹 ↾ 𝐵 ) “ { 𝑥 } ) ≠ { 𝑍 } ) )
11 ianor ⊢ ( ¬ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ∈ dom 𝐹 ) ↔ ( ¬ 𝑥 ∈ 𝐵 ∨ ¬ 𝑥 ∈ dom 𝐹 ) )
12 dmres ⊢ dom ( 𝐹 ↾ 𝐵 ) = ( 𝐵 ∩ dom 𝐹 )
13 12 elin2 ⊢ ( 𝑥 ∈ dom ( 𝐹 ↾ 𝐵 ) ↔ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ∈ dom 𝐹 ) )
14 11 13 xchnxbir ⊢ ( ¬ 𝑥 ∈ dom ( 𝐹 ↾ 𝐵 ) ↔ ( ¬ 𝑥 ∈ 𝐵 ∨ ¬ 𝑥 ∈ dom 𝐹 ) )
15 simpl ⊢ ( ( 𝑥 ∈ dom 𝐹 ∧ ( 𝐹 “ { 𝑥 } ) ≠ { 𝑍 } ) → 𝑥 ∈ dom 𝐹 )
16 15 anim2i ⊢ ( ( ¬ 𝑥 ∈ 𝐵 ∧ ( 𝑥 ∈ dom 𝐹 ∧ ( 𝐹 “ { 𝑥 } ) ≠ { 𝑍 } ) ) → ( ¬ 𝑥 ∈ 𝐵 ∧ 𝑥 ∈ dom 𝐹 ) )
17 16 ancomd ⊢ ( ( ¬ 𝑥 ∈ 𝐵 ∧ ( 𝑥 ∈ dom 𝐹 ∧ ( 𝐹 “ { 𝑥 } ) ≠ { 𝑍 } ) ) → ( 𝑥 ∈ dom 𝐹 ∧ ¬ 𝑥 ∈ 𝐵 ) )
18 eldif ⊢ ( 𝑥 ∈ ( dom 𝐹 ∖ 𝐵 ) ↔ ( 𝑥 ∈ dom 𝐹 ∧ ¬ 𝑥 ∈ 𝐵 ) )
19 17 18 sylibr ⊢ ( ( ¬ 𝑥 ∈ 𝐵 ∧ ( 𝑥 ∈ dom 𝐹 ∧ ( 𝐹 “ { 𝑥 } ) ≠ { 𝑍 } ) ) → 𝑥 ∈ ( dom 𝐹 ∖ 𝐵 ) )
20 19 ex ⊢ ( ¬ 𝑥 ∈ 𝐵 → ( ( 𝑥 ∈ dom 𝐹 ∧ ( 𝐹 “ { 𝑥 } ) ≠ { 𝑍 } ) → 𝑥 ∈ ( dom 𝐹 ∖ 𝐵 ) ) )
21 pm2.24 ⊢ ( 𝑥 ∈ dom 𝐹 → ( ¬ 𝑥 ∈ dom 𝐹 → 𝑥 ∈ ( dom 𝐹 ∖ 𝐵 ) ) )
22 21 adantr ⊢ ( ( 𝑥 ∈ dom 𝐹 ∧ ( 𝐹 “ { 𝑥 } ) ≠ { 𝑍 } ) → ( ¬ 𝑥 ∈ dom 𝐹 → 𝑥 ∈ ( dom 𝐹 ∖ 𝐵 ) ) )
23 22 com12 ⊢ ( ¬ 𝑥 ∈ dom 𝐹 → ( ( 𝑥 ∈ dom 𝐹 ∧ ( 𝐹 “ { 𝑥 } ) ≠ { 𝑍 } ) → 𝑥 ∈ ( dom 𝐹 ∖ 𝐵 ) ) )
24 20 23 jaoi ⊢ ( ( ¬ 𝑥 ∈ 𝐵 ∨ ¬ 𝑥 ∈ dom 𝐹 ) → ( ( 𝑥 ∈ dom 𝐹 ∧ ( 𝐹 “ { 𝑥 } ) ≠ { 𝑍 } ) → 𝑥 ∈ ( dom 𝐹 ∖ 𝐵 ) ) )
25 14 24 sylbi ⊢ ( ¬ 𝑥 ∈ dom ( 𝐹 ↾ 𝐵 ) → ( ( 𝑥 ∈ dom 𝐹 ∧ ( 𝐹 “ { 𝑥 } ) ≠ { 𝑍 } ) → 𝑥 ∈ ( dom 𝐹 ∖ 𝐵 ) ) )
26 15 adantl ⊢ ( ( ¬ ( ( 𝐹 ↾ 𝐵 ) “ { 𝑥 } ) ≠ { 𝑍 } ∧ ( 𝑥 ∈ dom 𝐹 ∧ ( 𝐹 “ { 𝑥 } ) ≠ { 𝑍 } ) ) → 𝑥 ∈ dom 𝐹 )
27 snssi ⊢ ( 𝑥 ∈ 𝐵 → { 𝑥 } ⊆ 𝐵 )
28 27 adantl ⊢ ( ( 𝑥 ∈ dom 𝐹 ∧ 𝑥 ∈ 𝐵 ) → { 𝑥 } ⊆ 𝐵 )
29 resima2 ⊢ ( { 𝑥 } ⊆ 𝐵 → ( ( 𝐹 ↾ 𝐵 ) “ { 𝑥 } ) = ( 𝐹 “ { 𝑥 } ) )
30 28 29 syl ⊢ ( ( 𝑥 ∈ dom 𝐹 ∧ 𝑥 ∈ 𝐵 ) → ( ( 𝐹 ↾ 𝐵 ) “ { 𝑥 } ) = ( 𝐹 “ { 𝑥 } ) )
31 30 eqcomd ⊢ ( ( 𝑥 ∈ dom 𝐹 ∧ 𝑥 ∈ 𝐵 ) → ( 𝐹 “ { 𝑥 } ) = ( ( 𝐹 ↾ 𝐵 ) “ { 𝑥 } ) )
32 31 adantr ⊢ ( ( ( 𝑥 ∈ dom 𝐹 ∧ 𝑥 ∈ 𝐵 ) ∧ ( ( 𝐹 ↾ 𝐵 ) “ { 𝑥 } ) = { 𝑍 } ) → ( 𝐹 “ { 𝑥 } ) = ( ( 𝐹 ↾ 𝐵 ) “ { 𝑥 } ) )
33 simpr ⊢ ( ( ( 𝑥 ∈ dom 𝐹 ∧ 𝑥 ∈ 𝐵 ) ∧ ( ( 𝐹 ↾ 𝐵 ) “ { 𝑥 } ) = { 𝑍 } ) → ( ( 𝐹 ↾ 𝐵 ) “ { 𝑥 } ) = { 𝑍 } )
34 32 33 eqtrd ⊢ ( ( ( 𝑥 ∈ dom 𝐹 ∧ 𝑥 ∈ 𝐵 ) ∧ ( ( 𝐹 ↾ 𝐵 ) “ { 𝑥 } ) = { 𝑍 } ) → ( 𝐹 “ { 𝑥 } ) = { 𝑍 } )
35 34 ex ⊢ ( ( 𝑥 ∈ dom 𝐹 ∧ 𝑥 ∈ 𝐵 ) → ( ( ( 𝐹 ↾ 𝐵 ) “ { 𝑥 } ) = { 𝑍 } → ( 𝐹 “ { 𝑥 } ) = { 𝑍 } ) )
36 35 necon3d ⊢ ( ( 𝑥 ∈ dom 𝐹 ∧ 𝑥 ∈ 𝐵 ) → ( ( 𝐹 “ { 𝑥 } ) ≠ { 𝑍 } → ( ( 𝐹 ↾ 𝐵 ) “ { 𝑥 } ) ≠ { 𝑍 } ) )
37 36 impancom ⊢ ( ( 𝑥 ∈ dom 𝐹 ∧ ( 𝐹 “ { 𝑥 } ) ≠ { 𝑍 } ) → ( 𝑥 ∈ 𝐵 → ( ( 𝐹 ↾ 𝐵 ) “ { 𝑥 } ) ≠ { 𝑍 } ) )
38 37 con3d ⊢ ( ( 𝑥 ∈ dom 𝐹 ∧ ( 𝐹 “ { 𝑥 } ) ≠ { 𝑍 } ) → ( ¬ ( ( 𝐹 ↾ 𝐵 ) “ { 𝑥 } ) ≠ { 𝑍 } → ¬ 𝑥 ∈ 𝐵 ) )
39 38 impcom ⊢ ( ( ¬ ( ( 𝐹 ↾ 𝐵 ) “ { 𝑥 } ) ≠ { 𝑍 } ∧ ( 𝑥 ∈ dom 𝐹 ∧ ( 𝐹 “ { 𝑥 } ) ≠ { 𝑍 } ) ) → ¬ 𝑥 ∈ 𝐵 )
40 26 39 eldifd ⊢ ( ( ¬ ( ( 𝐹 ↾ 𝐵 ) “ { 𝑥 } ) ≠ { 𝑍 } ∧ ( 𝑥 ∈ dom 𝐹 ∧ ( 𝐹 “ { 𝑥 } ) ≠ { 𝑍 } ) ) → 𝑥 ∈ ( dom 𝐹 ∖ 𝐵 ) )
41 40 ex ⊢ ( ¬ ( ( 𝐹 ↾ 𝐵 ) “ { 𝑥 } ) ≠ { 𝑍 } → ( ( 𝑥 ∈ dom 𝐹 ∧ ( 𝐹 “ { 𝑥 } ) ≠ { 𝑍 } ) → 𝑥 ∈ ( dom 𝐹 ∖ 𝐵 ) ) )
42 25 41 jaoi ⊢ ( ( ¬ 𝑥 ∈ dom ( 𝐹 ↾ 𝐵 ) ∨ ¬ ( ( 𝐹 ↾ 𝐵 ) “ { 𝑥 } ) ≠ { 𝑍 } ) → ( ( 𝑥 ∈ dom 𝐹 ∧ ( 𝐹 “ { 𝑥 } ) ≠ { 𝑍 } ) → 𝑥 ∈ ( dom 𝐹 ∖ 𝐵 ) ) )
43 42 impcom ⊢ ( ( ( 𝑥 ∈ dom 𝐹 ∧ ( 𝐹 “ { 𝑥 } ) ≠ { 𝑍 } ) ∧ ( ¬ 𝑥 ∈ dom ( 𝐹 ↾ 𝐵 ) ∨ ¬ ( ( 𝐹 ↾ 𝐵 ) “ { 𝑥 } ) ≠ { 𝑍 } ) ) → 𝑥 ∈ ( dom 𝐹 ∖ 𝐵 ) )
44 5 10 43 syl2anb ⊢ ( ( 𝑥 ∈ { 𝑧 ∈ dom 𝐹 ∣ ( 𝐹 “ { 𝑧 } ) ≠ { 𝑍 } } ∧ ¬ 𝑥 ∈ { 𝑧 ∈ dom ( 𝐹 ↾ 𝐵 ) ∣ ( ( 𝐹 ↾ 𝐵 ) “ { 𝑧 } ) ≠ { 𝑍 } } ) → 𝑥 ∈ ( dom 𝐹 ∖ 𝐵 ) )
45 1 44 sylbi ⊢ ( 𝑥 ∈ ( { 𝑧 ∈ dom 𝐹 ∣ ( 𝐹 “ { 𝑧 } ) ≠ { 𝑍 } } ∖ { 𝑧 ∈ dom ( 𝐹 ↾ 𝐵 ) ∣ ( ( 𝐹 ↾ 𝐵 ) “ { 𝑧 } ) ≠ { 𝑍 } } ) → 𝑥 ∈ ( dom 𝐹 ∖ 𝐵 ) )
46 45 a1i ⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( 𝑥 ∈ ( { 𝑧 ∈ dom 𝐹 ∣ ( 𝐹 “ { 𝑧 } ) ≠ { 𝑍 } } ∖ { 𝑧 ∈ dom ( 𝐹 ↾ 𝐵 ) ∣ ( ( 𝐹 ↾ 𝐵 ) “ { 𝑧 } ) ≠ { 𝑍 } } ) → 𝑥 ∈ ( dom 𝐹 ∖ 𝐵 ) ) )
47 46 ssrdv ⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( { 𝑧 ∈ dom 𝐹 ∣ ( 𝐹 “ { 𝑧 } ) ≠ { 𝑍 } } ∖ { 𝑧 ∈ dom ( 𝐹 ↾ 𝐵 ) ∣ ( ( 𝐹 ↾ 𝐵 ) “ { 𝑧 } ) ≠ { 𝑍 } } ) ⊆ ( dom 𝐹 ∖ 𝐵 ) )
48 ssundif ⊢ ( { 𝑧 ∈ dom 𝐹 ∣ ( 𝐹 “ { 𝑧 } ) ≠ { 𝑍 } } ⊆ ( { 𝑧 ∈ dom ( 𝐹 ↾ 𝐵 ) ∣ ( ( 𝐹 ↾ 𝐵 ) “ { 𝑧 } ) ≠ { 𝑍 } } ∪ ( dom 𝐹 ∖ 𝐵 ) ) ↔ ( { 𝑧 ∈ dom 𝐹 ∣ ( 𝐹 “ { 𝑧 } ) ≠ { 𝑍 } } ∖ { 𝑧 ∈ dom ( 𝐹 ↾ 𝐵 ) ∣ ( ( 𝐹 ↾ 𝐵 ) “ { 𝑧 } ) ≠ { 𝑍 } } ) ⊆ ( dom 𝐹 ∖ 𝐵 ) )
49 47 48 sylibr ⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → { 𝑧 ∈ dom 𝐹 ∣ ( 𝐹 “ { 𝑧 } ) ≠ { 𝑍 } } ⊆ ( { 𝑧 ∈ dom ( 𝐹 ↾ 𝐵 ) ∣ ( ( 𝐹 ↾ 𝐵 ) “ { 𝑧 } ) ≠ { 𝑍 } } ∪ ( dom 𝐹 ∖ 𝐵 ) ) )
50 suppval ⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( 𝐹 supp 𝑍 ) = { 𝑧 ∈ dom 𝐹 ∣ ( 𝐹 “ { 𝑧 } ) ≠ { 𝑍 } } )
51 resexg ⊢ ( 𝐹 ∈ 𝑉 → ( 𝐹 ↾ 𝐵 ) ∈ V )
52 suppval ⊢ ( ( ( 𝐹 ↾ 𝐵 ) ∈ V ∧ 𝑍 ∈ 𝑊 ) → ( ( 𝐹 ↾ 𝐵 ) supp 𝑍 ) = { 𝑧 ∈ dom ( 𝐹 ↾ 𝐵 ) ∣ ( ( 𝐹 ↾ 𝐵 ) “ { 𝑧 } ) ≠ { 𝑍 } } )
53 51 52 sylan ⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( ( 𝐹 ↾ 𝐵 ) supp 𝑍 ) = { 𝑧 ∈ dom ( 𝐹 ↾ 𝐵 ) ∣ ( ( 𝐹 ↾ 𝐵 ) “ { 𝑧 } ) ≠ { 𝑍 } } )
54 53 uneq1d ⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( ( ( 𝐹 ↾ 𝐵 ) supp 𝑍 ) ∪ ( dom 𝐹 ∖ 𝐵 ) ) = ( { 𝑧 ∈ dom ( 𝐹 ↾ 𝐵 ) ∣ ( ( 𝐹 ↾ 𝐵 ) “ { 𝑧 } ) ≠ { 𝑍 } } ∪ ( dom 𝐹 ∖ 𝐵 ) ) )
55 49 50 54 3sstr4d ⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( 𝐹 supp 𝑍 ) ⊆ ( ( ( 𝐹 ↾ 𝐵 ) supp 𝑍 ) ∪ ( dom 𝐹 ∖ 𝐵 ) ) )