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 )