mreexd

Description: In a Moore system, the closure operator is said to have theexchange property if, for all elements y and z of the base set and subsets S of the base set such that z is in the closure of ( S u. { y } ) but not in the closure of S , y is in the closure of ( S u. { z } ) (Definition 3.1.9 in FaureFrolicher p. 57 to 58.) This theorem allows us to construct substitution instances of this definition. (Contributed by David Moews, 1-May-2017)

	Ref	Expression
Hypotheses	mreexd.1	$⊢ φ \to X \in V$
	mreexd.2	$⊢ φ \to \forall s \in 𝒫 X \forall y \in X \forall z \in (N (s \cup \{y\}) ∖ N (s)) y \in N (s \cup \{z\})$
	mreexd.3	$⊢ φ \to S \subseteq X$
	mreexd.4	$⊢ φ \to Y \in X$
	mreexd.5	$⊢ φ \to Z \in N (S \cup \{Y\})$
	mreexd.6	$⊢ φ \to \neg Z \in N (S)$
Assertion	mreexd	$⊢ φ \to Y \in N (S \cup \{Z\})$

Proof

Step	Hyp	Ref	Expression
1		mreexd.1	$⊢ φ \to X \in V$
2		mreexd.2	$⊢ φ \to \forall s \in 𝒫 X \forall y \in X \forall z \in (N (s \cup \{y\}) ∖ N (s)) y \in N (s \cup \{z\})$
3		mreexd.3	$⊢ φ \to S \subseteq X$
4		mreexd.4	$⊢ φ \to Y \in X$
5		mreexd.5	$⊢ φ \to Z \in N (S \cup \{Y\})$
6		mreexd.6	$⊢ φ \to \neg Z \in N (S)$
7	1 3	sselpwd	$⊢ φ \to S \in 𝒫 X$
8	4	adantr	$⊢ (φ \land s = S) \to Y \in X$
9	5	ad2antrr	$⊢ ((φ \land s = S) \land y = Y) \to Z \in N (S \cup \{Y\})$
10		simplr	$⊢ ((φ \land s = S) \land y = Y) \to s = S$
11		simpr	$⊢ ((φ \land s = S) \land y = Y) \to y = Y$
12	11	sneqd	$⊢ ((φ \land s = S) \land y = Y) \to \{y\} = \{Y\}$
13	10 12	uneq12d	$⊢ ((φ \land s = S) \land y = Y) \to s \cup \{y\} = S \cup \{Y\}$
14	13	fveq2d	$⊢ ((φ \land s = S) \land y = Y) \to N (s \cup \{y\}) = N (S \cup \{Y\})$
15	9 14	eleqtrrd	$⊢ ((φ \land s = S) \land y = Y) \to Z \in N (s \cup \{y\})$
16	6	ad2antrr	$⊢ ((φ \land s = S) \land y = Y) \to \neg Z \in N (S)$
17	10	fveq2d	$⊢ ((φ \land s = S) \land y = Y) \to N (s) = N (S)$
18	16 17	neleqtrrd	$⊢ ((φ \land s = S) \land y = Y) \to \neg Z \in N (s)$
19	15 18	eldifd	$⊢ ((φ \land s = S) \land y = Y) \to Z \in (N (s \cup \{y\}) ∖ N (s))$
20		simplr	$⊢ (((φ \land s = S) \land y = Y) \land z = Z) \to y = Y$
21		simpllr	$⊢ (((φ \land s = S) \land y = Y) \land z = Z) \to s = S$
22		simpr	$⊢ (((φ \land s = S) \land y = Y) \land z = Z) \to z = Z$
23	22	sneqd	$⊢ (((φ \land s = S) \land y = Y) \land z = Z) \to \{z\} = \{Z\}$
24	21 23	uneq12d	$⊢ (((φ \land s = S) \land y = Y) \land z = Z) \to s \cup \{z\} = S \cup \{Z\}$
25	24	fveq2d	$⊢ (((φ \land s = S) \land y = Y) \land z = Z) \to N (s \cup \{z\}) = N (S \cup \{Z\})$
26	20 25	eleq12d	$⊢ (((φ \land s = S) \land y = Y) \land z = Z) \to (y \in N (s \cup \{z\}) \leftrightarrow Y \in N (S \cup \{Z\}))$
27	19 26	rspcdv	$⊢ ((φ \land s = S) \land y = Y) \to (\forall z \in (N (s \cup \{y\}) ∖ N (s)) y \in N (s \cup \{z\}) \to Y \in N (S \cup \{Z\}))$
28	8 27	rspcimdv	$⊢ (φ \land s = S) \to (\forall y \in X \forall z \in (N (s \cup \{y\}) ∖ N (s)) y \in N (s \cup \{z\}) \to Y \in N (S \cup \{Z\}))$
29	7 28	rspcimdv	$⊢ φ \to (\forall s \in 𝒫 X \forall y \in X \forall z \in (N (s \cup \{y\}) ∖ N (s)) y \in N (s \cup \{z\}) \to Y \in N (S \cup \{Z\}))$
30	2 29	mpd	$⊢ φ \to Y \in N (S \cup \{Z\})$

Metamath Proof Explorer

Theorem mreexd

Proof