ismrcd2

Description: Second half of ismrcd1 . (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	ismrcd2	$⊢ φ \to F = mrCls (dom (F \cap I))$

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	2	ffnd	$⊢ φ \to F Fn 𝒫 B$
7	1 2 3 4 5	ismrcd1	$⊢ φ \to dom (F \cap I) \in Moore (B)$
8		eqid	$⊢ mrCls (dom (F \cap I)) = mrCls (dom (F \cap I))$
9	8	mrcf	$⊢ dom (F \cap I) \in Moore (B) \to mrCls (dom (F \cap I)) : 𝒫 B ⟶ dom (F \cap I)$
10		ffn	$⊢ mrCls (dom (F \cap I)) : 𝒫 B ⟶ dom (F \cap I) \to mrCls (dom (F \cap I)) Fn 𝒫 B$
11	7 9 10	3syl	$⊢ φ \to mrCls (dom (F \cap I)) Fn 𝒫 B$
12	7 8	mrcssvd	$⊢ φ \to mrCls (dom (F \cap I)) (z) \subseteq B$
13	12	adantr	$⊢ (φ \land z \in 𝒫 B) \to mrCls (dom (F \cap I)) (z) \subseteq B$
14		elpwi	$⊢ z \in 𝒫 B \to z \subseteq B$
15	8	mrcssid	$⊢ (dom (F \cap I) \in Moore (B) \land z \subseteq B) \to z \subseteq mrCls (dom (F \cap I)) (z)$
16	7 14 15	syl2an	$⊢ (φ \land z \in 𝒫 B) \to z \subseteq mrCls (dom (F \cap I)) (z)$
17	4	3expib	$⊢ φ \to ((x \subseteq B \land y \subseteq x) \to F (y) \subseteq F (x))$
18	17	alrimivv	$⊢ φ \to \forall y \forall x ((x \subseteq B \land y \subseteq x) \to F (y) \subseteq F (x))$
19		vex	$⊢ z \in V$
20		fvex	$⊢ mrCls (dom (F \cap I)) (z) \in V$
21		sseq1	$⊢ x = mrCls (dom (F \cap I)) (z) \to (x \subseteq B \leftrightarrow mrCls (dom (F \cap I)) (z) \subseteq B)$
22	21	adantl	$⊢ (y = z \land x = mrCls (dom (F \cap I)) (z)) \to (x \subseteq B \leftrightarrow mrCls (dom (F \cap I)) (z) \subseteq B)$
23		sseq12	$⊢ (y = z \land x = mrCls (dom (F \cap I)) (z)) \to (y \subseteq x \leftrightarrow z \subseteq mrCls (dom (F \cap I)) (z))$
24	22 23	anbi12d	$⊢ (y = z \land x = mrCls (dom (F \cap I)) (z)) \to ((x \subseteq B \land y \subseteq x) \leftrightarrow (mrCls (dom (F \cap I)) (z) \subseteq B \land z \subseteq mrCls (dom (F \cap I)) (z)))$
25		fveq2	$⊢ y = z \to F (y) = F (z)$
26		fveq2	$⊢ x = mrCls (dom (F \cap I)) (z) \to F (x) = F (mrCls (dom (F \cap I)) (z))$
27		sseq12	$⊢ (F (y) = F (z) \land F (x) = F (mrCls (dom (F \cap I)) (z))) \to (F (y) \subseteq F (x) \leftrightarrow F (z) \subseteq F (mrCls (dom (F \cap I)) (z)))$
28	25 26 27	syl2an	$⊢ (y = z \land x = mrCls (dom (F \cap I)) (z)) \to (F (y) \subseteq F (x) \leftrightarrow F (z) \subseteq F (mrCls (dom (F \cap I)) (z)))$
29	24 28	imbi12d	$⊢ (y = z \land x = mrCls (dom (F \cap I)) (z)) \to (((x \subseteq B \land y \subseteq x) \to F (y) \subseteq F (x)) \leftrightarrow ((mrCls (dom (F \cap I)) (z) \subseteq B \land z \subseteq mrCls (dom (F \cap I)) (z)) \to F (z) \subseteq F (mrCls (dom (F \cap I)) (z))))$
30	29	spc2gv	$⊢ (z \in V \land mrCls (dom (F \cap I)) (z) \in V) \to (\forall y \forall x ((x \subseteq B \land y \subseteq x) \to F (y) \subseteq F (x)) \to ((mrCls (dom (F \cap I)) (z) \subseteq B \land z \subseteq mrCls (dom (F \cap I)) (z)) \to F (z) \subseteq F (mrCls (dom (F \cap I)) (z))))$
31	19 20 30	mp2an	$⊢ \forall y \forall x ((x \subseteq B \land y \subseteq x) \to F (y) \subseteq F (x)) \to ((mrCls (dom (F \cap I)) (z) \subseteq B \land z \subseteq mrCls (dom (F \cap I)) (z)) \to F (z) \subseteq F (mrCls (dom (F \cap I)) (z)))$
32	18 31	syl	$⊢ φ \to ((mrCls (dom (F \cap I)) (z) \subseteq B \land z \subseteq mrCls (dom (F \cap I)) (z)) \to F (z) \subseteq F (mrCls (dom (F \cap I)) (z)))$
33	32	adantr	$⊢ (φ \land z \in 𝒫 B) \to ((mrCls (dom (F \cap I)) (z) \subseteq B \land z \subseteq mrCls (dom (F \cap I)) (z)) \to F (z) \subseteq F (mrCls (dom (F \cap I)) (z)))$
34	13 16 33	mp2and	$⊢ (φ \land z \in 𝒫 B) \to F (z) \subseteq F (mrCls (dom (F \cap I)) (z))$
35	8	mrccl	$⊢ (dom (F \cap I) \in Moore (B) \land z \subseteq B) \to mrCls (dom (F \cap I)) (z) \in dom (F \cap I)$
36	7 14 35	syl2an	$⊢ (φ \land z \in 𝒫 B) \to mrCls (dom (F \cap I)) (z) \in dom (F \cap I)$
37	6	adantr	$⊢ (φ \land z \in 𝒫 B) \to F Fn 𝒫 B$
38	20	elpw	$⊢ mrCls (dom (F \cap I)) (z) \in 𝒫 B \leftrightarrow mrCls (dom (F \cap I)) (z) \subseteq B$
39	12 38	sylibr	$⊢ φ \to mrCls (dom (F \cap I)) (z) \in 𝒫 B$
40	39	adantr	$⊢ (φ \land z \in 𝒫 B) \to mrCls (dom (F \cap I)) (z) \in 𝒫 B$
41		fnelfp	$⊢ (F Fn 𝒫 B \land mrCls (dom (F \cap I)) (z) \in 𝒫 B) \to (mrCls (dom (F \cap I)) (z) \in dom (F \cap I) \leftrightarrow F (mrCls (dom (F \cap I)) (z)) = mrCls (dom (F \cap I)) (z))$
42	37 40 41	syl2anc	$⊢ (φ \land z \in 𝒫 B) \to (mrCls (dom (F \cap I)) (z) \in dom (F \cap I) \leftrightarrow F (mrCls (dom (F \cap I)) (z)) = mrCls (dom (F \cap I)) (z))$
43	36 42	mpbid	$⊢ (φ \land z \in 𝒫 B) \to F (mrCls (dom (F \cap I)) (z)) = mrCls (dom (F \cap I)) (z)$
44	34 43	sseqtrd	$⊢ (φ \land z \in 𝒫 B) \to F (z) \subseteq mrCls (dom (F \cap I)) (z)$
45	7	adantr	$⊢ (φ \land z \in 𝒫 B) \to dom (F \cap I) \in Moore (B)$
46		sseq1	$⊢ x = z \to (x \subseteq B \leftrightarrow z \subseteq B)$
47	46	anbi2d	$⊢ x = z \to ((φ \land x \subseteq B) \leftrightarrow (φ \land z \subseteq B))$
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	47 50	imbi12d	$⊢ x = z \to (((φ \land x \subseteq B) \to x \subseteq F (x)) \leftrightarrow ((φ \land z \subseteq B) \to z \subseteq F (z)))$
52	51 3	chvarvv	$⊢ (φ \land z \subseteq B) \to z \subseteq F (z)$
53	14 52	sylan2	$⊢ (φ \land z \in 𝒫 B) \to z \subseteq F (z)$
54		2fveq3	$⊢ x = z \to F (F (x)) = F (F (z))$
55	54 49	eqeq12d	$⊢ x = z \to (F (F (x)) = F (x) \leftrightarrow F (F (z)) = F (z))$
56	47 55	imbi12d	$⊢ x = z \to (((φ \land x \subseteq B) \to F (F (x)) = F (x)) \leftrightarrow ((φ \land z \subseteq B) \to F (F (z)) = F (z)))$
57	56 5	chvarvv	$⊢ (φ \land z \subseteq B) \to F (F (z)) = F (z)$
58	14 57	sylan2	$⊢ (φ \land z \in 𝒫 B) \to F (F (z)) = F (z)$
59	2	ffvelrnda	$⊢ (φ \land z \in 𝒫 B) \to F (z) \in 𝒫 B$
60		fnelfp	$⊢ (F Fn 𝒫 B \land F (z) \in 𝒫 B) \to (F (z) \in dom (F \cap I) \leftrightarrow F (F (z)) = F (z))$
61	37 59 60	syl2anc	$⊢ (φ \land z \in 𝒫 B) \to (F (z) \in dom (F \cap I) \leftrightarrow F (F (z)) = F (z))$
62	58 61	mpbird	$⊢ (φ \land z \in 𝒫 B) \to F (z) \in dom (F \cap I)$
63	8	mrcsscl	$⊢ (dom (F \cap I) \in Moore (B) \land z \subseteq F (z) \land F (z) \in dom (F \cap I)) \to mrCls (dom (F \cap I)) (z) \subseteq F (z)$
64	45 53 62 63	syl3anc	$⊢ (φ \land z \in 𝒫 B) \to mrCls (dom (F \cap I)) (z) \subseteq F (z)$
65	44 64	eqssd	$⊢ (φ \land z \in 𝒫 B) \to F (z) = mrCls (dom (F \cap I)) (z)$
66	6 11 65	eqfnfvd	$⊢ φ \to F = mrCls (dom (F \cap I))$

Metamath Proof Explorer

Theorem ismrcd2

Proof