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 φ B W
extmptsuppeq.a φ A B
extmptsuppeq.z φ n B A X = Z
Assertion extmptsuppeq φ n A X supp Z = n B X supp Z

Proof

Step Hyp Ref Expression
1 extmptsuppeq.b φ B W
2 extmptsuppeq.a φ A B
3 extmptsuppeq.z φ n B A X = Z
4 2 adantl Z V φ A B
5 4 sseld Z V φ n A n B
6 5 anim1d Z V φ n A X V Z n B X V Z
7 eldif n B A n B ¬ n A
8 3 adantll Z V φ n B A X = Z
9 7 8 sylan2br Z V φ n B ¬ n A X = Z
10 9 expr Z V φ n B ¬ n A X = Z
11 elsn2g Z V X Z X = Z
12 elndif X Z ¬ X V Z
13 11 12 syl6bir Z V X = Z ¬ X V Z
14 13 ad2antrr Z V φ n B X = Z ¬ X V Z
15 10 14 syld Z V φ n B ¬ n A ¬ X V Z
16 15 con4d Z V φ n B X V Z n A
17 16 impr Z V φ n B X V Z n A
18 simprr Z V φ n B X V Z X V Z
19 17 18 jca Z V φ n B X V Z n A X V Z
20 19 ex Z V φ n B X V Z n A X V Z
21 6 20 impbid Z V φ n A X V Z n B X V Z
22 21 rabbidva2 Z V φ n A | X V Z = n B | X V Z
23 eqid n A X = n A X
24 1 2 ssexd φ A V
25 24 adantl Z V φ A V
26 simpl Z V φ Z V
27 23 25 26 mptsuppdifd Z V φ n A X supp Z = n A | X V Z
28 eqid n B X = n B X
29 1 adantl Z V φ B W
30 28 29 26 mptsuppdifd Z V φ n B X supp Z = n B | X V Z
31 22 27 30 3eqtr4d Z V φ n A X supp Z = n B X supp Z
32 31 ex Z V φ n A X supp Z = n B X supp Z
33 simpr n A X V Z V Z V
34 33 con3i ¬ Z V ¬ n A X V Z V
35 supp0prc ¬ n A X V Z V n A X supp Z =
36 34 35 syl ¬ Z V n A X supp Z =
37 simpr n B X V Z V Z V
38 37 con3i ¬ Z V ¬ n B X V Z V
39 supp0prc ¬ n B X V Z V n B X supp Z =
40 38 39 syl ¬ Z V n B X supp Z =
41 36 40 eqtr4d ¬ Z V n A X supp Z = n B X supp Z
42 41 a1d ¬ Z V φ n A X supp Z = n B X supp Z
43 32 42 pm2.61i φ n A X supp Z = n B X supp Z