Theorem ismrcd1 39315

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

Hypotheses

Ref	Expression
ismrcd.b	⊢ (𝜑 → 𝐵 ∈ 𝑉)
ismrcd.f	⊢ (𝜑 → 𝐹:𝒫 𝐵⟶𝒫 𝐵)
ismrcd.e	⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐵) → 𝑥 ⊆ (𝐹‘𝑥))
ismrcd.m	⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐵 ∧ 𝑦 ⊆ 𝑥) → (𝐹‘𝑦) ⊆ (𝐹‘𝑥))
ismrcd.i	⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐵) → (𝐹‘(𝐹‘𝑥)) = (𝐹‘𝑥))

Assertion

Ref	Expression
ismrcd1	⊢ (𝜑 → dom (𝐹 ∩ I ) ∈ (Moore‘𝐵))

Distinct variable groups:   𝜑,𝑥,𝑦   𝑥,𝐵,𝑦   𝑥,𝐹,𝑦   𝑥,𝑉,𝑦

Proof of Theorem ismrcd1

Dummy variable 𝑧 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		inss1 4205	. . . 4 ⊢ (𝐹 ∩ I ) ⊆ 𝐹
2		dmss 5771	. . . 4 ⊢ ((𝐹 ∩ I ) ⊆ 𝐹 → dom (𝐹 ∩ I ) ⊆ dom 𝐹)
3	1, 2	ax-mp 5	. . 3 ⊢ dom (𝐹 ∩ I ) ⊆ dom 𝐹
4		ismrcd.f	. . 3 ⊢ (𝜑 → 𝐹:𝒫 𝐵⟶𝒫 𝐵)
5	3, 4	fssdm 6530	. 2 ⊢ (𝜑 → dom (𝐹 ∩ I ) ⊆ 𝒫 𝐵)
6		ssid 3989	. . . . . . 7 ⊢ 𝐵 ⊆ 𝐵
7		ismrcd.b	. . . . . . . 8 ⊢ (𝜑 → 𝐵 ∈ 𝑉)
8		elpwg 4542	. . . . . . . 8 ⊢ (𝐵 ∈ 𝑉 → (𝐵 ∈ 𝒫 𝐵 ↔ 𝐵 ⊆ 𝐵))
9	7, 8	syl 17	. . . . . . 7 ⊢ (𝜑 → (𝐵 ∈ 𝒫 𝐵 ↔ 𝐵 ⊆ 𝐵))
10	6, 9	mpbiri 260	. . . . . 6 ⊢ (𝜑 → 𝐵 ∈ 𝒫 𝐵)
11	4, 10	ffvelrnd 6852	. . . . 5 ⊢ (𝜑 → (𝐹‘𝐵) ∈ 𝒫 𝐵)
12	11	elpwid 4550	. . . 4 ⊢ (𝜑 → (𝐹‘𝐵) ⊆ 𝐵)
13		velpw 4544	. . . . . . 7 ⊢ (𝑥 ∈ 𝒫 𝐵 ↔ 𝑥 ⊆ 𝐵)
14		ismrcd.e	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐵) → 𝑥 ⊆ (𝐹‘𝑥))
15	13, 14	sylan2b 595	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝒫 𝐵) → 𝑥 ⊆ (𝐹‘𝑥))
16	15	ralrimiva 3182	. . . . 5 ⊢ (𝜑 → ∀𝑥 ∈ 𝒫 𝐵𝑥 ⊆ (𝐹‘𝑥))
17		id 22	. . . . . . 7 ⊢ (𝑥 = 𝐵 → 𝑥 = 𝐵)
18		fveq2 6670	. . . . . . 7 ⊢ (𝑥 = 𝐵 → (𝐹‘𝑥) = (𝐹‘𝐵))
19	17, 18	sseq12d 4000	. . . . . 6 ⊢ (𝑥 = 𝐵 → (𝑥 ⊆ (𝐹‘𝑥) ↔ 𝐵 ⊆ (𝐹‘𝐵)))
20	19	rspcva 3621	. . . . 5 ⊢ ((𝐵 ∈ 𝒫 𝐵 ∧ ∀𝑥 ∈ 𝒫 𝐵𝑥 ⊆ (𝐹‘𝑥)) → 𝐵 ⊆ (𝐹‘𝐵))
21	10, 16, 20	syl2anc 586	. . . 4 ⊢ (𝜑 → 𝐵 ⊆ (𝐹‘𝐵))
22	12, 21	eqssd 3984	. . 3 ⊢ (𝜑 → (𝐹‘𝐵) = 𝐵)
23	4	ffnd 6515	. . . 4 ⊢ (𝜑 → 𝐹 Fn 𝒫 𝐵)
24		fnelfp 6937	. . . 4 ⊢ ((𝐹 Fn 𝒫 𝐵 ∧ 𝐵 ∈ 𝒫 𝐵) → (𝐵 ∈ dom (𝐹 ∩ I ) ↔ (𝐹‘𝐵) = 𝐵))
25	23, 10, 24	syl2anc 586	. . 3 ⊢ (𝜑 → (𝐵 ∈ dom (𝐹 ∩ I ) ↔ (𝐹‘𝐵) = 𝐵))
26	22, 25	mpbird 259	. 2 ⊢ (𝜑 → 𝐵 ∈ dom (𝐹 ∩ I ))
27		simp2 1133	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → 𝑧 ⊆ dom (𝐹 ∩ I ))
28	5	3ad2ant1 1129	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → dom (𝐹 ∩ I ) ⊆ 𝒫 𝐵)
29	27, 28	sstrd 3977	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → 𝑧 ⊆ 𝒫 𝐵)
30		simp3 1134	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → 𝑧 ≠ ∅)
31		intssuni2 4901	. . . . . . . . . . . 12 ⊢ ((𝑧 ⊆ 𝒫 𝐵 ∧ 𝑧 ≠ ∅) → ∩ 𝑧 ⊆ ∪ 𝒫 𝐵)
32	29, 30, 31	syl2anc 586	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → ∩ 𝑧 ⊆ ∪ 𝒫 𝐵)
33		unipw 5343	. . . . . . . . . . 11 ⊢ ∪ 𝒫 𝐵 = 𝐵
34	32, 33	sseqtrdi 4017	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → ∩ 𝑧 ⊆ 𝐵)
35		intex 5240	. . . . . . . . . . . 12 ⊢ (𝑧 ≠ ∅ ↔ ∩ 𝑧 ∈ V)
36		elpwg 4542	. . . . . . . . . . . 12 ⊢ (∩ 𝑧 ∈ V → (∩ 𝑧 ∈ 𝒫 𝐵 ↔ ∩ 𝑧 ⊆ 𝐵))
37	35, 36	sylbi 219	. . . . . . . . . . 11 ⊢ (𝑧 ≠ ∅ → (∩ 𝑧 ∈ 𝒫 𝐵 ↔ ∩ 𝑧 ⊆ 𝐵))
38	37	3ad2ant3 1131	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → (∩ 𝑧 ∈ 𝒫 𝐵 ↔ ∩ 𝑧 ⊆ 𝐵))
39	34, 38	mpbird 259	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → ∩ 𝑧 ∈ 𝒫 𝐵)
40	39	adantr 483	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) ∧ 𝑥 ∈ 𝑧) → ∩ 𝑧 ∈ 𝒫 𝐵)
41		ismrcd.m	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐵 ∧ 𝑦 ⊆ 𝑥) → (𝐹‘𝑦) ⊆ (𝐹‘𝑥))
42	41	3expib 1118	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑥 ⊆ 𝐵 ∧ 𝑦 ⊆ 𝑥) → (𝐹‘𝑦) ⊆ (𝐹‘𝑥)))
43	42	alrimiv 1928	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑦((𝑥 ⊆ 𝐵 ∧ 𝑦 ⊆ 𝑥) → (𝐹‘𝑦) ⊆ (𝐹‘𝑥)))
44	43	3ad2ant1 1129	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → ∀𝑦((𝑥 ⊆ 𝐵 ∧ 𝑦 ⊆ 𝑥) → (𝐹‘𝑦) ⊆ (𝐹‘𝑥)))
45	44	adantr 483	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) ∧ 𝑥 ∈ 𝑧) → ∀𝑦((𝑥 ⊆ 𝐵 ∧ 𝑦 ⊆ 𝑥) → (𝐹‘𝑦) ⊆ (𝐹‘𝑥)))
46	29	sselda 3967	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) ∧ 𝑥 ∈ 𝑧) → 𝑥 ∈ 𝒫 𝐵)
47	46	elpwid 4550	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) ∧ 𝑥 ∈ 𝑧) → 𝑥 ⊆ 𝐵)
48		intss1 4891	. . . . . . . . . 10 ⊢ (𝑥 ∈ 𝑧 → ∩ 𝑧 ⊆ 𝑥)
49	48	adantl 484	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) ∧ 𝑥 ∈ 𝑧) → ∩ 𝑧 ⊆ 𝑥)
50	47, 49	jca 514	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) ∧ 𝑥 ∈ 𝑧) → (𝑥 ⊆ 𝐵 ∧ ∩ 𝑧 ⊆ 𝑥))
51		sseq1 3992	. . . . . . . . . . 11 ⊢ (𝑦 = ∩ 𝑧 → (𝑦 ⊆ 𝑥 ↔ ∩ 𝑧 ⊆ 𝑥))
52	51	anbi2d 630	. . . . . . . . . 10 ⊢ (𝑦 = ∩ 𝑧 → ((𝑥 ⊆ 𝐵 ∧ 𝑦 ⊆ 𝑥) ↔ (𝑥 ⊆ 𝐵 ∧ ∩ 𝑧 ⊆ 𝑥)))
53		fveq2 6670	. . . . . . . . . . 11 ⊢ (𝑦 = ∩ 𝑧 → (𝐹‘𝑦) = (𝐹‘∩ 𝑧))
54	53	sseq1d 3998	. . . . . . . . . 10 ⊢ (𝑦 = ∩ 𝑧 → ((𝐹‘𝑦) ⊆ (𝐹‘𝑥) ↔ (𝐹‘∩ 𝑧) ⊆ (𝐹‘𝑥)))
55	52, 54	imbi12d 347	. . . . . . . . 9 ⊢ (𝑦 = ∩ 𝑧 → (((𝑥 ⊆ 𝐵 ∧ 𝑦 ⊆ 𝑥) → (𝐹‘𝑦) ⊆ (𝐹‘𝑥)) ↔ ((𝑥 ⊆ 𝐵 ∧ ∩ 𝑧 ⊆ 𝑥) → (𝐹‘∩ 𝑧) ⊆ (𝐹‘𝑥))))
56	55	spcgv 3595	. . . . . . . 8 ⊢ (∩ 𝑧 ∈ 𝒫 𝐵 → (∀𝑦((𝑥 ⊆ 𝐵 ∧ 𝑦 ⊆ 𝑥) → (𝐹‘𝑦) ⊆ (𝐹‘𝑥)) → ((𝑥 ⊆ 𝐵 ∧ ∩ 𝑧 ⊆ 𝑥) → (𝐹‘∩ 𝑧) ⊆ (𝐹‘𝑥))))
57	40, 45, 50, 56	syl3c 66	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) ∧ 𝑥 ∈ 𝑧) → (𝐹‘∩ 𝑧) ⊆ (𝐹‘𝑥))
58	27	sselda 3967	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) ∧ 𝑥 ∈ 𝑧) → 𝑥 ∈ dom (𝐹 ∩ I ))
59	23	3ad2ant1 1129	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → 𝐹 Fn 𝒫 𝐵)
60	59	adantr 483	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) ∧ 𝑥 ∈ 𝑧) → 𝐹 Fn 𝒫 𝐵)
61		fnelfp 6937	. . . . . . . . 9 ⊢ ((𝐹 Fn 𝒫 𝐵 ∧ 𝑥 ∈ 𝒫 𝐵) → (𝑥 ∈ dom (𝐹 ∩ I ) ↔ (𝐹‘𝑥) = 𝑥))
62	60, 46, 61	syl2anc 586	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) ∧ 𝑥 ∈ 𝑧) → (𝑥 ∈ dom (𝐹 ∩ I ) ↔ (𝐹‘𝑥) = 𝑥))
63	58, 62	mpbid 234	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) ∧ 𝑥 ∈ 𝑧) → (𝐹‘𝑥) = 𝑥)
64	57, 63	sseqtrd 4007	. . . . . 6 ⊢ (((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) ∧ 𝑥 ∈ 𝑧) → (𝐹‘∩ 𝑧) ⊆ 𝑥)
65	64	ralrimiva 3182	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → ∀𝑥 ∈ 𝑧 (𝐹‘∩ 𝑧) ⊆ 𝑥)
66		ssint 4892	. . . . 5 ⊢ ((𝐹‘∩ 𝑧) ⊆ ∩ 𝑧 ↔ ∀𝑥 ∈ 𝑧 (𝐹‘∩ 𝑧) ⊆ 𝑥)
67	65, 66	sylibr 236	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → (𝐹‘∩ 𝑧) ⊆ ∩ 𝑧)
68	16	3ad2ant1 1129	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → ∀𝑥 ∈ 𝒫 𝐵𝑥 ⊆ (𝐹‘𝑥))
69		id 22	. . . . . . 7 ⊢ (𝑥 = ∩ 𝑧 → 𝑥 = ∩ 𝑧)
70		fveq2 6670	. . . . . . 7 ⊢ (𝑥 = ∩ 𝑧 → (𝐹‘𝑥) = (𝐹‘∩ 𝑧))
71	69, 70	sseq12d 4000	. . . . . 6 ⊢ (𝑥 = ∩ 𝑧 → (𝑥 ⊆ (𝐹‘𝑥) ↔ ∩ 𝑧 ⊆ (𝐹‘∩ 𝑧)))
72	71	rspcva 3621	. . . . 5 ⊢ ((∩ 𝑧 ∈ 𝒫 𝐵 ∧ ∀𝑥 ∈ 𝒫 𝐵𝑥 ⊆ (𝐹‘𝑥)) → ∩ 𝑧 ⊆ (𝐹‘∩ 𝑧))
73	39, 68, 72	syl2anc 586	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → ∩ 𝑧 ⊆ (𝐹‘∩ 𝑧))
74	67, 73	eqssd 3984	. . 3 ⊢ ((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → (𝐹‘∩ 𝑧) = ∩ 𝑧)
75		fnelfp 6937	. . . 4 ⊢ ((𝐹 Fn 𝒫 𝐵 ∧ ∩ 𝑧 ∈ 𝒫 𝐵) → (∩ 𝑧 ∈ dom (𝐹 ∩ I ) ↔ (𝐹‘∩ 𝑧) = ∩ 𝑧))
76	59, 39, 75	syl2anc 586	. . 3 ⊢ ((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → (∩ 𝑧 ∈ dom (𝐹 ∩ I ) ↔ (𝐹‘∩ 𝑧) = ∩ 𝑧))
77	74, 76	mpbird 259	. 2 ⊢ ((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → ∩ 𝑧 ∈ dom (𝐹 ∩ I ))
78	5, 26, 77	ismred 16873	1 ⊢ (𝜑 → dom (𝐹 ∩ I ) ∈ (Moore‘𝐵))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   ∧ w3a 1083  ∀wal 1535   = wceq 1537   ∈ wcel 2114   ≠ wne 3016  ∀wral 3138  Vcvv 3494   ∩ cin 3935   ⊆ wss 3936  ∅c0 4291  𝒫 cpw 4539  ∪ cuni 4838  ∩ cint 4876   I cid 5459  dom cdm 5555   Fn wfn 6350  ⟶wf 6351  ‘cfv 6355  Moorecmre 16853

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pow 5266  ax-pr 5330

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-sbc 3773  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-pw 4541  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4839  df-int 4877  df-br 5067  df-opab 5129  df-mpt 5147  df-id 5460  df-xp 5561  df-rel 5562  df-cnv 5563  df-co 5564  df-dm 5565  df-rn 5566  df-res 5567  df-iota 6314  df-fun 6357  df-fn 6358  df-f 6359  df-fv 6363  df-mre 16857

This theorem is referenced by:  ismrcd2  39316  istopclsd  39317  ismrc  39318