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