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

Metamath Proof Explorer

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 biimtrrdi ⊢ ( 𝑍 ∈ 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 supp0prc ⊢ ( ¬ ( ( 𝑛 ∈ 𝐴 ↦ 𝑋 ) ∈ V ∧ 𝑍 ∈ V ) → ( ( 𝑛 ∈ 𝐴 ↦ 𝑋 ) supp 𝑍 ) = ∅ )
35 33 34 nsyl5 ⊢ ( ¬ 𝑍 ∈ V → ( ( 𝑛 ∈ 𝐴 ↦ 𝑋 ) supp 𝑍 ) = ∅ )
36 simpr ⊢ ( ( ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) ∈ V ∧ 𝑍 ∈ V ) → 𝑍 ∈ V )
37 supp0prc ⊢ ( ¬ ( ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) ∈ V ∧ 𝑍 ∈ V ) → ( ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) supp 𝑍 ) = ∅ )
38 36 37 nsyl5 ⊢ ( ¬ 𝑍 ∈ V → ( ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) supp 𝑍 ) = ∅ )
39 35 38 eqtr4d ⊢ ( ¬ 𝑍 ∈ V → ( ( 𝑛 ∈ 𝐴 ↦ 𝑋 ) supp 𝑍 ) = ( ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) supp 𝑍 ) )
40 39 a1d ⊢ ( ¬ 𝑍 ∈ V → ( 𝜑 → ( ( 𝑛 ∈ 𝐴 ↦ 𝑋 ) supp 𝑍 ) = ( ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) supp 𝑍 ) ) )
41 32 40 pm2.61i ⊢ ( 𝜑 → ( ( 𝑛 ∈ 𝐴 ↦ 𝑋 ) supp 𝑍 ) = ( ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) supp 𝑍 ) )