This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem mreexdomd

Description: In a Moore system whose closure operator has the exchange property, if S is independent and contained in the closure of T , and either S or T is finite, then T dominates S . This is an immediate consequence of mreexexd . (Contributed by David Moews, 1-May-2017)

Ref Expression
Hypotheses mreexdomd.1 ⊢ ( 𝜑 → 𝐴 ∈ ( Moore ‘ 𝑋 ) )
mreexdomd.2 ⊢ 𝑁 = ( mrCls ‘ 𝐴 )
mreexdomd.3 ⊢ 𝐼 = ( mrInd ‘ 𝐴 )
mreexdomd.4 ⊢ ( 𝜑 → ∀ 𝑠 ∈ 𝒫 𝑋 ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ ( ( 𝑁 ‘ ( 𝑠 ∪ { 𝑦 } ) ) ∖ ( 𝑁 ‘ 𝑠 ) ) 𝑦 ∈ ( 𝑁 ‘ ( 𝑠 ∪ { 𝑧 } ) ) )
mreexdomd.5 ⊢ ( 𝜑 → 𝑆 ⊆ ( 𝑁 ‘ 𝑇 ) )
mreexdomd.6 ⊢ ( 𝜑 → 𝑇 ⊆ 𝑋 )
mreexdomd.7 ⊢ ( 𝜑 → ( 𝑆 ∈ Fin ∨ 𝑇 ∈ Fin ) )
mreexdomd.8 ⊢ ( 𝜑 → 𝑆 ∈ 𝐼 )
Assertion mreexdomd ( 𝜑 → 𝑆 ≼ 𝑇 )

Proof

Step Hyp Ref Expression
1 mreexdomd.1 ⊢ ( 𝜑 → 𝐴 ∈ ( Moore ‘ 𝑋 ) )
2 mreexdomd.2 ⊢ 𝑁 = ( mrCls ‘ 𝐴 )
3 mreexdomd.3 ⊢ 𝐼 = ( mrInd ‘ 𝐴 )
4 mreexdomd.4 ⊢ ( 𝜑 → ∀ 𝑠 ∈ 𝒫 𝑋 ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ ( ( 𝑁 ‘ ( 𝑠 ∪ { 𝑦 } ) ) ∖ ( 𝑁 ‘ 𝑠 ) ) 𝑦 ∈ ( 𝑁 ‘ ( 𝑠 ∪ { 𝑧 } ) ) )
5 mreexdomd.5 ⊢ ( 𝜑 → 𝑆 ⊆ ( 𝑁 ‘ 𝑇 ) )
6 mreexdomd.6 ⊢ ( 𝜑 → 𝑇 ⊆ 𝑋 )
7 mreexdomd.7 ⊢ ( 𝜑 → ( 𝑆 ∈ Fin ∨ 𝑇 ∈ Fin ) )
8 mreexdomd.8 ⊢ ( 𝜑 → 𝑆 ∈ 𝐼 )
9 3 1 8 mrissd ⊢ ( 𝜑 → 𝑆 ⊆ 𝑋 )
10 dif0 ⊢ ( 𝑋 ∖ ∅ ) = 𝑋
11 9 10 sseqtrrdi ⊢ ( 𝜑 → 𝑆 ⊆ ( 𝑋 ∖ ∅ ) )
12 6 10 sseqtrrdi ⊢ ( 𝜑 → 𝑇 ⊆ ( 𝑋 ∖ ∅ ) )
13 un0 ⊢ ( 𝑇 ∪ ∅ ) = 𝑇
14 13 fveq2i ⊢ ( 𝑁 ‘ ( 𝑇 ∪ ∅ ) ) = ( 𝑁 ‘ 𝑇 )
15 5 14 sseqtrrdi ⊢ ( 𝜑 → 𝑆 ⊆ ( 𝑁 ‘ ( 𝑇 ∪ ∅ ) ) )
16 un0 ⊢ ( 𝑆 ∪ ∅ ) = 𝑆
17 16 8 eqeltrid ⊢ ( 𝜑 → ( 𝑆 ∪ ∅ ) ∈ 𝐼 )
18 1 2 3 4 11 12 15 17 7 mreexexd ⊢ ( 𝜑 → ∃ 𝑖 ∈ 𝒫 𝑇 ( 𝑆 ≈ 𝑖 ∧ ( 𝑖 ∪ ∅ ) ∈ 𝐼 ) )
19 simprrl ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝒫 𝑇 ∧ ( 𝑆 ≈ 𝑖 ∧ ( 𝑖 ∪ ∅ ) ∈ 𝐼 ) ) ) → 𝑆 ≈ 𝑖 )
20 simprl ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝒫 𝑇 ∧ ( 𝑆 ≈ 𝑖 ∧ ( 𝑖 ∪ ∅ ) ∈ 𝐼 ) ) ) → 𝑖 ∈ 𝒫 𝑇 )
21 20 elpwid ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝒫 𝑇 ∧ ( 𝑆 ≈ 𝑖 ∧ ( 𝑖 ∪ ∅ ) ∈ 𝐼 ) ) ) → 𝑖 ⊆ 𝑇 )
22 1 elfvexd ⊢ ( 𝜑 → 𝑋 ∈ V )
23 22 6 ssexd ⊢ ( 𝜑 → 𝑇 ∈ V )
24 ssdomg ⊢ ( 𝑇 ∈ V → ( 𝑖 ⊆ 𝑇 → 𝑖 ≼ 𝑇 ) )
25 23 24 syl ⊢ ( 𝜑 → ( 𝑖 ⊆ 𝑇 → 𝑖 ≼ 𝑇 ) )
26 25 adantr ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝒫 𝑇 ∧ ( 𝑆 ≈ 𝑖 ∧ ( 𝑖 ∪ ∅ ) ∈ 𝐼 ) ) ) → ( 𝑖 ⊆ 𝑇 → 𝑖 ≼ 𝑇 ) )
27 21 26 mpd ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝒫 𝑇 ∧ ( 𝑆 ≈ 𝑖 ∧ ( 𝑖 ∪ ∅ ) ∈ 𝐼 ) ) ) → 𝑖 ≼ 𝑇 )
28 endomtr ⊢ ( ( 𝑆 ≈ 𝑖 ∧ 𝑖 ≼ 𝑇 ) → 𝑆 ≼ 𝑇 )
29 19 27 28 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝒫 𝑇 ∧ ( 𝑆 ≈ 𝑖 ∧ ( 𝑖 ∪ ∅ ) ∈ 𝐼 ) ) ) → 𝑆 ≼ 𝑇 )
30 18 29 rexlimddv ⊢ ( 𝜑 → 𝑆 ≼ 𝑇 )