This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem acsdomd

Description: In an algebraic closure system, if S and T have the same closure and S is infinite independent, then T dominates S . This follows from applying acsinfd and then applying unirnfdomd 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 acsdomd 
|- ( ph -> S ~<_ T )

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 simprr 
 |-  ( ( ph /\ ( f : T --> ( ~P S i^i Fin ) /\ S = U. ran f ) ) -> S = U. ran f )
10 simprl 
 |-  ( ( ph /\ ( f : T --> ( ~P S i^i Fin ) /\ S = U. ran f ) ) -> 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 ) ) -> f : T --> Fin )
14 1 2 3 4 5 6 7 acsinfd 
 |-  ( ph -> -. T e. Fin )
15 14 adantr 
 |-  ( ( ph /\ ( f : T --> ( ~P S i^i Fin ) /\ S = U. ran f ) ) -> -. T e. Fin )
16 1 adantr 
 |-  ( ( ph /\ ( f : T --> ( ~P S i^i Fin ) /\ S = U. ran f ) ) -> A e. ( ACS ` X ) )
17 16 elfvexd 
 |-  ( ( ph /\ ( f : T --> ( ~P S i^i Fin ) /\ S = U. ran f ) ) -> X e. _V )
18 5 adantr 
 |-  ( ( ph /\ ( f : T --> ( ~P S i^i Fin ) /\ S = U. ran f ) ) -> T C_ X )
19 17 18 ssexd 
 |-  ( ( ph /\ ( f : T --> ( ~P S i^i Fin ) /\ S = U. ran f ) ) -> T e. _V )
20 13 15 19 unirnfdomd 
 |-  ( ( ph /\ ( f : T --> ( ~P S i^i Fin ) /\ S = U. ran f ) ) -> U. ran f ~<_ T )
21 9 20 eqbrtrd 
 |-  ( ( ph /\ ( f : T --> ( ~P S i^i Fin ) /\ S = U. ran f ) ) -> S ~<_ T )
22 8 21 exlimddv 
 |-  ( ph -> S ~<_ T )