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 ACS X C Moore X s 𝒫 C toInc s Dirset s C

Proof

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