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	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
	mreexd.2	⊢ ( 𝜑 → ∀ 𝑠 ∈ 𝒫 𝑋 ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ ( ( 𝑁 ‘ ( 𝑠 ∪ { 𝑦 } ) ) ∖ ( 𝑁 ‘ 𝑠 ) ) 𝑦 ∈ ( 𝑁 ‘ ( 𝑠 ∪ { 𝑧 } ) ) )
	mreexd.3	⊢ ( 𝜑 → 𝑆 ⊆ 𝑋 )
	mreexd.4	⊢ ( 𝜑 → 𝑌 ∈ 𝑋 )
	mreexd.5	⊢ ( 𝜑 → 𝑍 ∈ ( 𝑁 ‘ ( 𝑆 ∪ { 𝑌 } ) ) )
	mreexd.6	⊢ ( 𝜑 → ¬ 𝑍 ∈ ( 𝑁 ‘ 𝑆 ) )
Assertion	mreexd	⊢ ( 𝜑 → 𝑌 ∈ ( 𝑁 ‘ ( 𝑆 ∪ { 𝑍 } ) ) )

Proof

Step	Hyp	Ref	Expression
1		mreexd.1	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
2		mreexd.2	⊢ ( 𝜑 → ∀ 𝑠 ∈ 𝒫 𝑋 ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ ( ( 𝑁 ‘ ( 𝑠 ∪ { 𝑦 } ) ) ∖ ( 𝑁 ‘ 𝑠 ) ) 𝑦 ∈ ( 𝑁 ‘ ( 𝑠 ∪ { 𝑧 } ) ) )
3		mreexd.3	⊢ ( 𝜑 → 𝑆 ⊆ 𝑋 )
4		mreexd.4	⊢ ( 𝜑 → 𝑌 ∈ 𝑋 )
5		mreexd.5	⊢ ( 𝜑 → 𝑍 ∈ ( 𝑁 ‘ ( 𝑆 ∪ { 𝑌 } ) ) )
6		mreexd.6	⊢ ( 𝜑 → ¬ 𝑍 ∈ ( 𝑁 ‘ 𝑆 ) )
7	1 3	sselpwd	⊢ ( 𝜑 → 𝑆 ∈ 𝒫 𝑋 )
8	4	adantr	⊢ ( ( 𝜑 ∧ 𝑠 = 𝑆 ) → 𝑌 ∈ 𝑋 )
9	5	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑦 = 𝑌 ) → 𝑍 ∈ ( 𝑁 ‘ ( 𝑆 ∪ { 𝑌 } ) ) )
10		simplr	⊢ ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑦 = 𝑌 ) → 𝑠 = 𝑆 )
11		simpr	⊢ ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑦 = 𝑌 ) → 𝑦 = 𝑌 )
12	11	sneqd	⊢ ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑦 = 𝑌 ) → { 𝑦 } = { 𝑌 } )
13	10 12	uneq12d	⊢ ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑦 = 𝑌 ) → ( 𝑠 ∪ { 𝑦 } ) = ( 𝑆 ∪ { 𝑌 } ) )
14	13	fveq2d	⊢ ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑦 = 𝑌 ) → ( 𝑁 ‘ ( 𝑠 ∪ { 𝑦 } ) ) = ( 𝑁 ‘ ( 𝑆 ∪ { 𝑌 } ) ) )
15	9 14	eleqtrrd	⊢ ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑦 = 𝑌 ) → 𝑍 ∈ ( 𝑁 ‘ ( 𝑠 ∪ { 𝑦 } ) ) )
16	6	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑦 = 𝑌 ) → ¬ 𝑍 ∈ ( 𝑁 ‘ 𝑆 ) )
17	10	fveq2d	⊢ ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑦 = 𝑌 ) → ( 𝑁 ‘ 𝑠 ) = ( 𝑁 ‘ 𝑆 ) )
18	16 17	neleqtrrd	⊢ ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑦 = 𝑌 ) → ¬ 𝑍 ∈ ( 𝑁 ‘ 𝑠 ) )
19	15 18	eldifd	⊢ ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑦 = 𝑌 ) → 𝑍 ∈ ( ( 𝑁 ‘ ( 𝑠 ∪ { 𝑦 } ) ) ∖ ( 𝑁 ‘ 𝑠 ) ) )
20		simplr	⊢ ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑧 = 𝑍 ) → 𝑦 = 𝑌 )
21		simpllr	⊢ ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑧 = 𝑍 ) → 𝑠 = 𝑆 )
22		simpr	⊢ ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑧 = 𝑍 ) → 𝑧 = 𝑍 )
23	22	sneqd	⊢ ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑧 = 𝑍 ) → { 𝑧 } = { 𝑍 } )
24	21 23	uneq12d	⊢ ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑧 = 𝑍 ) → ( 𝑠 ∪ { 𝑧 } ) = ( 𝑆 ∪ { 𝑍 } ) )
25	24	fveq2d	⊢ ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑧 = 𝑍 ) → ( 𝑁 ‘ ( 𝑠 ∪ { 𝑧 } ) ) = ( 𝑁 ‘ ( 𝑆 ∪ { 𝑍 } ) ) )
26	20 25	eleq12d	⊢ ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑧 = 𝑍 ) → ( 𝑦 ∈ ( 𝑁 ‘ ( 𝑠 ∪ { 𝑧 } ) ) ↔ 𝑌 ∈ ( 𝑁 ‘ ( 𝑆 ∪ { 𝑍 } ) ) ) )
27	19 26	rspcdv	⊢ ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑦 = 𝑌 ) → ( ∀ 𝑧 ∈ ( ( 𝑁 ‘ ( 𝑠 ∪ { 𝑦 } ) ) ∖ ( 𝑁 ‘ 𝑠 ) ) 𝑦 ∈ ( 𝑁 ‘ ( 𝑠 ∪ { 𝑧 } ) ) → 𝑌 ∈ ( 𝑁 ‘ ( 𝑆 ∪ { 𝑍 } ) ) ) )
28	8 27	rspcimdv	⊢ ( ( 𝜑 ∧ 𝑠 = 𝑆 ) → ( ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ ( ( 𝑁 ‘ ( 𝑠 ∪ { 𝑦 } ) ) ∖ ( 𝑁 ‘ 𝑠 ) ) 𝑦 ∈ ( 𝑁 ‘ ( 𝑠 ∪ { 𝑧 } ) ) → 𝑌 ∈ ( 𝑁 ‘ ( 𝑆 ∪ { 𝑍 } ) ) ) )
29	7 28	rspcimdv	⊢ ( 𝜑 → ( ∀ 𝑠 ∈ 𝒫 𝑋 ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ ( ( 𝑁 ‘ ( 𝑠 ∪ { 𝑦 } ) ) ∖ ( 𝑁 ‘ 𝑠 ) ) 𝑦 ∈ ( 𝑁 ‘ ( 𝑠 ∪ { 𝑧 } ) ) → 𝑌 ∈ ( 𝑁 ‘ ( 𝑆 ∪ { 𝑍 } ) ) ) )
30	2 29	mpd	⊢ ( 𝜑 → 𝑌 ∈ ( 𝑁 ‘ ( 𝑆 ∪ { 𝑍 } ) ) )