Metamath Proof Explorer


Theorem ismrcd1

Description: Any function from the subsets of a set to itself, which is extensive (satisfies mrcssid ), isotone (satisfies mrcss ), and idempotent (satisfies mrcidm ) has a collection of fixed points which is a Moore collection, and itself is the closure operator for that collection. This can be taken as an alternate definition for the closure operators. This is the first half, ismrcd2 is the second. (Contributed by Stefan O'Rear, 1-Feb-2015)

Ref Expression
Hypotheses ismrcd.b φ B V
ismrcd.f φ F : 𝒫 B 𝒫 B
ismrcd.e φ x B x F x
ismrcd.m φ x B y x F y F x
ismrcd.i φ x B F F x = F x
Assertion ismrcd1 φ dom F I Moore B

Proof

Step Hyp Ref Expression
1 ismrcd.b φ B V
2 ismrcd.f φ F : 𝒫 B 𝒫 B
3 ismrcd.e φ x B x F x
4 ismrcd.m φ x B y x F y F x
5 ismrcd.i φ x B F F x = F x
6 inss1 F I F
7 dmss F I F dom F I dom F
8 6 7 ax-mp dom F I dom F
9 8 2 fssdm φ dom F I 𝒫 B
10 ssid B B
11 elpwg B V B 𝒫 B B B
12 1 11 syl φ B 𝒫 B B B
13 10 12 mpbiri φ B 𝒫 B
14 2 13 ffvelrnd φ F B 𝒫 B
15 14 elpwid φ F B B
16 velpw x 𝒫 B x B
17 16 3 sylan2b φ x 𝒫 B x F x
18 17 ralrimiva φ x 𝒫 B x F x
19 id x = B x = B
20 fveq2 x = B F x = F B
21 19 20 sseq12d x = B x F x B F B
22 21 rspcva B 𝒫 B x 𝒫 B x F x B F B
23 13 18 22 syl2anc φ B F B
24 15 23 eqssd φ F B = B
25 2 ffnd φ F Fn 𝒫 B
26 fnelfp F Fn 𝒫 B B 𝒫 B B dom F I F B = B
27 25 13 26 syl2anc φ B dom F I F B = B
28 24 27 mpbird φ B dom F I
29 simp2 φ z dom F I z z dom F I
30 9 3ad2ant1 φ z dom F I z dom F I 𝒫 B
31 29 30 sstrd φ z dom F I z z 𝒫 B
32 simp3 φ z dom F I z z
33 intssuni2 z 𝒫 B z z 𝒫 B
34 31 32 33 syl2anc φ z dom F I z z 𝒫 B
35 unipw 𝒫 B = B
36 34 35 sseqtrdi φ z dom F I z z B
37 intex z z V
38 elpwg z V z 𝒫 B z B
39 37 38 sylbi z z 𝒫 B z B
40 39 3ad2ant3 φ z dom F I z z 𝒫 B z B
41 36 40 mpbird φ z dom F I z z 𝒫 B
42 41 adantr φ z dom F I z x z z 𝒫 B
43 4 3expib φ x B y x F y F x
44 43 alrimiv φ y x B y x F y F x
45 44 3ad2ant1 φ z dom F I z y x B y x F y F x
46 45 adantr φ z dom F I z x z y x B y x F y F x
47 31 sselda φ z dom F I z x z x 𝒫 B
48 47 elpwid φ z dom F I z x z x B
49 intss1 x z z x
50 49 adantl φ z dom F I z x z z x
51 48 50 jca φ z dom F I z x z x B z x
52 sseq1 y = z y x z x
53 52 anbi2d y = z x B y x x B z x
54 fveq2 y = z F y = F z
55 54 sseq1d y = z F y F x F z F x
56 53 55 imbi12d y = z x B y x F y F x x B z x F z F x
57 56 spcgv z 𝒫 B y x B y x F y F x x B z x F z F x
58 42 46 51 57 syl3c φ z dom F I z x z F z F x
59 29 sselda φ z dom F I z x z x dom F I
60 25 3ad2ant1 φ z dom F I z F Fn 𝒫 B
61 60 adantr φ z dom F I z x z F Fn 𝒫 B
62 fnelfp F Fn 𝒫 B x 𝒫 B x dom F I F x = x
63 61 47 62 syl2anc φ z dom F I z x z x dom F I F x = x
64 59 63 mpbid φ z dom F I z x z F x = x
65 58 64 sseqtrd φ z dom F I z x z F z x
66 65 ralrimiva φ z dom F I z x z F z x
67 ssint F z z x z F z x
68 66 67 sylibr φ z dom F I z F z z
69 18 3ad2ant1 φ z dom F I z x 𝒫 B x F x
70 id x = z x = z
71 fveq2 x = z F x = F z
72 70 71 sseq12d x = z x F x z F z
73 72 rspcva z 𝒫 B x 𝒫 B x F x z F z
74 41 69 73 syl2anc φ z dom F I z z F z
75 68 74 eqssd φ z dom F I z F z = z
76 fnelfp F Fn 𝒫 B z 𝒫 B z dom F I F z = z
77 60 41 76 syl2anc φ z dom F I z z dom F I F z = z
78 75 77 mpbird φ z dom F I z z dom F I
79 9 28 78 ismred φ dom F I Moore B