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

Theorem acsexdimd 14611
 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 13877 for the finite case and acsinfdimd 14610 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 13883 . . . 4 Moore
32adantr 453 . . 3 Moore
4 acsexdimd.2 . . 3 mrCls
5 acsexdimd.3 . . 3 mrInd
6 acsexdimd.4 . . . 4
8 acsexdimd.5 . . . 4
10 acsexdimd.6 . . . 4