Metamath Proof Explorer


Theorem acsmapd

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 φAACSX
acsmapd.2 N=mrClsA
acsmapd.3 φSX
acsmapd.4 φTNS
Assertion acsmapd φff:T𝒫SFinTNranf

Proof

Step Hyp Ref Expression
1 acsmapd.1 φAACSX
2 acsmapd.2 N=mrClsA
3 acsmapd.3 φSX
4 acsmapd.4 φTNS
5 fvex NSV
6 5 ssex TNSTV
7 4 6 syl φTV
8 4 sseld φxTxNS
9 1 2 3 acsficl2d φxNSy𝒫SFinxNy
10 8 9 sylibd φxTy𝒫SFinxNy
11 10 ralrimiv φxTy𝒫SFinxNy
12 fveq2 y=fxNy=Nfx
13 12 eleq2d y=fxxNyxNfx
14 13 ac6sg TVxTy𝒫SFinxNyff:T𝒫SFinxTxNfx
15 7 11 14 sylc φff:T𝒫SFinxTxNfx
16 simprl φf:T𝒫SFinxTxNfxf:T𝒫SFin
17 nfv xφ
18 nfv xf:T𝒫SFin
19 nfra1 xxTxNfx
20 18 19 nfan xf:T𝒫SFinxTxNfx
21 17 20 nfan xφf:T𝒫SFinxTxNfx
22 1 ad2antrr φf:T𝒫SFinxTxNfxxTAACSX
23 22 acsmred φf:T𝒫SFinxTxNfxxTAMooreX
24 simplrl φf:T𝒫SFinxTxNfxxTf:T𝒫SFin
25 24 ffnd φf:T𝒫SFinxTxNfxxTfFnT
26 fnfvelrn fFnTxTfxranf
27 25 26 sylancom φf:T𝒫SFinxTxNfxxTfxranf
28 27 snssd φf:T𝒫SFinxTxNfxxTfxranf
29 28 unissd φf:T𝒫SFinxTxNfxxTfxranf
30 frn f:T𝒫SFinranf𝒫SFin
31 30 unissd f:T𝒫SFinranf𝒫SFin
32 unifpw 𝒫SFin=S
33 31 32 sseqtrdi f:T𝒫SFinranfS
34 24 33 syl φf:T𝒫SFinxTxNfxxTranfS
35 3 ad2antrr φf:T𝒫SFinxTxNfxxTSX
36 34 35 sstrd φf:T𝒫SFinxTxNfxxTranfX
37 23 2 29 36 mrcssd φf:T𝒫SFinxTxNfxxTNfxNranf
38 simprr φf:T𝒫SFinxTxNfxxTxNfx
39 38 r19.21bi φf:T𝒫SFinxTxNfxxTxNfx
40 fvex fxV
41 40 unisn fx=fx
42 41 fveq2i Nfx=Nfx
43 39 42 eleqtrrdi φf:T𝒫SFinxTxNfxxTxNfx
44 37 43 sseldd φf:T𝒫SFinxTxNfxxTxNranf
45 44 ex φf:T𝒫SFinxTxNfxxTxNranf
46 21 45 alrimi φf:T𝒫SFinxTxNfxxxTxNranf
47 dfss2 TNranfxxTxNranf
48 46 47 sylibr φf:T𝒫SFinxTxNfxTNranf
49 16 48 jca φf:T𝒫SFinxTxNfxf:T𝒫SFinTNranf
50 49 ex φf:T𝒫SFinxTxNfxf:T𝒫SFinTNranf
51 50 eximdv φff:T𝒫SFinxTxNfxff:T𝒫SFinTNranf
52 15 51 mpd φff:T𝒫SFinTNranf