Metamath Proof Explorer

Theorem mrieqvlemd

Description: In a Moore system, if Y is a member of S , ( S \ { Y } ) and S have the same closure if and only if Y is in the closure of ( S \ { Y } ) . Used in the proof of mrieqvd and mrieqv2d . Deduction form. (Contributed by David Moews, 1-May-2017)

Ref Expression
Hypotheses mrieqvlemd.1 ⊢ ( 𝜑 → 𝐴 ∈ ( Moore ‘ 𝑋 ) )
mrieqvlemd.2 ⊢ 𝑁 = ( mrCls ‘ 𝐴 )
mrieqvlemd.3 ⊢ ( 𝜑 → 𝑆 ⊆ 𝑋 )
mrieqvlemd.4 ⊢ ( 𝜑 → 𝑌 ∈ 𝑆 )
Assertion mrieqvlemd ( 𝜑 → ( 𝑌 ∈ ( 𝑁 ‘ ( 𝑆 ∖ { 𝑌 } ) ) ↔ ( 𝑁 ‘ ( 𝑆 ∖ { 𝑌 } ) ) = ( 𝑁 ‘ 𝑆 ) ) )

Proof

Step Hyp Ref Expression
1 mrieqvlemd.1 ⊢ ( 𝜑 → 𝐴 ∈ ( Moore ‘ 𝑋 ) )
2 mrieqvlemd.2 ⊢ 𝑁 = ( mrCls ‘ 𝐴 )
3 mrieqvlemd.3 ⊢ ( 𝜑 → 𝑆 ⊆ 𝑋 )
4 mrieqvlemd.4 ⊢ ( 𝜑 → 𝑌 ∈ 𝑆 )
5 1 adantr ⊢ ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑁 ‘ ( 𝑆 ∖ { 𝑌 } ) ) ) → 𝐴 ∈ ( Moore ‘ 𝑋 ) )
6 undif1 ⊢ ( ( 𝑆 ∖ { 𝑌 } ) ∪ { 𝑌 } ) = ( 𝑆 ∪ { 𝑌 } )
7 3 adantr ⊢ ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑁 ‘ ( 𝑆 ∖ { 𝑌 } ) ) ) → 𝑆 ⊆ 𝑋 )
8 7 ssdifssd ⊢ ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑁 ‘ ( 𝑆 ∖ { 𝑌 } ) ) ) → ( 𝑆 ∖ { 𝑌 } ) ⊆ 𝑋 )
9 5 2 8 mrcssidd ⊢ ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑁 ‘ ( 𝑆 ∖ { 𝑌 } ) ) ) → ( 𝑆 ∖ { 𝑌 } ) ⊆ ( 𝑁 ‘ ( 𝑆 ∖ { 𝑌 } ) ) )
10 simpr ⊢ ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑁 ‘ ( 𝑆 ∖ { 𝑌 } ) ) ) → 𝑌 ∈ ( 𝑁 ‘ ( 𝑆 ∖ { 𝑌 } ) ) )
11 10 snssd ⊢ ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑁 ‘ ( 𝑆 ∖ { 𝑌 } ) ) ) → { 𝑌 } ⊆ ( 𝑁 ‘ ( 𝑆 ∖ { 𝑌 } ) ) )
12 9 11 unssd ⊢ ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑁 ‘ ( 𝑆 ∖ { 𝑌 } ) ) ) → ( ( 𝑆 ∖ { 𝑌 } ) ∪ { 𝑌 } ) ⊆ ( 𝑁 ‘ ( 𝑆 ∖ { 𝑌 } ) ) )
13 6 12 eqsstrrid ⊢ ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑁 ‘ ( 𝑆 ∖ { 𝑌 } ) ) ) → ( 𝑆 ∪ { 𝑌 } ) ⊆ ( 𝑁 ‘ ( 𝑆 ∖ { 𝑌 } ) ) )
14 13 unssad ⊢ ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑁 ‘ ( 𝑆 ∖ { 𝑌 } ) ) ) → 𝑆 ⊆ ( 𝑁 ‘ ( 𝑆 ∖ { 𝑌 } ) ) )
15 difssd ⊢ ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑁 ‘ ( 𝑆 ∖ { 𝑌 } ) ) ) → ( 𝑆 ∖ { 𝑌 } ) ⊆ 𝑆 )
16 5 2 14 15 mressmrcd ⊢ ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑁 ‘ ( 𝑆 ∖ { 𝑌 } ) ) ) → ( 𝑁 ‘ 𝑆 ) = ( 𝑁 ‘ ( 𝑆 ∖ { 𝑌 } ) ) )
17 16 eqcomd ⊢ ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑁 ‘ ( 𝑆 ∖ { 𝑌 } ) ) ) → ( 𝑁 ‘ ( 𝑆 ∖ { 𝑌 } ) ) = ( 𝑁 ‘ 𝑆 ) )
18 1 2 3 mrcssidd ⊢ ( 𝜑 → 𝑆 ⊆ ( 𝑁 ‘ 𝑆 ) )
19 18 4 sseldd ⊢ ( 𝜑 → 𝑌 ∈ ( 𝑁 ‘ 𝑆 ) )
20 19 adantr ⊢ ( ( 𝜑 ∧ ( 𝑁 ‘ ( 𝑆 ∖ { 𝑌 } ) ) = ( 𝑁 ‘ 𝑆 ) ) → 𝑌 ∈ ( 𝑁 ‘ 𝑆 ) )
21 simpr ⊢ ( ( 𝜑 ∧ ( 𝑁 ‘ ( 𝑆 ∖ { 𝑌 } ) ) = ( 𝑁 ‘ 𝑆 ) ) → ( 𝑁 ‘ ( 𝑆 ∖ { 𝑌 } ) ) = ( 𝑁 ‘ 𝑆 ) )
22 20 21 eleqtrrd ⊢ ( ( 𝜑 ∧ ( 𝑁 ‘ ( 𝑆 ∖ { 𝑌 } ) ) = ( 𝑁 ‘ 𝑆 ) ) → 𝑌 ∈ ( 𝑁 ‘ ( 𝑆 ∖ { 𝑌 } ) ) )
23 17 22 impbida ⊢ ( 𝜑 → ( 𝑌 ∈ ( 𝑁 ‘ ( 𝑆 ∖ { 𝑌 } ) ) ↔ ( 𝑁 ‘ ( 𝑆 ∖ { 𝑌 } ) ) = ( 𝑁 ‘ 𝑆 ) ) )