Theorem suppssfv

Description: Formula building theorem for support restriction, on a function which preserves zero. (Contributed by Stefan O'Rear, 9-Mar-2015) (Revised by AV, 28-May-2019)

	Ref	Expression
Hypotheses	suppssfv.a	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐷 ↦ 𝐴 ) supp 𝑌 ) ⊆ 𝐿 )
	suppssfv.f	⊢ ( 𝜑 → ( 𝐹 ‘ 𝑌 ) = 𝑍 )
	suppssfv.v	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → 𝐴 ∈ 𝑉 )
	suppssfv.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑈 )
Assertion	suppssfv	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐷 ↦ ( 𝐹 ‘ 𝐴 ) ) supp 𝑍 ) ⊆ 𝐿 )

Proof

Step	Hyp	Ref	Expression
1		suppssfv.a	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐷 ↦ 𝐴 ) supp 𝑌 ) ⊆ 𝐿 )
2		suppssfv.f	⊢ ( 𝜑 → ( 𝐹 ‘ 𝑌 ) = 𝑍 )
3		suppssfv.v	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → 𝐴 ∈ 𝑉 )
4		suppssfv.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑈 )
5		eldifsni	⊢ ( ( 𝐹 ‘ 𝐴 ) ∈ ( V ∖ { 𝑍 } ) → ( 𝐹 ‘ 𝐴 ) ≠ 𝑍 )
6	3	elexd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → 𝐴 ∈ V )
7	6	ad4ant23	⊢ ( ( ( ( ( 𝐷 ∈ V ∧ 𝑍 ∈ V ) ∧ 𝜑 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐹 ‘ 𝐴 ) ≠ 𝑍 ) → 𝐴 ∈ V )
8		fveqeq2	⊢ ( 𝐴 = 𝑌 → ( ( 𝐹 ‘ 𝐴 ) = 𝑍 ↔ ( 𝐹 ‘ 𝑌 ) = 𝑍 ) )
9	2 8	syl5ibrcom	⊢ ( 𝜑 → ( 𝐴 = 𝑌 → ( 𝐹 ‘ 𝐴 ) = 𝑍 ) )
10	9	necon3d	⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝐴 ) ≠ 𝑍 → 𝐴 ≠ 𝑌 ) )
11	10	ad2antlr	⊢ ( ( ( ( 𝐷 ∈ V ∧ 𝑍 ∈ V ) ∧ 𝜑 ) ∧ 𝑥 ∈ 𝐷 ) → ( ( 𝐹 ‘ 𝐴 ) ≠ 𝑍 → 𝐴 ≠ 𝑌 ) )
12	11	imp	⊢ ( ( ( ( ( 𝐷 ∈ V ∧ 𝑍 ∈ V ) ∧ 𝜑 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐹 ‘ 𝐴 ) ≠ 𝑍 ) → 𝐴 ≠ 𝑌 )
13		eldifsn	⊢ ( 𝐴 ∈ ( V ∖ { 𝑌 } ) ↔ ( 𝐴 ∈ V ∧ 𝐴 ≠ 𝑌 ) )
14	7 12 13	sylanbrc	⊢ ( ( ( ( ( 𝐷 ∈ V ∧ 𝑍 ∈ V ) ∧ 𝜑 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐹 ‘ 𝐴 ) ≠ 𝑍 ) → 𝐴 ∈ ( V ∖ { 𝑌 } ) )
15	14	ex	⊢ ( ( ( ( 𝐷 ∈ V ∧ 𝑍 ∈ V ) ∧ 𝜑 ) ∧ 𝑥 ∈ 𝐷 ) → ( ( 𝐹 ‘ 𝐴 ) ≠ 𝑍 → 𝐴 ∈ ( V ∖ { 𝑌 } ) ) )
16	5 15	syl5	⊢ ( ( ( ( 𝐷 ∈ V ∧ 𝑍 ∈ V ) ∧ 𝜑 ) ∧ 𝑥 ∈ 𝐷 ) → ( ( 𝐹 ‘ 𝐴 ) ∈ ( V ∖ { 𝑍 } ) → 𝐴 ∈ ( V ∖ { 𝑌 } ) ) )
17	16	ss2rabdv	⊢ ( ( ( 𝐷 ∈ V ∧ 𝑍 ∈ V ) ∧ 𝜑 ) → { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝐴 ) ∈ ( V ∖ { 𝑍 } ) } ⊆ { 𝑥 ∈ 𝐷 ∣ 𝐴 ∈ ( V ∖ { 𝑌 } ) } )
18		eqid	⊢ ( 𝑥 ∈ 𝐷 ↦ ( 𝐹 ‘ 𝐴 ) ) = ( 𝑥 ∈ 𝐷 ↦ ( 𝐹 ‘ 𝐴 ) )
19		simpll	⊢ ( ( ( 𝐷 ∈ V ∧ 𝑍 ∈ V ) ∧ 𝜑 ) → 𝐷 ∈ V )
20		simplr	⊢ ( ( ( 𝐷 ∈ V ∧ 𝑍 ∈ V ) ∧ 𝜑 ) → 𝑍 ∈ V )
21	18 19 20	mptsuppdifd	⊢ ( ( ( 𝐷 ∈ V ∧ 𝑍 ∈ V ) ∧ 𝜑 ) → ( ( 𝑥 ∈ 𝐷 ↦ ( 𝐹 ‘ 𝐴 ) ) supp 𝑍 ) = { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝐴 ) ∈ ( V ∖ { 𝑍 } ) } )
22		eqid	⊢ ( 𝑥 ∈ 𝐷 ↦ 𝐴 ) = ( 𝑥 ∈ 𝐷 ↦ 𝐴 )
23	4	adantl	⊢ ( ( ( 𝐷 ∈ V ∧ 𝑍 ∈ V ) ∧ 𝜑 ) → 𝑌 ∈ 𝑈 )
24	22 19 23	mptsuppdifd	⊢ ( ( ( 𝐷 ∈ V ∧ 𝑍 ∈ V ) ∧ 𝜑 ) → ( ( 𝑥 ∈ 𝐷 ↦ 𝐴 ) supp 𝑌 ) = { 𝑥 ∈ 𝐷 ∣ 𝐴 ∈ ( V ∖ { 𝑌 } ) } )
25	17 21 24	3sstr4d	⊢ ( ( ( 𝐷 ∈ V ∧ 𝑍 ∈ V ) ∧ 𝜑 ) → ( ( 𝑥 ∈ 𝐷 ↦ ( 𝐹 ‘ 𝐴 ) ) supp 𝑍 ) ⊆ ( ( 𝑥 ∈ 𝐷 ↦ 𝐴 ) supp 𝑌 ) )
26	1	adantl	⊢ ( ( ( 𝐷 ∈ V ∧ 𝑍 ∈ V ) ∧ 𝜑 ) → ( ( 𝑥 ∈ 𝐷 ↦ 𝐴 ) supp 𝑌 ) ⊆ 𝐿 )
27	25 26	sstrd	⊢ ( ( ( 𝐷 ∈ V ∧ 𝑍 ∈ V ) ∧ 𝜑 ) → ( ( 𝑥 ∈ 𝐷 ↦ ( 𝐹 ‘ 𝐴 ) ) supp 𝑍 ) ⊆ 𝐿 )
28	27	ex	⊢ ( ( 𝐷 ∈ V ∧ 𝑍 ∈ V ) → ( 𝜑 → ( ( 𝑥 ∈ 𝐷 ↦ ( 𝐹 ‘ 𝐴 ) ) supp 𝑍 ) ⊆ 𝐿 ) )
29		mptexg	⊢ ( 𝐷 ∈ V → ( 𝑥 ∈ 𝐷 ↦ ( 𝐹 ‘ 𝐴 ) ) ∈ V )
30		fvex	⊢ ( 𝐹 ‘ 𝐴 ) ∈ V
31	30	rgenw	⊢ ∀ 𝑥 ∈ 𝐷 ( 𝐹 ‘ 𝐴 ) ∈ V
32		dmmptg	⊢ ( ∀ 𝑥 ∈ 𝐷 ( 𝐹 ‘ 𝐴 ) ∈ V → dom ( 𝑥 ∈ 𝐷 ↦ ( 𝐹 ‘ 𝐴 ) ) = 𝐷 )
33	31 32	ax-mp	⊢ dom ( 𝑥 ∈ 𝐷 ↦ ( 𝐹 ‘ 𝐴 ) ) = 𝐷
34		dmexg	⊢ ( ( 𝑥 ∈ 𝐷 ↦ ( 𝐹 ‘ 𝐴 ) ) ∈ V → dom ( 𝑥 ∈ 𝐷 ↦ ( 𝐹 ‘ 𝐴 ) ) ∈ V )
35	33 34	eqeltrrid	⊢ ( ( 𝑥 ∈ 𝐷 ↦ ( 𝐹 ‘ 𝐴 ) ) ∈ V → 𝐷 ∈ V )
36	29 35	impbii	⊢ ( 𝐷 ∈ V ↔ ( 𝑥 ∈ 𝐷 ↦ ( 𝐹 ‘ 𝐴 ) ) ∈ V )
37	36	anbi1i	⊢ ( ( 𝐷 ∈ V ∧ 𝑍 ∈ V ) ↔ ( ( 𝑥 ∈ 𝐷 ↦ ( 𝐹 ‘ 𝐴 ) ) ∈ V ∧ 𝑍 ∈ V ) )
38		supp0prc	⊢ ( ¬ ( ( 𝑥 ∈ 𝐷 ↦ ( 𝐹 ‘ 𝐴 ) ) ∈ V ∧ 𝑍 ∈ V ) → ( ( 𝑥 ∈ 𝐷 ↦ ( 𝐹 ‘ 𝐴 ) ) supp 𝑍 ) = ∅ )
39	37 38	sylnbi	⊢ ( ¬ ( 𝐷 ∈ V ∧ 𝑍 ∈ V ) → ( ( 𝑥 ∈ 𝐷 ↦ ( 𝐹 ‘ 𝐴 ) ) supp 𝑍 ) = ∅ )
40		0ss	⊢ ∅ ⊆ 𝐿
41	39 40	eqsstrdi	⊢ ( ¬ ( 𝐷 ∈ V ∧ 𝑍 ∈ V ) → ( ( 𝑥 ∈ 𝐷 ↦ ( 𝐹 ‘ 𝐴 ) ) supp 𝑍 ) ⊆ 𝐿 )
42	41	a1d	⊢ ( ¬ ( 𝐷 ∈ V ∧ 𝑍 ∈ V ) → ( 𝜑 → ( ( 𝑥 ∈ 𝐷 ↦ ( 𝐹 ‘ 𝐴 ) ) supp 𝑍 ) ⊆ 𝐿 ) )
43	28 42	pm2.61i	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐷 ↦ ( 𝐹 ‘ 𝐴 ) ) supp 𝑍 ) ⊆ 𝐿 )