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⟼XsuppZ=n∈B⟼XsuppZ

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⟼XsuppZ=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⟼XsuppZ=n∈B|X∈V∖Z
31 22 27 30 3eqtr4d ⊢Z∈V∧φ→n∈A⟼XsuppZ=n∈B⟼XsuppZ
32 31 ex ⊢Z∈V→φ→n∈A⟼XsuppZ=n∈B⟼XsuppZ
33 simpr ⊢n∈A⟼X∈V∧Z∈V→Z∈V
34 supp0prc ⊢¬n∈A⟼X∈V∧Z∈V→n∈A⟼XsuppZ=∅
35 33 34 nsyl5 ⊢¬Z∈V→n∈A⟼XsuppZ=∅
36 simpr ⊢n∈B⟼X∈V∧Z∈V→Z∈V
37 supp0prc ⊢¬n∈B⟼X∈V∧Z∈V→n∈B⟼XsuppZ=∅
38 36 37 nsyl5 ⊢¬Z∈V→n∈B⟼XsuppZ=∅
39 35 38 eqtr4d ⊢¬Z∈V→n∈A⟼XsuppZ=n∈B⟼XsuppZ
40 39 a1d ⊢¬Z∈V→φ→n∈A⟼XsuppZ=n∈B⟼XsuppZ
41 32 40 pm2.61i ⊢φ→n∈A⟼XsuppZ=n∈B⟼XsuppZ