Metamath Proof Explorer

Theorem acsmap2d

Description: In an algebraic closure system, if S and T have the same closure and S is independent, then there is a map f from T into the set of finite subsets of S such that S equals the union of ran f . This is proven by taking the map f from acsmapd and observing that, since S and T have the same closure, the closure of U. ran f must contain S . Since S is independent, by mrissmrcd , U. ran f must equal S . 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 ) )
Assertion acsmap2d 
|- ( ph -> E. f ( f : T --> ( ~P S i^i Fin ) /\ S = U. ran f ) )

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 1 acsmred 
 |-  ( ph -> A e. ( Moore ` X ) )
8 3 7 4 mrissd 
 |-  ( ph -> S C_ X )
9 7 2 5 mrcssidd 
 |-  ( ph -> T C_ ( N ` T ) )
10 9 6 sseqtrrd 
 |-  ( ph -> T C_ ( N ` S ) )
11 1 2 8 10 acsmapd 
 |-  ( ph -> E. f ( f : T --> ( ~P S i^i Fin ) /\ T C_ ( N ` U. ran f ) ) )
12 simprl 
 |-  ( ( ph /\ ( f : T --> ( ~P S i^i Fin ) /\ T C_ ( N ` U. ran f ) ) ) -> f : T --> ( ~P S i^i Fin ) )
13 7 adantr 
 |-  ( ( ph /\ ( f : T --> ( ~P S i^i Fin ) /\ T C_ ( N ` U. ran f ) ) ) -> A e. ( Moore ` X ) )
14 4 adantr 
 |-  ( ( ph /\ ( f : T --> ( ~P S i^i Fin ) /\ T C_ ( N ` U. ran f ) ) ) -> S e. I )
15 3 13 14 mrissd 
 |-  ( ( ph /\ ( f : T --> ( ~P S i^i Fin ) /\ T C_ ( N ` U. ran f ) ) ) -> S C_ X )
16 13 2 15 mrcssidd 
 |-  ( ( ph /\ ( f : T --> ( ~P S i^i Fin ) /\ T C_ ( N ` U. ran f ) ) ) -> S C_ ( N ` S ) )
17 6 adantr 
 |-  ( ( ph /\ ( f : T --> ( ~P S i^i Fin ) /\ T C_ ( N ` U. ran f ) ) ) -> ( N ` S ) = ( N ` T ) )
18 simprr 
 |-  ( ( ph /\ ( f : T --> ( ~P S i^i Fin ) /\ T C_ ( N ` U. ran f ) ) ) -> T C_ ( N ` U. ran f ) )
19 13 2 mrcssvd 
 |-  ( ( ph /\ ( f : T --> ( ~P S i^i Fin ) /\ T C_ ( N ` U. ran f ) ) ) -> ( N ` U. ran f ) C_ X )
20 13 2 18 19 mrcssd 
 |-  ( ( ph /\ ( f : T --> ( ~P S i^i Fin ) /\ T C_ ( N ` U. ran f ) ) ) -> ( N ` T ) C_ ( N ` ( N ` U. ran f ) ) )
21 frn 
 |-  ( f : T --> ( ~P S i^i Fin ) -> ran f C_ ( ~P S i^i Fin ) )
22 21 unissd 
 |-  ( f : T --> ( ~P S i^i Fin ) -> U. ran f C_ U. ( ~P S i^i Fin ) )
23 unifpw 
 |-  U. ( ~P S i^i Fin ) = S
24 22 23 sseqtrdi 
 |-  ( f : T --> ( ~P S i^i Fin ) -> U. ran f C_ S )
25 24 ad2antrl 
 |-  ( ( ph /\ ( f : T --> ( ~P S i^i Fin ) /\ T C_ ( N ` U. ran f ) ) ) -> U. ran f C_ S )
26 25 15 sstrd 
 |-  ( ( ph /\ ( f : T --> ( ~P S i^i Fin ) /\ T C_ ( N ` U. ran f ) ) ) -> U. ran f C_ X )
27 13 2 26 mrcidmd 
 |-  ( ( ph /\ ( f : T --> ( ~P S i^i Fin ) /\ T C_ ( N ` U. ran f ) ) ) -> ( N ` ( N ` U. ran f ) ) = ( N ` U. ran f ) )
28 20 27 sseqtrd 
 |-  ( ( ph /\ ( f : T --> ( ~P S i^i Fin ) /\ T C_ ( N ` U. ran f ) ) ) -> ( N ` T ) C_ ( N ` U. ran f ) )
29 17 28 eqsstrd 
 |-  ( ( ph /\ ( f : T --> ( ~P S i^i Fin ) /\ T C_ ( N ` U. ran f ) ) ) -> ( N ` S ) C_ ( N ` U. ran f ) )
30 16 29 sstrd 
 |-  ( ( ph /\ ( f : T --> ( ~P S i^i Fin ) /\ T C_ ( N ` U. ran f ) ) ) -> S C_ ( N ` U. ran f ) )
31 13 2 3 30 25 14 mrissmrcd 
 |-  ( ( ph /\ ( f : T --> ( ~P S i^i Fin ) /\ T C_ ( N ` U. ran f ) ) ) -> S = U. ran f )
32 12 31 jca 
 |-  ( ( ph /\ ( f : T --> ( ~P S i^i Fin ) /\ T C_ ( N ` U. ran f ) ) ) -> ( f : T --> ( ~P S i^i Fin ) /\ S = U. ran f ) )
33 32 ex 
 |-  ( ph -> ( ( f : T --> ( ~P S i^i Fin ) /\ T C_ ( N ` U. ran f ) ) -> ( f : T --> ( ~P S i^i Fin ) /\ S = U. ran f ) ) )
34 33 eximdv 
 |-  ( ph -> ( E. f ( f : T --> ( ~P S i^i Fin ) /\ T C_ ( N ` U. ran f ) ) -> E. f ( f : T --> ( ~P S i^i Fin ) /\ S = U. ran f ) ) )
35 11 34 mpd 
 |-  ( ph -> E. f ( f : T --> ( ~P S i^i Fin ) /\ S = U. ran f ) )