This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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