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 
|- ( ph -> A e. ( ACS ` X ) )
acsmap2d.2 
|- N = ( mrCls ` A )
acsmap2d.3 
|- I = ( mrInd ` A )
acsmap2d.4 
|- ( ph -> S e. I )
acsmap2d.5 
|- ( ph -> T C_ X )
acsmap2d.6 
|- ( ph -> ( N ` S ) = ( N ` T ) )
acsinfd.7 
|- ( ph -> -. S e. Fin )
Assertion acsinfd 
|- ( ph -> -. T e. Fin )

Proof

Step Hyp Ref Expression
1 acsmap2d.1 
 |-  ( ph -> A e. ( ACS ` X ) )
2 acsmap2d.2 
 |-  N = ( mrCls ` A )
3 acsmap2d.3 
 |-  I = ( mrInd ` A )
4 acsmap2d.4 
 |-  ( ph -> S e. I )
5 acsmap2d.5 
 |-  ( ph -> T C_ X )
6 acsmap2d.6 
 |-  ( ph -> ( N ` S ) = ( N ` T ) )
7 acsinfd.7 
 |-  ( ph -> -. S e. Fin )
8 1 2 3 4 5 6 acsmap2d 
 |-  ( ph -> E. f ( f : T --> ( ~P S i^i Fin ) /\ S = U. ran f ) )
9 simplrr 
 |-  ( ( ( ph /\ ( f : T --> ( ~P S i^i Fin ) /\ S = U. ran f ) ) /\ T e. Fin ) -> S = U. ran f )
10 simplrl 
 |-  ( ( ( ph /\ ( f : T --> ( ~P S i^i Fin ) /\ S = U. ran f ) ) /\ T e. Fin ) -> f : T --> ( ~P S i^i Fin ) )
11 inss2 
 |-  ( ~P S i^i Fin ) C_ Fin
12 fss 
 |-  ( ( f : T --> ( ~P S i^i Fin ) /\ ( ~P S i^i Fin ) C_ Fin ) -> f : T --> Fin )
13 10 11 12 sylancl 
 |-  ( ( ( ph /\ ( f : T --> ( ~P S i^i Fin ) /\ S = U. ran f ) ) /\ T e. Fin ) -> f : T --> Fin )
14 simpr 
 |-  ( ( ( ph /\ ( f : T --> ( ~P S i^i Fin ) /\ S = U. ran f ) ) /\ T e. Fin ) -> T e. Fin )
15 13 14 unirnffid 
 |-  ( ( ( ph /\ ( f : T --> ( ~P S i^i Fin ) /\ S = U. ran f ) ) /\ T e. Fin ) -> U. ran f e. Fin )
16 9 15 eqeltrd 
 |-  ( ( ( ph /\ ( f : T --> ( ~P S i^i Fin ) /\ S = U. ran f ) ) /\ T e. Fin ) -> S e. Fin )
17 7 ad2antrr 
 |-  ( ( ( ph /\ ( f : T --> ( ~P S i^i Fin ) /\ S = U. ran f ) ) /\ T e. Fin ) -> -. S e. Fin )
18 16 17 pm2.65da 
 |-  ( ( ph /\ ( f : T --> ( ~P S i^i Fin ) /\ S = U. ran f ) ) -> -. T e. Fin )
19 8 18 exlimddv 
 |-  ( ph -> -. T e. Fin )