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 | |
|
acsmap2d.2 | |
||
acsmap2d.3 | |
||
acsmap2d.4 | |
||
acsmap2d.5 | |
||
acsmap2d.6 | |
||
Assertion | acsmap2d | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | acsmap2d.1 | |
|
2 | acsmap2d.2 | |
|
3 | acsmap2d.3 | |
|
4 | acsmap2d.4 | |
|
5 | acsmap2d.5 | |
|
6 | acsmap2d.6 | |
|
7 | 1 | acsmred | |
8 | 3 7 4 | mrissd | |
9 | 7 2 5 | mrcssidd | |
10 | 9 6 | sseqtrrd | |
11 | 1 2 8 10 | acsmapd | |
12 | simprl | |
|
13 | 7 | adantr | |
14 | 4 | adantr | |
15 | 3 13 14 | mrissd | |
16 | 13 2 15 | mrcssidd | |
17 | 6 | adantr | |
18 | simprr | |
|
19 | 13 2 | mrcssvd | |
20 | 13 2 18 19 | mrcssd | |
21 | frn | |
|
22 | 21 | unissd | |
23 | unifpw | |
|
24 | 22 23 | sseqtrdi | |
25 | 24 | ad2antrl | |
26 | 25 15 | sstrd | |
27 | 13 2 26 | mrcidmd | |
28 | 20 27 | sseqtrd | |
29 | 17 28 | eqsstrd | |
30 | 16 29 | sstrd | |
31 | 13 2 3 30 25 14 | mrissmrcd | |
32 | 12 31 | jca | |
33 | 32 | ex | |
34 | 33 | eximdv | |
35 | 11 34 | mpd | |