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	$⊢ φ \to B \in V$
	ismrcd.f	$⊢ φ \to F : 𝒫 B ⟶ 𝒫 B$
	ismrcd.e	$⊢ (φ \land x \subseteq B) \to x \subseteq F (x)$
	ismrcd.m	$⊢ (φ \land x \subseteq B \land y \subseteq x) \to F (y) \subseteq F (x)$
	ismrcd.i	$⊢ (φ \land x \subseteq B) \to F (F (x)) = F (x)$
Assertion	ismrcd1	$⊢ φ \to dom (F \cap I) \in Moore (B)$

Proof

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

Metamath Proof Explorer

Theorem ismrcd1

Proof