Theorem ismrcd1 43544

Description: Any function from the subsets of a set to itself, which is extensive (satisfies mrcssid 17706), isotone (satisfies mrcss 17705), and idempotent (satisfies mrcidm 17708) 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 43545 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 4182	. . . 4 ⊢ (𝐹 ∩ I ) ⊆ 𝐹
2		dmss 5886	. . . 4 ⊢ ((𝐹 ∩ I ) ⊆ 𝐹 → dom (𝐹 ∩ I ) ⊆ dom 𝐹)
3	1, 2	ax-mp 5	. . 3 ⊢ dom (𝐹 ∩ I ) ⊆ dom 𝐹
4		ismrcd.f	. . 3 ⊢ (𝜑 → 𝐹:𝒫 𝐵⟶𝒫 𝐵)
5	3, 4	fssdm 6723	. 2 ⊢ (𝜑 → dom (𝐹 ∩ I ) ⊆ 𝒫 𝐵)
6		ssid 3953	. . . . . . 7 ⊢ 𝐵 ⊆ 𝐵
7		ismrcd.b	. . . . . . . 8 ⊢ (𝜑 → 𝐵 ∈ 𝑉)
8		elpwg 4560	. . . . . . . 8 ⊢ (𝐵 ∈ 𝑉 → (𝐵 ∈ 𝒫 𝐵 ↔ 𝐵 ⊆ 𝐵))
9	7, 8	syl 18	. . . . . . 7 ⊢ (𝜑 → (𝐵 ∈ 𝒫 𝐵 ↔ 𝐵 ⊆ 𝐵))
10	6, 9	mpbiri 261	. . . . . 6 ⊢ (𝜑 → 𝐵 ∈ 𝒫 𝐵)
11	4, 10	ffvelcdmd 7079	. . . . 5 ⊢ (𝜑 → (𝐹‘𝐵) ∈ 𝒫 𝐵)
12	11	elpwid 4566	. . . 4 ⊢ (𝜑 → (𝐹‘𝐵) ⊆ 𝐵)
13		velpw 4562	. . . . . . 7 ⊢ (𝑥 ∈ 𝒫 𝐵 ↔ 𝑥 ⊆ 𝐵)
14		ismrcd.e	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐵) → 𝑥 ⊆ (𝐹‘𝑥))
15	13, 14	sylan2b 606	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝒫 𝐵) → 𝑥 ⊆ (𝐹‘𝑥))
16	15	ralrimiva 3154	. . . . 5 ⊢ (𝜑 → ∀𝑥 ∈ 𝒫 𝐵𝑥 ⊆ (𝐹‘𝑥))
17		id 23	. . . . . . 7 ⊢ (𝑥 = 𝐵 → 𝑥 = 𝐵)
18		fveq2 6879	. . . . . . 7 ⊢ (𝑥 = 𝐵 → (𝐹‘𝑥) = (𝐹‘𝐵))
19	17, 18	sseq12d 3964	. . . . . 6 ⊢ (𝑥 = 𝐵 → (𝑥 ⊆ (𝐹‘𝑥) ↔ 𝐵 ⊆ (𝐹‘𝐵)))
20	19	rspcva 3574	. . . . 5 ⊢ ((𝐵 ∈ 𝒫 𝐵 ∧ ∀𝑥 ∈ 𝒫 𝐵𝑥 ⊆ (𝐹‘𝑥)) → 𝐵 ⊆ (𝐹‘𝐵))
21	10, 16, 20	syl2anc 596	. . . 4 ⊢ (𝜑 → 𝐵 ⊆ (𝐹‘𝐵))
22	12, 21	eqssd 3948	. . 3 ⊢ (𝜑 → (𝐹‘𝐵) = 𝐵)
23	4	ffnd 6704	. . . 4 ⊢ (𝜑 → 𝐹 Fn 𝒫 𝐵)
24		fnelfp 7174	. . . 4 ⊢ ((𝐹 Fn 𝒫 𝐵 ∧ 𝐵 ∈ 𝒫 𝐵) → (𝐵 ∈ dom (𝐹 ∩ I ) ↔ (𝐹‘𝐵) = 𝐵))
25	23, 10, 24	syl2anc 596	. . 3 ⊢ (𝜑 → (𝐵 ∈ dom (𝐹 ∩ I ) ↔ (𝐹‘𝐵) = 𝐵))
26	22, 25	mpbird 260	. 2 ⊢ (𝜑 → 𝐵 ∈ dom (𝐹 ∩ I ))
27		simp2 1155	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → 𝑧 ⊆ dom (𝐹 ∩ I ))
28	5	3ad2ant1 1151	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → dom (𝐹 ∩ I ) ⊆ 𝒫 𝐵)
29	27, 28	sstrd 3941	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → 𝑧 ⊆ 𝒫 𝐵)
30		simp3 1156	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → 𝑧 ≠ ∅)
31		intssuni2 4933	. . . . . . . . . . . 12 ⊢ ((𝑧 ⊆ 𝒫 𝐵 ∧ 𝑧 ≠ ∅) → ∩ 𝑧 ⊆ ∪ 𝒫 𝐵)
32	29, 30, 31	syl2anc 596	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → ∩ 𝑧 ⊆ ∪ 𝒫 𝐵)
33		unipw 5425	. . . . . . . . . . 11 ⊢ ∪ 𝒫 𝐵 = 𝐵
34	32, 33	sseqtrdi 3971	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → ∩ 𝑧 ⊆ 𝐵)
35		intex 5308	. . . . . . . . . . . 12 ⊢ (𝑧 ≠ ∅ ↔ ∩ 𝑧 ∈ V)
36		elpwg 4560	. . . . . . . . . . . 12 ⊢ (∩ 𝑧 ∈ V → (∩ 𝑧 ∈ 𝒫 𝐵 ↔ ∩ 𝑧 ⊆ 𝐵))
37	35, 36	sylbi 220	. . . . . . . . . . 11 ⊢ (𝑧 ≠ ∅ → (∩ 𝑧 ∈ 𝒫 𝐵 ↔ ∩ 𝑧 ⊆ 𝐵))
38	37	3ad2ant3 1153	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → (∩ 𝑧 ∈ 𝒫 𝐵 ↔ ∩ 𝑧 ⊆ 𝐵))
39	34, 38	mpbird 260	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → ∩ 𝑧 ∈ 𝒫 𝐵)
40	39	adantr 486	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) ∧ 𝑥 ∈ 𝑧) → ∩ 𝑧 ∈ 𝒫 𝐵)
41		ismrcd.m	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐵 ∧ 𝑦 ⊆ 𝑥) → (𝐹‘𝑦) ⊆ (𝐹‘𝑥))
42	41	3expib 1140	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑥 ⊆ 𝐵 ∧ 𝑦 ⊆ 𝑥) → (𝐹‘𝑦) ⊆ (𝐹‘𝑥)))
43	42	alrimiv 1960	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑦((𝑥 ⊆ 𝐵 ∧ 𝑦 ⊆ 𝑥) → (𝐹‘𝑦) ⊆ (𝐹‘𝑥)))
44	43	3ad2ant1 1151	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → ∀𝑦((𝑥 ⊆ 𝐵 ∧ 𝑦 ⊆ 𝑥) → (𝐹‘𝑦) ⊆ (𝐹‘𝑥)))
45	44	adantr 486	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) ∧ 𝑥 ∈ 𝑧) → ∀𝑦((𝑥 ⊆ 𝐵 ∧ 𝑦 ⊆ 𝑥) → (𝐹‘𝑦) ⊆ (𝐹‘𝑥)))
46	29	sselda 3931	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) ∧ 𝑥 ∈ 𝑧) → 𝑥 ∈ 𝒫 𝐵)
47	46	elpwid 4566	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) ∧ 𝑥 ∈ 𝑧) → 𝑥 ⊆ 𝐵)
48		intss1 4923	. . . . . . . . . 10 ⊢ (𝑥 ∈ 𝑧 → ∩ 𝑧 ⊆ 𝑥)
49	48	adantl 487	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) ∧ 𝑥 ∈ 𝑧) → ∩ 𝑧 ⊆ 𝑥)
50	47, 49	jca 521	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) ∧ 𝑥 ∈ 𝑧) → (𝑥 ⊆ 𝐵 ∧ ∩ 𝑧 ⊆ 𝑥))
51		sseq1 3956	. . . . . . . . . . 11 ⊢ (𝑦 = ∩ 𝑧 → (𝑦 ⊆ 𝑥 ↔ ∩ 𝑧 ⊆ 𝑥))
52	51	anbi2d 642	. . . . . . . . . 10 ⊢ (𝑦 = ∩ 𝑧 → ((𝑥 ⊆ 𝐵 ∧ 𝑦 ⊆ 𝑥) ↔ (𝑥 ⊆ 𝐵 ∧ ∩ 𝑧 ⊆ 𝑥)))
53		fveq2 6879	. . . . . . . . . . 11 ⊢ (𝑦 = ∩ 𝑧 → (𝐹‘𝑦) = (𝐹‘∩ 𝑧))
54	53	sseq1d 3962	. . . . . . . . . 10 ⊢ (𝑦 = ∩ 𝑧 → ((𝐹‘𝑦) ⊆ (𝐹‘𝑥) ↔ (𝐹‘∩ 𝑧) ⊆ (𝐹‘𝑥)))
55	52, 54	imbi12d 347	. . . . . . . . 9 ⊢ (𝑦 = ∩ 𝑧 → (((𝑥 ⊆ 𝐵 ∧ 𝑦 ⊆ 𝑥) → (𝐹‘𝑦) ⊆ (𝐹‘𝑥)) ↔ ((𝑥 ⊆ 𝐵 ∧ ∩ 𝑧 ⊆ 𝑥) → (𝐹‘∩ 𝑧) ⊆ (𝐹‘𝑥))))
56	55	spcgv 3550	. . . . . . . 8 ⊢ (∩ 𝑧 ∈ 𝒫 𝐵 → (∀𝑦((𝑥 ⊆ 𝐵 ∧ 𝑦 ⊆ 𝑥) → (𝐹‘𝑦) ⊆ (𝐹‘𝑥)) → ((𝑥 ⊆ 𝐵 ∧ ∩ 𝑧 ⊆ 𝑥) → (𝐹‘∩ 𝑧) ⊆ (𝐹‘𝑥))))
57	40, 45, 50, 56	syl3c 67	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) ∧ 𝑥 ∈ 𝑧) → (𝐹‘∩ 𝑧) ⊆ (𝐹‘𝑥))
58	27	sselda 3931	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) ∧ 𝑥 ∈ 𝑧) → 𝑥 ∈ dom (𝐹 ∩ I ))
59	23	3ad2ant1 1151	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → 𝐹 Fn 𝒫 𝐵)
60	59	adantr 486	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) ∧ 𝑥 ∈ 𝑧) → 𝐹 Fn 𝒫 𝐵)
61		fnelfp 7174	. . . . . . . . 9 ⊢ ((𝐹 Fn 𝒫 𝐵 ∧ 𝑥 ∈ 𝒫 𝐵) → (𝑥 ∈ dom (𝐹 ∩ I ) ↔ (𝐹‘𝑥) = 𝑥))
62	60, 46, 61	syl2anc 596	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) ∧ 𝑥 ∈ 𝑧) → (𝑥 ∈ dom (𝐹 ∩ I ) ↔ (𝐹‘𝑥) = 𝑥))
63	58, 62	mpbid 235	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) ∧ 𝑥 ∈ 𝑧) → (𝐹‘𝑥) = 𝑥)
64	57, 63	sseqtrd 3967	. . . . . 6 ⊢ (((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) ∧ 𝑥 ∈ 𝑧) → (𝐹‘∩ 𝑧) ⊆ 𝑥)
65	64	ralrimiva 3154	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → ∀𝑥 ∈ 𝑧 (𝐹‘∩ 𝑧) ⊆ 𝑥)
66		ssint 4924	. . . . 5 ⊢ ((𝐹‘∩ 𝑧) ⊆ ∩ 𝑧 ↔ ∀𝑥 ∈ 𝑧 (𝐹‘∩ 𝑧) ⊆ 𝑥)
67	65, 66	sylibr 237	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → (𝐹‘∩ 𝑧) ⊆ ∩ 𝑧)
68	16	3ad2ant1 1151	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → ∀𝑥 ∈ 𝒫 𝐵𝑥 ⊆ (𝐹‘𝑥))
69		id 23	. . . . . . 7 ⊢ (𝑥 = ∩ 𝑧 → 𝑥 = ∩ 𝑧)
70		fveq2 6879	. . . . . . 7 ⊢ (𝑥 = ∩ 𝑧 → (𝐹‘𝑥) = (𝐹‘∩ 𝑧))
71	69, 70	sseq12d 3964	. . . . . 6 ⊢ (𝑥 = ∩ 𝑧 → (𝑥 ⊆ (𝐹‘𝑥) ↔ ∩ 𝑧 ⊆ (𝐹‘∩ 𝑧)))
72	71	rspcva 3574	. . . . 5 ⊢ ((∩ 𝑧 ∈ 𝒫 𝐵 ∧ ∀𝑥 ∈ 𝒫 𝐵𝑥 ⊆ (𝐹‘𝑥)) → ∩ 𝑧 ⊆ (𝐹‘∩ 𝑧))
73	39, 68, 72	syl2anc 596	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → ∩ 𝑧 ⊆ (𝐹‘∩ 𝑧))
74	67, 73	eqssd 3948	. . 3 ⊢ ((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → (𝐹‘∩ 𝑧) = ∩ 𝑧)
75		fnelfp 7174	. . . 4 ⊢ ((𝐹 Fn 𝒫 𝐵 ∧ ∩ 𝑧 ∈ 𝒫 𝐵) → (∩ 𝑧 ∈ dom (𝐹 ∩ I ) ↔ (𝐹‘∩ 𝑧) = ∩ 𝑧))
76	59, 39, 75	syl2anc 596	. . 3 ⊢ ((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → (∩ 𝑧 ∈ dom (𝐹 ∩ I ) ↔ (𝐹‘∩ 𝑧) = ∩ 𝑧))
77	74, 76	mpbird 260	. 2 ⊢ ((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → ∩ 𝑧 ∈ dom (𝐹 ∩ I ))
78	5, 26, 77	ismred 17687	1 ⊢ (𝜑 → dom (𝐹 ∩ I ) ∈ (Moore‘𝐵))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∧ w3a 1103  ∀wal 1568   = wceq 1570   ∈ wcel 2145   ≠ wne 2955  ∀wral 3076  Vcvv 3450   ∩ cin 3898   ⊆ wss 3899  ∅c0 4279  𝒫 cpw 4557  ∪ cuni 4867  ∩ cint 4907   I cid 5549  dom cdm 5655   Fn wfn 6528  ⟶wf 6529  ‘cfv 6533  Moorecmre 17667

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-sep 5251  ax-nul 5263  ax-pow 5330  ax-pr 5398

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-int 4908  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-iota 6489  df-fun 6535  df-fn 6536  df-f 6537  df-fv 6541  df-mre 17671

This theorem is used by:  ismrcd2  43545  istopclsd  43546  ismrc  43547