Metamath Proof Explorer


Theorem isacs2

Description: In the definition of an algebraic closure system, we may always take the operation being closed over as the Moore closure. (Contributed by Stefan O'Rear, 2-Apr-2015)

Ref Expression
Hypothesis isacs2.f F = mrCls C
Assertion isacs2 C ACS X C Moore X s 𝒫 X s C y 𝒫 s Fin F y s

Proof

Step Hyp Ref Expression
1 isacs2.f F = mrCls C
2 isacs C ACS X C Moore X f f : 𝒫 X 𝒫 X t 𝒫 X t C f 𝒫 t Fin t
3 ffun f : 𝒫 X 𝒫 X Fun f
4 funiunfv Fun f z 𝒫 t Fin f z = f 𝒫 t Fin
5 3 4 syl f : 𝒫 X 𝒫 X z 𝒫 t Fin f z = f 𝒫 t Fin
6 5 sseq1d f : 𝒫 X 𝒫 X z 𝒫 t Fin f z t f 𝒫 t Fin t
7 iunss z 𝒫 t Fin f z t z 𝒫 t Fin f z t
8 6 7 bitr3di f : 𝒫 X 𝒫 X f 𝒫 t Fin t z 𝒫 t Fin f z t
9 8 bibi2d f : 𝒫 X 𝒫 X t C f 𝒫 t Fin t t C z 𝒫 t Fin f z t
10 9 ralbidv f : 𝒫 X 𝒫 X t 𝒫 X t C f 𝒫 t Fin t t 𝒫 X t C z 𝒫 t Fin f z t
11 10 pm5.32i f : 𝒫 X 𝒫 X t 𝒫 X t C f 𝒫 t Fin t f : 𝒫 X 𝒫 X t 𝒫 X t C z 𝒫 t Fin f z t
12 11 exbii f f : 𝒫 X 𝒫 X t 𝒫 X t C f 𝒫 t Fin t f f : 𝒫 X 𝒫 X t 𝒫 X t C z 𝒫 t Fin f z t
13 simpll C Moore X s C y 𝒫 s Fin C Moore X
14 elinel1 y 𝒫 s Fin y 𝒫 s
15 14 elpwid y 𝒫 s Fin y s
16 15 adantl C Moore X s C y 𝒫 s Fin y s
17 simplr C Moore X s C y 𝒫 s Fin s C
18 1 mrcsscl C Moore X y s s C F y s
19 13 16 17 18 syl3anc C Moore X s C y 𝒫 s Fin F y s
20 19 ralrimiva C Moore X s C y 𝒫 s Fin F y s
21 20 ad4ant14 C Moore X f : 𝒫 X 𝒫 X t 𝒫 X t C z 𝒫 t Fin f z t s 𝒫 X s C y 𝒫 s Fin F y s
22 fveq2 z = y f z = f y
23 22 sseq1d z = y f z F y f y F y
24 simplll C Moore X f : 𝒫 X 𝒫 X t 𝒫 X t C z 𝒫 t Fin f z t s 𝒫 X y 𝒫 s Fin C Moore X
25 15 adantl C Moore X f : 𝒫 X 𝒫 X t 𝒫 X t C z 𝒫 t Fin f z t s 𝒫 X y 𝒫 s Fin y s
26 elpwi s 𝒫 X s X
27 26 ad2antlr C Moore X f : 𝒫 X 𝒫 X t 𝒫 X t C z 𝒫 t Fin f z t s 𝒫 X y 𝒫 s Fin s X
28 25 27 sstrd C Moore X f : 𝒫 X 𝒫 X t 𝒫 X t C z 𝒫 t Fin f z t s 𝒫 X y 𝒫 s Fin y X
29 1 mrccl C Moore X y X F y C
30 24 28 29 syl2anc C Moore X f : 𝒫 X 𝒫 X t 𝒫 X t C z 𝒫 t Fin f z t s 𝒫 X y 𝒫 s Fin F y C
31 eleq1 t = F y t C F y C
32 pweq t = F y 𝒫 t = 𝒫 F y
33 32 ineq1d t = F y 𝒫 t Fin = 𝒫 F y Fin
34 sseq2 t = F y f z t f z F y
35 33 34 raleqbidv t = F y z 𝒫 t Fin f z t z 𝒫 F y Fin f z F y
36 31 35 bibi12d t = F y t C z 𝒫 t Fin f z t F y C z 𝒫 F y Fin f z F y
37 simprr C Moore X f : 𝒫 X 𝒫 X t 𝒫 X t C z 𝒫 t Fin f z t t 𝒫 X t C z 𝒫 t Fin f z t
38 37 ad2antrr C Moore X f : 𝒫 X 𝒫 X t 𝒫 X t C z 𝒫 t Fin f z t s 𝒫 X y 𝒫 s Fin t 𝒫 X t C z 𝒫 t Fin f z t
39 mresspw C Moore X C 𝒫 X
40 39 ad3antrrr C Moore X f : 𝒫 X 𝒫 X t 𝒫 X t C z 𝒫 t Fin f z t s 𝒫 X y 𝒫 s Fin C 𝒫 X
41 40 30 sseldd C Moore X f : 𝒫 X 𝒫 X t 𝒫 X t C z 𝒫 t Fin f z t s 𝒫 X y 𝒫 s Fin F y 𝒫 X
42 36 38 41 rspcdva C Moore X f : 𝒫 X 𝒫 X t 𝒫 X t C z 𝒫 t Fin f z t s 𝒫 X y 𝒫 s Fin F y C z 𝒫 F y Fin f z F y
43 30 42 mpbid C Moore X f : 𝒫 X 𝒫 X t 𝒫 X t C z 𝒫 t Fin f z t s 𝒫 X y 𝒫 s Fin z 𝒫 F y Fin f z F y
44 24 1 28 mrcssidd C Moore X f : 𝒫 X 𝒫 X t 𝒫 X t C z 𝒫 t Fin f z t s 𝒫 X y 𝒫 s Fin y F y
45 vex y V
46 45 elpw y 𝒫 F y y F y
47 44 46 sylibr C Moore X f : 𝒫 X 𝒫 X t 𝒫 X t C z 𝒫 t Fin f z t s 𝒫 X y 𝒫 s Fin y 𝒫 F y
48 elinel2 y 𝒫 s Fin y Fin
49 48 adantl C Moore X f : 𝒫 X 𝒫 X t 𝒫 X t C z 𝒫 t Fin f z t s 𝒫 X y 𝒫 s Fin y Fin
50 47 49 elind C Moore X f : 𝒫 X 𝒫 X t 𝒫 X t C z 𝒫 t Fin f z t s 𝒫 X y 𝒫 s Fin y 𝒫 F y Fin
51 23 43 50 rspcdva C Moore X f : 𝒫 X 𝒫 X t 𝒫 X t C z 𝒫 t Fin f z t s 𝒫 X y 𝒫 s Fin f y F y
52 sstr2 f y F y F y s f y s
53 51 52 syl C Moore X f : 𝒫 X 𝒫 X t 𝒫 X t C z 𝒫 t Fin f z t s 𝒫 X y 𝒫 s Fin F y s f y s
54 53 ralimdva C Moore X f : 𝒫 X 𝒫 X t 𝒫 X t C z 𝒫 t Fin f z t s 𝒫 X y 𝒫 s Fin F y s y 𝒫 s Fin f y s
55 54 imp C Moore X f : 𝒫 X 𝒫 X t 𝒫 X t C z 𝒫 t Fin f z t s 𝒫 X y 𝒫 s Fin F y s y 𝒫 s Fin f y s
56 fveq2 y = z f y = f z
57 56 sseq1d y = z f y s f z s
58 57 cbvralvw y 𝒫 s Fin f y s z 𝒫 s Fin f z s
59 55 58 sylib C Moore X f : 𝒫 X 𝒫 X t 𝒫 X t C z 𝒫 t Fin f z t s 𝒫 X y 𝒫 s Fin F y s z 𝒫 s Fin f z s
60 eleq1 t = s t C s C
61 pweq t = s 𝒫 t = 𝒫 s
62 61 ineq1d t = s 𝒫 t Fin = 𝒫 s Fin
63 sseq2 t = s f z t f z s
64 62 63 raleqbidv t = s z 𝒫 t Fin f z t z 𝒫 s Fin f z s
65 60 64 bibi12d t = s t C z 𝒫 t Fin f z t s C z 𝒫 s Fin f z s
66 37 ad2antrr C Moore X f : 𝒫 X 𝒫 X t 𝒫 X t C z 𝒫 t Fin f z t s 𝒫 X y 𝒫 s Fin F y s t 𝒫 X t C z 𝒫 t Fin f z t
67 simplr C Moore X f : 𝒫 X 𝒫 X t 𝒫 X t C z 𝒫 t Fin f z t s 𝒫 X y 𝒫 s Fin F y s s 𝒫 X
68 65 66 67 rspcdva C Moore X f : 𝒫 X 𝒫 X t 𝒫 X t C z 𝒫 t Fin f z t s 𝒫 X y 𝒫 s Fin F y s s C z 𝒫 s Fin f z s
69 59 68 mpbird C Moore X f : 𝒫 X 𝒫 X t 𝒫 X t C z 𝒫 t Fin f z t s 𝒫 X y 𝒫 s Fin F y s s C
70 21 69 impbida C Moore X f : 𝒫 X 𝒫 X t 𝒫 X t C z 𝒫 t Fin f z t s 𝒫 X s C y 𝒫 s Fin F y s
71 70 ralrimiva C Moore X f : 𝒫 X 𝒫 X t 𝒫 X t C z 𝒫 t Fin f z t s 𝒫 X s C y 𝒫 s Fin F y s
72 71 ex C Moore X f : 𝒫 X 𝒫 X t 𝒫 X t C z 𝒫 t Fin f z t s 𝒫 X s C y 𝒫 s Fin F y s
73 72 exlimdv C Moore X f f : 𝒫 X 𝒫 X t 𝒫 X t C z 𝒫 t Fin f z t s 𝒫 X s C y 𝒫 s Fin F y s
74 1 mrcf C Moore X F : 𝒫 X C
75 74 39 fssd C Moore X F : 𝒫 X 𝒫 X
76 1 fvexi F V
77 feq1 f = F f : 𝒫 X 𝒫 X F : 𝒫 X 𝒫 X
78 fveq1 f = F f z = F z
79 78 sseq1d f = F f z t F z t
80 79 ralbidv f = F z 𝒫 t Fin f z t z 𝒫 t Fin F z t
81 fveq2 z = y F z = F y
82 81 sseq1d z = y F z t F y t
83 82 cbvralvw z 𝒫 t Fin F z t y 𝒫 t Fin F y t
84 80 83 bitrdi f = F z 𝒫 t Fin f z t y 𝒫 t Fin F y t
85 84 bibi2d f = F t C z 𝒫 t Fin f z t t C y 𝒫 t Fin F y t
86 85 ralbidv f = F t 𝒫 X t C z 𝒫 t Fin f z t t 𝒫 X t C y 𝒫 t Fin F y t
87 sseq2 t = s F y t F y s
88 62 87 raleqbidv t = s y 𝒫 t Fin F y t y 𝒫 s Fin F y s
89 60 88 bibi12d t = s t C y 𝒫 t Fin F y t s C y 𝒫 s Fin F y s
90 89 cbvralvw t 𝒫 X t C y 𝒫 t Fin F y t s 𝒫 X s C y 𝒫 s Fin F y s
91 86 90 bitrdi f = F t 𝒫 X t C z 𝒫 t Fin f z t s 𝒫 X s C y 𝒫 s Fin F y s
92 77 91 anbi12d f = F f : 𝒫 X 𝒫 X t 𝒫 X t C z 𝒫 t Fin f z t F : 𝒫 X 𝒫 X s 𝒫 X s C y 𝒫 s Fin F y s
93 76 92 spcev F : 𝒫 X 𝒫 X s 𝒫 X s C y 𝒫 s Fin F y s f f : 𝒫 X 𝒫 X t 𝒫 X t C z 𝒫 t Fin f z t
94 75 93 sylan C Moore X s 𝒫 X s C y 𝒫 s Fin F y s f f : 𝒫 X 𝒫 X t 𝒫 X t C z 𝒫 t Fin f z t
95 94 ex C Moore X s 𝒫 X s C y 𝒫 s Fin F y s f f : 𝒫 X 𝒫 X t 𝒫 X t C z 𝒫 t Fin f z t
96 73 95 impbid C Moore X f f : 𝒫 X 𝒫 X t 𝒫 X t C z 𝒫 t Fin f z t s 𝒫 X s C y 𝒫 s Fin F y s
97 12 96 syl5bb C Moore X f f : 𝒫 X 𝒫 X t 𝒫 X t C f 𝒫 t Fin t s 𝒫 X s C y 𝒫 s Fin F y s
98 97 pm5.32i C Moore X f f : 𝒫 X 𝒫 X t 𝒫 X t C f 𝒫 t Fin t C Moore X s 𝒫 X s C y 𝒫 s Fin F y s
99 2 98 bitri C ACS X C Moore X s 𝒫 X s C y 𝒫 s Fin F y s