Metamath Proof Explorer


Theorem acsinfd

Description: In an algebraic closure system, if S and T have the same closure and S is infinite independent, then T is infinite. This follows from applying unirnffid to the map given in acsmap2d . See Section II.5 in Cohn p. 81 to 82. (Contributed by David Moews, 1-May-2017)

Ref Expression
Hypotheses acsmap2d.1 φAACSX
acsmap2d.2 N=mrClsA
acsmap2d.3 I=mrIndA
acsmap2d.4 φSI
acsmap2d.5 φTX
acsmap2d.6 φNS=NT
acsinfd.7 φ¬SFin
Assertion acsinfd φ¬TFin

Proof

Step Hyp Ref Expression
1 acsmap2d.1 φAACSX
2 acsmap2d.2 N=mrClsA
3 acsmap2d.3 I=mrIndA
4 acsmap2d.4 φSI
5 acsmap2d.5 φTX
6 acsmap2d.6 φNS=NT
7 acsinfd.7 φ¬SFin
8 1 2 3 4 5 6 acsmap2d φff:T𝒫SFinS=ranf
9 simplrr φf:T𝒫SFinS=ranfTFinS=ranf
10 simplrl φf:T𝒫SFinS=ranfTFinf:T𝒫SFin
11 inss2 𝒫SFinFin
12 fss f:T𝒫SFin𝒫SFinFinf:TFin
13 10 11 12 sylancl φf:T𝒫SFinS=ranfTFinf:TFin
14 simpr φf:T𝒫SFinS=ranfTFinTFin
15 13 14 unirnffid φf:T𝒫SFinS=ranfTFinranfFin
16 9 15 eqeltrd φf:T𝒫SFinS=ranfTFinSFin
17 7 ad2antrr φf:T𝒫SFinS=ranfTFin¬SFin
18 16 17 pm2.65da φf:T𝒫SFinS=ranf¬TFin
19 8 18 exlimddv φ¬TFin