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) Remove dependency on ax-reg and ax-inf2 . (Revised by Timothy J. O'Malley, 15-Oct-2026)

Ref Expression
Hypotheses acsmapd.1 
|- ( ph -> A e. ( ACS ` X ) )
acsmapd.2 
|- N = ( mrCls ` A )
acsmapd.3 
|- ( ph -> S C_ X )
acsmapd.4 
|- ( ph -> T C_ ( N ` S ) )
Assertion acsmapd 
|- ( ph -> E. f ( f : T --> ( ~P S i^i Fin ) /\ T C_ ( N ` U. ran f ) ) )

Proof

Step Hyp Ref Expression
1 acsmapd.1 
 |-  ( ph -> A e. ( ACS ` X ) )
2 acsmapd.2 
 |-  N = ( mrCls ` A )
3 acsmapd.3 
 |-  ( ph -> S C_ X )
4 acsmapd.4 
 |-  ( ph -> T C_ ( N ` S ) )
5 fvex 
 |-  ( N ` S ) e. _V
6 5 ssex 
 |-  ( T C_ ( N ` S ) -> T e. _V )
7 4 6 syl 
 |-  ( ph -> T e. _V )
8 1 elfvexd 
 |-  ( ph -> X e. _V )
9 8 3 ssexd 
 |-  ( ph -> S e. _V )
10 9 pwexd 
 |-  ( ph -> ~P S e. _V )
11 inex1g 
 |-  ( ~P S e. _V -> ( ~P S i^i Fin ) e. _V )
12 10 11 syl 
 |-  ( ph -> ( ~P S i^i Fin ) e. _V )
13 4 sseld 
 |-  ( ph -> ( x e. T -> x e. ( N ` S ) ) )
14 1 2 3 acsficl2d 
 |-  ( ph -> ( x e. ( N ` S ) <-> E. y e. ( ~P S i^i Fin ) x e. ( N ` y ) ) )
15 13 14 sylibd 
 |-  ( ph -> ( x e. T -> E. y e. ( ~P S i^i Fin ) x e. ( N ` y ) ) )
16 15 ralrimiv 
 |-  ( ph -> A. x e. T E. y e. ( ~P S i^i Fin ) x e. ( N ` y ) )
17 fveq2 
 |-  ( y = ( f ` x ) -> ( N ` y ) = ( N ` ( f ` x ) ) )
18 17 eleq2d 
 |-  ( y = ( f ` x ) -> ( x e. ( N ` y ) <-> x e. ( N ` ( f ` x ) ) ) )
19 18 ac6 
 |-  ( ( T e. _V /\ ( ~P S i^i Fin ) e. _V /\ A. x e. T E. y e. ( ~P S i^i Fin ) x e. ( N ` y ) ) -> E. f ( f : T --> ( ~P S i^i Fin ) /\ A. x e. T x e. ( N ` ( f ` x ) ) ) )
20 7 12 16 19 syl3anc 
 |-  ( ph -> E. f ( f : T --> ( ~P S i^i Fin ) /\ A. x e. T x e. ( N ` ( f ` x ) ) ) )
21 simprl 
 |-  ( ( ph /\ ( f : T --> ( ~P S i^i Fin ) /\ A. x e. T x e. ( N ` ( f ` x ) ) ) ) -> f : T --> ( ~P S i^i Fin ) )
22 nfv 
 |-  F/ x ph
23 nfv 
 |-  F/ x f : T --> ( ~P S i^i Fin )
24 nfra1 
 |-  F/ x A. x e. T x e. ( N ` ( f ` x ) )
25 23 24 nfan 
 |-  F/ x ( f : T --> ( ~P S i^i Fin ) /\ A. x e. T x e. ( N ` ( f ` x ) ) )
26 22 25 nfan 
 |-  F/ x ( ph /\ ( f : T --> ( ~P S i^i Fin ) /\ A. x e. T x e. ( N ` ( f ` x ) ) ) )
27 1 ad2antrr 
 |-  ( ( ( ph /\ ( f : T --> ( ~P S i^i Fin ) /\ A. x e. T x e. ( N ` ( f ` x ) ) ) ) /\ x e. T ) -> A e. ( ACS ` X ) )
28 27 acsmred 
 |-  ( ( ( ph /\ ( f : T --> ( ~P S i^i Fin ) /\ A. x e. T x e. ( N ` ( f ` x ) ) ) ) /\ x e. T ) -> A e. ( Moore ` X ) )
29 simplrl 
 |-  ( ( ( ph /\ ( f : T --> ( ~P S i^i Fin ) /\ A. x e. T x e. ( N ` ( f ` x ) ) ) ) /\ x e. T ) -> f : T --> ( ~P S i^i Fin ) )
30 29 ffnd 
 |-  ( ( ( ph /\ ( f : T --> ( ~P S i^i Fin ) /\ A. x e. T x e. ( N ` ( f ` x ) ) ) ) /\ x e. T ) -> f Fn T )
31 fnfvelrn 
 |-  ( ( f Fn T /\ x e. T ) -> ( f ` x ) e. ran f )
32 30 31 sylancom 
 |-  ( ( ( ph /\ ( f : T --> ( ~P S i^i Fin ) /\ A. x e. T x e. ( N ` ( f ` x ) ) ) ) /\ x e. T ) -> ( f ` x ) e. ran f )
33 32 snssd 
 |-  ( ( ( ph /\ ( f : T --> ( ~P S i^i Fin ) /\ A. x e. T x e. ( N ` ( f ` x ) ) ) ) /\ x e. T ) -> { ( f ` x ) } C_ ran f )
34 33 unissd 
 |-  ( ( ( ph /\ ( f : T --> ( ~P S i^i Fin ) /\ A. x e. T x e. ( N ` ( f ` x ) ) ) ) /\ x e. T ) -> U. { ( f ` x ) } C_ U. ran f )
35 frn 
 |-  ( f : T --> ( ~P S i^i Fin ) -> ran f C_ ( ~P S i^i Fin ) )
36 35 unissd 
 |-  ( f : T --> ( ~P S i^i Fin ) -> U. ran f C_ U. ( ~P S i^i Fin ) )
37 unifpw 
 |-  U. ( ~P S i^i Fin ) = S
38 36 37 sseqtrdi 
 |-  ( f : T --> ( ~P S i^i Fin ) -> U. ran f C_ S )
39 29 38 syl 
 |-  ( ( ( ph /\ ( f : T --> ( ~P S i^i Fin ) /\ A. x e. T x e. ( N ` ( f ` x ) ) ) ) /\ x e. T ) -> U. ran f C_ S )
40 3 ad2antrr 
 |-  ( ( ( ph /\ ( f : T --> ( ~P S i^i Fin ) /\ A. x e. T x e. ( N ` ( f ` x ) ) ) ) /\ x e. T ) -> S C_ X )
41 39 40 sstrd 
 |-  ( ( ( ph /\ ( f : T --> ( ~P S i^i Fin ) /\ A. x e. T x e. ( N ` ( f ` x ) ) ) ) /\ x e. T ) -> U. ran f C_ X )
42 28 2 34 41 mrcssd 
 |-  ( ( ( ph /\ ( f : T --> ( ~P S i^i Fin ) /\ A. x e. T x e. ( N ` ( f ` x ) ) ) ) /\ x e. T ) -> ( N ` U. { ( f ` x ) } ) C_ ( N ` U. ran f ) )
43 simprr 
 |-  ( ( ph /\ ( f : T --> ( ~P S i^i Fin ) /\ A. x e. T x e. ( N ` ( f ` x ) ) ) ) -> A. x e. T x e. ( N ` ( f ` x ) ) )
44 43 r19.21bi 
 |-  ( ( ( ph /\ ( f : T --> ( ~P S i^i Fin ) /\ A. x e. T x e. ( N ` ( f ` x ) ) ) ) /\ x e. T ) -> x e. ( N ` ( f ` x ) ) )
45 fvex 
 |-  ( f ` x ) e. _V
46 45 unisn 
 |-  U. { ( f ` x ) } = ( f ` x )
47 46 fveq2i 
 |-  ( N ` U. { ( f ` x ) } ) = ( N ` ( f ` x ) )
48 44 47 eleqtrrdi 
 |-  ( ( ( ph /\ ( f : T --> ( ~P S i^i Fin ) /\ A. x e. T x e. ( N ` ( f ` x ) ) ) ) /\ x e. T ) -> x e. ( N ` U. { ( f ` x ) } ) )
49 42 48 sseldd 
 |-  ( ( ( ph /\ ( f : T --> ( ~P S i^i Fin ) /\ A. x e. T x e. ( N ` ( f ` x ) ) ) ) /\ x e. T ) -> x e. ( N ` U. ran f ) )
50 49 ex 
 |-  ( ( ph /\ ( f : T --> ( ~P S i^i Fin ) /\ A. x e. T x e. ( N ` ( f ` x ) ) ) ) -> ( x e. T -> x e. ( N ` U. ran f ) ) )
51 26 50 alrimi 
 |-  ( ( ph /\ ( f : T --> ( ~P S i^i Fin ) /\ A. x e. T x e. ( N ` ( f ` x ) ) ) ) -> A. x ( x e. T -> x e. ( N ` U. ran f ) ) )
52 df-ss 
 |-  ( T C_ ( N ` U. ran f ) <-> A. x ( x e. T -> x e. ( N ` U. ran f ) ) )
53 51 52 sylibr 
 |-  ( ( ph /\ ( f : T --> ( ~P S i^i Fin ) /\ A. x e. T x e. ( N ` ( f ` x ) ) ) ) -> T C_ ( N ` U. ran f ) )
54 21 53 jca 
 |-  ( ( ph /\ ( f : T --> ( ~P S i^i Fin ) /\ A. x e. T x e. ( N ` ( f ` x ) ) ) ) -> ( f : T --> ( ~P S i^i Fin ) /\ T C_ ( N ` U. ran f ) ) )
55 54 ex 
 |-  ( ph -> ( ( f : T --> ( ~P S i^i Fin ) /\ A. x e. T x e. ( N ` ( f ` x ) ) ) -> ( f : T --> ( ~P S i^i Fin ) /\ T C_ ( N ` U. ran f ) ) ) )
56 55 eximdv 
 |-  ( ph -> ( E. f ( f : T --> ( ~P S i^i Fin ) /\ A. x e. T x e. ( N ` ( f ` x ) ) ) -> E. f ( f : T --> ( ~P S i^i Fin ) /\ T C_ ( N ` U. ran f ) ) ) )
57 20 56 mpd 
 |-  ( ph -> E. f ( f : T --> ( ~P S i^i Fin ) /\ T C_ ( N ` U. ran f ) ) )