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 φAMooreX
mreexdomd.2 N=mrClsA
mreexdomd.3 I=mrIndA
mreexdomd.4 φs𝒫XyXzNsyNsyNsz
mreexdomd.5 φSNT
mreexdomd.6 φTX
mreexdomd.7 φSFinTFin
mreexdomd.8 φSI
Assertion mreexdomd φST

Proof

Step Hyp Ref Expression
1 mreexdomd.1 φAMooreX
2 mreexdomd.2 N=mrClsA
3 mreexdomd.3 I=mrIndA
4 mreexdomd.4 φs𝒫XyXzNsyNsyNsz
5 mreexdomd.5 φSNT
6 mreexdomd.6 φTX
7 mreexdomd.7 φSFinTFin
8 mreexdomd.8 φSI
9 3 1 8 mrissd φSX
10 dif0 X=X
11 9 10 sseqtrrdi φSX
12 6 10 sseqtrrdi φTX
13 un0 T=T
14 13 fveq2i NT=NT
15 5 14 sseqtrrdi φSNT
16 un0 S=S
17 16 8 eqeltrid φSI
18 1 2 3 4 11 12 15 17 7 mreexexd φi𝒫TSiiI
19 simprrl φi𝒫TSiiISi
20 simprl φi𝒫TSiiIi𝒫T
21 20 elpwid φi𝒫TSiiIiT
22 1 elfvexd φXV
23 22 6 ssexd φTV
24 ssdomg TViTiT
25 23 24 syl φiTiT
26 25 adantr φi𝒫TSiiIiTiT
27 21 26 mpd φi𝒫TSiiIiT
28 endomtr SiiTST
29 19 27 28 syl2anc φi𝒫TSiiIST
30 18 29 rexlimddv φST