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∈𝒫Xs∈C↔∀y∈𝒫s∩FinF⁡y⊆s

Proof

Step Hyp Ref Expression
1 isacs2.f ⊢F=mrCls⁡C
2 isacs ⊢C∈ACS⁡X↔C∈Moore⁡X∧∃ff:𝒫X⟶𝒫X∧∀t∈𝒫Xt∈C↔⋃f𝒫t∩Fin⊆t
3 ffun ⊢f:𝒫X⟶𝒫X→Fun⁡f
4 funiunfv ⊢Fun⁡f→⋃z∈𝒫t∩Finf⁡z=⋃f𝒫t∩Fin
5 3 4 syl ⊢f:𝒫X⟶𝒫X→⋃z∈𝒫t∩Finf⁡z=⋃f𝒫t∩Fin
6 5 sseq1d ⊢f:𝒫X⟶𝒫X→⋃z∈𝒫t∩Finf⁡z⊆t↔⋃f𝒫t∩Fin⊆t
7 iunss ⊢⋃z∈𝒫t∩Finf⁡z⊆t↔∀z∈𝒫t∩Finf⁡z⊆t
8 6 7 bitr3di ⊢f:𝒫X⟶𝒫X→⋃f𝒫t∩Fin⊆t↔∀z∈𝒫t∩Finf⁡z⊆t
9 8 bibi2d ⊢f:𝒫X⟶𝒫X→t∈C↔⋃f𝒫t∩Fin⊆t↔t∈C↔∀z∈𝒫t∩Finf⁡z⊆t
10 9 ralbidv ⊢f:𝒫X⟶𝒫X→∀t∈𝒫Xt∈C↔⋃f𝒫t∩Fin⊆t↔∀t∈𝒫Xt∈C↔∀z∈𝒫t∩Finf⁡z⊆t
11 10 pm5.32i ⊢f:𝒫X⟶𝒫X∧∀t∈𝒫Xt∈C↔⋃f𝒫t∩Fin⊆t↔f:𝒫X⟶𝒫X∧∀t∈𝒫Xt∈C↔∀z∈𝒫t∩Finf⁡z⊆t
12 11 exbii ⊢∃ff:𝒫X⟶𝒫X∧∀t∈𝒫Xt∈C↔⋃f𝒫t∩Fin⊆t↔∃ff:𝒫X⟶𝒫X∧∀t∈𝒫Xt∈C↔∀z∈𝒫t∩Finf⁡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∩FinF⁡y⊆s
21 20 ad4ant14 ⊢C∈Moore⁡X∧f:𝒫X⟶𝒫X∧∀t∈𝒫Xt∈C↔∀z∈𝒫t∩Finf⁡z⊆t∧s∈𝒫X∧s∈C→∀y∈𝒫s∩FinF⁡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∈𝒫Xt∈C↔∀z∈𝒫t∩Finf⁡z⊆t∧s∈𝒫X∧y∈𝒫s∩Fin→C∈Moore⁡X
25 15 adantl ⊢C∈Moore⁡X∧f:𝒫X⟶𝒫X∧∀t∈𝒫Xt∈C↔∀z∈𝒫t∩Finf⁡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∈𝒫Xt∈C↔∀z∈𝒫t∩Finf⁡z⊆t∧s∈𝒫X∧y∈𝒫s∩Fin→s⊆X
28 25 27 sstrd ⊢C∈Moore⁡X∧f:𝒫X⟶𝒫X∧∀t∈𝒫Xt∈C↔∀z∈𝒫t∩Finf⁡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∈𝒫Xt∈C↔∀z∈𝒫t∩Finf⁡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∩Finf⁡z⊆t↔∀z∈𝒫F⁡y∩Finf⁡z⊆F⁡y
36 31 35 bibi12d ⊢t=F⁡y→t∈C↔∀z∈𝒫t∩Finf⁡z⊆t↔F⁡y∈C↔∀z∈𝒫F⁡y∩Finf⁡z⊆F⁡y
37 simprr ⊢C∈Moore⁡X∧f:𝒫X⟶𝒫X∧∀t∈𝒫Xt∈C↔∀z∈𝒫t∩Finf⁡z⊆t→∀t∈𝒫Xt∈C↔∀z∈𝒫t∩Finf⁡z⊆t
38 37 ad2antrr ⊢C∈Moore⁡X∧f:𝒫X⟶𝒫X∧∀t∈𝒫Xt∈C↔∀z∈𝒫t∩Finf⁡z⊆t∧s∈𝒫X∧y∈𝒫s∩Fin→∀t∈𝒫Xt∈C↔∀z∈𝒫t∩Finf⁡z⊆t
39 mresspw ⊢C∈Moore⁡X→C⊆𝒫X
40 39 ad3antrrr ⊢C∈Moore⁡X∧f:𝒫X⟶𝒫X∧∀t∈𝒫Xt∈C↔∀z∈𝒫t∩Finf⁡z⊆t∧s∈𝒫X∧y∈𝒫s∩Fin→C⊆𝒫X
41 40 30 sseldd ⊢C∈Moore⁡X∧f:𝒫X⟶𝒫X∧∀t∈𝒫Xt∈C↔∀z∈𝒫t∩Finf⁡z⊆t∧s∈𝒫X∧y∈𝒫s∩Fin→F⁡y∈𝒫X
42 36 38 41 rspcdva ⊢C∈Moore⁡X∧f:𝒫X⟶𝒫X∧∀t∈𝒫Xt∈C↔∀z∈𝒫t∩Finf⁡z⊆t∧s∈𝒫X∧y∈𝒫s∩Fin→F⁡y∈C↔∀z∈𝒫F⁡y∩Finf⁡z⊆F⁡y
43 30 42 mpbid ⊢C∈Moore⁡X∧f:𝒫X⟶𝒫X∧∀t∈𝒫Xt∈C↔∀z∈𝒫t∩Finf⁡z⊆t∧s∈𝒫X∧y∈𝒫s∩Fin→∀z∈𝒫F⁡y∩Finf⁡z⊆F⁡y
44 24 1 28 mrcssidd ⊢C∈Moore⁡X∧f:𝒫X⟶𝒫X∧∀t∈𝒫Xt∈C↔∀z∈𝒫t∩Finf⁡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∈𝒫Xt∈C↔∀z∈𝒫t∩Finf⁡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∈𝒫Xt∈C↔∀z∈𝒫t∩Finf⁡z⊆t∧s∈𝒫X∧y∈𝒫s∩Fin→y∈Fin
50 47 49 elind ⊢C∈Moore⁡X∧f:𝒫X⟶𝒫X∧∀t∈𝒫Xt∈C↔∀z∈𝒫t∩Finf⁡z⊆t∧s∈𝒫X∧y∈𝒫s∩Fin→y∈𝒫F⁡y∩Fin
51 23 43 50 rspcdva ⊢C∈Moore⁡X∧f:𝒫X⟶𝒫X∧∀t∈𝒫Xt∈C↔∀z∈𝒫t∩Finf⁡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∈𝒫Xt∈C↔∀z∈𝒫t∩Finf⁡z⊆t∧s∈𝒫X∧y∈𝒫s∩Fin→F⁡y⊆s→f⁡y⊆s
54 53 ralimdva ⊢C∈Moore⁡X∧f:𝒫X⟶𝒫X∧∀t∈𝒫Xt∈C↔∀z∈𝒫t∩Finf⁡z⊆t∧s∈𝒫X→∀y∈𝒫s∩FinF⁡y⊆s→∀y∈𝒫s∩Finf⁡y⊆s
55 54 imp ⊢C∈Moore⁡X∧f:𝒫X⟶𝒫X∧∀t∈𝒫Xt∈C↔∀z∈𝒫t∩Finf⁡z⊆t∧s∈𝒫X∧∀y∈𝒫s∩FinF⁡y⊆s→∀y∈𝒫s∩Finf⁡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∩Finf⁡y⊆s↔∀z∈𝒫s∩Finf⁡z⊆s
59 55 58 sylib ⊢C∈Moore⁡X∧f:𝒫X⟶𝒫X∧∀t∈𝒫Xt∈C↔∀z∈𝒫t∩Finf⁡z⊆t∧s∈𝒫X∧∀y∈𝒫s∩FinF⁡y⊆s→∀z∈𝒫s∩Finf⁡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∩Finf⁡z⊆t↔∀z∈𝒫s∩Finf⁡z⊆s
65 60 64 bibi12d ⊢t=s→t∈C↔∀z∈𝒫t∩Finf⁡z⊆t↔s∈C↔∀z∈𝒫s∩Finf⁡z⊆s
66 37 ad2antrr ⊢C∈Moore⁡X∧f:𝒫X⟶𝒫X∧∀t∈𝒫Xt∈C↔∀z∈𝒫t∩Finf⁡z⊆t∧s∈𝒫X∧∀y∈𝒫s∩FinF⁡y⊆s→∀t∈𝒫Xt∈C↔∀z∈𝒫t∩Finf⁡z⊆t
67 simplr ⊢C∈Moore⁡X∧f:𝒫X⟶𝒫X∧∀t∈𝒫Xt∈C↔∀z∈𝒫t∩Finf⁡z⊆t∧s∈𝒫X∧∀y∈𝒫s∩FinF⁡y⊆s→s∈𝒫X
68 65 66 67 rspcdva ⊢C∈Moore⁡X∧f:𝒫X⟶𝒫X∧∀t∈𝒫Xt∈C↔∀z∈𝒫t∩Finf⁡z⊆t∧s∈𝒫X∧∀y∈𝒫s∩FinF⁡y⊆s→s∈C↔∀z∈𝒫s∩Finf⁡z⊆s
69 59 68 mpbird ⊢C∈Moore⁡X∧f:𝒫X⟶𝒫X∧∀t∈𝒫Xt∈C↔∀z∈𝒫t∩Finf⁡z⊆t∧s∈𝒫X∧∀y∈𝒫s∩FinF⁡y⊆s→s∈C
70 21 69 impbida ⊢C∈Moore⁡X∧f:𝒫X⟶𝒫X∧∀t∈𝒫Xt∈C↔∀z∈𝒫t∩Finf⁡z⊆t∧s∈𝒫X→s∈C↔∀y∈𝒫s∩FinF⁡y⊆s
71 70 ralrimiva ⊢C∈Moore⁡X∧f:𝒫X⟶𝒫X∧∀t∈𝒫Xt∈C↔∀z∈𝒫t∩Finf⁡z⊆t→∀s∈𝒫Xs∈C↔∀y∈𝒫s∩FinF⁡y⊆s
72 71 ex ⊢C∈Moore⁡X→f:𝒫X⟶𝒫X∧∀t∈𝒫Xt∈C↔∀z∈𝒫t∩Finf⁡z⊆t→∀s∈𝒫Xs∈C↔∀y∈𝒫s∩FinF⁡y⊆s
73 72 exlimdv ⊢C∈Moore⁡X→∃ff:𝒫X⟶𝒫X∧∀t∈𝒫Xt∈C↔∀z∈𝒫t∩Finf⁡z⊆t→∀s∈𝒫Xs∈C↔∀y∈𝒫s∩FinF⁡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∩Finf⁡z⊆t↔∀z∈𝒫t∩FinF⁡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∩FinF⁡z⊆t↔∀y∈𝒫t∩FinF⁡y⊆t
84 80 83 bitrdi ⊢f=F→∀z∈𝒫t∩Finf⁡z⊆t↔∀y∈𝒫t∩FinF⁡y⊆t
85 84 bibi2d ⊢f=F→t∈C↔∀z∈𝒫t∩Finf⁡z⊆t↔t∈C↔∀y∈𝒫t∩FinF⁡y⊆t
86 85 ralbidv ⊢f=F→∀t∈𝒫Xt∈C↔∀z∈𝒫t∩Finf⁡z⊆t↔∀t∈𝒫Xt∈C↔∀y∈𝒫t∩FinF⁡y⊆t
87 sseq2 ⊢t=s→F⁡y⊆t↔F⁡y⊆s
88 62 87 raleqbidv ⊢t=s→∀y∈𝒫t∩FinF⁡y⊆t↔∀y∈𝒫s∩FinF⁡y⊆s
89 60 88 bibi12d ⊢t=s→t∈C↔∀y∈𝒫t∩FinF⁡y⊆t↔s∈C↔∀y∈𝒫s∩FinF⁡y⊆s
90 89 cbvralvw ⊢∀t∈𝒫Xt∈C↔∀y∈𝒫t∩FinF⁡y⊆t↔∀s∈𝒫Xs∈C↔∀y∈𝒫s∩FinF⁡y⊆s
91 86 90 bitrdi ⊢f=F→∀t∈𝒫Xt∈C↔∀z∈𝒫t∩Finf⁡z⊆t↔∀s∈𝒫Xs∈C↔∀y∈𝒫s∩FinF⁡y⊆s
92 77 91 anbi12d ⊢f=F→f:𝒫X⟶𝒫X∧∀t∈𝒫Xt∈C↔∀z∈𝒫t∩Finf⁡z⊆t↔F:𝒫X⟶𝒫X∧∀s∈𝒫Xs∈C↔∀y∈𝒫s∩FinF⁡y⊆s
93 76 92 spcev ⊢F:𝒫X⟶𝒫X∧∀s∈𝒫Xs∈C↔∀y∈𝒫s∩FinF⁡y⊆s→∃ff:𝒫X⟶𝒫X∧∀t∈𝒫Xt∈C↔∀z∈𝒫t∩Finf⁡z⊆t
94 75 93 sylan ⊢C∈Moore⁡X∧∀s∈𝒫Xs∈C↔∀y∈𝒫s∩FinF⁡y⊆s→∃ff:𝒫X⟶𝒫X∧∀t∈𝒫Xt∈C↔∀z∈𝒫t∩Finf⁡z⊆t
95 94 ex ⊢C∈Moore⁡X→∀s∈𝒫Xs∈C↔∀y∈𝒫s∩FinF⁡y⊆s→∃ff:𝒫X⟶𝒫X∧∀t∈𝒫Xt∈C↔∀z∈𝒫t∩Finf⁡z⊆t
96 73 95 impbid ⊢C∈Moore⁡X→∃ff:𝒫X⟶𝒫X∧∀t∈𝒫Xt∈C↔∀z∈𝒫t∩Finf⁡z⊆t↔∀s∈𝒫Xs∈C↔∀y∈𝒫s∩FinF⁡y⊆s
97 12 96 bitrid ⊢C∈Moore⁡X→∃ff:𝒫X⟶𝒫X∧∀t∈𝒫Xt∈C↔⋃f𝒫t∩Fin⊆t↔∀s∈𝒫Xs∈C↔∀y∈𝒫s∩FinF⁡y⊆s
98 97 pm5.32i ⊢C∈Moore⁡X∧∃ff:𝒫X⟶𝒫X∧∀t∈𝒫Xt∈C↔⋃f𝒫t∩Fin⊆t↔C∈Moore⁡X∧∀s∈𝒫Xs∈C↔∀y∈𝒫s∩FinF⁡y⊆s
99 2 98 bitri ⊢C∈ACS⁡X↔C∈Moore⁡X∧∀s∈𝒫Xs∈C↔∀y∈𝒫s∩FinF⁡y⊆s