Theorem extmptsuppeq

Description: The support of an extended function is the same as the original. (Contributed by Mario Carneiro, 25-May-2015) (Revised by AV, 30-Jun-2019)

	Ref	Expression
Hypotheses	extmptsuppeq.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
	extmptsuppeq.a	⊢ ( 𝜑 → 𝐴 ⊆ 𝐵 )
	extmptsuppeq.z	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝐵 ∖ 𝐴 ) ) → 𝑋 = 𝑍 )
Assertion	extmptsuppeq	⊢ ( 𝜑 → ( ( 𝑛 ∈ 𝐴 ↦ 𝑋 ) supp 𝑍 ) = ( ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) supp 𝑍 ) )

Proof

Step	Hyp	Ref	Expression
1		extmptsuppeq.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
2		extmptsuppeq.a	⊢ ( 𝜑 → 𝐴 ⊆ 𝐵 )
3		extmptsuppeq.z	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝐵 ∖ 𝐴 ) ) → 𝑋 = 𝑍 )
4	2	adantl	⊢ ( ( 𝑍 ∈ V ∧ 𝜑 ) → 𝐴 ⊆ 𝐵 )
5	4	sseld	⊢ ( ( 𝑍 ∈ V ∧ 𝜑 ) → ( 𝑛 ∈ 𝐴 → 𝑛 ∈ 𝐵 ) )
6	5	anim1d	⊢ ( ( 𝑍 ∈ V ∧ 𝜑 ) → ( ( 𝑛 ∈ 𝐴 ∧ 𝑋 ∈ ( V ∖ { 𝑍 } ) ) → ( 𝑛 ∈ 𝐵 ∧ 𝑋 ∈ ( V ∖ { 𝑍 } ) ) ) )
7		eldif	⊢ ( 𝑛 ∈ ( 𝐵 ∖ 𝐴 ) ↔ ( 𝑛 ∈ 𝐵 ∧ ¬ 𝑛 ∈ 𝐴 ) )
8	3	adantll	⊢ ( ( ( 𝑍 ∈ V ∧ 𝜑 ) ∧ 𝑛 ∈ ( 𝐵 ∖ 𝐴 ) ) → 𝑋 = 𝑍 )
9	7 8	sylan2br	⊢ ( ( ( 𝑍 ∈ V ∧ 𝜑 ) ∧ ( 𝑛 ∈ 𝐵 ∧ ¬ 𝑛 ∈ 𝐴 ) ) → 𝑋 = 𝑍 )
10	9	expr	⊢ ( ( ( 𝑍 ∈ V ∧ 𝜑 ) ∧ 𝑛 ∈ 𝐵 ) → ( ¬ 𝑛 ∈ 𝐴 → 𝑋 = 𝑍 ) )
11		elsn2g	⊢ ( 𝑍 ∈ V → ( 𝑋 ∈ { 𝑍 } ↔ 𝑋 = 𝑍 ) )
12		elndif	⊢ ( 𝑋 ∈ { 𝑍 } → ¬ 𝑋 ∈ ( V ∖ { 𝑍 } ) )
13	11 12	syl6bir	⊢ ( 𝑍 ∈ V → ( 𝑋 = 𝑍 → ¬ 𝑋 ∈ ( V ∖ { 𝑍 } ) ) )
14	13	ad2antrr	⊢ ( ( ( 𝑍 ∈ V ∧ 𝜑 ) ∧ 𝑛 ∈ 𝐵 ) → ( 𝑋 = 𝑍 → ¬ 𝑋 ∈ ( V ∖ { 𝑍 } ) ) )
15	10 14	syld	⊢ ( ( ( 𝑍 ∈ V ∧ 𝜑 ) ∧ 𝑛 ∈ 𝐵 ) → ( ¬ 𝑛 ∈ 𝐴 → ¬ 𝑋 ∈ ( V ∖ { 𝑍 } ) ) )
16	15	con4d	⊢ ( ( ( 𝑍 ∈ V ∧ 𝜑 ) ∧ 𝑛 ∈ 𝐵 ) → ( 𝑋 ∈ ( V ∖ { 𝑍 } ) → 𝑛 ∈ 𝐴 ) )
17	16	impr	⊢ ( ( ( 𝑍 ∈ V ∧ 𝜑 ) ∧ ( 𝑛 ∈ 𝐵 ∧ 𝑋 ∈ ( V ∖ { 𝑍 } ) ) ) → 𝑛 ∈ 𝐴 )
18		simprr	⊢ ( ( ( 𝑍 ∈ V ∧ 𝜑 ) ∧ ( 𝑛 ∈ 𝐵 ∧ 𝑋 ∈ ( V ∖ { 𝑍 } ) ) ) → 𝑋 ∈ ( V ∖ { 𝑍 } ) )
19	17 18	jca	⊢ ( ( ( 𝑍 ∈ V ∧ 𝜑 ) ∧ ( 𝑛 ∈ 𝐵 ∧ 𝑋 ∈ ( V ∖ { 𝑍 } ) ) ) → ( 𝑛 ∈ 𝐴 ∧ 𝑋 ∈ ( V ∖ { 𝑍 } ) ) )
20	19	ex	⊢ ( ( 𝑍 ∈ V ∧ 𝜑 ) → ( ( 𝑛 ∈ 𝐵 ∧ 𝑋 ∈ ( V ∖ { 𝑍 } ) ) → ( 𝑛 ∈ 𝐴 ∧ 𝑋 ∈ ( V ∖ { 𝑍 } ) ) ) )
21	6 20	impbid	⊢ ( ( 𝑍 ∈ V ∧ 𝜑 ) → ( ( 𝑛 ∈ 𝐴 ∧ 𝑋 ∈ ( V ∖ { 𝑍 } ) ) ↔ ( 𝑛 ∈ 𝐵 ∧ 𝑋 ∈ ( V ∖ { 𝑍 } ) ) ) )
22	21	rabbidva2	⊢ ( ( 𝑍 ∈ V ∧ 𝜑 ) → { 𝑛 ∈ 𝐴 ∣ 𝑋 ∈ ( V ∖ { 𝑍 } ) } = { 𝑛 ∈ 𝐵 ∣ 𝑋 ∈ ( V ∖ { 𝑍 } ) } )
23		eqid	⊢ ( 𝑛 ∈ 𝐴 ↦ 𝑋 ) = ( 𝑛 ∈ 𝐴 ↦ 𝑋 )
24	1 2	ssexd	⊢ ( 𝜑 → 𝐴 ∈ V )
25	24	adantl	⊢ ( ( 𝑍 ∈ V ∧ 𝜑 ) → 𝐴 ∈ V )
26		simpl	⊢ ( ( 𝑍 ∈ V ∧ 𝜑 ) → 𝑍 ∈ V )
27	23 25 26	mptsuppdifd	⊢ ( ( 𝑍 ∈ V ∧ 𝜑 ) → ( ( 𝑛 ∈ 𝐴 ↦ 𝑋 ) supp 𝑍 ) = { 𝑛 ∈ 𝐴 ∣ 𝑋 ∈ ( V ∖ { 𝑍 } ) } )
28		eqid	⊢ ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) = ( 𝑛 ∈ 𝐵 ↦ 𝑋 )
29	1	adantl	⊢ ( ( 𝑍 ∈ V ∧ 𝜑 ) → 𝐵 ∈ 𝑊 )
30	28 29 26	mptsuppdifd	⊢ ( ( 𝑍 ∈ V ∧ 𝜑 ) → ( ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) supp 𝑍 ) = { 𝑛 ∈ 𝐵 ∣ 𝑋 ∈ ( V ∖ { 𝑍 } ) } )
31	22 27 30	3eqtr4d	⊢ ( ( 𝑍 ∈ V ∧ 𝜑 ) → ( ( 𝑛 ∈ 𝐴 ↦ 𝑋 ) supp 𝑍 ) = ( ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) supp 𝑍 ) )
32	31	ex	⊢ ( 𝑍 ∈ V → ( 𝜑 → ( ( 𝑛 ∈ 𝐴 ↦ 𝑋 ) supp 𝑍 ) = ( ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) supp 𝑍 ) ) )
33		simpr	⊢ ( ( ( 𝑛 ∈ 𝐴 ↦ 𝑋 ) ∈ V ∧ 𝑍 ∈ V ) → 𝑍 ∈ V )
34	33	con3i	⊢ ( ¬ 𝑍 ∈ V → ¬ ( ( 𝑛 ∈ 𝐴 ↦ 𝑋 ) ∈ V ∧ 𝑍 ∈ V ) )
35		supp0prc	⊢ ( ¬ ( ( 𝑛 ∈ 𝐴 ↦ 𝑋 ) ∈ V ∧ 𝑍 ∈ V ) → ( ( 𝑛 ∈ 𝐴 ↦ 𝑋 ) supp 𝑍 ) = ∅ )
36	34 35	syl	⊢ ( ¬ 𝑍 ∈ V → ( ( 𝑛 ∈ 𝐴 ↦ 𝑋 ) supp 𝑍 ) = ∅ )
37		simpr	⊢ ( ( ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) ∈ V ∧ 𝑍 ∈ V ) → 𝑍 ∈ V )
38	37	con3i	⊢ ( ¬ 𝑍 ∈ V → ¬ ( ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) ∈ V ∧ 𝑍 ∈ V ) )
39		supp0prc	⊢ ( ¬ ( ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) ∈ V ∧ 𝑍 ∈ V ) → ( ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) supp 𝑍 ) = ∅ )
40	38 39	syl	⊢ ( ¬ 𝑍 ∈ V → ( ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) supp 𝑍 ) = ∅ )
41	36 40	eqtr4d	⊢ ( ¬ 𝑍 ∈ V → ( ( 𝑛 ∈ 𝐴 ↦ 𝑋 ) supp 𝑍 ) = ( ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) supp 𝑍 ) )
42	41	a1d	⊢ ( ¬ 𝑍 ∈ V → ( 𝜑 → ( ( 𝑛 ∈ 𝐴 ↦ 𝑋 ) supp 𝑍 ) = ( ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) supp 𝑍 ) ) )
43	32 42	pm2.61i	⊢ ( 𝜑 → ( ( 𝑛 ∈ 𝐴 ↦ 𝑋 ) supp 𝑍 ) = ( ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) supp 𝑍 ) )