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 
|- ( 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 4 sseld 
 |-  ( ph -> ( x e. T -> x e. ( N ` S ) ) )
9 1 2 3 acsficl2d 
 |-  ( ph -> ( x e. ( N ` S ) <-> E. y e. ( ~P S i^i Fin ) x e. ( N ` y ) ) )
10 8 9 sylibd 
 |-  ( ph -> ( x e. T -> E. y e. ( ~P S i^i Fin ) x e. ( N ` y ) ) )
11 10 ralrimiv 
 |-  ( ph -> A. x e. T E. y e. ( ~P S i^i Fin ) x e. ( N ` y ) )
12 fveq2 
 |-  ( y = ( f ` x ) -> ( N ` y ) = ( N ` ( f ` x ) ) )
13 12 eleq2d 
 |-  ( y = ( f ` x ) -> ( x e. ( N ` y ) <-> x e. ( N ` ( f ` x ) ) ) )
14 13 ac6sg 
 |-  ( T 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 ) ) ) ) )
15 7 11 14 sylc 
 |-  ( ph -> E. f ( f : T --> ( ~P S i^i Fin ) /\ A. x e. T x e. ( N ` ( f ` x ) ) ) )
16 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 ) )
17 nfv 
 |-  F/ x ph
18 nfv 
 |-  F/ x f : T --> ( ~P S i^i Fin )
19 nfra1 
 |-  F/ x A. x e. T x e. ( N ` ( f ` x ) )
20 18 19 nfan 
 |-  F/ x ( f : T --> ( ~P S i^i Fin ) /\ A. x e. T x e. ( N ` ( f ` x ) ) )
21 17 20 nfan 
 |-  F/ x ( ph /\ ( f : T --> ( ~P S i^i Fin ) /\ A. x e. T x e. ( N ` ( f ` x ) ) ) )
22 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 ) )
23 22 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 ) )
24 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 ) )
25 24 ffnd 
 |-  ( ( ( ph /\ ( f : T --> ( ~P S i^i Fin ) /\ A. x e. T x e. ( N ` ( f ` x ) ) ) ) /\ x e. T ) -> f Fn T )
26 fnfvelrn 
 |-  ( ( f Fn T /\ x e. T ) -> ( f ` x ) e. ran f )
27 25 26 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 )
28 27 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 )
29 28 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 )
30 frn 
 |-  ( f : T --> ( ~P S i^i Fin ) -> ran f C_ ( ~P S i^i Fin ) )
31 30 unissd 
 |-  ( f : T --> ( ~P S i^i Fin ) -> U. ran f C_ U. ( ~P S i^i Fin ) )
32 unifpw 
 |-  U. ( ~P S i^i Fin ) = S
33 31 32 sseqtrdi 
 |-  ( f : T --> ( ~P S i^i Fin ) -> U. ran f C_ S )
34 24 33 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 )
35 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 )
36 34 35 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 )
37 23 2 29 36 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 ) )
38 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 ) ) )
39 38 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 ) ) )
40 fvex 
 |-  ( f ` x ) e. _V
41 40 unisn 
 |-  U. { ( f ` x ) } = ( f ` x )
42 41 fveq2i 
 |-  ( N ` U. { ( f ` x ) } ) = ( N ` ( f ` x ) )
43 39 42 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 ) } ) )
44 37 43 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 ) )
45 44 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 ) ) )
46 21 45 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 ) ) )
47 dfss2 
 |-  ( T C_ ( N ` U. ran f ) <-> A. x ( x e. T -> x e. ( N ` U. ran f ) ) )
48 46 47 sylibr 
 |-  ( ( ph /\ ( f : T --> ( ~P S i^i Fin ) /\ A. x e. T x e. ( N ` ( f ` x ) ) ) ) -> T C_ ( N ` U. ran f ) )
49 16 48 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 ) ) )
50 49 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 ) ) ) )
51 50 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 ) ) ) )
52 15 51 mpd 
 |-  ( ph -> E. f ( f : T --> ( ~P S i^i Fin ) /\ T C_ ( N ` U. ran f ) ) )