Metamath Proof Explorer

Theorem isacs3lem

Description: An algebraic closure system satisfies isacs3 . (Contributed by Stefan O'Rear, 2-Apr-2015)

Ref Expression
Assertion isacs3lem 
|- ( C e. ( ACS ` X ) -> ( C e. ( Moore ` X ) /\ A. s e. ~P C ( ( toInc ` s ) e. Dirset -> U. s e. C ) ) )

Proof

Step Hyp Ref Expression
1 acsmre 
 |-  ( C e. ( ACS ` X ) -> C e. ( Moore ` X ) )
2 mresspw 
 |-  ( C e. ( Moore ` X ) -> C C_ ~P X )
3 1 2 syl 
 |-  ( C e. ( ACS ` X ) -> C C_ ~P X )
4 3 sspwd 
 |-  ( C e. ( ACS ` X ) -> ~P C C_ ~P ~P X )
5 4 sselda 
 |-  ( ( C e. ( ACS ` X ) /\ s e. ~P C ) -> s e. ~P ~P X )
6 5 elpwid 
 |-  ( ( C e. ( ACS ` X ) /\ s e. ~P C ) -> s C_ ~P X )
7 sspwuni 
 |-  ( s C_ ~P X <-> U. s C_ X )
8 6 7 sylib 
 |-  ( ( C e. ( ACS ` X ) /\ s e. ~P C ) -> U. s C_ X )
9 8 adantr 
 |-  ( ( ( C e. ( ACS ` X ) /\ s e. ~P C ) /\ ( toInc ` s ) e. Dirset ) -> U. s C_ X )
10 elinel1 
 |-  ( x e. ( ~P U. s i^i Fin ) -> x e. ~P U. s )
11 10 elpwid 
 |-  ( x e. ( ~P U. s i^i Fin ) -> x C_ U. s )
12 elinel2 
 |-  ( x e. ( ~P U. s i^i Fin ) -> x e. Fin )
13 fissuni 
 |-  ( ( x C_ U. s /\ x e. Fin ) -> E. y e. ( ~P s i^i Fin ) x C_ U. y )
14 11 12 13 syl2anc 
 |-  ( x e. ( ~P U. s i^i Fin ) -> E. y e. ( ~P s i^i Fin ) x C_ U. y )
15 14 ad2antll 
 |-  ( ( ( C e. ( ACS ` X ) /\ s e. ~P C ) /\ ( ( toInc ` s ) e. Dirset /\ x e. ( ~P U. s i^i Fin ) ) ) -> E. y e. ( ~P s i^i Fin ) x C_ U. y )
16 1 ad3antrrr 
 |-  ( ( ( ( C e. ( ACS ` X ) /\ s e. ~P C ) /\ ( ( toInc ` s ) e. Dirset /\ x e. ( ~P U. s i^i Fin ) ) ) /\ ( y e. ( ~P s i^i Fin ) /\ x C_ U. y ) ) -> C e. ( Moore ` X ) )
17 eqid 
 |-  ( mrCls ` C ) = ( mrCls ` C )
18 simprr 
 |-  ( ( ( ( C e. ( ACS ` X ) /\ s e. ~P C ) /\ ( ( toInc ` s ) e. Dirset /\ x e. ( ~P U. s i^i Fin ) ) ) /\ ( y e. ( ~P s i^i Fin ) /\ x C_ U. y ) ) -> x C_ U. y )
19 elinel1 
 |-  ( y e. ( ~P s i^i Fin ) -> y e. ~P s )
20 19 elpwid 
 |-  ( y e. ( ~P s i^i Fin ) -> y C_ s )
21 20 unissd 
 |-  ( y e. ( ~P s i^i Fin ) -> U. y C_ U. s )
22 21 ad2antrl 
 |-  ( ( ( ( C e. ( ACS ` X ) /\ s e. ~P C ) /\ ( ( toInc ` s ) e. Dirset /\ x e. ( ~P U. s i^i Fin ) ) ) /\ ( y e. ( ~P s i^i Fin ) /\ x C_ U. y ) ) -> U. y C_ U. s )
23 8 ad2antrr 
 |-  ( ( ( ( C e. ( ACS ` X ) /\ s e. ~P C ) /\ ( ( toInc ` s ) e. Dirset /\ x e. ( ~P U. s i^i Fin ) ) ) /\ ( y e. ( ~P s i^i Fin ) /\ x C_ U. y ) ) -> U. s C_ X )
24 22 23 sstrd 
 |-  ( ( ( ( C e. ( ACS ` X ) /\ s e. ~P C ) /\ ( ( toInc ` s ) e. Dirset /\ x e. ( ~P U. s i^i Fin ) ) ) /\ ( y e. ( ~P s i^i Fin ) /\ x C_ U. y ) ) -> U. y C_ X )
25 16 17 18 24 mrcssd 
 |-  ( ( ( ( C e. ( ACS ` X ) /\ s e. ~P C ) /\ ( ( toInc ` s ) e. Dirset /\ x e. ( ~P U. s i^i Fin ) ) ) /\ ( y e. ( ~P s i^i Fin ) /\ x C_ U. y ) ) -> ( ( mrCls ` C ) ` x ) C_ ( ( mrCls ` C ) ` U. y ) )
26 simpl 
 |-  ( ( ( toInc ` s ) e. Dirset /\ y e. ( ~P s i^i Fin ) ) -> ( toInc ` s ) e. Dirset )
27 20 adantl 
 |-  ( ( ( toInc ` s ) e. Dirset /\ y e. ( ~P s i^i Fin ) ) -> y C_ s )
28 elinel2 
 |-  ( y e. ( ~P s i^i Fin ) -> y e. Fin )
29 28 adantl 
 |-  ( ( ( toInc ` s ) e. Dirset /\ y e. ( ~P s i^i Fin ) ) -> y e. Fin )
30 ipodrsfi 
 |-  ( ( ( toInc ` s ) e. Dirset /\ y C_ s /\ y e. Fin ) -> E. x e. s U. y C_ x )
31 26 27 29 30 syl3anc 
 |-  ( ( ( toInc ` s ) e. Dirset /\ y e. ( ~P s i^i Fin ) ) -> E. x e. s U. y C_ x )
32 31 adantl 
 |-  ( ( ( C e. ( ACS ` X ) /\ s e. ~P C ) /\ ( ( toInc ` s ) e. Dirset /\ y e. ( ~P s i^i Fin ) ) ) -> E. x e. s U. y C_ x )
33 1 ad3antrrr 
 |-  ( ( ( ( C e. ( ACS ` X ) /\ s e. ~P C ) /\ ( ( toInc ` s ) e. Dirset /\ y e. ( ~P s i^i Fin ) ) ) /\ ( x e. s /\ U. y C_ x ) ) -> C e. ( Moore ` X ) )
34 simprr 
 |-  ( ( ( ( C e. ( ACS ` X ) /\ s e. ~P C ) /\ ( ( toInc ` s ) e. Dirset /\ y e. ( ~P s i^i Fin ) ) ) /\ ( x e. s /\ U. y C_ x ) ) -> U. y C_ x )
35 elpwi 
 |-  ( s e. ~P C -> s C_ C )
36 35 adantl 
 |-  ( ( C e. ( ACS ` X ) /\ s e. ~P C ) -> s C_ C )
37 36 ad2antrr 
 |-  ( ( ( ( C e. ( ACS ` X ) /\ s e. ~P C ) /\ ( ( toInc ` s ) e. Dirset /\ y e. ( ~P s i^i Fin ) ) ) /\ ( x e. s /\ U. y C_ x ) ) -> s C_ C )
38 simprl 
 |-  ( ( ( ( C e. ( ACS ` X ) /\ s e. ~P C ) /\ ( ( toInc ` s ) e. Dirset /\ y e. ( ~P s i^i Fin ) ) ) /\ ( x e. s /\ U. y C_ x ) ) -> x e. s )
39 37 38 sseldd 
 |-  ( ( ( ( C e. ( ACS ` X ) /\ s e. ~P C ) /\ ( ( toInc ` s ) e. Dirset /\ y e. ( ~P s i^i Fin ) ) ) /\ ( x e. s /\ U. y C_ x ) ) -> x e. C )
40 17 mrcsscl 
 |-  ( ( C e. ( Moore ` X ) /\ U. y C_ x /\ x e. C ) -> ( ( mrCls ` C ) ` U. y ) C_ x )
41 33 34 39 40 syl3anc 
 |-  ( ( ( ( C e. ( ACS ` X ) /\ s e. ~P C ) /\ ( ( toInc ` s ) e. Dirset /\ y e. ( ~P s i^i Fin ) ) ) /\ ( x e. s /\ U. y C_ x ) ) -> ( ( mrCls ` C ) ` U. y ) C_ x )
42 elssuni 
 |-  ( x e. s -> x C_ U. s )
43 42 ad2antrl 
 |-  ( ( ( ( C e. ( ACS ` X ) /\ s e. ~P C ) /\ ( ( toInc ` s ) e. Dirset /\ y e. ( ~P s i^i Fin ) ) ) /\ ( x e. s /\ U. y C_ x ) ) -> x C_ U. s )
44 41 43 sstrd 
 |-  ( ( ( ( C e. ( ACS ` X ) /\ s e. ~P C ) /\ ( ( toInc ` s ) e. Dirset /\ y e. ( ~P s i^i Fin ) ) ) /\ ( x e. s /\ U. y C_ x ) ) -> ( ( mrCls ` C ) ` U. y ) C_ U. s )
45 32 44 rexlimddv 
 |-  ( ( ( C e. ( ACS ` X ) /\ s e. ~P C ) /\ ( ( toInc ` s ) e. Dirset /\ y e. ( ~P s i^i Fin ) ) ) -> ( ( mrCls ` C ) ` U. y ) C_ U. s )
46 45 anassrs 
 |-  ( ( ( ( C e. ( ACS ` X ) /\ s e. ~P C ) /\ ( toInc ` s ) e. Dirset ) /\ y e. ( ~P s i^i Fin ) ) -> ( ( mrCls ` C ) ` U. y ) C_ U. s )
47 46 adantrr 
 |-  ( ( ( ( C e. ( ACS ` X ) /\ s e. ~P C ) /\ ( toInc ` s ) e. Dirset ) /\ ( y e. ( ~P s i^i Fin ) /\ x C_ U. y ) ) -> ( ( mrCls ` C ) ` U. y ) C_ U. s )
48 47 adantlrr 
 |-  ( ( ( ( C e. ( ACS ` X ) /\ s e. ~P C ) /\ ( ( toInc ` s ) e. Dirset /\ x e. ( ~P U. s i^i Fin ) ) ) /\ ( y e. ( ~P s i^i Fin ) /\ x C_ U. y ) ) -> ( ( mrCls ` C ) ` U. y ) C_ U. s )
49 25 48 sstrd 
 |-  ( ( ( ( C e. ( ACS ` X ) /\ s e. ~P C ) /\ ( ( toInc ` s ) e. Dirset /\ x e. ( ~P U. s i^i Fin ) ) ) /\ ( y e. ( ~P s i^i Fin ) /\ x C_ U. y ) ) -> ( ( mrCls ` C ) ` x ) C_ U. s )
50 15 49 rexlimddv 
 |-  ( ( ( C e. ( ACS ` X ) /\ s e. ~P C ) /\ ( ( toInc ` s ) e. Dirset /\ x e. ( ~P U. s i^i Fin ) ) ) -> ( ( mrCls ` C ) ` x ) C_ U. s )
51 50 anassrs 
 |-  ( ( ( ( C e. ( ACS ` X ) /\ s e. ~P C ) /\ ( toInc ` s ) e. Dirset ) /\ x e. ( ~P U. s i^i Fin ) ) -> ( ( mrCls ` C ) ` x ) C_ U. s )
52 51 ralrimiva 
 |-  ( ( ( C e. ( ACS ` X ) /\ s e. ~P C ) /\ ( toInc ` s ) e. Dirset ) -> A. x e. ( ~P U. s i^i Fin ) ( ( mrCls ` C ) ` x ) C_ U. s )
53 17 acsfiel 
 |-  ( C e. ( ACS ` X ) -> ( U. s e. C <-> ( U. s C_ X /\ A. x e. ( ~P U. s i^i Fin ) ( ( mrCls ` C ) ` x ) C_ U. s ) ) )
54 53 ad2antrr 
 |-  ( ( ( C e. ( ACS ` X ) /\ s e. ~P C ) /\ ( toInc ` s ) e. Dirset ) -> ( U. s e. C <-> ( U. s C_ X /\ A. x e. ( ~P U. s i^i Fin ) ( ( mrCls ` C ) ` x ) C_ U. s ) ) )
55 9 52 54 mpbir2and 
 |-  ( ( ( C e. ( ACS ` X ) /\ s e. ~P C ) /\ ( toInc ` s ) e. Dirset ) -> U. s e. C )
56 55 ex 
 |-  ( ( C e. ( ACS ` X ) /\ s e. ~P C ) -> ( ( toInc ` s ) e. Dirset -> U. s e. C ) )
57 56 ralrimiva 
 |-  ( C e. ( ACS ` X ) -> A. s e. ~P C ( ( toInc ` s ) e. Dirset -> U. s e. C ) )
58 1 57 jca 
 |-  ( C e. ( ACS ` X ) -> ( C e. ( Moore ` X ) /\ A. s e. ~P C ( ( toInc ` s ) e. Dirset -> U. s e. C ) ) )