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