Theorem mreexd 16302

Description: In a Moore system, the closure operator is said to have the exchange 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.)

Hypotheses

Ref	Expression
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

Ref	Expression
mreexd	|- ( ph -> Y e. ( N ` ( S u. { Z } ) ) )

Distinct variable groups:   X, s, y   S, s, z, y   ph, s, y, z   Y, s, y, z   Z, s, y, z   N, s, y, z

Allowed substitution hints:   V( y, z, s)   X( z)

Proof of Theorem mreexd

Step	Hyp	Ref	Expression
1		mreexd.2	. 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 } ) ) )
2		mreexd.1	. . . 4 |- ( ph -> X e. V )
3		mreexd.3	. . . 4 |- ( ph -> S C_ X )
4	2, 3	sselpwd 4807	. . 3 |- ( ph -> S e. ~P X )
5		mreexd.4	. . . . 5 |- ( ph -> Y e. X )
6	5	adantr 481	. . . 4 |- ( ( ph /\ s = S ) -> Y e. X )
7		mreexd.5	. . . . . . . 8 |- ( ph -> Z e. ( N ` ( S u. { Y } ) ) )
8	7	ad2antrr 762	. . . . . . 7 |- ( ( ( ph /\ s = S ) /\ y = Y ) -> Z e. ( N ` ( S u. { Y } ) ) )
9		simplr 792	. . . . . . . . 9 |- ( ( ( ph /\ s = S ) /\ y = Y ) -> s = S )
10		simpr 477	. . . . . . . . . 10 |- ( ( ( ph /\ s = S ) /\ y = Y ) -> y = Y )
11	10	sneqd 4189	. . . . . . . . 9 |- ( ( ( ph /\ s = S ) /\ y = Y ) -> { y } = { Y } )
12	9, 11	uneq12d 3768	. . . . . . . 8 |- ( ( ( ph /\ s = S ) /\ y = Y ) -> ( s u. { y } ) = ( S u. { Y } ) )
13	12	fveq2d 6195	. . . . . . 7 |- ( ( ( ph /\ s = S ) /\ y = Y ) -> ( N ` ( s u. { y } ) ) = ( N ` ( S u. { Y } ) ) )
14	8, 13	eleqtrrd 2704	. . . . . 6 |- ( ( ( ph /\ s = S ) /\ y = Y ) -> Z e. ( N ` ( s u. { y } ) ) )
15		mreexd.6	. . . . . . . 8 |- ( ph -> -. Z e. ( N ` S ) )
16	15	ad2antrr 762	. . . . . . 7 |- ( ( ( ph /\ s = S ) /\ y = Y ) -> -. Z e. ( N ` S ) )
17	9	fveq2d 6195	. . . . . . 7 |- ( ( ( ph /\ s = S ) /\ y = Y ) -> ( N ` s ) = ( N ` S ) )
18	16, 17	neleqtrrd 2723	. . . . . 6 |- ( ( ( ph /\ s = S ) /\ y = Y ) -> -. Z e. ( N ` s ) )
19	14, 18	eldifd 3585	. . . . 5 |- ( ( ( ph /\ s = S ) /\ y = Y ) -> Z e. ( ( N ` ( s u. { y } ) ) \ ( N ` s ) ) )
20		simplr 792	. . . . . 6 |- ( ( ( ( ph /\ s = S ) /\ y = Y ) /\ z = Z ) -> y = Y )
21		simpllr 799	. . . . . . . 8 |- ( ( ( ( ph /\ s = S ) /\ y = Y ) /\ z = Z ) -> s = S )
22		simpr 477	. . . . . . . . 9 |- ( ( ( ( ph /\ s = S ) /\ y = Y ) /\ z = Z ) -> z = Z )
23	22	sneqd 4189	. . . . . . . 8 |- ( ( ( ( ph /\ s = S ) /\ y = Y ) /\ z = Z ) -> { z } = { Z } )
24	21, 23	uneq12d 3768	. . . . . . 7 |- ( ( ( ( ph /\ s = S ) /\ y = Y ) /\ z = Z ) -> ( s u. { z } ) = ( S u. { Z } ) )
25	24	fveq2d 6195	. . . . . 6 |- ( ( ( ( ph /\ s = S ) /\ y = Y ) /\ z = Z ) -> ( N ` ( s u. { z } ) ) = ( N ` ( S u. { Z } ) ) )
26	20, 25	eleq12d 2695	. . . . 5 |- ( ( ( ( ph /\ s = S ) /\ y = Y ) /\ z = Z ) -> ( y e. ( N ` ( s u. { z } ) ) <-> Y e. ( N ` ( S u. { Z } ) ) ) )
27	19, 26	rspcdv 3312	. . . 4 |- ( ( ( 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	6, 27	rspcimdv 3310	. . 3 |- ( ( 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	4, 28	rspcimdv 3310	. 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 } ) ) -> Y e. ( N ` ( S u. { Z } ) ) ) )
30	1, 29	mpd 15	1 |- ( ph -> Y e. ( N ` ( S u. { Z } ) ) )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 384   = wceq 1483   e. wcel 1990   A.wral 2912   \ cdif 3571   u. cun 3572   C_ wss 3574   ~Pcpw 4158   {csn 4177   ` cfv 5888

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-iota 5851  df-fv 5896

This theorem is referenced by:  mreexmrid  16303