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	$⊢ φ \to B \in W$
	extmptsuppeq.a	$⊢ φ \to A \subseteq B$
	extmptsuppeq.z	$⊢ (φ \land n \in (B ∖ A)) \to X = Z$
Assertion	extmptsuppeq	$⊢ φ \to (n \in A ⟼ X) supp Z = (n \in B ⟼ X) supp Z$

Proof

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

Metamath Proof Explorer

Theorem extmptsuppeq

Proof