Theorem 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 to construct substitution instances of this definition. (Contributed by David Moews, 1-May-2017)

	Ref	Expression
Hypotheses	mreexd.1	|- ( ph -> X e. V )
	mreexd.2	|- ( ph -> A. s e. ~P X A. y e. X A. z e. ( ( N ` ( s u. { y } ) ) \ ( N ` s ) ) y e. ( N ` ( s u. { z } ) ) )
	mreexd.3	|- ( ph -> S C_ X )
	mreexd.4	|- ( ph -> Y e. X )
	mreexd.5	|- ( ph -> Z e. ( N ` ( S u. { Y } ) ) )
	mreexd.6	|- ( ph -> -. Z e. ( N ` S ) )
Assertion	mreexd	|- ( ph -> Y e. ( N ` ( S u. { Z } ) ) )

Proof

Step	Hyp	Ref	Expression
1		mreexd.1	|- ( ph -> X e. V )
2		mreexd.2	|- ( ph -> A. s e. ~P X A. y e. X A. z e. ( ( N ` ( s u. { y } ) ) \ ( N ` s ) ) y e. ( N ` ( s u. { z } ) ) )
3		mreexd.3	|- ( ph -> S C_ X )
4		mreexd.4	|- ( ph -> Y e. X )
5		mreexd.5	|- ( ph -> Z e. ( N ` ( S u. { Y } ) ) )
6		mreexd.6	|- ( ph -> -. Z e. ( N ` S ) )
7	1 3	sselpwd	|- ( ph -> S e. ~P X )
8	4	adantr	|- ( ( ph /\ s = S ) -> Y e. X )
9	5	ad2antrr	|- ( ( ( ph /\ s = S ) /\ y = Y ) -> Z e. ( N ` ( S u. { Y } ) ) )
10		simplr	|- ( ( ( ph /\ s = S ) /\ y = Y ) -> s = S )
11		simpr	|- ( ( ( ph /\ s = S ) /\ y = Y ) -> y = Y )
12	11	sneqd	|- ( ( ( ph /\ s = S ) /\ y = Y ) -> { y } = { Y } )
13	10 12	uneq12d	|- ( ( ( ph /\ s = S ) /\ y = Y ) -> ( s u. { y } ) = ( S u. { Y } ) )
14	13	fveq2d	|- ( ( ( ph /\ s = S ) /\ y = Y ) -> ( N ` ( s u. { y } ) ) = ( N ` ( S u. { Y } ) ) )
15	9 14	eleqtrrd	|- ( ( ( ph /\ s = S ) /\ y = Y ) -> Z e. ( N ` ( s u. { y } ) ) )
16	6	ad2antrr	|- ( ( ( ph /\ s = S ) /\ y = Y ) -> -. Z e. ( N ` S ) )
17	10	fveq2d	|- ( ( ( ph /\ s = S ) /\ y = Y ) -> ( N ` s ) = ( N ` S ) )
18	16 17	neleqtrrd	|- ( ( ( ph /\ s = S ) /\ y = Y ) -> -. Z e. ( N ` s ) )
19	15 18	eldifd	|- ( ( ( ph /\ s = S ) /\ y = Y ) -> Z e. ( ( N ` ( s u. { y } ) ) \ ( N ` s ) ) )
20		simplr	|- ( ( ( ( ph /\ s = S ) /\ y = Y ) /\ z = Z ) -> y = Y )
21		simpllr	|- ( ( ( ( ph /\ s = S ) /\ y = Y ) /\ z = Z ) -> s = S )
22		simpr	|- ( ( ( ( ph /\ s = S ) /\ y = Y ) /\ z = Z ) -> z = Z )
23	22	sneqd	|- ( ( ( ( ph /\ s = S ) /\ y = Y ) /\ z = Z ) -> { z } = { Z } )
24	21 23	uneq12d	|- ( ( ( ( ph /\ s = S ) /\ y = Y ) /\ z = Z ) -> ( s u. { z } ) = ( S u. { Z } ) )
25	24	fveq2d	|- ( ( ( ( ph /\ s = S ) /\ y = Y ) /\ z = Z ) -> ( N ` ( s u. { z } ) ) = ( N ` ( S u. { Z } ) ) )
26	20 25	eleq12d	|- ( ( ( ( ph /\ s = S ) /\ y = Y ) /\ z = Z ) -> ( y e. ( N ` ( s u. { z } ) ) <-> Y e. ( N ` ( S u. { Z } ) ) ) )
27	19 26	rspcdv	|- ( ( ( ph /\ s = S ) /\ y = Y ) -> ( A. z e. ( ( N ` ( s u. { y } ) ) \ ( N ` s ) ) y e. ( N ` ( s u. { z } ) ) -> Y e. ( N ` ( S u. { Z } ) ) ) )
28	8 27	rspcimdv	|- ( ( ph /\ s = S ) -> ( A. y e. X A. z e. ( ( N ` ( s u. { y } ) ) \ ( N ` s ) ) y e. ( N ` ( s u. { z } ) ) -> Y e. ( N ` ( S u. { Z } ) ) ) )
29	7 28	rspcimdv	|- ( ph -> ( A. s e. ~P X A. y e. X A. z e. ( ( N ` ( s u. { y } ) ) \ ( N ` s ) ) y e. ( N ` ( s u. { z } ) ) -> Y e. ( N ` ( S u. { Z } ) ) ) )
30	2 29	mpd	|- ( ph -> Y e. ( N ` ( S u. { Z } ) ) )