Description: In an algebraic closure system, if T is contained in the closure of S , there is a map f from T into the set of finite subsets of S such that the closure of U. ran f contains T . This is proven by applying acsficl2d to each element of T . See Section II.5 in Cohn p. 81 to 82. (Contributed by David Moews, 1-May-2017)
Ref | Expression | ||
---|---|---|---|
Hypotheses | acsmapd.1 | |
|
acsmapd.2 | |
||
acsmapd.3 | |
||
acsmapd.4 | |
||
Assertion | acsmapd | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | acsmapd.1 | |
|
2 | acsmapd.2 | |
|
3 | acsmapd.3 | |
|
4 | acsmapd.4 | |
|
5 | fvex | |
|
6 | 5 | ssex | |
7 | 4 6 | syl | |
8 | 4 | sseld | |
9 | 1 2 3 | acsficl2d | |
10 | 8 9 | sylibd | |
11 | 10 | ralrimiv | |
12 | fveq2 | |
|
13 | 12 | eleq2d | |
14 | 13 | ac6sg | |
15 | 7 11 14 | sylc | |
16 | simprl | |
|
17 | nfv | |
|
18 | nfv | |
|
19 | nfra1 | |
|
20 | 18 19 | nfan | |
21 | 17 20 | nfan | |
22 | 1 | ad2antrr | |
23 | 22 | acsmred | |
24 | simplrl | |
|
25 | 24 | ffnd | |
26 | fnfvelrn | |
|
27 | 25 26 | sylancom | |
28 | 27 | snssd | |
29 | 28 | unissd | |
30 | frn | |
|
31 | 30 | unissd | |
32 | unifpw | |
|
33 | 31 32 | sseqtrdi | |
34 | 24 33 | syl | |
35 | 3 | ad2antrr | |
36 | 34 35 | sstrd | |
37 | 23 2 29 36 | mrcssd | |
38 | simprr | |
|
39 | 38 | r19.21bi | |
40 | fvex | |
|
41 | 40 | unisn | |
42 | 41 | fveq2i | |
43 | 39 42 | eleqtrrdi | |
44 | 37 43 | sseldd | |
45 | 44 | ex | |
46 | 21 45 | alrimi | |
47 | dfss2 | |
|
48 | 46 47 | sylibr | |
49 | 16 48 | jca | |
50 | 49 | ex | |
51 | 50 | eximdv | |
52 | 15 51 | mpd | |