Metamath Proof Explorer


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 us 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 } ) ) )