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