cvmlift2lem10

	Ref	Expression
Hypotheses	cvmlift2.b	$⊢ B = ⋃ C$
	cvmlift2.f	$⊢ φ \to F \in (C CovMap J)$
	cvmlift2.g	$⊢ φ \to G \in ((II \times_{t} II) Cn J)$
	cvmlift2.p	$⊢ φ \to P \in B$
	cvmlift2.i	$⊢ φ \to F (P) = 0 G 0$
	cvmlift2.h	$⊢ H = (ι f \in (II Cn C) \| (F \circ f = (z \in [0, 1] ⟼ z G 0) \land f (0) = P))$
	cvmlift2.k	$⊢ K = (x \in [0, 1], y \in [0, 1] ⟼ (ι f \in (II Cn C) \| (F \circ f = (z \in [0, 1] ⟼ x G z) \land f (0) = H (x))) (y))$
	cvmlift2lem10.s	$⊢ S = (k \in J ⟼ \{s \in (𝒫 C ∖ \{\emptyset\}) \| (⋃ s = F^{-1} [k] \land \forall c \in s (\forall d \in (s ∖ \{c\}) c \cap d = \emptyset \land {F ↾}_{c} \in ((C ↾_{𝑡} c) Homeo (J ↾_{𝑡} k))))\})$
	cvmlift2lem10.1	$⊢ φ \to X \in [0, 1]$
	cvmlift2lem10.2	$⊢ φ \to Y \in [0, 1]$
Assertion	cvmlift2lem10	$⊢ φ \to \exists u \in II \exists v \in II (X \in u \land Y \in v \land (\exists w \in v {K ↾}_{(u \times \{w\})} \in (((II \times_{t} II) ↾_{𝑡} (u \times \{w\})) Cn C) \to {K ↾}_{(u \times v)} \in (((II \times_{t} II) ↾_{𝑡} (u \times v)) Cn C)))$

Proof

Step	Hyp	Ref	Expression
1		cvmlift2.b	$⊢ B = ⋃ C$
2		cvmlift2.f	$⊢ φ \to F \in (C CovMap J)$
3		cvmlift2.g	$⊢ φ \to G \in ((II \times_{t} II) Cn J)$
4		cvmlift2.p	$⊢ φ \to P \in B$
5		cvmlift2.i	$⊢ φ \to F (P) = 0 G 0$
6		cvmlift2.h	$⊢ H = (ι f \in (II Cn C) \| (F \circ f = (z \in [0, 1] ⟼ z G 0) \land f (0) = P))$
7		cvmlift2.k	$⊢ K = (x \in [0, 1], y \in [0, 1] ⟼ (ι f \in (II Cn C) \| (F \circ f = (z \in [0, 1] ⟼ x G z) \land f (0) = H (x))) (y))$
8		cvmlift2lem10.s	$⊢ S = (k \in J ⟼ \{s \in (𝒫 C ∖ \{\emptyset\}) \| (⋃ s = F^{-1} [k] \land \forall c \in s (\forall d \in (s ∖ \{c\}) c \cap d = \emptyset \land {F ↾}_{c} \in ((C ↾_{𝑡} c) Homeo (J ↾_{𝑡} k))))\})$
9		cvmlift2lem10.1	$⊢ φ \to X \in [0, 1]$
10		cvmlift2lem10.2	$⊢ φ \to Y \in [0, 1]$
11		iitop	$⊢ II \in Top$
12		iiuni	$⊢ [0, 1] = ⋃ II$
13	11 11 12 12	txunii	$⊢ [0, 1] \times [0, 1] = ⋃ (II \times_{t} II)$
14		eqid	$⊢ ⋃ J = ⋃ J$
15	13 14	cnf	$⊢ G \in ((II \times_{t} II) Cn J) \to G : [0, 1] \times [0, 1] ⟶ ⋃ J$
16	3 15	syl	$⊢ φ \to G : [0, 1] \times [0, 1] ⟶ ⋃ J$
17	9 10	opelxpd	$⊢ φ \to ⟨X, Y⟩ \in ([0, 1] \times [0, 1])$
18	16 17	ffvelrnd	$⊢ φ \to G (⟨X, Y⟩) \in ⋃ J$
19	8 14	cvmcov	$⊢ (F \in (C CovMap J) \land G (⟨X, Y⟩) \in ⋃ J) \to \exists m \in J (G (⟨X, Y⟩) \in m \land S (m) \neq \emptyset)$
20	2 18 19	syl2anc	$⊢ φ \to \exists m \in J (G (⟨X, Y⟩) \in m \land S (m) \neq \emptyset)$
21		n0	$⊢ S (m) \neq \emptyset \leftrightarrow \exists t t \in S (m)$
22		eleq1	$⊢ z = ⟨X, Y⟩ \to (z \in (a \times b) \leftrightarrow ⟨X, Y⟩ \in (a \times b))$
23		opelxp	$⊢ ⟨X, Y⟩ \in (a \times b) \leftrightarrow (X \in a \land Y \in b)$
24	22 23	syl6bb	$⊢ z = ⟨X, Y⟩ \to (z \in (a \times b) \leftrightarrow (X \in a \land Y \in b))$
25	24	anbi1d	$⊢ z = ⟨X, Y⟩ \to ((z \in (a \times b) \land a \times b \subseteq G^{-1} [m]) \leftrightarrow ((X \in a \land Y \in b) \land a \times b \subseteq G^{-1} [m]))$
26	25	2rexbidv	$⊢ z = ⟨X, Y⟩ \to (\exists a \in II \exists b \in II (z \in (a \times b) \land a \times b \subseteq G^{-1} [m]) \leftrightarrow \exists a \in II \exists b \in II ((X \in a \land Y \in b) \land a \times b \subseteq G^{-1} [m]))$
27	3	adantr	$⊢ (φ \land (G (⟨X, Y⟩) \in m \land t \in S (m))) \to G \in ((II \times_{t} II) Cn J)$
28	8	cvmsrcl	$⊢ t \in S (m) \to m \in J$
29	28	ad2antll	$⊢ (φ \land (G (⟨X, Y⟩) \in m \land t \in S (m))) \to m \in J$
30		cnima	$⊢ (G \in ((II \times_{t} II) Cn J) \land m \in J) \to G^{-1} [m] \in (II \times_{t} II)$
31	27 29 30	syl2anc	$⊢ (φ \land (G (⟨X, Y⟩) \in m \land t \in S (m))) \to G^{-1} [m] \in (II \times_{t} II)$
32		eltx	$⊢ (II \in Top \land II \in Top) \to (G^{-1} [m] \in (II \times_{t} II) \leftrightarrow \forall z \in G^{-1} [m] \exists a \in II \exists b \in II (z \in (a \times b) \land a \times b \subseteq G^{-1} [m]))$
33	11 11 32	mp2an	$⊢ G^{-1} [m] \in (II \times_{t} II) \leftrightarrow \forall z \in G^{-1} [m] \exists a \in II \exists b \in II (z \in (a \times b) \land a \times b \subseteq G^{-1} [m])$
34	31 33	sylib	$⊢ (φ \land (G (⟨X, Y⟩) \in m \land t \in S (m))) \to \forall z \in G^{-1} [m] \exists a \in II \exists b \in II (z \in (a \times b) \land a \times b \subseteq G^{-1} [m])$
35	17	adantr	$⊢ (φ \land (G (⟨X, Y⟩) \in m \land t \in S (m))) \to ⟨X, Y⟩ \in ([0, 1] \times [0, 1])$
36		simprl	$⊢ (φ \land (G (⟨X, Y⟩) \in m \land t \in S (m))) \to G (⟨X, Y⟩) \in m$
37	16	adantr	$⊢ (φ \land (G (⟨X, Y⟩) \in m \land t \in S (m))) \to G : [0, 1] \times [0, 1] ⟶ ⋃ J$
38		ffn	$⊢ G : [0, 1] \times [0, 1] ⟶ ⋃ J \to G Fn ([0, 1] \times [0, 1])$
39		elpreima	$⊢ G Fn ([0, 1] \times [0, 1]) \to (⟨X, Y⟩ \in G^{-1} [m] \leftrightarrow (⟨X, Y⟩ \in ([0, 1] \times [0, 1]) \land G (⟨X, Y⟩) \in m))$
40	37 38 39	3syl	$⊢ (φ \land (G (⟨X, Y⟩) \in m \land t \in S (m))) \to (⟨X, Y⟩ \in G^{-1} [m] \leftrightarrow (⟨X, Y⟩ \in ([0, 1] \times [0, 1]) \land G (⟨X, Y⟩) \in m))$
41	35 36 40	mpbir2and	$⊢ (φ \land (G (⟨X, Y⟩) \in m \land t \in S (m))) \to ⟨X, Y⟩ \in G^{-1} [m]$
42	26 34 41	rspcdva	$⊢ (φ \land (G (⟨X, Y⟩) \in m \land t \in S (m))) \to \exists a \in II \exists b \in II ((X \in a \land Y \in b) \land a \times b \subseteq G^{-1} [m])$
43		iillysconn	$⊢ II \in LocallySConn$
44		simplrl	$⊢ (((φ \land (G (⟨X, Y⟩) \in m \land t \in S (m))) \land (a \in II \land b \in II)) \land ((X \in a \land Y \in b) \land a \times b \subseteq G^{-1} [m])) \to a \in II$
45		simprll	$⊢ (((φ \land (G (⟨X, Y⟩) \in m \land t \in S (m))) \land (a \in II \land b \in II)) \land ((X \in a \land Y \in b) \land a \times b \subseteq G^{-1} [m])) \to X \in a$
46		llyi	$⊢ (II \in LocallySConn\landa \in II\landX \in a\to\exists u \in II)$
47	43 44 45 46	mp3an2i	$⊢ (((φ \land (G (⟨X, Y⟩) \in m \land t \in S (m))) \land (a \in II \land b \in II)) \land ((X \in a \land Y \in b) \land a \times b \subseteq G^{-1} [m])) \to \exists u \in II (u \subseteq a \land X \in u \land II ↾_{𝑡} u \in SConn)$
48		simplrr	$⊢ (((φ \land (G (⟨X, Y⟩) \in m \land t \in S (m))) \land (a \in II \land b \in II)) \land ((X \in a \land Y \in b) \land a \times b \subseteq G^{-1} [m])) \to b \in II$
49		simprlr	$⊢ (((φ \land (G (⟨X, Y⟩) \in m \land t \in S (m))) \land (a \in II \land b \in II)) \land ((X \in a \land Y \in b) \land a \times b \subseteq G^{-1} [m])) \to Y \in b$
50		llyi	$⊢ (II \in LocallySConn\landb \in II\landY \in b\to\exists v \in II)$
51	43 48 49 50	mp3an2i	$⊢ (((φ \land (G (⟨X, Y⟩) \in m \land t \in S (m))) \land (a \in II \land b \in II)) \land ((X \in a \land Y \in b) \land a \times b \subseteq G^{-1} [m])) \to \exists v \in II (v \subseteq b \land Y \in v \land II ↾_{𝑡} v \in SConn)$
52		reeanv	$⊢ \exists u \in II \exists v \in II ((u \subseteq a \land X \in u \land II ↾_{𝑡} u \in SConn) \land (v \subseteq b \land Y \in v \land II ↾_{𝑡} v \in SConn)) \leftrightarrow (\exists u \in II (u \subseteq a \land X \in u \land II ↾_{𝑡} u \in SConn) \land \exists v \in II (v \subseteq b \land Y \in v \land II ↾_{𝑡} v \in SConn))$
53		simpl2	$⊢ ((u \subseteq a \land X \in u \land II ↾_{𝑡} u \in SConn) \land (v \subseteq b \land Y \in v \land II ↾_{𝑡} v \in SConn)) \to X \in u$
54	53	a1i	$⊢ (((φ \land (G (⟨X, Y⟩) \in m \land t \in S (m))) \land (a \in II \land b \in II)) \land ((X \in a \land Y \in b) \land a \times b \subseteq G^{-1} [m])) \to (((u \subseteq a \land X \in u \land II ↾_{𝑡} u \in SConn) \land (v \subseteq b \land Y \in v \land II ↾_{𝑡} v \in SConn)) \to X \in u)$
55		simpr2	$⊢ ((u \subseteq a \land X \in u \land II ↾_{𝑡} u \in SConn) \land (v \subseteq b \land Y \in v \land II ↾_{𝑡} v \in SConn)) \to Y \in v$
56	55	a1i	$⊢ (((φ \land (G (⟨X, Y⟩) \in m \land t \in S (m))) \land (a \in II \land b \in II)) \land ((X \in a \land Y \in b) \land a \times b \subseteq G^{-1} [m])) \to (((u \subseteq a \land X \in u \land II ↾_{𝑡} u \in SConn) \land (v \subseteq b \land Y \in v \land II ↾_{𝑡} v \in SConn)) \to Y \in v)$
57		simprl1	$⊢ ((((φ \land (G (⟨X, Y⟩) \in m \land t \in S (m))) \land (a \in II \land b \in II)) \land ((X \in a \land Y \in b) \land a \times b \subseteq G^{-1} [m])) \land ((u \subseteq a \land X \in u \land II ↾_{𝑡} u \in SConn) \land (v \subseteq b \land Y \in v \land II ↾_{𝑡} v \in SConn))) \to u \subseteq a$
58		simprr1	$⊢ ((((φ \land (G (⟨X, Y⟩) \in m \land t \in S (m))) \land (a \in II \land b \in II)) \land ((X \in a \land Y \in b) \land a \times b \subseteq G^{-1} [m])) \land ((u \subseteq a \land X \in u \land II ↾_{𝑡} u \in SConn) \land (v \subseteq b \land Y \in v \land II ↾_{𝑡} v \in SConn))) \to v \subseteq b$
59		xpss12	$⊢ (u \subseteq a \land v \subseteq b) \to u \times v \subseteq a \times b$
60	57 58 59	syl2anc	$⊢ ((((φ \land (G (⟨X, Y⟩) \in m \land t \in S (m))) \land (a \in II \land b \in II)) \land ((X \in a \land Y \in b) \land a \times b \subseteq G^{-1} [m])) \land ((u \subseteq a \land X \in u \land II ↾_{𝑡} u \in SConn) \land (v \subseteq b \land Y \in v \land II ↾_{𝑡} v \in SConn))) \to u \times v \subseteq a \times b$
61		simplrr	$⊢ ((((φ \land (G (⟨X, Y⟩) \in m \land t \in S (m))) \land (a \in II \land b \in II)) \land ((X \in a \land Y \in b) \land a \times b \subseteq G^{-1} [m])) \land ((u \subseteq a \land X \in u \land II ↾_{𝑡} u \in SConn) \land (v \subseteq b \land Y \in v \land II ↾_{𝑡} v \in SConn))) \to a \times b \subseteq G^{-1} [m]$
62	60 61	sstrd	$⊢ ((((φ \land (G (⟨X, Y⟩) \in m \land t \in S (m))) \land (a \in II \land b \in II)) \land ((X \in a \land Y \in b) \land a \times b \subseteq G^{-1} [m])) \land ((u \subseteq a \land X \in u \land II ↾_{𝑡} u \in SConn) \land (v \subseteq b \land Y \in v \land II ↾_{𝑡} v \in SConn))) \to u \times v \subseteq G^{-1} [m]$
63	62	ex	$⊢ (((φ \land (G (⟨X, Y⟩) \in m \land t \in S (m))) \land (a \in II \land b \in II)) \land ((X \in a \land Y \in b) \land a \times b \subseteq G^{-1} [m])) \to (((u \subseteq a \land X \in u \land II ↾_{𝑡} u \in SConn) \land (v \subseteq b \land Y \in v \land II ↾_{𝑡} v \in SConn)) \to u \times v \subseteq G^{-1} [m])$
64	54 56 63	3jcad	$⊢ (((φ \land (G (⟨X, Y⟩) \in m \land t \in S (m))) \land (a \in II \land b \in II)) \land ((X \in a \land Y \in b) \land a \times b \subseteq G^{-1} [m])) \to (((u \subseteq a \land X \in u \land II ↾_{𝑡} u \in SConn) \land (v \subseteq b \land Y \in v \land II ↾_{𝑡} v \in SConn)) \to (X \in u \land Y \in v \land u \times v \subseteq G^{-1} [m]))$
65		simp3	$⊢ (u \subseteq a \land X \in u \land II ↾_{𝑡} u \in SConn) \to II ↾_{𝑡} u \in SConn$
66		simp3	$⊢ (v \subseteq b \land Y \in v \land II ↾_{𝑡} v \in SConn) \to II ↾_{𝑡} v \in SConn$
67	65 66	anim12i	$⊢ ((u \subseteq a \land X \in u \land II ↾_{𝑡} u \in SConn) \land (v \subseteq b \land Y \in v \land II ↾_{𝑡} v \in SConn)) \to (II ↾_{𝑡} u \in SConn \land II ↾_{𝑡} v \in SConn)$
68	64 67	jca2	$⊢ (((φ \land (G (⟨X, Y⟩) \in m \land t \in S (m))) \land (a \in II \land b \in II)) \land ((X \in a \land Y \in b) \land a \times b \subseteq G^{-1} [m])) \to (((u \subseteq a \land X \in u \land II ↾_{𝑡} u \in SConn) \land (v \subseteq b \land Y \in v \land II ↾_{𝑡} v \in SConn)) \to ((X \in u \land Y \in v \land u \times v \subseteq G^{-1} [m]) \land (II ↾_{𝑡} u \in SConn \land II ↾_{𝑡} v \in SConn)))$
69	68	reximdv	$⊢ (((φ \land (G (⟨X, Y⟩) \in m \land t \in S (m))) \land (a \in II \land b \in II)) \land ((X \in a \land Y \in b) \land a \times b \subseteq G^{-1} [m])) \to (\exists v \in II ((u \subseteq a \land X \in u \land II ↾_{𝑡} u \in SConn) \land (v \subseteq b \land Y \in v \land II ↾_{𝑡} v \in SConn)) \to \exists v \in II ((X \in u \land Y \in v \land u \times v \subseteq G^{-1} [m]) \land (II ↾_{𝑡} u \in SConn \land II ↾_{𝑡} v \in SConn)))$
70	69	reximdv	$⊢ (((φ \land (G (⟨X, Y⟩) \in m \land t \in S (m))) \land (a \in II \land b \in II)) \land ((X \in a \land Y \in b) \land a \times b \subseteq G^{-1} [m])) \to (\exists u \in II \exists v \in II ((u \subseteq a \land X \in u \land II ↾_{𝑡} u \in SConn) \land (v \subseteq b \land Y \in v \land II ↾_{𝑡} v \in SConn)) \to \exists u \in II \exists v \in II ((X \in u \land Y \in v \land u \times v \subseteq G^{-1} [m]) \land (II ↾_{𝑡} u \in SConn \land II ↾_{𝑡} v \in SConn)))$
71	52 70	syl5bir	$⊢ (((φ \land (G (⟨X, Y⟩) \in m \land t \in S (m))) \land (a \in II \land b \in II)) \land ((X \in a \land Y \in b) \land a \times b \subseteq G^{-1} [m])) \to ((\exists u \in II (u \subseteq a \land X \in u \land II ↾_{𝑡} u \in SConn) \land \exists v \in II (v \subseteq b \land Y \in v \land II ↾_{𝑡} v \in SConn)) \to \exists u \in II \exists v \in II ((X \in u \land Y \in v \land u \times v \subseteq G^{-1} [m]) \land (II ↾_{𝑡} u \in SConn \land II ↾_{𝑡} v \in SConn)))$
72	47 51 71	mp2and	$⊢ (((φ \land (G (⟨X, Y⟩) \in m \land t \in S (m))) \land (a \in II \land b \in II)) \land ((X \in a \land Y \in b) \land a \times b \subseteq G^{-1} [m])) \to \exists u \in II \exists v \in II ((X \in u \land Y \in v \land u \times v \subseteq G^{-1} [m]) \land (II ↾_{𝑡} u \in SConn \land II ↾_{𝑡} v \in SConn))$
73	72	ex	$⊢ ((φ \land (G (⟨X, Y⟩) \in m \land t \in S (m))) \land (a \in II \land b \in II)) \to (((X \in a \land Y \in b) \land a \times b \subseteq G^{-1} [m]) \to \exists u \in II \exists v \in II ((X \in u \land Y \in v \land u \times v \subseteq G^{-1} [m]) \land (II ↾_{𝑡} u \in SConn \land II ↾_{𝑡} v \in SConn)))$
74	73	rexlimdvva	$⊢ (φ \land (G (⟨X, Y⟩) \in m \land t \in S (m))) \to (\exists a \in II \exists b \in II ((X \in a \land Y \in b) \land a \times b \subseteq G^{-1} [m]) \to \exists u \in II \exists v \in II ((X \in u \land Y \in v \land u \times v \subseteq G^{-1} [m]) \land (II ↾_{𝑡} u \in SConn \land II ↾_{𝑡} v \in SConn)))$
75	42 74	mpd	$⊢ (φ \land (G (⟨X, Y⟩) \in m \land t \in S (m))) \to \exists u \in II \exists v \in II ((X \in u \land Y \in v \land u \times v \subseteq G^{-1} [m]) \land (II ↾_{𝑡} u \in SConn \land II ↾_{𝑡} v \in SConn))$
76		simp3l1	$⊢ ((φ \land (G (⟨X, Y⟩) \in m \land t \in S (m))) \land (u \in II \land v \in II) \land ((X \in u \land Y \in v \land u \times v \subseteq G^{-1} [m]) \land (II ↾_{𝑡} u \in SConn \land II ↾_{𝑡} v \in SConn))) \to X \in u$
77		simp3l2	$⊢ ((φ \land (G (⟨X, Y⟩) \in m \land t \in S (m))) \land (u \in II \land v \in II) \land ((X \in u \land Y \in v \land u \times v \subseteq G^{-1} [m]) \land (II ↾_{𝑡} u \in SConn \land II ↾_{𝑡} v \in SConn))) \to Y \in v$
78		simpl1l	$⊢ (((φ \land (G (⟨X, Y⟩) \in m \land t \in S (m))) \land (u \in II \land v \in II) \land ((X \in u \land Y \in v \land u \times v \subseteq G^{-1} [m]) \land (II ↾_{𝑡} u \in SConn \land II ↾_{𝑡} v \in SConn))) \land (w \in v \land {K ↾}_{(u \times \{w\})} \in (((II \times_{t} II) ↾_{𝑡} (u \times \{w\})) Cn C))) \to φ$
79	78 2	syl	$⊢ (((φ \land (G (⟨X, Y⟩) \in m \land t \in S (m))) \land (u \in II \land v \in II) \land ((X \in u \land Y \in v \land u \times v \subseteq G^{-1} [m]) \land (II ↾_{𝑡} u \in SConn \land II ↾_{𝑡} v \in SConn))) \land (w \in v \land {K ↾}_{(u \times \{w\})} \in (((II \times_{t} II) ↾_{𝑡} (u \times \{w\})) Cn C))) \to F \in (C CovMap J)$
80	78 3	syl	$⊢ (((φ \land (G (⟨X, Y⟩) \in m \land t \in S (m))) \land (u \in II \land v \in II) \land ((X \in u \land Y \in v \land u \times v \subseteq G^{-1} [m]) \land (II ↾_{𝑡} u \in SConn \land II ↾_{𝑡} v \in SConn))) \land (w \in v \land {K ↾}_{(u \times \{w\})} \in (((II \times_{t} II) ↾_{𝑡} (u \times \{w\})) Cn C))) \to G \in ((II \times_{t} II) Cn J)$
81	78 4	syl	$⊢ (((φ \land (G (⟨X, Y⟩) \in m \land t \in S (m))) \land (u \in II \land v \in II) \land ((X \in u \land Y \in v \land u \times v \subseteq G^{-1} [m]) \land (II ↾_{𝑡} u \in SConn \land II ↾_{𝑡} v \in SConn))) \land (w \in v \land {K ↾}_{(u \times \{w\})} \in (((II \times_{t} II) ↾_{𝑡} (u \times \{w\})) Cn C))) \to P \in B$
82	78 5	syl	$⊢ (((φ \land (G (⟨X, Y⟩) \in m \land t \in S (m))) \land (u \in II \land v \in II) \land ((X \in u \land Y \in v \land u \times v \subseteq G^{-1} [m]) \land (II ↾_{𝑡} u \in SConn \land II ↾_{𝑡} v \in SConn))) \land (w \in v \land {K ↾}_{(u \times \{w\})} \in (((II \times_{t} II) ↾_{𝑡} (u \times \{w\})) Cn C))) \to F (P) = 0 G 0$
83		df-ov	$⊢ X G Y = G (⟨X, Y⟩)$
84		simpl1r	$⊢ (((φ \land (G (⟨X, Y⟩) \in m \land t \in S (m))) \land (u \in II \land v \in II) \land ((X \in u \land Y \in v \land u \times v \subseteq G^{-1} [m]) \land (II ↾_{𝑡} u \in SConn \land II ↾_{𝑡} v \in SConn))) \land (w \in v \land {K ↾}_{(u \times \{w\})} \in (((II \times_{t} II) ↾_{𝑡} (u \times \{w\})) Cn C))) \to (G (⟨X, Y⟩) \in m \land t \in S (m))$
85	84	simpld	$⊢ (((φ \land (G (⟨X, Y⟩) \in m \land t \in S (m))) \land (u \in II \land v \in II) \land ((X \in u \land Y \in v \land u \times v \subseteq G^{-1} [m]) \land (II ↾_{𝑡} u \in SConn \land II ↾_{𝑡} v \in SConn))) \land (w \in v \land {K ↾}_{(u \times \{w\})} \in (((II \times_{t} II) ↾_{𝑡} (u \times \{w\})) Cn C))) \to G (⟨X, Y⟩) \in m$
86	83 85	eqeltrid	$⊢ (((φ \land (G (⟨X, Y⟩) \in m \land t \in S (m))) \land (u \in II \land v \in II) \land ((X \in u \land Y \in v \land u \times v \subseteq G^{-1} [m]) \land (II ↾_{𝑡} u \in SConn \land II ↾_{𝑡} v \in SConn))) \land (w \in v \land {K ↾}_{(u \times \{w\})} \in (((II \times_{t} II) ↾_{𝑡} (u \times \{w\})) Cn C))) \to X G Y \in m$
87	84	simprd	$⊢ (((φ \land (G (⟨X, Y⟩) \in m \land t \in S (m))) \land (u \in II \land v \in II) \land ((X \in u \land Y \in v \land u \times v \subseteq G^{-1} [m]) \land (II ↾_{𝑡} u \in SConn \land II ↾_{𝑡} v \in SConn))) \land (w \in v \land {K ↾}_{(u \times \{w\})} \in (((II \times_{t} II) ↾_{𝑡} (u \times \{w\})) Cn C))) \to t \in S (m)$
88		simpl2l	$⊢ (((φ \land (G (⟨X, Y⟩) \in m \land t \in S (m))) \land (u \in II \land v \in II) \land ((X \in u \land Y \in v \land u \times v \subseteq G^{-1} [m]) \land (II ↾_{𝑡} u \in SConn \land II ↾_{𝑡} v \in SConn))) \land (w \in v \land {K ↾}_{(u \times \{w\})} \in (((II \times_{t} II) ↾_{𝑡} (u \times \{w\})) Cn C))) \to u \in II$
89		simpl2r	$⊢ (((φ \land (G (⟨X, Y⟩) \in m \land t \in S (m))) \land (u \in II \land v \in II) \land ((X \in u \land Y \in v \land u \times v \subseteq G^{-1} [m]) \land (II ↾_{𝑡} u \in SConn \land II ↾_{𝑡} v \in SConn))) \land (w \in v \land {K ↾}_{(u \times \{w\})} \in (((II \times_{t} II) ↾_{𝑡} (u \times \{w\})) Cn C))) \to v \in II$
90		simp3rl	$⊢ ((φ \land (G (⟨X, Y⟩) \in m \land t \in S (m))) \land (u \in II \land v \in II) \land ((X \in u \land Y \in v \land u \times v \subseteq G^{-1} [m]) \land (II ↾_{𝑡} u \in SConn \land II ↾_{𝑡} v \in SConn))) \to II ↾_{𝑡} u \in SConn$
91	90	adantr	$⊢ (((φ \land (G (⟨X, Y⟩) \in m \land t \in S (m))) \land (u \in II \land v \in II) \land ((X \in u \land Y \in v \land u \times v \subseteq G^{-1} [m]) \land (II ↾_{𝑡} u \in SConn \land II ↾_{𝑡} v \in SConn))) \land (w \in v \land {K ↾}_{(u \times \{w\})} \in (((II \times_{t} II) ↾_{𝑡} (u \times \{w\})) Cn C))) \to II ↾_{𝑡} u \in SConn$
92		sconnpconn	$⊢ II ↾_{𝑡} u \in SConn \to II ↾_{𝑡} u \in PConn$
93		pconnconn	$⊢ II ↾_{𝑡} u \in PConn \to II ↾_{𝑡} u \in Conn$
94	91 92 93	3syl	$⊢ (((φ \land (G (⟨X, Y⟩) \in m \land t \in S (m))) \land (u \in II \land v \in II) \land ((X \in u \land Y \in v \land u \times v \subseteq G^{-1} [m]) \land (II ↾_{𝑡} u \in SConn \land II ↾_{𝑡} v \in SConn))) \land (w \in v \land {K ↾}_{(u \times \{w\})} \in (((II \times_{t} II) ↾_{𝑡} (u \times \{w\})) Cn C))) \to II ↾_{𝑡} u \in Conn$
95		simp3rr	$⊢ ((φ \land (G (⟨X, Y⟩) \in m \land t \in S (m))) \land (u \in II \land v \in II) \land ((X \in u \land Y \in v \land u \times v \subseteq G^{-1} [m]) \land (II ↾_{𝑡} u \in SConn \land II ↾_{𝑡} v \in SConn))) \to II ↾_{𝑡} v \in SConn$
96	95	adantr	$⊢ (((φ \land (G (⟨X, Y⟩) \in m \land t \in S (m))) \land (u \in II \land v \in II) \land ((X \in u \land Y \in v \land u \times v \subseteq G^{-1} [m]) \land (II ↾_{𝑡} u \in SConn \land II ↾_{𝑡} v \in SConn))) \land (w \in v \land {K ↾}_{(u \times \{w\})} \in (((II \times_{t} II) ↾_{𝑡} (u \times \{w\})) Cn C))) \to II ↾_{𝑡} v \in SConn$
97		sconnpconn	$⊢ II ↾_{𝑡} v \in SConn \to II ↾_{𝑡} v \in PConn$
98		pconnconn	$⊢ II ↾_{𝑡} v \in PConn \to II ↾_{𝑡} v \in Conn$
99	96 97 98	3syl	$⊢ (((φ \land (G (⟨X, Y⟩) \in m \land t \in S (m))) \land (u \in II \land v \in II) \land ((X \in u \land Y \in v \land u \times v \subseteq G^{-1} [m]) \land (II ↾_{𝑡} u \in SConn \land II ↾_{𝑡} v \in SConn))) \land (w \in v \land {K ↾}_{(u \times \{w\})} \in (((II \times_{t} II) ↾_{𝑡} (u \times \{w\})) Cn C))) \to II ↾_{𝑡} v \in Conn$
100	76	adantr	$⊢ (((φ \land (G (⟨X, Y⟩) \in m \land t \in S (m))) \land (u \in II \land v \in II) \land ((X \in u \land Y \in v \land u \times v \subseteq G^{-1} [m]) \land (II ↾_{𝑡} u \in SConn \land II ↾_{𝑡} v \in SConn))) \land (w \in v \land {K ↾}_{(u \times \{w\})} \in (((II \times_{t} II) ↾_{𝑡} (u \times \{w\})) Cn C))) \to X \in u$
101	77	adantr	$⊢ (((φ \land (G (⟨X, Y⟩) \in m \land t \in S (m))) \land (u \in II \land v \in II) \land ((X \in u \land Y \in v \land u \times v \subseteq G^{-1} [m]) \land (II ↾_{𝑡} u \in SConn \land II ↾_{𝑡} v \in SConn))) \land (w \in v \land {K ↾}_{(u \times \{w\})} \in (((II \times_{t} II) ↾_{𝑡} (u \times \{w\})) Cn C))) \to Y \in v$
102		simp3l3	$⊢ ((φ \land (G (⟨X, Y⟩) \in m \land t \in S (m))) \land (u \in II \land v \in II) \land ((X \in u \land Y \in v \land u \times v \subseteq G^{-1} [m]) \land (II ↾_{𝑡} u \in SConn \land II ↾_{𝑡} v \in SConn))) \to u \times v \subseteq G^{-1} [m]$
103	102	adantr	$⊢ (((φ \land (G (⟨X, Y⟩) \in m \land t \in S (m))) \land (u \in II \land v \in II) \land ((X \in u \land Y \in v \land u \times v \subseteq G^{-1} [m]) \land (II ↾_{𝑡} u \in SConn \land II ↾_{𝑡} v \in SConn))) \land (w \in v \land {K ↾}_{(u \times \{w\})} \in (((II \times_{t} II) ↾_{𝑡} (u \times \{w\})) Cn C))) \to u \times v \subseteq G^{-1} [m]$
104		simprl	$⊢ (((φ \land (G (⟨X, Y⟩) \in m \land t \in S (m))) \land (u \in II \land v \in II) \land ((X \in u \land Y \in v \land u \times v \subseteq G^{-1} [m]) \land (II ↾_{𝑡} u \in SConn \land II ↾_{𝑡} v \in SConn))) \land (w \in v \land {K ↾}_{(u \times \{w\})} \in (((II \times_{t} II) ↾_{𝑡} (u \times \{w\})) Cn C))) \to w \in v$
105		simprr	$⊢ (((φ \land (G (⟨X, Y⟩) \in m \land t \in S (m))) \land (u \in II \land v \in II) \land ((X \in u \land Y \in v \land u \times v \subseteq G^{-1} [m]) \land (II ↾_{𝑡} u \in SConn \land II ↾_{𝑡} v \in SConn))) \land (w \in v \land {K ↾}_{(u \times \{w\})} \in (((II \times_{t} II) ↾_{𝑡} (u \times \{w\})) Cn C))) \to {K ↾}_{(u \times \{w\})} \in (((II \times_{t} II) ↾_{𝑡} (u \times \{w\})) Cn C)$
106		eqid	$⊢ (ι b \in t \| X K Y \in b) = (ι b \in t \| X K Y \in b)$
107	1 79 80 81 82 6 7 8 86 87 88 89 94 99 100 101 103 104 105 106	cvmlift2lem9	$⊢ (((φ \land (G (⟨X, Y⟩) \in m \land t \in S (m))) \land (u \in II \land v \in II) \land ((X \in u \land Y \in v \land u \times v \subseteq G^{-1} [m]) \land (II ↾_{𝑡} u \in SConn \land II ↾_{𝑡} v \in SConn))) \land (w \in v \land {K ↾}_{(u \times \{w\})} \in (((II \times_{t} II) ↾_{𝑡} (u \times \{w\})) Cn C))) \to {K ↾}_{(u \times v)} \in (((II \times_{t} II) ↾_{𝑡} (u \times v)) Cn C)$
108	107	rexlimdvaa	$⊢ ((φ \land (G (⟨X, Y⟩) \in m \land t \in S (m))) \land (u \in II \land v \in II) \land ((X \in u \land Y \in v \land u \times v \subseteq G^{-1} [m]) \land (II ↾_{𝑡} u \in SConn \land II ↾_{𝑡} v \in SConn))) \to (\exists w \in v {K ↾}_{(u \times \{w\})} \in (((II \times_{t} II) ↾_{𝑡} (u \times \{w\})) Cn C) \to {K ↾}_{(u \times v)} \in (((II \times_{t} II) ↾_{𝑡} (u \times v)) Cn C))$
109	76 77 108	3jca	$⊢ ((φ \land (G (⟨X, Y⟩) \in m \land t \in S (m))) \land (u \in II \land v \in II) \land ((X \in u \land Y \in v \land u \times v \subseteq G^{-1} [m]) \land (II ↾_{𝑡} u \in SConn \land II ↾_{𝑡} v \in SConn))) \to (X \in u \land Y \in v \land (\exists w \in v {K ↾}_{(u \times \{w\})} \in (((II \times_{t} II) ↾_{𝑡} (u \times \{w\})) Cn C) \to {K ↾}_{(u \times v)} \in (((II \times_{t} II) ↾_{𝑡} (u \times v)) Cn C)))$
110	109	3expia	$⊢ ((φ \land (G (⟨X, Y⟩) \in m \land t \in S (m))) \land (u \in II \land v \in II)) \to (((X \in u \land Y \in v \land u \times v \subseteq G^{-1} [m]) \land (II ↾_{𝑡} u \in SConn \land II ↾_{𝑡} v \in SConn)) \to (X \in u \land Y \in v \land (\exists w \in v {K ↾}_{(u \times \{w\})} \in (((II \times_{t} II) ↾_{𝑡} (u \times \{w\})) Cn C) \to {K ↾}_{(u \times v)} \in (((II \times_{t} II) ↾_{𝑡} (u \times v)) Cn C))))$
111	110	reximdvva	$⊢ (φ \land (G (⟨X, Y⟩) \in m \land t \in S (m))) \to (\exists u \in II \exists v \in II ((X \in u \land Y \in v \land u \times v \subseteq G^{-1} [m]) \land (II ↾_{𝑡} u \in SConn \land II ↾_{𝑡} v \in SConn)) \to \exists u \in II \exists v \in II (X \in u \land Y \in v \land (\exists w \in v {K ↾}_{(u \times \{w\})} \in (((II \times_{t} II) ↾_{𝑡} (u \times \{w\})) Cn C) \to {K ↾}_{(u \times v)} \in (((II \times_{t} II) ↾_{𝑡} (u \times v)) Cn C))))$
112	75 111	mpd	$⊢ (φ \land (G (⟨X, Y⟩) \in m \land t \in S (m))) \to \exists u \in II \exists v \in II (X \in u \land Y \in v \land (\exists w \in v {K ↾}_{(u \times \{w\})} \in (((II \times_{t} II) ↾_{𝑡} (u \times \{w\})) Cn C) \to {K ↾}_{(u \times v)} \in (((II \times_{t} II) ↾_{𝑡} (u \times v)) Cn C)))$
113	112	expr	$⊢ (φ \land G (⟨X, Y⟩) \in m) \to (t \in S (m) \to \exists u \in II \exists v \in II (X \in u \land Y \in v \land (\exists w \in v {K ↾}_{(u \times \{w\})} \in (((II \times_{t} II) ↾_{𝑡} (u \times \{w\})) Cn C) \to {K ↾}_{(u \times v)} \in (((II \times_{t} II) ↾_{𝑡} (u \times v)) Cn C))))$
114	113	exlimdv	$⊢ (φ \land G (⟨X, Y⟩) \in m) \to (\exists t t \in S (m) \to \exists u \in II \exists v \in II (X \in u \land Y \in v \land (\exists w \in v {K ↾}_{(u \times \{w\})} \in (((II \times_{t} II) ↾_{𝑡} (u \times \{w\})) Cn C) \to {K ↾}_{(u \times v)} \in (((II \times_{t} II) ↾_{𝑡} (u \times v)) Cn C))))$
115	21 114	syl5bi	$⊢ (φ \land G (⟨X, Y⟩) \in m) \to (S (m) \neq \emptyset \to \exists u \in II \exists v \in II (X \in u \land Y \in v \land (\exists w \in v {K ↾}_{(u \times \{w\})} \in (((II \times_{t} II) ↾_{𝑡} (u \times \{w\})) Cn C) \to {K ↾}_{(u \times v)} \in (((II \times_{t} II) ↾_{𝑡} (u \times v)) Cn C))))$
116	115	expimpd	$⊢ φ \to ((G (⟨X, Y⟩) \in m \land S (m) \neq \emptyset) \to \exists u \in II \exists v \in II (X \in u \land Y \in v \land (\exists w \in v {K ↾}_{(u \times \{w\})} \in (((II \times_{t} II) ↾_{𝑡} (u \times \{w\})) Cn C) \to {K ↾}_{(u \times v)} \in (((II \times_{t} II) ↾_{𝑡} (u \times v)) Cn C))))$
117	116	rexlimdvw	$⊢ φ \to (\exists m \in J (G (⟨X, Y⟩) \in m \land S (m) \neq \emptyset) \to \exists u \in II \exists v \in II (X \in u \land Y \in v \land (\exists w \in v {K ↾}_{(u \times \{w\})} \in (((II \times_{t} II) ↾_{𝑡} (u \times \{w\})) Cn C) \to {K ↾}_{(u \times v)} \in (((II \times_{t} II) ↾_{𝑡} (u \times v)) Cn C))))$
118	20 117	mpd	$⊢ φ \to \exists u \in II \exists v \in II (X \in u \land Y \in v \land (\exists w \in v {K ↾}_{(u \times \{w\})} \in (((II \times_{t} II) ↾_{𝑡} (u \times \{w\})) Cn C) \to {K ↾}_{(u \times v)} \in (((II \times_{t} II) ↾_{𝑡} (u \times v)) Cn C)))$

Metamath Proof Explorer

Theorem cvmlift2lem10

Proof