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 ( 𝜑𝑋𝑉 )
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 ( 𝜑𝑌 ∈ ( 𝑁 ‘ ( 𝑆 ∪ { 𝑍 } ) ) )