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 𝑍 ) )