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 φAACSX
acsmap2d.2 N=mrClsA
acsmap2d.3 I=mrIndA
acsmap2d.4 φSI
acsmap2d.5 φTX
acsmap2d.6 φNS=NT
Assertion acsmap2d φff:T𝒫SFinS=ranf

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 1 acsmred φAMooreX
8 3 7 4 mrissd φSX
9 7 2 5 mrcssidd φTNT
10 9 6 sseqtrrd φTNS
11 1 2 8 10 acsmapd φff:T𝒫SFinTNranf
12 simprl φf:T𝒫SFinTNranff:T𝒫SFin
13 7 adantr φf:T𝒫SFinTNranfAMooreX
14 4 adantr φf:T𝒫SFinTNranfSI
15 3 13 14 mrissd φf:T𝒫SFinTNranfSX
16 13 2 15 mrcssidd φf:T𝒫SFinTNranfSNS
17 6 adantr φf:T𝒫SFinTNranfNS=NT
18 simprr φf:T𝒫SFinTNranfTNranf
19 13 2 mrcssvd φf:T𝒫SFinTNranfNranfX
20 13 2 18 19 mrcssd φf:T𝒫SFinTNranfNTNNranf
21 frn f:T𝒫SFinranf𝒫SFin
22 21 unissd f:T𝒫SFinranf𝒫SFin
23 unifpw 𝒫SFin=S
24 22 23 sseqtrdi f:T𝒫SFinranfS
25 24 ad2antrl φf:T𝒫SFinTNranfranfS
26 25 15 sstrd φf:T𝒫SFinTNranfranfX
27 13 2 26 mrcidmd φf:T𝒫SFinTNranfNNranf=Nranf
28 20 27 sseqtrd φf:T𝒫SFinTNranfNTNranf
29 17 28 eqsstrd φf:T𝒫SFinTNranfNSNranf
30 16 29 sstrd φf:T𝒫SFinTNranfSNranf
31 13 2 3 30 25 14 mrissmrcd φf:T𝒫SFinTNranfS=ranf
32 12 31 jca φf:T𝒫SFinTNranff:T𝒫SFinS=ranf
33 32 ex φf:T𝒫SFinTNranff:T𝒫SFinS=ranf
34 33 eximdv φff:T𝒫SFinTNranfff:T𝒫SFinS=ranf
35 11 34 mpd φff:T𝒫SFinS=ranf