Theorem ismrcd1 35611

Description: Any function from the subsets of a set to itself, which is extensive (satisfies mrcssid 15601), isotone (satisfies mrcss 15600), and idempotent (satisfies mrcidm 15603) 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 35612 is the second. (Contributed by Stefan O'Rear, 1-Feb-2015.)

Hypotheses

Ref	Expression
ismrcd.b	|- ( ph -> B e. V )
ismrcd.f	|- ( ph -> F : ~P B --> ~P B )
ismrcd.e	|- ( ( ph /\ x C_ B ) -> x C_ ( F ` x ) )
ismrcd.m	|- ( ( ph /\ x C_ B /\ y C_ x ) -> ( F ` y ) C_ ( F ` x ) )
ismrcd.i	|- ( ( ph /\ x C_ B ) -> ( F ` ( F ` x ) ) = ( F ` x ) )

Assertion

Ref	Expression
ismrcd1	|- ( ph -> dom ( F i^i _I ) e. (Moore ` B ) )

Distinct variable groups:   ph, x, y   x, B, y   x, F, y   x, V, y

Proof of Theorem ismrcd1

Dummy variable z is distinct from all other variables.

Step	Hyp	Ref	Expression
1		inss1 3643	. . . 4 |- ( F i^i _I ) C_ F
2		dmss 5039	. . . 4 |- ( ( F i^i _I ) C_ F -> dom ( F i^i _I ) C_ dom F )
3	1, 2	ax-mp 5	. . 3 |- dom ( F i^i _I ) C_ dom F
4		ismrcd.f	. . . 4 |- ( ph -> F : ~P B --> ~P B )
5		fdm 5745	. . . 4 |- ( F : ~P B --> ~P B -> dom F = ~P B )
6	4, 5	syl 17	. . 3 |- ( ph -> dom F = ~P B )
7	3, 6	syl5sseq 3466	. 2 |- ( ph -> dom ( F i^i _I ) C_ ~P B )
8		ssid 3437	. . . . . . 7 |- B C_ B
9		ismrcd.b	. . . . . . . 8 |- ( ph -> B e. V )
10		elpwg 3950	. . . . . . . 8 |- ( B e. V -> ( B e. ~P B <-> B C_ B ) )
11	9, 10	syl 17	. . . . . . 7 |- ( ph -> ( B e. ~P B <-> B C_ B ) )
12	8, 11	mpbiri 241	. . . . . 6 |- ( ph -> B e. ~P B )
13	4, 12	ffvelrnd 6038	. . . . 5 |- ( ph -> ( F ` B ) e. ~P B )
14	13	elpwid 3952	. . . 4 |- ( ph -> ( F ` B ) C_ B )
15		selpw 3949	. . . . . . 7 |- ( x e. ~P B <-> x C_ B )
16		ismrcd.e	. . . . . . 7 |- ( ( ph /\ x C_ B ) -> x C_ ( F ` x ) )
17	15, 16	sylan2b 483	. . . . . 6 |- ( ( ph /\ x e. ~P B ) -> x C_ ( F ` x ) )
18	17	ralrimiva 2809	. . . . 5 |- ( ph -> A. x e. ~P B x C_ ( F ` x ) )
19		id 22	. . . . . . 7 |- ( x = B -> x = B )
20		fveq2 5879	. . . . . . 7 |- ( x = B -> ( F ` x ) = ( F ` B ) )
21	19, 20	sseq12d 3447	. . . . . 6 |- ( x = B -> ( x C_ ( F ` x ) <-> B C_ ( F ` B ) ) )
22	21	rspcva 3134	. . . . 5 |- ( ( B e. ~P B /\ A. x e. ~P B x C_ ( F ` x ) ) -> B C_ ( F ` B ) )
23	12, 18, 22	syl2anc 673	. . . 4 |- ( ph -> B C_ ( F ` B ) )
24	14, 23	eqssd 3435	. . 3 |- ( ph -> ( F ` B ) = B )
25		ffn 5739	. . . . 5 |- ( F : ~P B --> ~P B -> F Fn ~P B )
26	4, 25	syl 17	. . . 4 |- ( ph -> F Fn ~P B )
27		fnelfp 6108	. . . 4 |- ( ( F Fn ~P B /\ B e. ~P B ) -> ( B e. dom ( F i^i _I ) <-> ( F ` B ) = B ) )
28	26, 12, 27	syl2anc 673	. . 3 |- ( ph -> ( B e. dom ( F i^i _I ) <-> ( F ` B ) = B ) )
29	24, 28	mpbird 240	. 2 |- ( ph -> B e. dom ( F i^i _I ) )
30		simp2 1031	. . . . . . . . . . . . 13 |- ( ( ph /\ z C_ dom ( F i^i _I ) /\ z =/= (/) ) -> z C_ dom ( F i^i _I ) )
31	7	3ad2ant1 1051	. . . . . . . . . . . . 13 |- ( ( ph /\ z C_ dom ( F i^i _I ) /\ z =/= (/) ) -> dom ( F i^i _I ) C_ ~P B )
32	30, 31	sstrd 3428	. . . . . . . . . . . 12 |- ( ( ph /\ z C_ dom ( F i^i _I ) /\ z =/= (/) ) -> z C_ ~P B )
33		simp3 1032	. . . . . . . . . . . 12 |- ( ( ph /\ z C_ dom ( F i^i _I ) /\ z =/= (/) ) -> z =/= (/) )
34		intssuni2 4251	. . . . . . . . . . . 12 |- ( ( z C_ ~P B /\ z =/= (/) ) -> |^| z C_ U. ~P B )
35	32, 33, 34	syl2anc 673	. . . . . . . . . . 11 |- ( ( ph /\ z C_ dom ( F i^i _I ) /\ z =/= (/) ) -> |^| z C_ U. ~P B )
36		unipw 4650	. . . . . . . . . . 11 |- U. ~P B = B
37	35, 36	syl6sseq 3464	. . . . . . . . . 10 |- ( ( ph /\ z C_ dom ( F i^i _I ) /\ z =/= (/) ) -> |^| z C_ B )
38		intex 4557	. . . . . . . . . . . 12 |- ( z =/= (/) <-> |^| z e. _V )
39		elpwg 3950	. . . . . . . . . . . 12 |- ( |^| z e. _V -> ( |^| z e. ~P B <-> |^| z C_ B ) )
40	38, 39	sylbi 200	. . . . . . . . . . 11 |- ( z =/= (/) -> ( |^| z e. ~P B <-> |^| z C_ B ) )
41	40	3ad2ant3 1053	. . . . . . . . . 10 |- ( ( ph /\ z C_ dom ( F i^i _I ) /\ z =/= (/) ) -> ( |^| z e. ~P B <-> |^| z C_ B ) )
42	37, 41	mpbird 240	. . . . . . . . 9 |- ( ( ph /\ z C_ dom ( F i^i _I ) /\ z =/= (/) ) -> |^| z e. ~P B )
43	42	adantr 472	. . . . . . . 8 |- ( ( ( ph /\ z C_ dom ( F i^i _I ) /\ z =/= (/) ) /\ x e. z ) -> |^| z e. ~P B )
44		ismrcd.m	. . . . . . . . . . . 12 |- ( ( ph /\ x C_ B /\ y C_ x ) -> ( F ` y ) C_ ( F ` x ) )
45	44	3expib 1234	. . . . . . . . . . 11 |- ( ph -> ( ( x C_ B /\ y C_ x ) -> ( F ` y ) C_ ( F ` x ) ) )
46	45	alrimiv 1781	. . . . . . . . . 10 |- ( ph -> A. y ( ( x C_ B /\ y C_ x ) -> ( F ` y ) C_ ( F ` x ) ) )
47	46	3ad2ant1 1051	. . . . . . . . 9 |- ( ( ph /\ z C_ dom ( F i^i _I ) /\ z =/= (/) ) -> A. y ( ( x C_ B /\ y C_ x ) -> ( F ` y ) C_ ( F ` x ) ) )
48	47	adantr 472	. . . . . . . 8 |- ( ( ( ph /\ z C_ dom ( F i^i _I ) /\ z =/= (/) ) /\ x e. z ) -> A. y ( ( x C_ B /\ y C_ x ) -> ( F ` y ) C_ ( F ` x ) ) )
49	32	sselda 3418	. . . . . . . . . 10 |- ( ( ( ph /\ z C_ dom ( F i^i _I ) /\ z =/= (/) ) /\ x e. z ) -> x e. ~P B )
50	49	elpwid 3952	. . . . . . . . 9 |- ( ( ( ph /\ z C_ dom ( F i^i _I ) /\ z =/= (/) ) /\ x e. z ) -> x C_ B )
51		intss1 4241	. . . . . . . . . 10 |- ( x e. z -> |^| z C_ x )
52	51	adantl 473	. . . . . . . . 9 |- ( ( ( ph /\ z C_ dom ( F i^i _I ) /\ z =/= (/) ) /\ x e. z ) -> |^| z C_ x )
53	50, 52	jca 541	. . . . . . . 8 |- ( ( ( ph /\ z C_ dom ( F i^i _I ) /\ z =/= (/) ) /\ x e. z ) -> ( x C_ B /\ |^| z C_ x ) )
54		sseq1 3439	. . . . . . . . . . 11 |- ( y = |^| z -> ( y C_ x <-> |^| z C_ x ) )
55	54	anbi2d 718	. . . . . . . . . 10 |- ( y = |^| z -> ( ( x C_ B /\ y C_ x ) <-> ( x C_ B /\ |^| z C_ x ) ) )
56		fveq2 5879	. . . . . . . . . . 11 |- ( y = |^| z -> ( F ` y ) = ( F ` |^| z ) )
57	56	sseq1d 3445	. . . . . . . . . 10 |- ( y = |^| z -> ( ( F ` y ) C_ ( F ` x ) <-> ( F ` |^| z ) C_ ( F ` x ) ) )
58	55, 57	imbi12d 327	. . . . . . . . 9 |- ( y = |^| z -> ( ( ( x C_ B /\ y C_ x ) -> ( F ` y ) C_ ( F ` x ) ) <-> ( ( x C_ B /\ |^| z C_ x ) -> ( F ` |^| z ) C_ ( F ` x ) ) ) )
59	58	spcgv 3120	. . . . . . . 8 |- ( |^| z e. ~P B -> ( A. y ( ( x C_ B /\ y C_ x ) -> ( F ` y ) C_ ( F ` x ) ) -> ( ( x C_ B /\ |^| z C_ x ) -> ( F ` |^| z ) C_ ( F ` x ) ) ) )
60	43, 48, 53, 59	syl3c 62	. . . . . . 7 |- ( ( ( ph /\ z C_ dom ( F i^i _I ) /\ z =/= (/) ) /\ x e. z ) -> ( F ` |^| z ) C_ ( F ` x ) )
61	30	sselda 3418	. . . . . . . 8 |- ( ( ( ph /\ z C_ dom ( F i^i _I ) /\ z =/= (/) ) /\ x e. z ) -> x e. dom ( F i^i _I ) )
62	26	3ad2ant1 1051	. . . . . . . . . 10 |- ( ( ph /\ z C_ dom ( F i^i _I ) /\ z =/= (/) ) -> F Fn ~P B )
63	62	adantr 472	. . . . . . . . 9 |- ( ( ( ph /\ z C_ dom ( F i^i _I ) /\ z =/= (/) ) /\ x e. z ) -> F Fn ~P B )
64		fnelfp 6108	. . . . . . . . 9 |- ( ( F Fn ~P B /\ x e. ~P B ) -> ( x e. dom ( F i^i _I ) <-> ( F ` x ) = x ) )
65	63, 49, 64	syl2anc 673	. . . . . . . 8 |- ( ( ( ph /\ z C_ dom ( F i^i _I ) /\ z =/= (/) ) /\ x e. z ) -> ( x e. dom ( F i^i _I ) <-> ( F ` x ) = x ) )
66	61, 65	mpbid 215	. . . . . . 7 |- ( ( ( ph /\ z C_ dom ( F i^i _I ) /\ z =/= (/) ) /\ x e. z ) -> ( F ` x ) = x )
67	60, 66	sseqtrd 3454	. . . . . 6 |- ( ( ( ph /\ z C_ dom ( F i^i _I ) /\ z =/= (/) ) /\ x e. z ) -> ( F ` |^| z ) C_ x )
68	67	ralrimiva 2809	. . . . 5 |- ( ( ph /\ z C_ dom ( F i^i _I ) /\ z =/= (/) ) -> A. x e. z ( F ` |^| z ) C_ x )
69		ssint 4242	. . . . 5 |- ( ( F ` |^| z ) C_ |^| z <-> A. x e. z ( F ` |^| z ) C_ x )
70	68, 69	sylibr 217	. . . 4 |- ( ( ph /\ z C_ dom ( F i^i _I ) /\ z =/= (/) ) -> ( F ` |^| z ) C_ |^| z )
71	18	3ad2ant1 1051	. . . . 5 |- ( ( ph /\ z C_ dom ( F i^i _I ) /\ z =/= (/) ) -> A. x e. ~P B x C_ ( F ` x ) )
72		id 22	. . . . . . 7 |- ( x = |^| z -> x = |^| z )
73		fveq2 5879	. . . . . . 7 |- ( x = |^| z -> ( F ` x ) = ( F ` |^| z ) )
74	72, 73	sseq12d 3447	. . . . . 6 |- ( x = |^| z -> ( x C_ ( F ` x ) <-> |^| z C_ ( F ` |^| z ) ) )
75	74	rspcva 3134	. . . . 5 |- ( ( |^| z e. ~P B /\ A. x e. ~P B x C_ ( F ` x ) ) -> |^| z C_ ( F ` |^| z ) )
76	42, 71, 75	syl2anc 673	. . . 4 |- ( ( ph /\ z C_ dom ( F i^i _I ) /\ z =/= (/) ) -> |^| z C_ ( F ` |^| z ) )
77	70, 76	eqssd 3435	. . 3 |- ( ( ph /\ z C_ dom ( F i^i _I ) /\ z =/= (/) ) -> ( F ` |^| z ) = |^| z )
78		fnelfp 6108	. . . 4 |- ( ( F Fn ~P B /\ |^| z e. ~P B ) -> ( |^| z e. dom ( F i^i _I ) <-> ( F ` |^| z ) = |^| z ) )
79	62, 42, 78	syl2anc 673	. . 3 |- ( ( ph /\ z C_ dom ( F i^i _I ) /\ z =/= (/) ) -> ( |^| z e. dom ( F i^i _I ) <-> ( F ` |^| z ) = |^| z ) )
80	77, 79	mpbird 240	. 2 |- ( ( ph /\ z C_ dom ( F i^i _I ) /\ z =/= (/) ) -> |^| z e. dom ( F i^i _I ) )
81	7, 29, 80	ismred 15586	1 |- ( ph -> dom ( F i^i _I ) e. (Moore ` B ) )

Syntax hints:   -> wi 4   <-> wb 189   /\ wa 376   /\ w3a 1007   A.wal 1450   = wceq 1452   e. wcel 1904   =/= wne 2641   A.wral 2756   _Vcvv 3031   i^i cin 3389   C_ wss 3390   (/)c0 3722   ~Pcpw 3942   U.cuni 4190   |^|cint 4226   _I cid 4749   dom cdm 4839   Fn wfn 5584   -->wf 5585   ` cfv 5589  Moorecmre 15566

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-8 1906  ax-9 1913  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-sep 4518  ax-nul 4527  ax-pow 4579  ax-pr 4639

This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3an 1009  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-eu 2323  df-mo 2324  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ne 2643  df-ral 2761  df-rex 2762  df-rab 2765  df-v 3033  df-sbc 3256  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-nul 3723  df-if 3873  df-pw 3944  df-sn 3960  df-pr 3962  df-op 3966  df-uni 4191  df-int 4227  df-br 4396  df-opab 4455  df-mpt 4456  df-id 4754  df-xp 4845  df-rel 4846  df-cnv 4847  df-co 4848  df-dm 4849  df-rn 4850  df-res 4851  df-iota 5553  df-fun 5591  df-fn 5592  df-f 5593  df-fv 5597  df-mre 15570

This theorem is referenced by:  ismrcd2  35612  istopclsd  35613  ismrc  35614