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 ⊢ φ → A ∈ Moore ⁡ X
mreexdomd.2 ⊢ N = mrCls ⁡ A
mreexdomd.3 ⊢ I = mrInd ⁡ A
mreexdomd.4 ⊢ φ → ∀ s ∈ 𝒫 X ∀ y ∈ X ∀ z ∈ N ⁡ s ∪ y ∖ N ⁡ s y ∈ N ⁡ s ∪ z
mreexdomd.5 ⊢ φ → S ⊆ N ⁡ T
mreexdomd.6 ⊢ φ → T ⊆ X
mreexdomd.7 ⊢ φ → S ∈ Fin ∨ T ∈ Fin
mreexdomd.8 ⊢ φ → S ∈ I
Assertion mreexdomd ⊢ φ → S ≼ T

Proof

Step Hyp Ref Expression
1 mreexdomd.1 ⊢ φ → A ∈ Moore ⁡ X
2 mreexdomd.2 ⊢ N = mrCls ⁡ A
3 mreexdomd.3 ⊢ I = mrInd ⁡ A
4 mreexdomd.4 ⊢ φ → ∀ s ∈ 𝒫 X ∀ y ∈ X ∀ z ∈ N ⁡ s ∪ y ∖ N ⁡ s y ∈ N ⁡ s ∪ z
5 mreexdomd.5 ⊢ φ → S ⊆ N ⁡ T
6 mreexdomd.6 ⊢ φ → T ⊆ X
7 mreexdomd.7 ⊢ φ → S ∈ Fin ∨ T ∈ Fin
8 mreexdomd.8 ⊢ φ → S ∈ I
9 3 1 8 mrissd ⊢ φ → S ⊆ X
10 dif0 ⊢ X ∖ ∅ = X
11 9 10 sseqtrrdi ⊢ φ → S ⊆ X ∖ ∅
12 6 10 sseqtrrdi ⊢ φ → T ⊆ X ∖ ∅
13 un0 ⊢ T ∪ ∅ = T
14 13 fveq2i ⊢ N ⁡ T ∪ ∅ = N ⁡ T
15 5 14 sseqtrrdi ⊢ φ → S ⊆ N ⁡ T ∪ ∅
16 un0 ⊢ S ∪ ∅ = S
17 16 8 eqeltrid ⊢ φ → S ∪ ∅ ∈ I
18 1 2 3 4 11 12 15 17 7 mreexexd ⊢ φ → ∃ i ∈ 𝒫 T S ≈ i ∧ i ∪ ∅ ∈ I
19 simprrl ⊢ φ ∧ i ∈ 𝒫 T ∧ S ≈ i ∧ i ∪ ∅ ∈ I → S ≈ i
20 simprl ⊢ φ ∧ i ∈ 𝒫 T ∧ S ≈ i ∧ i ∪ ∅ ∈ I → i ∈ 𝒫 T
21 20 elpwid ⊢ φ ∧ i ∈ 𝒫 T ∧ S ≈ i ∧ i ∪ ∅ ∈ I → i ⊆ T
22 1 elfvexd ⊢ φ → X ∈ V
23 22 6 ssexd ⊢ φ → T ∈ V
24 ssdomg ⊢ T ∈ V → i ⊆ T → i ≼ T
25 23 24 syl ⊢ φ → i ⊆ T → i ≼ T
26 25 adantr ⊢ φ ∧ i ∈ 𝒫 T ∧ S ≈ i ∧ i ∪ ∅ ∈ I → i ⊆ T → i ≼ T
27 21 26 mpd ⊢ φ ∧ i ∈ 𝒫 T ∧ S ≈ i ∧ i ∪ ∅ ∈ I → i ≼ T
28 endomtr ⊢ S ≈ i ∧ i ≼ T → S ≼ T
29 19 27 28 syl2anc ⊢ φ ∧ i ∈ 𝒫 T ∧ S ≈ i ∧ i ∪ ∅ ∈ I → S ≼ T
30 18 29 rexlimddv ⊢ φ → S ≼ T