mrcuni

Description: Idempotence of closure under a general union. (Contributed by Stefan O'Rear, 31-Jan-2015)

		Ref	Expression
	Hypothesis	mrcfval.f	$⊢ F = mrCls (C)$
	Assertion	mrcuni	$⊢ (C \in Moore (X) \land U \subseteq 𝒫 X) \to F (⋃ U) = F (⋃ F [U])$

Proof

Step	Hyp	Ref	Expression
1		mrcfval.f	$⊢ F = mrCls (C)$
2		simpl	$⊢ (C \in Moore (X) \land U \subseteq 𝒫 X) \to C \in Moore (X)$
3		simpll	$⊢ ((C \in Moore (X) \land U \subseteq 𝒫 X) \land s \in U) \to C \in Moore (X)$
4		ssel2	$⊢ (U \subseteq 𝒫 X \land s \in U) \to s \in 𝒫 X$
5	4	elpwid	$⊢ (U \subseteq 𝒫 X \land s \in U) \to s \subseteq X$
6	5	adantll	$⊢ ((C \in Moore (X) \land U \subseteq 𝒫 X) \land s \in U) \to s \subseteq X$
7	1	mrcssid	$⊢ (C \in Moore (X) \land s \subseteq X) \to s \subseteq F (s)$
8	3 6 7	syl2anc	$⊢ ((C \in Moore (X) \land U \subseteq 𝒫 X) \land s \in U) \to s \subseteq F (s)$
9	1	mrcf	$⊢ C \in Moore (X) \to F : 𝒫 X ⟶ C$
10	9	ffund	$⊢ C \in Moore (X) \to Fun F$
11	10	adantr	$⊢ (C \in Moore (X) \land U \subseteq 𝒫 X) \to Fun F$
12	9	fdmd	$⊢ C \in Moore (X) \to dom F = 𝒫 X$
13	12	sseq2d	$⊢ C \in Moore (X) \to (U \subseteq dom F \leftrightarrow U \subseteq 𝒫 X)$
14	13	biimpar	$⊢ (C \in Moore (X) \land U \subseteq 𝒫 X) \to U \subseteq dom F$
15		funfvima2	$⊢ (Fun F \land U \subseteq dom F) \to (s \in U \to F (s) \in F [U])$
16	11 14 15	syl2anc	$⊢ (C \in Moore (X) \land U \subseteq 𝒫 X) \to (s \in U \to F (s) \in F [U])$
17	16	imp	$⊢ ((C \in Moore (X) \land U \subseteq 𝒫 X) \land s \in U) \to F (s) \in F [U]$
18		elssuni	$⊢ F (s) \in F [U] \to F (s) \subseteq ⋃ F [U]$
19	17 18	syl	$⊢ ((C \in Moore (X) \land U \subseteq 𝒫 X) \land s \in U) \to F (s) \subseteq ⋃ F [U]$
20	8 19	sstrd	$⊢ ((C \in Moore (X) \land U \subseteq 𝒫 X) \land s \in U) \to s \subseteq ⋃ F [U]$
21	20	ralrimiva	$⊢ (C \in Moore (X) \land U \subseteq 𝒫 X) \to \forall s \in U s \subseteq ⋃ F [U]$
22		unissb	$⊢ ⋃ U \subseteq ⋃ F [U] \leftrightarrow \forall s \in U s \subseteq ⋃ F [U]$
23	21 22	sylibr	$⊢ (C \in Moore (X) \land U \subseteq 𝒫 X) \to ⋃ U \subseteq ⋃ F [U]$
24	1	mrcssv	$⊢ C \in Moore (X) \to F (x) \subseteq X$
25	24	adantr	$⊢ (C \in Moore (X) \land U \subseteq 𝒫 X) \to F (x) \subseteq X$
26	25	ralrimivw	$⊢ (C \in Moore (X) \land U \subseteq 𝒫 X) \to \forall x \in U F (x) \subseteq X$
27	9	ffnd	$⊢ C \in Moore (X) \to F Fn 𝒫 X$
28		sseq1	$⊢ s = F (x) \to (s \subseteq X \leftrightarrow F (x) \subseteq X)$
29	28	ralima	$⊢ (F Fn 𝒫 X \land U \subseteq 𝒫 X) \to (\forall s \in F [U] s \subseteq X \leftrightarrow \forall x \in U F (x) \subseteq X)$
30	27 29	sylan	$⊢ (C \in Moore (X) \land U \subseteq 𝒫 X) \to (\forall s \in F [U] s \subseteq X \leftrightarrow \forall x \in U F (x) \subseteq X)$
31	26 30	mpbird	$⊢ (C \in Moore (X) \land U \subseteq 𝒫 X) \to \forall s \in F [U] s \subseteq X$
32		unissb	$⊢ ⋃ F [U] \subseteq X \leftrightarrow \forall s \in F [U] s \subseteq X$
33	31 32	sylibr	$⊢ (C \in Moore (X) \land U \subseteq 𝒫 X) \to ⋃ F [U] \subseteq X$
34	1	mrcss	$⊢ (C \in Moore (X) \land ⋃ U \subseteq ⋃ F [U] \land ⋃ F [U] \subseteq X) \to F (⋃ U) \subseteq F (⋃ F [U])$
35	2 23 33 34	syl3anc	$⊢ (C \in Moore (X) \land U \subseteq 𝒫 X) \to F (⋃ U) \subseteq F (⋃ F [U])$
36		simpll	$⊢ ((C \in Moore (X) \land U \subseteq 𝒫 X) \land x \in U) \to C \in Moore (X)$
37		elssuni	$⊢ x \in U \to x \subseteq ⋃ U$
38	37	adantl	$⊢ ((C \in Moore (X) \land U \subseteq 𝒫 X) \land x \in U) \to x \subseteq ⋃ U$
39		sspwuni	$⊢ U \subseteq 𝒫 X \leftrightarrow ⋃ U \subseteq X$
40	39	bilani	$⊢ (C \in Moore (X) \land U \subseteq 𝒫 X) \to ⋃ U \subseteq X$
41	40	adantr	$⊢ ((C \in Moore (X) \land U \subseteq 𝒫 X) \land x \in U) \to ⋃ U \subseteq X$
42	1	mrcss	$⊢ (C \in Moore (X) \land x \subseteq ⋃ U \land ⋃ U \subseteq X) \to F (x) \subseteq F (⋃ U)$
43	36 38 41 42	syl3anc	$⊢ ((C \in Moore (X) \land U \subseteq 𝒫 X) \land x \in U) \to F (x) \subseteq F (⋃ U)$
44	43	ralrimiva	$⊢ (C \in Moore (X) \land U \subseteq 𝒫 X) \to \forall x \in U F (x) \subseteq F (⋃ U)$
45		sseq1	$⊢ s = F (x) \to (s \subseteq F (⋃ U) \leftrightarrow F (x) \subseteq F (⋃ U))$
46	45	ralima	$⊢ (F Fn 𝒫 X \land U \subseteq 𝒫 X) \to (\forall s \in F [U] s \subseteq F (⋃ U) \leftrightarrow \forall x \in U F (x) \subseteq F (⋃ U))$
47	27 46	sylan	$⊢ (C \in Moore (X) \land U \subseteq 𝒫 X) \to (\forall s \in F [U] s \subseteq F (⋃ U) \leftrightarrow \forall x \in U F (x) \subseteq F (⋃ U))$
48	44 47	mpbird	$⊢ (C \in Moore (X) \land U \subseteq 𝒫 X) \to \forall s \in F [U] s \subseteq F (⋃ U)$
49		unissb	$⊢ ⋃ F [U] \subseteq F (⋃ U) \leftrightarrow \forall s \in F [U] s \subseteq F (⋃ U)$
50	48 49	sylibr	$⊢ (C \in Moore (X) \land U \subseteq 𝒫 X) \to ⋃ F [U] \subseteq F (⋃ U)$
51	1	mrcssv	$⊢ C \in Moore (X) \to F (⋃ U) \subseteq X$
52	51	adantr	$⊢ (C \in Moore (X) \land U \subseteq 𝒫 X) \to F (⋃ U) \subseteq X$
53	1	mrcss	$⊢ (C \in Moore (X) \land ⋃ F [U] \subseteq F (⋃ U) \land F (⋃ U) \subseteq X) \to F (⋃ F [U]) \subseteq F (F (⋃ U))$
54	2 50 52 53	syl3anc	$⊢ (C \in Moore (X) \land U \subseteq 𝒫 X) \to F (⋃ F [U]) \subseteq F (F (⋃ U))$
55	1	mrcidm	$⊢ (C \in Moore (X) \land ⋃ U \subseteq X) \to F (F (⋃ U)) = F (⋃ U)$
56	2 40 55	syl2anc	$⊢ (C \in Moore (X) \land U \subseteq 𝒫 X) \to F (F (⋃ U)) = F (⋃ U)$
57	54 56	sseqtrd	$⊢ (C \in Moore (X) \land U \subseteq 𝒫 X) \to F (⋃ F [U]) \subseteq F (⋃ U)$
58	35 57	eqssd	$⊢ (C \in Moore (X) \land U \subseteq 𝒫 X) \to F (⋃ U) = F (⋃ F [U])$

Metamath Proof Explorer

Theorem mrcuni

Proof