ismrc

Description: A function is a Moore closure operator iff it satisfies mrcssid , mrcss , and mrcidm . (Contributed by Stefan O'Rear, 1-Feb-2015)

		Ref	Expression
	Assertion	ismrc	$⊢ F \in mrCls [Moore (B)] \leftrightarrow (B \in V \land F : 𝒫 B ⟶ 𝒫 B \land \forall x \forall y ((x \subseteq B \land y \subseteq x) \to (x \subseteq F (x) \land F (y) \subseteq F (x) \land F (F (x)) = F (x))))$

Proof

Step	Hyp	Ref	Expression
1		fnmrc	$⊢ mrCls Fn ⋃ ran Moore$
2		fnfun	$⊢ mrCls Fn ⋃ ran Moore \to Fun mrCls$
3	1 2	ax-mp	$⊢ Fun mrCls$
4		fvelima	$⊢ (Fun mrCls \land F \in mrCls [Moore (B)]) \to \exists z \in Moore (B) mrCls (z) = F$
5	3 4	mpan	$⊢ F \in mrCls [Moore (B)] \to \exists z \in Moore (B) mrCls (z) = F$
6		elfvex	$⊢ z \in Moore (B) \to B \in V$
7		eqid	$⊢ mrCls (z) = mrCls (z)$
8	7	mrcf	$⊢ z \in Moore (B) \to mrCls (z) : 𝒫 B ⟶ z$
9		mresspw	$⊢ z \in Moore (B) \to z \subseteq 𝒫 B$
10	8 9	fssd	$⊢ z \in Moore (B) \to mrCls (z) : 𝒫 B ⟶ 𝒫 B$
11	7	mrcssid	$⊢ (z \in Moore (B) \land x \subseteq B) \to x \subseteq mrCls (z) (x)$
12	11	adantrr	$⊢ (z \in Moore (B) \land (x \subseteq B \land y \subseteq x)) \to x \subseteq mrCls (z) (x)$
13	7	mrcss	$⊢ (z \in Moore (B) \land y \subseteq x \land x \subseteq B) \to mrCls (z) (y) \subseteq mrCls (z) (x)$
14	13	3expb	$⊢ (z \in Moore (B) \land (y \subseteq x \land x \subseteq B)) \to mrCls (z) (y) \subseteq mrCls (z) (x)$
15	14	ancom2s	$⊢ (z \in Moore (B) \land (x \subseteq B \land y \subseteq x)) \to mrCls (z) (y) \subseteq mrCls (z) (x)$
16	7	mrcidm	$⊢ (z \in Moore (B) \land x \subseteq B) \to mrCls (z) (mrCls (z) (x)) = mrCls (z) (x)$
17	16	adantrr	$⊢ (z \in Moore (B) \land (x \subseteq B \land y \subseteq x)) \to mrCls (z) (mrCls (z) (x)) = mrCls (z) (x)$
18	12 15 17	3jca	$⊢ (z \in Moore (B) \land (x \subseteq B \land y \subseteq x)) \to (x \subseteq mrCls (z) (x) \land mrCls (z) (y) \subseteq mrCls (z) (x) \land mrCls (z) (mrCls (z) (x)) = mrCls (z) (x))$
19	18	ex	$⊢ z \in Moore (B) \to ((x \subseteq B \land y \subseteq x) \to (x \subseteq mrCls (z) (x) \land mrCls (z) (y) \subseteq mrCls (z) (x) \land mrCls (z) (mrCls (z) (x)) = mrCls (z) (x)))$
20	19	alrimivv	$⊢ z \in Moore (B) \to \forall x \forall y ((x \subseteq B \land y \subseteq x) \to (x \subseteq mrCls (z) (x) \land mrCls (z) (y) \subseteq mrCls (z) (x) \land mrCls (z) (mrCls (z) (x)) = mrCls (z) (x)))$
21	6 10 20	3jca	$⊢ z \in Moore (B) \to (B \in V \land mrCls (z) : 𝒫 B ⟶ 𝒫 B \land \forall x \forall y ((x \subseteq B \land y \subseteq x) \to (x \subseteq mrCls (z) (x) \land mrCls (z) (y) \subseteq mrCls (z) (x) \land mrCls (z) (mrCls (z) (x)) = mrCls (z) (x))))$
22		feq1	$⊢ mrCls (z) = F \to (mrCls (z) : 𝒫 B ⟶ 𝒫 B \leftrightarrow F : 𝒫 B ⟶ 𝒫 B)$
23		fveq1	$⊢ mrCls (z) = F \to mrCls (z) (x) = F (x)$
24	23	sseq2d	$⊢ mrCls (z) = F \to (x \subseteq mrCls (z) (x) \leftrightarrow x \subseteq F (x))$
25		fveq1	$⊢ mrCls (z) = F \to mrCls (z) (y) = F (y)$
26	25 23	sseq12d	$⊢ mrCls (z) = F \to (mrCls (z) (y) \subseteq mrCls (z) (x) \leftrightarrow F (y) \subseteq F (x))$
27		id	$⊢ mrCls (z) = F \to mrCls (z) = F$
28	27 23	fveq12d	$⊢ mrCls (z) = F \to mrCls (z) (mrCls (z) (x)) = F (F (x))$
29	28 23	eqeq12d	$⊢ mrCls (z) = F \to (mrCls (z) (mrCls (z) (x)) = mrCls (z) (x) \leftrightarrow F (F (x)) = F (x))$
30	24 26 29	3anbi123d	$⊢ mrCls (z) = F \to ((x \subseteq mrCls (z) (x) \land mrCls (z) (y) \subseteq mrCls (z) (x) \land mrCls (z) (mrCls (z) (x)) = mrCls (z) (x)) \leftrightarrow (x \subseteq F (x) \land F (y) \subseteq F (x) \land F (F (x)) = F (x)))$
31	30	imbi2d	$⊢ mrCls (z) = F \to (((x \subseteq B \land y \subseteq x) \to (x \subseteq mrCls (z) (x) \land mrCls (z) (y) \subseteq mrCls (z) (x) \land mrCls (z) (mrCls (z) (x)) = mrCls (z) (x))) \leftrightarrow ((x \subseteq B \land y \subseteq x) \to (x \subseteq F (x) \land F (y) \subseteq F (x) \land F (F (x)) = F (x))))$
32	31	2albidv	$⊢ mrCls (z) = F \to (\forall x \forall y ((x \subseteq B \land y \subseteq x) \to (x \subseteq mrCls (z) (x) \land mrCls (z) (y) \subseteq mrCls (z) (x) \land mrCls (z) (mrCls (z) (x)) = mrCls (z) (x))) \leftrightarrow \forall x \forall y ((x \subseteq B \land y \subseteq x) \to (x \subseteq F (x) \land F (y) \subseteq F (x) \land F (F (x)) = F (x))))$
33	22 32	3anbi23d	$⊢ mrCls (z) = F \to ((B \in V \land mrCls (z) : 𝒫 B ⟶ 𝒫 B \land \forall x \forall y ((x \subseteq B \land y \subseteq x) \to (x \subseteq mrCls (z) (x) \land mrCls (z) (y) \subseteq mrCls (z) (x) \land mrCls (z) (mrCls (z) (x)) = mrCls (z) (x)))) \leftrightarrow (B \in V \land F : 𝒫 B ⟶ 𝒫 B \land \forall x \forall y ((x \subseteq B \land y \subseteq x) \to (x \subseteq F (x) \land F (y) \subseteq F (x) \land F (F (x)) = F (x)))))$
34	21 33	syl5ibcom	$⊢ z \in Moore (B) \to (mrCls (z) = F \to (B \in V \land F : 𝒫 B ⟶ 𝒫 B \land \forall x \forall y ((x \subseteq B \land y \subseteq x) \to (x \subseteq F (x) \land F (y) \subseteq F (x) \land F (F (x)) = F (x)))))$
35	34	rexlimiv	$⊢ \exists z \in Moore (B) mrCls (z) = F \to (B \in V \land F : 𝒫 B ⟶ 𝒫 B \land \forall x \forall y ((x \subseteq B \land y \subseteq x) \to (x \subseteq F (x) \land F (y) \subseteq F (x) \land F (F (x)) = F (x))))$
36	5 35	syl	$⊢ F \in mrCls [Moore (B)] \to (B \in V \land F : 𝒫 B ⟶ 𝒫 B \land \forall x \forall y ((x \subseteq B \land y \subseteq x) \to (x \subseteq F (x) \land F (y) \subseteq F (x) \land F (F (x)) = F (x))))$
37		simp1	$⊢ (B \in V \land F : 𝒫 B ⟶ 𝒫 B \land \forall x \forall y ((x \subseteq B \land y \subseteq x) \to (x \subseteq F (x) \land F (y) \subseteq F (x) \land F (F (x)) = F (x)))) \to B \in V$
38		simp2	$⊢ (B \in V \land F : 𝒫 B ⟶ 𝒫 B \land \forall x \forall y ((x \subseteq B \land y \subseteq x) \to (x \subseteq F (x) \land F (y) \subseteq F (x) \land F (F (x)) = F (x)))) \to F : 𝒫 B ⟶ 𝒫 B$
39		ssid	$⊢ z \subseteq z$
40		3simpb	$⊢ (x \subseteq F (x) \land F (y) \subseteq F (x) \land F (F (x)) = F (x)) \to (x \subseteq F (x) \land F (F (x)) = F (x))$
41	40	imim2i	$⊢ ((x \subseteq B \land y \subseteq x) \to (x \subseteq F (x) \land F (y) \subseteq F (x) \land F (F (x)) = F (x))) \to ((x \subseteq B \land y \subseteq x) \to (x \subseteq F (x) \land F (F (x)) = F (x)))$
42	41	2alimi	$⊢ \forall x \forall y ((x \subseteq B \land y \subseteq x) \to (x \subseteq F (x) \land F (y) \subseteq F (x) \land F (F (x)) = F (x))) \to \forall x \forall y ((x \subseteq B \land y \subseteq x) \to (x \subseteq F (x) \land F (F (x)) = F (x)))$
43		sseq1	$⊢ x = z \to (x \subseteq B \leftrightarrow z \subseteq B)$
44	43	adantr	$⊢ (x = z \land y = z) \to (x \subseteq B \leftrightarrow z \subseteq B)$
45		sseq12	$⊢ (y = z \land x = z) \to (y \subseteq x \leftrightarrow z \subseteq z)$
46	45	ancoms	$⊢ (x = z \land y = z) \to (y \subseteq x \leftrightarrow z \subseteq z)$
47	44 46	anbi12d	$⊢ (x = z \land y = z) \to ((x \subseteq B \land y \subseteq x) \leftrightarrow (z \subseteq B \land z \subseteq z))$
48		id	$⊢ x = z \to x = z$
49		fveq2	$⊢ x = z \to F (x) = F (z)$
50	48 49	sseq12d	$⊢ x = z \to (x \subseteq F (x) \leftrightarrow z \subseteq F (z))$
51	50	adantr	$⊢ (x = z \land y = z) \to (x \subseteq F (x) \leftrightarrow z \subseteq F (z))$
52		2fveq3	$⊢ x = z \to F (F (x)) = F (F (z))$
53	52 49	eqeq12d	$⊢ x = z \to (F (F (x)) = F (x) \leftrightarrow F (F (z)) = F (z))$
54	53	adantr	$⊢ (x = z \land y = z) \to (F (F (x)) = F (x) \leftrightarrow F (F (z)) = F (z))$
55	51 54	anbi12d	$⊢ (x = z \land y = z) \to ((x \subseteq F (x) \land F (F (x)) = F (x)) \leftrightarrow (z \subseteq F (z) \land F (F (z)) = F (z)))$
56	47 55	imbi12d	$⊢ (x = z \land y = z) \to (((x \subseteq B \land y \subseteq x) \to (x \subseteq F (x) \land F (F (x)) = F (x))) \leftrightarrow ((z \subseteq B \land z \subseteq z) \to (z \subseteq F (z) \land F (F (z)) = F (z))))$
57	56	spc2gv	$⊢ (z \in V \land z \in V) \to (\forall x \forall y ((x \subseteq B \land y \subseteq x) \to (x \subseteq F (x) \land F (F (x)) = F (x))) \to ((z \subseteq B \land z \subseteq z) \to (z \subseteq F (z) \land F (F (z)) = F (z))))$
58	57	el2v	$⊢ \forall x \forall y ((x \subseteq B \land y \subseteq x) \to (x \subseteq F (x) \land F (F (x)) = F (x))) \to ((z \subseteq B \land z \subseteq z) \to (z \subseteq F (z) \land F (F (z)) = F (z)))$
59	42 58	syl	$⊢ \forall x \forall y ((x \subseteq B \land y \subseteq x) \to (x \subseteq F (x) \land F (y) \subseteq F (x) \land F (F (x)) = F (x))) \to ((z \subseteq B \land z \subseteq z) \to (z \subseteq F (z) \land F (F (z)) = F (z)))$
60	59	3ad2ant3	$⊢ (B \in V \land F : 𝒫 B ⟶ 𝒫 B \land \forall x \forall y ((x \subseteq B \land y \subseteq x) \to (x \subseteq F (x) \land F (y) \subseteq F (x) \land F (F (x)) = F (x)))) \to ((z \subseteq B \land z \subseteq z) \to (z \subseteq F (z) \land F (F (z)) = F (z)))$
61	39 60	mpan2i	$⊢ (B \in V \land F : 𝒫 B ⟶ 𝒫 B \land \forall x \forall y ((x \subseteq B \land y \subseteq x) \to (x \subseteq F (x) \land F (y) \subseteq F (x) \land F (F (x)) = F (x)))) \to (z \subseteq B \to (z \subseteq F (z) \land F (F (z)) = F (z)))$
62	61	imp	$⊢ ((B \in V \land F : 𝒫 B ⟶ 𝒫 B \land \forall x \forall y ((x \subseteq B \land y \subseteq x) \to (x \subseteq F (x) \land F (y) \subseteq F (x) \land F (F (x)) = F (x)))) \land z \subseteq B) \to (z \subseteq F (z) \land F (F (z)) = F (z))$
63	62	simpld	$⊢ ((B \in V \land F : 𝒫 B ⟶ 𝒫 B \land \forall x \forall y ((x \subseteq B \land y \subseteq x) \to (x \subseteq F (x) \land F (y) \subseteq F (x) \land F (F (x)) = F (x)))) \land z \subseteq B) \to z \subseteq F (z)$
64		simp2	$⊢ (x \subseteq F (x) \land F (y) \subseteq F (x) \land F (F (x)) = F (x)) \to F (y) \subseteq F (x)$
65	64	imim2i	$⊢ ((x \subseteq B \land y \subseteq x) \to (x \subseteq F (x) \land F (y) \subseteq F (x) \land F (F (x)) = F (x))) \to ((x \subseteq B \land y \subseteq x) \to F (y) \subseteq F (x))$
66	65	2alimi	$⊢ \forall x \forall y ((x \subseteq B \land y \subseteq x) \to (x \subseteq F (x) \land F (y) \subseteq F (x) \land F (F (x)) = F (x))) \to \forall x \forall y ((x \subseteq B \land y \subseteq x) \to F (y) \subseteq F (x))$
67	66	3ad2ant3	$⊢ (B \in V \land F : 𝒫 B ⟶ 𝒫 B \land \forall x \forall y ((x \subseteq B \land y \subseteq x) \to (x \subseteq F (x) \land F (y) \subseteq F (x) \land F (F (x)) = F (x)))) \to \forall x \forall y ((x \subseteq B \land y \subseteq x) \to F (y) \subseteq F (x))$
68	43	adantr	$⊢ (x = z \land y = w) \to (x \subseteq B \leftrightarrow z \subseteq B)$
69		sseq12	$⊢ (y = w \land x = z) \to (y \subseteq x \leftrightarrow w \subseteq z)$
70	69	ancoms	$⊢ (x = z \land y = w) \to (y \subseteq x \leftrightarrow w \subseteq z)$
71	68 70	anbi12d	$⊢ (x = z \land y = w) \to ((x \subseteq B \land y \subseteq x) \leftrightarrow (z \subseteq B \land w \subseteq z))$
72		fveq2	$⊢ y = w \to F (y) = F (w)$
73		sseq12	$⊢ (F (y) = F (w) \land F (x) = F (z)) \to (F (y) \subseteq F (x) \leftrightarrow F (w) \subseteq F (z))$
74	72 49 73	syl2anr	$⊢ (x = z \land y = w) \to (F (y) \subseteq F (x) \leftrightarrow F (w) \subseteq F (z))$
75	71 74	imbi12d	$⊢ (x = z \land y = w) \to (((x \subseteq B \land y \subseteq x) \to F (y) \subseteq F (x)) \leftrightarrow ((z \subseteq B \land w \subseteq z) \to F (w) \subseteq F (z)))$
76	75	spc2gv	$⊢ (z \in V \land w \in V) \to (\forall x \forall y ((x \subseteq B \land y \subseteq x) \to F (y) \subseteq F (x)) \to ((z \subseteq B \land w \subseteq z) \to F (w) \subseteq F (z)))$
77	76	el2v	$⊢ \forall x \forall y ((x \subseteq B \land y \subseteq x) \to F (y) \subseteq F (x)) \to ((z \subseteq B \land w \subseteq z) \to F (w) \subseteq F (z))$
78	67 77	syl	$⊢ (B \in V \land F : 𝒫 B ⟶ 𝒫 B \land \forall x \forall y ((x \subseteq B \land y \subseteq x) \to (x \subseteq F (x) \land F (y) \subseteq F (x) \land F (F (x)) = F (x)))) \to ((z \subseteq B \land w \subseteq z) \to F (w) \subseteq F (z))$
79	78	3impib	$⊢ ((B \in V \land F : 𝒫 B ⟶ 𝒫 B \land \forall x \forall y ((x \subseteq B \land y \subseteq x) \to (x \subseteq F (x) \land F (y) \subseteq F (x) \land F (F (x)) = F (x)))) \land z \subseteq B \land w \subseteq z) \to F (w) \subseteq F (z)$
80	62	simprd	$⊢ ((B \in V \land F : 𝒫 B ⟶ 𝒫 B \land \forall x \forall y ((x \subseteq B \land y \subseteq x) \to (x \subseteq F (x) \land F (y) \subseteq F (x) \land F (F (x)) = F (x)))) \land z \subseteq B) \to F (F (z)) = F (z)$
81	37 38 63 79 80	ismrcd2	$⊢ (B \in V \land F : 𝒫 B ⟶ 𝒫 B \land \forall x \forall y ((x \subseteq B \land y \subseteq x) \to (x \subseteq F (x) \land F (y) \subseteq F (x) \land F (F (x)) = F (x)))) \to F = mrCls (dom (F \cap I))$
82	37 38 63 79 80	ismrcd1	$⊢ (B \in V \land F : 𝒫 B ⟶ 𝒫 B \land \forall x \forall y ((x \subseteq B \land y \subseteq x) \to (x \subseteq F (x) \land F (y) \subseteq F (x) \land F (F (x)) = F (x)))) \to dom (F \cap I) \in Moore (B)$
83		fvssunirn	$⊢ Moore (B) \subseteq ⋃ ran Moore$
84	1	fndmi	$⊢ dom mrCls = ⋃ ran Moore$
85	83 84	sseqtrri	$⊢ Moore (B) \subseteq dom mrCls$
86		funfvima2	$⊢ (Fun mrCls \land Moore (B) \subseteq dom mrCls) \to (dom (F \cap I) \in Moore (B) \to mrCls (dom (F \cap I)) \in mrCls [Moore (B)])$
87	3 85 86	mp2an	$⊢ dom (F \cap I) \in Moore (B) \to mrCls (dom (F \cap I)) \in mrCls [Moore (B)]$
88	82 87	syl	$⊢ (B \in V \land F : 𝒫 B ⟶ 𝒫 B \land \forall x \forall y ((x \subseteq B \land y \subseteq x) \to (x \subseteq F (x) \land F (y) \subseteq F (x) \land F (F (x)) = F (x)))) \to mrCls (dom (F \cap I)) \in mrCls [Moore (B)]$
89	81 88	eqeltrd	$⊢ (B \in V \land F : 𝒫 B ⟶ 𝒫 B \land \forall x \forall y ((x \subseteq B \land y \subseteq x) \to (x \subseteq F (x) \land F (y) \subseteq F (x) \land F (F (x)) = F (x)))) \to F \in mrCls [Moore (B)]$
90	36 89	impbii	$⊢ F \in mrCls [Moore (B)] \leftrightarrow (B \in V \land F : 𝒫 B ⟶ 𝒫 B \land \forall x \forall y ((x \subseteq B \land y \subseteq x) \to (x \subseteq F (x) \land F (y) \subseteq F (x) \land F (F (x)) = F (x))))$

Metamath Proof Explorer

Theorem ismrc

Proof