Metamath Proof Explorer

Theorem ismrc

Description: A function is a Moore closure operator iff it satisfies mrcssid , mrcss , and mrcidm . (Contributed by Stefan O'Rear, 1-Feb-2015)

Ref Expression
Assertion ismrc ⊢F∈mrClsMoore⁡B↔B∈V∧F:𝒫B⟶𝒫B∧∀x∀yx⊆B∧y⊆x→x⊆F⁡x∧F⁡y⊆F⁡x∧F⁡F⁡x=F⁡x

Proof

Step Hyp Ref Expression
1 fnmrc ⊢mrClsFn⋃ran⁡Moore
2 fnfun ⊢mrClsFn⋃ran⁡Moore→Fun⁡mrCls
3 1 2 ax-mp ⊢Fun⁡mrCls
4 fvelima ⊢Fun⁡mrCls∧F∈mrClsMoore⁡B→∃z∈Moore⁡BmrCls⁡z=F
5 3 4 mpan ⊢F∈mrClsMoore⁡B→∃z∈Moore⁡BmrCls⁡z=F
6 elfvex ⊢z∈Moore⁡B→B∈V
7 eqid ⊢mrCls⁡z=mrCls⁡z
8 7 mrcf ⊢z∈Moore⁡B→mrCls⁡z:𝒫B⟶z
9 mresspw ⊢z∈Moore⁡B→z⊆𝒫B
10 8 9 fssd ⊢z∈Moore⁡B→mrCls⁡z:𝒫B⟶𝒫B
11 7 mrcssid ⊢z∈Moore⁡B∧x⊆B→x⊆mrCls⁡z⁡x
12 11 adantrr ⊢z∈Moore⁡B∧x⊆B∧y⊆x→x⊆mrCls⁡z⁡x
13 7 mrcss ⊢z∈Moore⁡B∧y⊆x∧x⊆B→mrCls⁡z⁡y⊆mrCls⁡z⁡x
14 13 3expb ⊢z∈Moore⁡B∧y⊆x∧x⊆B→mrCls⁡z⁡y⊆mrCls⁡z⁡x
15 14 ancom2s ⊢z∈Moore⁡B∧x⊆B∧y⊆x→mrCls⁡z⁡y⊆mrCls⁡z⁡x
16 7 mrcidm ⊢z∈Moore⁡B∧x⊆B→mrCls⁡z⁡mrCls⁡z⁡x=mrCls⁡z⁡x
17 16 adantrr ⊢z∈Moore⁡B∧x⊆B∧y⊆x→mrCls⁡z⁡mrCls⁡z⁡x=mrCls⁡z⁡x
18 12 15 17 3jca ⊢z∈Moore⁡B∧x⊆B∧y⊆x→x⊆mrCls⁡z⁡x∧mrCls⁡z⁡y⊆mrCls⁡z⁡x∧mrCls⁡z⁡mrCls⁡z⁡x=mrCls⁡z⁡x
19 18 ex ⊢z∈Moore⁡B→x⊆B∧y⊆x→x⊆mrCls⁡z⁡x∧mrCls⁡z⁡y⊆mrCls⁡z⁡x∧mrCls⁡z⁡mrCls⁡z⁡x=mrCls⁡z⁡x
20 19 alrimivv ⊢z∈Moore⁡B→∀x∀yx⊆B∧y⊆x→x⊆mrCls⁡z⁡x∧mrCls⁡z⁡y⊆mrCls⁡z⁡x∧mrCls⁡z⁡mrCls⁡z⁡x=mrCls⁡z⁡x
21 6 10 20 3jca ⊢z∈Moore⁡B→B∈V∧mrCls⁡z:𝒫B⟶𝒫B∧∀x∀yx⊆B∧y⊆x→x⊆mrCls⁡z⁡x∧mrCls⁡z⁡y⊆mrCls⁡z⁡x∧mrCls⁡z⁡mrCls⁡z⁡x=mrCls⁡z⁡x
22 feq1 ⊢mrCls⁡z=F→mrCls⁡z:𝒫B⟶𝒫B↔F:𝒫B⟶𝒫B
23 fveq1 ⊢mrCls⁡z=F→mrCls⁡z⁡x=F⁡x
24 23 sseq2d ⊢mrCls⁡z=F→x⊆mrCls⁡z⁡x↔x⊆F⁡x
25 fveq1 ⊢mrCls⁡z=F→mrCls⁡z⁡y=F⁡y
26 25 23 sseq12d ⊢mrCls⁡z=F→mrCls⁡z⁡y⊆mrCls⁡z⁡x↔F⁡y⊆F⁡x
27 id ⊢mrCls⁡z=F→mrCls⁡z=F
28 27 23 fveq12d ⊢mrCls⁡z=F→mrCls⁡z⁡mrCls⁡z⁡x=F⁡F⁡x
29 28 23 eqeq12d ⊢mrCls⁡z=F→mrCls⁡z⁡mrCls⁡z⁡x=mrCls⁡z⁡x↔F⁡F⁡x=F⁡x
30 24 26 29 3anbi123d ⊢mrCls⁡z=F→x⊆mrCls⁡z⁡x∧mrCls⁡z⁡y⊆mrCls⁡z⁡x∧mrCls⁡z⁡mrCls⁡z⁡x=mrCls⁡z⁡x↔x⊆F⁡x∧F⁡y⊆F⁡x∧F⁡F⁡x=F⁡x
31 30 imbi2d ⊢mrCls⁡z=F→x⊆B∧y⊆x→x⊆mrCls⁡z⁡x∧mrCls⁡z⁡y⊆mrCls⁡z⁡x∧mrCls⁡z⁡mrCls⁡z⁡x=mrCls⁡z⁡x↔x⊆B∧y⊆x→x⊆F⁡x∧F⁡y⊆F⁡x∧F⁡F⁡x=F⁡x
32 31 2albidv ⊢mrCls⁡z=F→∀x∀yx⊆B∧y⊆x→x⊆mrCls⁡z⁡x∧mrCls⁡z⁡y⊆mrCls⁡z⁡x∧mrCls⁡z⁡mrCls⁡z⁡x=mrCls⁡z⁡x↔∀x∀yx⊆B∧y⊆x→x⊆F⁡x∧F⁡y⊆F⁡x∧F⁡F⁡x=F⁡x
33 22 32 3anbi23d ⊢mrCls⁡z=F→B∈V∧mrCls⁡z:𝒫B⟶𝒫B∧∀x∀yx⊆B∧y⊆x→x⊆mrCls⁡z⁡x∧mrCls⁡z⁡y⊆mrCls⁡z⁡x∧mrCls⁡z⁡mrCls⁡z⁡x=mrCls⁡z⁡x↔B∈V∧F:𝒫B⟶𝒫B∧∀x∀yx⊆B∧y⊆x→x⊆F⁡x∧F⁡y⊆F⁡x∧F⁡F⁡x=F⁡x
34 21 33 syl5ibcom ⊢z∈Moore⁡B→mrCls⁡z=F→B∈V∧F:𝒫B⟶𝒫B∧∀x∀yx⊆B∧y⊆x→x⊆F⁡x∧F⁡y⊆F⁡x∧F⁡F⁡x=F⁡x
35 34 rexlimiv ⊢∃z∈Moore⁡BmrCls⁡z=F→B∈V∧F:𝒫B⟶𝒫B∧∀x∀yx⊆B∧y⊆x→x⊆F⁡x∧F⁡y⊆F⁡x∧F⁡F⁡x=F⁡x
36 5 35 syl ⊢F∈mrClsMoore⁡B→B∈V∧F:𝒫B⟶𝒫B∧∀x∀yx⊆B∧y⊆x→x⊆F⁡x∧F⁡y⊆F⁡x∧F⁡F⁡x=F⁡x
37 simp1 ⊢B∈V∧F:𝒫B⟶𝒫B∧∀x∀yx⊆B∧y⊆x→x⊆F⁡x∧F⁡y⊆F⁡x∧F⁡F⁡x=F⁡x→B∈V
38 simp2 ⊢B∈V∧F:𝒫B⟶𝒫B∧∀x∀yx⊆B∧y⊆x→x⊆F⁡x∧F⁡y⊆F⁡x∧F⁡F⁡x=F⁡x→F:𝒫B⟶𝒫B
39 ssid ⊢z⊆z
40 3simpb ⊢x⊆F⁡x∧F⁡y⊆F⁡x∧F⁡F⁡x=F⁡x→x⊆F⁡x∧F⁡F⁡x=F⁡x
41 40 imim2i ⊢x⊆B∧y⊆x→x⊆F⁡x∧F⁡y⊆F⁡x∧F⁡F⁡x=F⁡x→x⊆B∧y⊆x→x⊆F⁡x∧F⁡F⁡x=F⁡x
42 41 2alimi ⊢∀x∀yx⊆B∧y⊆x→x⊆F⁡x∧F⁡y⊆F⁡x∧F⁡F⁡x=F⁡x→∀x∀yx⊆B∧y⊆x→x⊆F⁡x∧F⁡F⁡x=F⁡x
43 sseq1 ⊢x=z→x⊆B↔z⊆B
44 43 adantr ⊢x=z∧y=z→x⊆B↔z⊆B
45 sseq12 ⊢y=z∧x=z→y⊆x↔z⊆z
46 45 ancoms ⊢x=z∧y=z→y⊆x↔z⊆z
47 44 46 anbi12d ⊢x=z∧y=z→x⊆B∧y⊆x↔z⊆B∧z⊆z
48 id ⊢x=z→x=z
49 fveq2 ⊢x=z→F⁡x=F⁡z
50 48 49 sseq12d ⊢x=z→x⊆F⁡x↔z⊆F⁡z
51 50 adantr ⊢x=z∧y=z→x⊆F⁡x↔z⊆F⁡z
52 2fveq3 ⊢x=z→F⁡F⁡x=F⁡F⁡z
53 52 49 eqeq12d ⊢x=z→F⁡F⁡x=F⁡x↔F⁡F⁡z=F⁡z
54 53 adantr ⊢x=z∧y=z→F⁡F⁡x=F⁡x↔F⁡F⁡z=F⁡z
55 51 54 anbi12d ⊢x=z∧y=z→x⊆F⁡x∧F⁡F⁡x=F⁡x↔z⊆F⁡z∧F⁡F⁡z=F⁡z
56 47 55 imbi12d ⊢x=z∧y=z→x⊆B∧y⊆x→x⊆F⁡x∧F⁡F⁡x=F⁡x↔z⊆B∧z⊆z→z⊆F⁡z∧F⁡F⁡z=F⁡z
57 56 spc2gv ⊢z∈V∧z∈V→∀x∀yx⊆B∧y⊆x→x⊆F⁡x∧F⁡F⁡x=F⁡x→z⊆B∧z⊆z→z⊆F⁡z∧F⁡F⁡z=F⁡z
58 57 el2v ⊢∀x∀yx⊆B∧y⊆x→x⊆F⁡x∧F⁡F⁡x=F⁡x→z⊆B∧z⊆z→z⊆F⁡z∧F⁡F⁡z=F⁡z
59 42 58 syl ⊢∀x∀yx⊆B∧y⊆x→x⊆F⁡x∧F⁡y⊆F⁡x∧F⁡F⁡x=F⁡x→z⊆B∧z⊆z→z⊆F⁡z∧F⁡F⁡z=F⁡z
60 59 3ad2ant3 ⊢B∈V∧F:𝒫B⟶𝒫B∧∀x∀yx⊆B∧y⊆x→x⊆F⁡x∧F⁡y⊆F⁡x∧F⁡F⁡x=F⁡x→z⊆B∧z⊆z→z⊆F⁡z∧F⁡F⁡z=F⁡z
61 39 60 mpan2i ⊢B∈V∧F:𝒫B⟶𝒫B∧∀x∀yx⊆B∧y⊆x→x⊆F⁡x∧F⁡y⊆F⁡x∧F⁡F⁡x=F⁡x→z⊆B→z⊆F⁡z∧F⁡F⁡z=F⁡z
62 61 imp ⊢B∈V∧F:𝒫B⟶𝒫B∧∀x∀yx⊆B∧y⊆x→x⊆F⁡x∧F⁡y⊆F⁡x∧F⁡F⁡x=F⁡x∧z⊆B→z⊆F⁡z∧F⁡F⁡z=F⁡z
63 62 simpld ⊢B∈V∧F:𝒫B⟶𝒫B∧∀x∀yx⊆B∧y⊆x→x⊆F⁡x∧F⁡y⊆F⁡x∧F⁡F⁡x=F⁡x∧z⊆B→z⊆F⁡z
64 simp2 ⊢x⊆F⁡x∧F⁡y⊆F⁡x∧F⁡F⁡x=F⁡x→F⁡y⊆F⁡x
65 64 imim2i ⊢x⊆B∧y⊆x→x⊆F⁡x∧F⁡y⊆F⁡x∧F⁡F⁡x=F⁡x→x⊆B∧y⊆x→F⁡y⊆F⁡x
66 65 2alimi ⊢∀x∀yx⊆B∧y⊆x→x⊆F⁡x∧F⁡y⊆F⁡x∧F⁡F⁡x=F⁡x→∀x∀yx⊆B∧y⊆x→F⁡y⊆F⁡x
67 66 3ad2ant3 ⊢B∈V∧F:𝒫B⟶𝒫B∧∀x∀yx⊆B∧y⊆x→x⊆F⁡x∧F⁡y⊆F⁡x∧F⁡F⁡x=F⁡x→∀x∀yx⊆B∧y⊆x→F⁡y⊆F⁡x
68 43 adantr ⊢x=z∧y=w→x⊆B↔z⊆B
69 sseq12 ⊢y=w∧x=z→y⊆x↔w⊆z
70 69 ancoms ⊢x=z∧y=w→y⊆x↔w⊆z
71 68 70 anbi12d ⊢x=z∧y=w→x⊆B∧y⊆x↔z⊆B∧w⊆z
72 fveq2 ⊢y=w→F⁡y=F⁡w
73 sseq12 ⊢F⁡y=F⁡w∧F⁡x=F⁡z→F⁡y⊆F⁡x↔F⁡w⊆F⁡z
74 72 49 73 syl2anr ⊢x=z∧y=w→F⁡y⊆F⁡x↔F⁡w⊆F⁡z
75 71 74 imbi12d ⊢x=z∧y=w→x⊆B∧y⊆x→F⁡y⊆F⁡x↔z⊆B∧w⊆z→F⁡w⊆F⁡z
76 75 spc2gv ⊢z∈V∧w∈V→∀x∀yx⊆B∧y⊆x→F⁡y⊆F⁡x→z⊆B∧w⊆z→F⁡w⊆F⁡z
77 76 el2v ⊢∀x∀yx⊆B∧y⊆x→F⁡y⊆F⁡x→z⊆B∧w⊆z→F⁡w⊆F⁡z
78 67 77 syl ⊢B∈V∧F:𝒫B⟶𝒫B∧∀x∀yx⊆B∧y⊆x→x⊆F⁡x∧F⁡y⊆F⁡x∧F⁡F⁡x=F⁡x→z⊆B∧w⊆z→F⁡w⊆F⁡z
79 78 3impib ⊢B∈V∧F:𝒫B⟶𝒫B∧∀x∀yx⊆B∧y⊆x→x⊆F⁡x∧F⁡y⊆F⁡x∧F⁡F⁡x=F⁡x∧z⊆B∧w⊆z→F⁡w⊆F⁡z
80 62 simprd ⊢B∈V∧F:𝒫B⟶𝒫B∧∀x∀yx⊆B∧y⊆x→x⊆F⁡x∧F⁡y⊆F⁡x∧F⁡F⁡x=F⁡x∧z⊆B→F⁡F⁡z=F⁡z
81 37 38 63 79 80 ismrcd2 ⊢B∈V∧F:𝒫B⟶𝒫B∧∀x∀yx⊆B∧y⊆x→x⊆F⁡x∧F⁡y⊆F⁡x∧F⁡F⁡x=F⁡x→F=mrCls⁡dom⁡F∩I
82 37 38 63 79 80 ismrcd1 ⊢B∈V∧F:𝒫B⟶𝒫B∧∀x∀yx⊆B∧y⊆x→x⊆F⁡x∧F⁡y⊆F⁡x∧F⁡F⁡x=F⁡x→dom⁡F∩I∈Moore⁡B
83 fvssunirn ⊢Moore⁡B⊆⋃ran⁡Moore
84 1 fndmi ⊢dom⁡mrCls=⋃ran⁡Moore
85 83 84 sseqtrri ⊢Moore⁡B⊆dom⁡mrCls
86 funfvima2 ⊢Fun⁡mrCls∧Moore⁡B⊆dom⁡mrCls→dom⁡F∩I∈Moore⁡B→mrCls⁡dom⁡F∩I∈mrClsMoore⁡B
87 3 85 86 mp2an ⊢dom⁡F∩I∈Moore⁡B→mrCls⁡dom⁡F∩I∈mrClsMoore⁡B
88 82 87 syl ⊢B∈V∧F:𝒫B⟶𝒫B∧∀x∀yx⊆B∧y⊆x→x⊆F⁡x∧F⁡y⊆F⁡x∧F⁡F⁡x=F⁡x→mrCls⁡dom⁡F∩I∈mrClsMoore⁡B
89 81 88 eqeltrd ⊢B∈V∧F:𝒫B⟶𝒫B∧∀x∀yx⊆B∧y⊆x→x⊆F⁡x∧F⁡y⊆F⁡x∧F⁡F⁡x=F⁡x→F∈mrClsMoore⁡B
90 36 89 impbii ⊢F∈mrClsMoore⁡B↔B∈V∧F:𝒫B⟶𝒫B∧∀x∀yx⊆B∧y⊆x→x⊆F⁡x∧F⁡y⊆F⁡x∧F⁡F⁡x=F⁡x