This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐺 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
suppss3.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
suppss3.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑊 )
suppss3.2 ⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
suppss3.3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑥 ) = 𝑍 ) → 𝐵 = 𝑍 )
Assertion suppss3 ( 𝜑 → ( 𝐺 supp 𝑍 ) ⊆ ( 𝐹 supp 𝑍 ) )

Proof

Step Hyp Ref Expression
1 suppss3.1 ⊢ 𝐺 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
2 suppss3.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
3 suppss3.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑊 )
4 suppss3.2 ⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
5 suppss3.3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑥 ) = 𝑍 ) → 𝐵 = 𝑍 )
6 1 oveq1i ⊢ ( 𝐺 supp 𝑍 ) = ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) supp 𝑍 )
7 simpl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∖ ( 𝐹 supp 𝑍 ) ) ) → 𝜑 )
8 eldifi ⊢ ( 𝑥 ∈ ( 𝐴 ∖ ( 𝐹 supp 𝑍 ) ) → 𝑥 ∈ 𝐴 )
9 8 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∖ ( 𝐹 supp 𝑍 ) ) ) → 𝑥 ∈ 𝐴 )
10 fnex ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐴 ∈ 𝑉 ) → 𝐹 ∈ V )
11 4 2 10 syl2anc ⊢ ( 𝜑 → 𝐹 ∈ V )
12 suppimacnv ⊢ ( ( 𝐹 ∈ V ∧ 𝑍 ∈ 𝑊 ) → ( 𝐹 supp 𝑍 ) = ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) )
13 11 3 12 syl2anc ⊢ ( 𝜑 → ( 𝐹 supp 𝑍 ) = ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) )
14 13 eleq2d ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐹 supp 𝑍 ) ↔ 𝑥 ∈ ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) ) )
15 elpreima ⊢ ( 𝐹 Fn 𝐴 → ( 𝑥 ∈ ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑥 ) ∈ ( V ∖ { 𝑍 } ) ) ) )
16 4 15 syl ⊢ ( 𝜑 → ( 𝑥 ∈ ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑥 ) ∈ ( V ∖ { 𝑍 } ) ) ) )
17 14 16 bitrd ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐹 supp 𝑍 ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑥 ) ∈ ( V ∖ { 𝑍 } ) ) ) )
18 17 baibd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑥 ∈ ( 𝐹 supp 𝑍 ) ↔ ( 𝐹 ‘ 𝑥 ) ∈ ( V ∖ { 𝑍 } ) ) )
19 18 notbid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ¬ 𝑥 ∈ ( 𝐹 supp 𝑍 ) ↔ ¬ ( 𝐹 ‘ 𝑥 ) ∈ ( V ∖ { 𝑍 } ) ) )
20 19 biimpd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ¬ 𝑥 ∈ ( 𝐹 supp 𝑍 ) → ¬ ( 𝐹 ‘ 𝑥 ) ∈ ( V ∖ { 𝑍 } ) ) )
21 20 expimpd ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ ( 𝐹 supp 𝑍 ) ) → ¬ ( 𝐹 ‘ 𝑥 ) ∈ ( V ∖ { 𝑍 } ) ) )
22 eldif ⊢ ( 𝑥 ∈ ( 𝐴 ∖ ( 𝐹 supp 𝑍 ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ ( 𝐹 supp 𝑍 ) ) )
23 fvex ⊢ ( 𝐹 ‘ 𝑥 ) ∈ V
24 eldifsn ⊢ ( ( 𝐹 ‘ 𝑥 ) ∈ ( V ∖ { 𝑍 } ) ↔ ( ( 𝐹 ‘ 𝑥 ) ∈ V ∧ ( 𝐹 ‘ 𝑥 ) ≠ 𝑍 ) )
25 23 24 mpbiran ⊢ ( ( 𝐹 ‘ 𝑥 ) ∈ ( V ∖ { 𝑍 } ) ↔ ( 𝐹 ‘ 𝑥 ) ≠ 𝑍 )
26 25 necon2bbii ⊢ ( ( 𝐹 ‘ 𝑥 ) = 𝑍 ↔ ¬ ( 𝐹 ‘ 𝑥 ) ∈ ( V ∖ { 𝑍 } ) )
27 21 22 26 3imtr4g ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 ∖ ( 𝐹 supp 𝑍 ) ) → ( 𝐹 ‘ 𝑥 ) = 𝑍 ) )
28 27 imp ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∖ ( 𝐹 supp 𝑍 ) ) ) → ( 𝐹 ‘ 𝑥 ) = 𝑍 )
29 7 9 28 5 syl3anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∖ ( 𝐹 supp 𝑍 ) ) ) → 𝐵 = 𝑍 )
30 29 2 suppss2 ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) supp 𝑍 ) ⊆ ( 𝐹 supp 𝑍 ) )
31 6 30 eqsstrid ⊢ ( 𝜑 → ( 𝐺 supp 𝑍 ) ⊆ ( 𝐹 supp 𝑍 ) )