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

Theorem acsinfd 14299
 Description: In an algebraic closure system, if and have the same closure and is infinite independent, then is infinite. This follows from applying unirnffid 7163 to the map given in acsmap2d 14298. See Section II.5 in [Cohn] p. 81 to 82. (Contributed by David Moews, 1-May-2017.)
Hypotheses
Ref Expression
acsmap2d.1 ACS
acsmap2d.2 mrCls
acsmap2d.3 mrInd
acsmap2d.4
acsmap2d.5
acsmap2d.6
acsinfd.7
Assertion
Ref Expression
acsinfd

Proof of Theorem acsinfd
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 acsmap2d.1 . . 3 ACS
2 acsmap2d.2 . . 3 mrCls
3 acsmap2d.3 . . 3 mrInd
4 acsmap2d.4 . . 3
5 acsmap2d.5 . . 3
6 acsmap2d.6 . . 3
71, 2, 3, 4, 5, 6acsmap2d 14298 . 2
8 simplrr 737 . . . 4
9 simplrl 736 . . . . . 6
10 inss2 3403 . . . . . 6
11 fss 5413 . . . . . 6
129, 10, 11sylancl 643 . . . . 5
13 simpr 447 . . . . 5
1412, 13unirnffid 7163 . . . 4
158, 14eqeltrd 2370 . . 3
16 acsinfd.7 . . . 4