Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  acsexdimd Unicode version

Theorem acsexdimd 14302
 Description: In an algebraic closure system whose closure operator has the exchange property, if two independent sets have equal closure, they are equinumerous. See mreexfidimd 13568 for the finite case and acsinfdimd 14301 for the infinite case. This is a special case of Theorem 4.2.2 in [FaureFrolicher] p. 87. (Contributed by David Moews, 1-May-2017.)
Hypotheses
Ref Expression
acsexdimd.1 ACS
acsexdimd.2 mrCls
acsexdimd.3 mrInd
acsexdimd.4
acsexdimd.5
acsexdimd.6
acsexdimd.7
Assertion
Ref Expression
acsexdimd
Distinct variable groups:   ,,,   ,,,   ,,,   ,,,   ,,,
Allowed substitution hints:   (,,)   (,,)

Proof of Theorem acsexdimd
StepHypRef Expression
1 acsexdimd.1 . . . . 5 ACS
21acsmred 13574 . . . 4 Moore
32adantr 451 . . 3 Moore
4 acsexdimd.2 . . 3 mrCls
5 acsexdimd.3 . . 3 mrInd
6 acsexdimd.4 . . . 4
8 acsexdimd.5 . . . 4
10 acsexdimd.6 . . . 4