Metamath Proof Explorer


Theorem mreexfidimd

Description: In a Moore system whose closure operator has the exchange property, if two independent sets have equal closure and one is finite, then they are equinumerous. Proven by using mreexdomd twice. This implies a special case of Theorem 4.2.2 in FaureFrolicher p. 87. (Contributed by David Moews, 1-May-2017)

Ref Expression
Hypotheses mreexfidimd.1 φAMooreX
mreexfidimd.2 N=mrClsA
mreexfidimd.3 I=mrIndA
mreexfidimd.4 φs𝒫XyXzNsyNsyNsz
mreexfidimd.5 φSI
mreexfidimd.6 φTI
mreexfidimd.7 φSFin
mreexfidimd.8 φNS=NT
Assertion mreexfidimd φST

Proof

Step Hyp Ref Expression
1 mreexfidimd.1 φAMooreX
2 mreexfidimd.2 N=mrClsA
3 mreexfidimd.3 I=mrIndA
4 mreexfidimd.4 φs𝒫XyXzNsyNsyNsz
5 mreexfidimd.5 φSI
6 mreexfidimd.6 φTI
7 mreexfidimd.7 φSFin
8 mreexfidimd.8 φNS=NT
9 3 1 5 mrissd φSX
10 1 2 9 mrcssidd φSNS
11 10 8 sseqtrd φSNT
12 3 1 6 mrissd φTX
13 7 orcd φSFinTFin
14 1 2 3 4 11 12 13 5 mreexdomd φST
15 1 2 12 mrcssidd φTNT
16 15 8 sseqtrrd φTNS
17 7 olcd φTFinSFin
18 1 2 3 4 16 9 17 6 mreexdomd φTS
19 sbth STTSST
20 14 18 19 syl2anc φST