cvmliftmolem2

	Ref	Expression
Hypotheses	cvmliftmo.b	$⊢ B = ⋃ C$
	cvmliftmo.y	$⊢ Y = ⋃ K$
	cvmliftmo.f	$⊢ φ \to F \in (C CovMap J)$
	cvmliftmo.k	$⊢ φ \to K \in Conn$
	cvmliftmo.l	$⊢ φ \to K \in N-LocallyConn$
	cvmliftmo.o	$⊢ φ \to O \in Y$
	cvmliftmoi.m	$⊢ φ \to M \in (K Cn C)$
	cvmliftmoi.n	$⊢ φ \to N \in (K Cn C)$
	cvmliftmoi.g	$⊢ φ \to F \circ M = F \circ N$
	cvmliftmoi.p	$⊢ φ \to M (O) = N (O)$
	cvmliftmolem.1	$⊢ S = (k \in J ⟼ \{s \in (𝒫 C ∖ \{\emptyset\}) \| (⋃ s = F^{-1} [k] \land \forall u \in s (\forall v \in (s ∖ \{u\}) u \cap v = \emptyset \land {F ↾}_{u} \in ((C ↾_{𝑡} u) Homeo (J ↾_{𝑡} k))))\})$
Assertion	cvmliftmolem2	$⊢ φ \to M = N$

Proof

Step	Hyp	Ref	Expression
1		cvmliftmo.b	$⊢ B = ⋃ C$
2		cvmliftmo.y	$⊢ Y = ⋃ K$
3		cvmliftmo.f	$⊢ φ \to F \in (C CovMap J)$
4		cvmliftmo.k	$⊢ φ \to K \in Conn$
5		cvmliftmo.l	$⊢ φ \to K \in N-LocallyConn$
6		cvmliftmo.o	$⊢ φ \to O \in Y$
7		cvmliftmoi.m	$⊢ φ \to M \in (K Cn C)$
8		cvmliftmoi.n	$⊢ φ \to N \in (K Cn C)$
9		cvmliftmoi.g	$⊢ φ \to F \circ M = F \circ N$
10		cvmliftmoi.p	$⊢ φ \to M (O) = N (O)$
11		cvmliftmolem.1	$⊢ S = (k \in J ⟼ \{s \in (𝒫 C ∖ \{\emptyset\}) \| (⋃ s = F^{-1} [k] \land \forall u \in s (\forall v \in (s ∖ \{u\}) u \cap v = \emptyset \land {F ↾}_{u} \in ((C ↾_{𝑡} u) Homeo (J ↾_{𝑡} k))))\})$
12	2 1	cnf	$⊢ M \in (K Cn C) \to M : Y ⟶ B$
13		ffn	$⊢ M : Y ⟶ B \to M Fn Y$
14	7 12 13	3syl	$⊢ φ \to M Fn Y$
15	2 1	cnf	$⊢ N \in (K Cn C) \to N : Y ⟶ B$
16		ffn	$⊢ N : Y ⟶ B \to N Fn Y$
17	8 15 16	3syl	$⊢ φ \to N Fn Y$
18		inss1	$⊢ K \cap Clsd (K) \subseteq K$
19	3	adantr	$⊢ (φ \land x \in Y) \to F \in (C CovMap J)$
20	7 12	syl	$⊢ φ \to M : Y ⟶ B$
21	20	ffvelcdmda	$⊢ (φ \land x \in Y) \to M (x) \in B$
22		cvmcn	$⊢ F \in (C CovMap J) \to F \in (C Cn J)$
23		eqid	$⊢ ⋃ J = ⋃ J$
24	1 23	cnf	$⊢ F \in (C Cn J) \to F : B ⟶ ⋃ J$
25	3 22 24	3syl	$⊢ φ \to F : B ⟶ ⋃ J$
26	25	ffvelcdmda	$⊢ (φ \land M (x) \in B) \to F (M (x)) \in ⋃ J$
27	21 26	syldan	$⊢ (φ \land x \in Y) \to F (M (x)) \in ⋃ J$
28	11 23	cvmcov	$⊢ (F \in (C CovMap J) \land F (M (x)) \in ⋃ J) \to \exists a \in J (F (M (x)) \in a \land S (a) \neq \emptyset)$
29	19 27 28	syl2anc	$⊢ (φ \land x \in Y) \to \exists a \in J (F (M (x)) \in a \land S (a) \neq \emptyset)$
30		n0	$⊢ S (a) \neq \emptyset \leftrightarrow \exists t t \in S (a)$
31	5	adantr	$⊢ (φ \land ((x \in Y \land a \in J) \land (F (M (x)) \in a \land t \in S (a)))) \to K \in N-LocallyConn$
32	7	adantr	$⊢ (φ \land ((x \in Y \land a \in J) \land (F (M (x)) \in a \land t \in S (a)))) \to M \in (K Cn C)$
33		simprrr	$⊢ (φ \land ((x \in Y \land a \in J) \land (F (M (x)) \in a \land t \in S (a)))) \to t \in S (a)$
34	11	cvmsss	$⊢ t \in S (a) \to t \subseteq C$
35	33 34	syl	$⊢ (φ \land ((x \in Y \land a \in J) \land (F (M (x)) \in a \land t \in S (a)))) \to t \subseteq C$
36	3	adantr	$⊢ (φ \land ((x \in Y \land a \in J) \land (F (M (x)) \in a \land t \in S (a)))) \to F \in (C CovMap J)$
37	20	adantr	$⊢ (φ \land ((x \in Y \land a \in J) \land (F (M (x)) \in a \land t \in S (a)))) \to M : Y ⟶ B$
38		simprll	$⊢ (φ \land ((x \in Y \land a \in J) \land (F (M (x)) \in a \land t \in S (a)))) \to x \in Y$
39	37 38	ffvelcdmd	$⊢ (φ \land ((x \in Y \land a \in J) \land (F (M (x)) \in a \land t \in S (a)))) \to M (x) \in B$
40		simprrl	$⊢ (φ \land ((x \in Y \land a \in J) \land (F (M (x)) \in a \land t \in S (a)))) \to F (M (x)) \in a$
41		eqid	$⊢ (ι b \in t \| M (x) \in b) = (ι b \in t \| M (x) \in b)$
42	11 1 41	cvmsiota	$⊢ (F \in (C CovMap J) \land (t \in S (a) \land M (x) \in B \land F (M (x)) \in a)) \to ((ι b \in t \| M (x) \in b) \in t \land M (x) \in (ι b \in t \| M (x) \in b))$
43	36 33 39 40 42	syl13anc	$⊢ (φ \land ((x \in Y \land a \in J) \land (F (M (x)) \in a \land t \in S (a)))) \to ((ι b \in t \| M (x) \in b) \in t \land M (x) \in (ι b \in t \| M (x) \in b))$
44	43	simpld	$⊢ (φ \land ((x \in Y \land a \in J) \land (F (M (x)) \in a \land t \in S (a)))) \to (ι b \in t \| M (x) \in b) \in t$
45	35 44	sseldd	$⊢ (φ \land ((x \in Y \land a \in J) \land (F (M (x)) \in a \land t \in S (a)))) \to (ι b \in t \| M (x) \in b) \in C$
46		cnima	$⊢ (M \in (K Cn C) \land (ι b \in t \| M (x) \in b) \in C) \to M^{-1} [(ι b \in t \| M (x) \in b)] \in K$
47	32 45 46	syl2anc	$⊢ (φ \land ((x \in Y \land a \in J) \land (F (M (x)) \in a \land t \in S (a)))) \to M^{-1} [(ι b \in t \| M (x) \in b)] \in K$
48	43	simprd	$⊢ (φ \land ((x \in Y \land a \in J) \land (F (M (x)) \in a \land t \in S (a)))) \to M (x) \in (ι b \in t \| M (x) \in b)$
49		elpreima	$⊢ M Fn Y \to (x \in M^{-1} [(ι b \in t \| M (x) \in b)] \leftrightarrow (x \in Y \land M (x) \in (ι b \in t \| M (x) \in b)))$
50	37 13 49	3syl	$⊢ (φ \land ((x \in Y \land a \in J) \land (F (M (x)) \in a \land t \in S (a)))) \to (x \in M^{-1} [(ι b \in t \| M (x) \in b)] \leftrightarrow (x \in Y \land M (x) \in (ι b \in t \| M (x) \in b)))$
51	38 48 50	mpbir2and	$⊢ (φ \land ((x \in Y \land a \in J) \land (F (M (x)) \in a \land t \in S (a)))) \to x \in M^{-1} [(ι b \in t \| M (x) \in b)]$
52		nlly2i	$⊢ (K \in N-LocallyConn\landM^{-1} [(ι b \in t \| M (x) \in b)] \in K\landx \in M^{-1} [(ι b \in t \| M (x) \in b)]\to\exists s \in 𝒫 M^{-1} [(ι b \in t \| M (x) \in b)] \exists y \in K (x \in y \land y \subseteq s \land K ↾_{𝑡} s \in Conn))$
53	31 47 51 52	syl3anc	$⊢ (φ \land ((x \in Y \land a \in J) \land (F (M (x)) \in a \land t \in S (a)))) \to \exists s \in 𝒫 M^{-1} [(ι b \in t \| M (x) \in b)] \exists y \in K (x \in y \land y \subseteq s \land K ↾_{𝑡} s \in Conn)$
54		simprr1	$⊢ ((φ \land ((x \in Y \land a \in J) \land (F (M (x)) \in a \land t \in S (a)))) \land ((s \in 𝒫 M^{-1} [(ι b \in t \| M (x) \in b)] \land y \in K) \land (x \in y \land y \subseteq s \land K ↾_{𝑡} s \in Conn))) \to x \in y$
55		simplrr	$⊢ (((x \in Y \land a \in J) \land (F (M (x)) \in a \land t \in S (a))) \land (((s \in 𝒫 M^{-1} [(ι b \in t \| M (x) \in b)] \land y \in K) \land (x \in y \land y \subseteq s \land K ↾_{𝑡} s \in Conn)) \land z \in y)) \to t \in S (a)$
56	55	adantl	$⊢ (φ \land (((x \in Y \land a \in J) \land (F (M (x)) \in a \land t \in S (a))) \land (((s \in 𝒫 M^{-1} [(ι b \in t \| M (x) \in b)] \land y \in K) \land (x \in y \land y \subseteq s \land K ↾_{𝑡} s \in Conn)) \land z \in y))) \to t \in S (a)$
57	44	adantrr	$⊢ (φ \land (((x \in Y \land a \in J) \land (F (M (x)) \in a \land t \in S (a))) \land (((s \in 𝒫 M^{-1} [(ι b \in t \| M (x) \in b)] \land y \in K) \land (x \in y \land y \subseteq s \land K ↾_{𝑡} s \in Conn)) \land z \in y))) \to (ι b \in t \| M (x) \in b) \in t$
58		simplll	$⊢ (((s \in 𝒫 M^{-1} [(ι b \in t \| M (x) \in b)] \land y \in K) \land (x \in y \land y \subseteq s \land K ↾_{𝑡} s \in Conn)) \land z \in y) \to s \in 𝒫 M^{-1} [(ι b \in t \| M (x) \in b)]$
59	58	ad2antll	$⊢ (φ \land (((x \in Y \land a \in J) \land (F (M (x)) \in a \land t \in S (a))) \land (((s \in 𝒫 M^{-1} [(ι b \in t \| M (x) \in b)] \land y \in K) \land (x \in y \land y \subseteq s \land K ↾_{𝑡} s \in Conn)) \land z \in y))) \to s \in 𝒫 M^{-1} [(ι b \in t \| M (x) \in b)]$
60	59	elpwid	$⊢ (φ \land (((x \in Y \land a \in J) \land (F (M (x)) \in a \land t \in S (a))) \land (((s \in 𝒫 M^{-1} [(ι b \in t \| M (x) \in b)] \land y \in K) \land (x \in y \land y \subseteq s \land K ↾_{𝑡} s \in Conn)) \land z \in y))) \to s \subseteq M^{-1} [(ι b \in t \| M (x) \in b)]$
61		simplr3	$⊢ (((s \in 𝒫 M^{-1} [(ι b \in t \| M (x) \in b)] \land y \in K) \land (x \in y \land y \subseteq s \land K ↾_{𝑡} s \in Conn)) \land z \in y) \to K ↾_{𝑡} s \in Conn$
62	61	ad2antll	$⊢ (φ \land (((x \in Y \land a \in J) \land (F (M (x)) \in a \land t \in S (a))) \land (((s \in 𝒫 M^{-1} [(ι b \in t \| M (x) \in b)] \land y \in K) \land (x \in y \land y \subseteq s \land K ↾_{𝑡} s \in Conn)) \land z \in y))) \to K ↾_{𝑡} s \in Conn$
63		simplr2	$⊢ (((s \in 𝒫 M^{-1} [(ι b \in t \| M (x) \in b)] \land y \in K) \land (x \in y \land y \subseteq s \land K ↾_{𝑡} s \in Conn)) \land z \in y) \to y \subseteq s$
64	63	ad2antll	$⊢ (φ \land (((x \in Y \land a \in J) \land (F (M (x)) \in a \land t \in S (a))) \land (((s \in 𝒫 M^{-1} [(ι b \in t \| M (x) \in b)] \land y \in K) \land (x \in y \land y \subseteq s \land K ↾_{𝑡} s \in Conn)) \land z \in y))) \to y \subseteq s$
65		simprr1	$⊢ (((x \in Y \land a \in J) \land (F (M (x)) \in a \land t \in S (a))) \land ((s \in 𝒫 M^{-1} [(ι b \in t \| M (x) \in b)] \land y \in K) \land (x \in y \land y \subseteq s \land K ↾_{𝑡} s \in Conn))) \to x \in y$
66	65	adantl	$⊢ (φ \land (((x \in Y \land a \in J) \land (F (M (x)) \in a \land t \in S (a))) \land ((s \in 𝒫 M^{-1} [(ι b \in t \| M (x) \in b)] \land y \in K) \land (x \in y \land y \subseteq s \land K ↾_{𝑡} s \in Conn)))) \to x \in y$
67	66	adantrrr	$⊢ (φ \land (((x \in Y \land a \in J) \land (F (M (x)) \in a \land t \in S (a))) \land (((s \in 𝒫 M^{-1} [(ι b \in t \| M (x) \in b)] \land y \in K) \land (x \in y \land y \subseteq s \land K ↾_{𝑡} s \in Conn)) \land z \in y))) \to x \in y$
68	64 67	sseldd	$⊢ (φ \land (((x \in Y \land a \in J) \land (F (M (x)) \in a \land t \in S (a))) \land (((s \in 𝒫 M^{-1} [(ι b \in t \| M (x) \in b)] \land y \in K) \land (x \in y \land y \subseteq s \land K ↾_{𝑡} s \in Conn)) \land z \in y))) \to x \in s$
69		simprrr	$⊢ (φ \land (((x \in Y \land a \in J) \land (F (M (x)) \in a \land t \in S (a))) \land (((s \in 𝒫 M^{-1} [(ι b \in t \| M (x) \in b)] \land y \in K) \land (x \in y \land y \subseteq s \land K ↾_{𝑡} s \in Conn)) \land z \in y))) \to z \in y$
70	64 69	sseldd	$⊢ (φ \land (((x \in Y \land a \in J) \land (F (M (x)) \in a \land t \in S (a))) \land (((s \in 𝒫 M^{-1} [(ι b \in t \| M (x) \in b)] \land y \in K) \land (x \in y \land y \subseteq s \land K ↾_{𝑡} s \in Conn)) \land z \in y))) \to z \in s$
71	40	adantrr	$⊢ (φ \land (((x \in Y \land a \in J) \land (F (M (x)) \in a \land t \in S (a))) \land (((s \in 𝒫 M^{-1} [(ι b \in t \| M (x) \in b)] \land y \in K) \land (x \in y \land y \subseteq s \land K ↾_{𝑡} s \in Conn)) \land z \in y))) \to F (M (x)) \in a$
72	1 2 3 4 5 6 7 8 9 10 11 56 57 60 62 68 68 70 71	cvmliftmolem1	$⊢ (φ \land (((x \in Y \land a \in J) \land (F (M (x)) \in a \land t \in S (a))) \land (((s \in 𝒫 M^{-1} [(ι b \in t \| M (x) \in b)] \land y \in K) \land (x \in y \land y \subseteq s \land K ↾_{𝑡} s \in Conn)) \land z \in y))) \to (x \in dom (M \cap N) \to z \in dom (M \cap N))$
73	1 2 3 4 5 6 7 8 9 10 11 56 57 60 62 68 70 68 71	cvmliftmolem1	$⊢ (φ \land (((x \in Y \land a \in J) \land (F (M (x)) \in a \land t \in S (a))) \land (((s \in 𝒫 M^{-1} [(ι b \in t \| M (x) \in b)] \land y \in K) \land (x \in y \land y \subseteq s \land K ↾_{𝑡} s \in Conn)) \land z \in y))) \to (z \in dom (M \cap N) \to x \in dom (M \cap N))$
74	72 73	impbid	$⊢ (φ \land (((x \in Y \land a \in J) \land (F (M (x)) \in a \land t \in S (a))) \land (((s \in 𝒫 M^{-1} [(ι b \in t \| M (x) \in b)] \land y \in K) \land (x \in y \land y \subseteq s \land K ↾_{𝑡} s \in Conn)) \land z \in y))) \to (x \in dom (M \cap N) \leftrightarrow z \in dom (M \cap N))$
75	74	anassrs	$⊢ ((φ \land ((x \in Y \land a \in J) \land (F (M (x)) \in a \land t \in S (a)))) \land (((s \in 𝒫 M^{-1} [(ι b \in t \| M (x) \in b)] \land y \in K) \land (x \in y \land y \subseteq s \land K ↾_{𝑡} s \in Conn)) \land z \in y)) \to (x \in dom (M \cap N) \leftrightarrow z \in dom (M \cap N))$
76	75	anassrs	$⊢ (((φ \land ((x \in Y \land a \in J) \land (F (M (x)) \in a \land t \in S (a)))) \land ((s \in 𝒫 M^{-1} [(ι b \in t \| M (x) \in b)] \land y \in K) \land (x \in y \land y \subseteq s \land K ↾_{𝑡} s \in Conn))) \land z \in y) \to (x \in dom (M \cap N) \leftrightarrow z \in dom (M \cap N))$
77	76	ralrimiva	$⊢ ((φ \land ((x \in Y \land a \in J) \land (F (M (x)) \in a \land t \in S (a)))) \land ((s \in 𝒫 M^{-1} [(ι b \in t \| M (x) \in b)] \land y \in K) \land (x \in y \land y \subseteq s \land K ↾_{𝑡} s \in Conn))) \to \forall z \in y (x \in dom (M \cap N) \leftrightarrow z \in dom (M \cap N))$
78	54 77	jca	$⊢ ((φ \land ((x \in Y \land a \in J) \land (F (M (x)) \in a \land t \in S (a)))) \land ((s \in 𝒫 M^{-1} [(ι b \in t \| M (x) \in b)] \land y \in K) \land (x \in y \land y \subseteq s \land K ↾_{𝑡} s \in Conn))) \to (x \in y \land \forall z \in y (x \in dom (M \cap N) \leftrightarrow z \in dom (M \cap N)))$
79	78	expr	$⊢ ((φ \land ((x \in Y \land a \in J) \land (F (M (x)) \in a \land t \in S (a)))) \land (s \in 𝒫 M^{-1} [(ι b \in t \| M (x) \in b)] \land y \in K)) \to ((x \in y \land y \subseteq s \land K ↾_{𝑡} s \in Conn) \to (x \in y \land \forall z \in y (x \in dom (M \cap N) \leftrightarrow z \in dom (M \cap N))))$
80	79	anassrs	$⊢ (((φ \land ((x \in Y \land a \in J) \land (F (M (x)) \in a \land t \in S (a)))) \land s \in 𝒫 M^{-1} [(ι b \in t \| M (x) \in b)]) \land y \in K) \to ((x \in y \land y \subseteq s \land K ↾_{𝑡} s \in Conn) \to (x \in y \land \forall z \in y (x \in dom (M \cap N) \leftrightarrow z \in dom (M \cap N))))$
81	80	reximdva	$⊢ ((φ \land ((x \in Y \land a \in J) \land (F (M (x)) \in a \land t \in S (a)))) \land s \in 𝒫 M^{-1} [(ι b \in t \| M (x) \in b)]) \to (\exists y \in K (x \in y \land y \subseteq s \land K ↾_{𝑡} s \in Conn) \to \exists y \in K (x \in y \land \forall z \in y (x \in dom (M \cap N) \leftrightarrow z \in dom (M \cap N))))$
82	81	rexlimdva	$⊢ (φ \land ((x \in Y \land a \in J) \land (F (M (x)) \in a \land t \in S (a)))) \to (\exists s \in 𝒫 M^{-1} [(ι b \in t \| M (x) \in b)] \exists y \in K (x \in y \land y \subseteq s \land K ↾_{𝑡} s \in Conn) \to \exists y \in K (x \in y \land \forall z \in y (x \in dom (M \cap N) \leftrightarrow z \in dom (M \cap N))))$
83	53 82	mpd	$⊢ (φ \land ((x \in Y \land a \in J) \land (F (M (x)) \in a \land t \in S (a)))) \to \exists y \in K (x \in y \land \forall z \in y (x \in dom (M \cap N) \leftrightarrow z \in dom (M \cap N)))$
84	83	anassrs	$⊢ ((φ \land (x \in Y \land a \in J)) \land (F (M (x)) \in a \land t \in S (a))) \to \exists y \in K (x \in y \land \forall z \in y (x \in dom (M \cap N) \leftrightarrow z \in dom (M \cap N)))$
85	84	expr	$⊢ ((φ \land (x \in Y \land a \in J)) \land F (M (x)) \in a) \to (t \in S (a) \to \exists y \in K (x \in y \land \forall z \in y (x \in dom (M \cap N) \leftrightarrow z \in dom (M \cap N))))$
86	85	exlimdv	$⊢ ((φ \land (x \in Y \land a \in J)) \land F (M (x)) \in a) \to (\exists t t \in S (a) \to \exists y \in K (x \in y \land \forall z \in y (x \in dom (M \cap N) \leftrightarrow z \in dom (M \cap N))))$
87	30 86	biimtrid	$⊢ ((φ \land (x \in Y \land a \in J)) \land F (M (x)) \in a) \to (S (a) \neq \emptyset \to \exists y \in K (x \in y \land \forall z \in y (x \in dom (M \cap N) \leftrightarrow z \in dom (M \cap N))))$
88	87	expimpd	$⊢ (φ \land (x \in Y \land a \in J)) \to ((F (M (x)) \in a \land S (a) \neq \emptyset) \to \exists y \in K (x \in y \land \forall z \in y (x \in dom (M \cap N) \leftrightarrow z \in dom (M \cap N))))$
89	88	anassrs	$⊢ ((φ \land x \in Y) \land a \in J) \to ((F (M (x)) \in a \land S (a) \neq \emptyset) \to \exists y \in K (x \in y \land \forall z \in y (x \in dom (M \cap N) \leftrightarrow z \in dom (M \cap N))))$
90	89	rexlimdva	$⊢ (φ \land x \in Y) \to (\exists a \in J (F (M (x)) \in a \land S (a) \neq \emptyset) \to \exists y \in K (x \in y \land \forall z \in y (x \in dom (M \cap N) \leftrightarrow z \in dom (M \cap N))))$
91	29 90	mpd	$⊢ (φ \land x \in Y) \to \exists y \in K (x \in y \land \forall z \in y (x \in dom (M \cap N) \leftrightarrow z \in dom (M \cap N)))$
92	91	ralrimiva	$⊢ φ \to \forall x \in Y \exists y \in K (x \in y \land \forall z \in y (x \in dom (M \cap N) \leftrightarrow z \in dom (M \cap N)))$
93		conntop	$⊢ K \in Conn \to K \in Top$
94	4 93	syl	$⊢ φ \to K \in Top$
95		fndmin	$⊢ (M Fn Y \land N Fn Y) \to dom (M \cap N) = \{x \in Y \| M (x) = N (x)\}$
96	14 17 95	syl2anc	$⊢ φ \to dom (M \cap N) = \{x \in Y \| M (x) = N (x)\}$
97		ssrab2	$⊢ \{x \in Y \| M (x) = N (x)\} \subseteq Y$
98	96 97	eqsstrdi	$⊢ φ \to dom (M \cap N) \subseteq Y$
99	2	isclo	$⊢ (K \in Top \land dom (M \cap N) \subseteq Y) \to (dom (M \cap N) \in (K \cap Clsd (K)) \leftrightarrow \forall x \in Y \exists y \in K (x \in y \land \forall z \in y (x \in dom (M \cap N) \leftrightarrow z \in dom (M \cap N))))$
100	94 98 99	syl2anc	$⊢ φ \to (dom (M \cap N) \in (K \cap Clsd (K)) \leftrightarrow \forall x \in Y \exists y \in K (x \in y \land \forall z \in y (x \in dom (M \cap N) \leftrightarrow z \in dom (M \cap N))))$
101	92 100	mpbird	$⊢ φ \to dom (M \cap N) \in (K \cap Clsd (K))$
102	18 101	sselid	$⊢ φ \to dom (M \cap N) \in K$
103		fveq2	$⊢ x = O \to M (x) = M (O)$
104		fveq2	$⊢ x = O \to N (x) = N (O)$
105	103 104	eqeq12d	$⊢ x = O \to (M (x) = N (x) \leftrightarrow M (O) = N (O))$
106	105	elrab	$⊢ O \in \{x \in Y \| M (x) = N (x)\} \leftrightarrow (O \in Y \land M (O) = N (O))$
107	6 10 106	sylanbrc	$⊢ φ \to O \in \{x \in Y \| M (x) = N (x)\}$
108	107 96	eleqtrrd	$⊢ φ \to O \in dom (M \cap N)$
109	108	ne0d	$⊢ φ \to dom (M \cap N) \neq \emptyset$
110		inss2	$⊢ K \cap Clsd (K) \subseteq Clsd (K)$
111	110 101	sselid	$⊢ φ \to dom (M \cap N) \in Clsd (K)$
112	2 4 102 109 111	connclo	$⊢ φ \to dom (M \cap N) = Y$
113	112 96	eqtr3d	$⊢ φ \to Y = \{x \in Y \| M (x) = N (x)\}$
114		rabid2	$⊢ Y = \{x \in Y \| M (x) = N (x)\} \leftrightarrow \forall x \in Y M (x) = N (x)$
115	113 114	sylib	$⊢ φ \to \forall x \in Y M (x) = N (x)$
116	115	r19.21bi	$⊢ (φ \land x \in Y) \to M (x) = N (x)$
117	14 17 116	eqfnfvd	$⊢ φ \to M = N$

Metamath Proof Explorer

Theorem cvmliftmolem2

Proof