cvmlift2lem1

		Ref	Expression
	Assertion	cvmlift2lem1	$⊢ \forall y \in [0, 1] \exists u \in nei (II) (\{y\}) (u \times \{x\} \subseteq M \leftrightarrow u \times \{t\} \subseteq M) \to ([0, 1] \times \{x\} \subseteq M \to [0, 1] \times \{t\} \subseteq M)$

Proof

Step	Hyp	Ref	Expression
1		biimp	$⊢ (u \times \{x\} \subseteq M \leftrightarrow u \times \{t\} \subseteq M) \to (u \times \{x\} \subseteq M \to u \times \{t\} \subseteq M)$
2		iitop	$⊢ II \in Top$
3		iiuni	$⊢ [0, 1] = ⋃ II$
4	3	neii1	$⊢ (II \in Top \land u \in nei (II) (\{y\})) \to u \subseteq [0, 1]$
5	2 4	mpan	$⊢ u \in nei (II) (\{y\}) \to u \subseteq [0, 1]$
6	5	adantl	$⊢ ([0, 1] \times \{x\} \subseteq M \land u \in nei (II) (\{y\})) \to u \subseteq [0, 1]$
7		xpss1	$⊢ u \subseteq [0, 1] \to u \times \{x\} \subseteq [0, 1] \times \{x\}$
8	6 7	syl	$⊢ ([0, 1] \times \{x\} \subseteq M \land u \in nei (II) (\{y\})) \to u \times \{x\} \subseteq [0, 1] \times \{x\}$
9		simpl	$⊢ ([0, 1] \times \{x\} \subseteq M \land u \in nei (II) (\{y\})) \to [0, 1] \times \{x\} \subseteq M$
10	8 9	sstrd	$⊢ ([0, 1] \times \{x\} \subseteq M \land u \in nei (II) (\{y\})) \to u \times \{x\} \subseteq M$
11		ssnei	$⊢ (II \in Top \land u \in nei (II) (\{y\})) \to \{y\} \subseteq u$
12	2 11	mpan	$⊢ u \in nei (II) (\{y\}) \to \{y\} \subseteq u$
13	12	adantl	$⊢ ([0, 1] \times \{x\} \subseteq M \land u \in nei (II) (\{y\})) \to \{y\} \subseteq u$
14		vex	$⊢ y \in V$
15	14	snss	$⊢ y \in u \leftrightarrow \{y\} \subseteq u$
16	13 15	sylibr	$⊢ ([0, 1] \times \{x\} \subseteq M \land u \in nei (II) (\{y\})) \to y \in u$
17		vsnid	$⊢ t \in \{t\}$
18		opelxpi	$⊢ (y \in u \land t \in \{t\}) \to ⟨y, t⟩ \in (u \times \{t\})$
19	16 17 18	sylancl	$⊢ ([0, 1] \times \{x\} \subseteq M \land u \in nei (II) (\{y\})) \to ⟨y, t⟩ \in (u \times \{t\})$
20		ssel	$⊢ u \times \{t\} \subseteq M \to (⟨y, t⟩ \in (u \times \{t\}) \to ⟨y, t⟩ \in M)$
21	19 20	syl5com	$⊢ ([0, 1] \times \{x\} \subseteq M \land u \in nei (II) (\{y\})) \to (u \times \{t\} \subseteq M \to ⟨y, t⟩ \in M)$
22	10 21	embantd	$⊢ ([0, 1] \times \{x\} \subseteq M \land u \in nei (II) (\{y\})) \to ((u \times \{x\} \subseteq M \to u \times \{t\} \subseteq M) \to ⟨y, t⟩ \in M)$
23	1 22	syl5	$⊢ ([0, 1] \times \{x\} \subseteq M \land u \in nei (II) (\{y\})) \to ((u \times \{x\} \subseteq M \leftrightarrow u \times \{t\} \subseteq M) \to ⟨y, t⟩ \in M)$
24	23	rexlimdva	$⊢ [0, 1] \times \{x\} \subseteq M \to (\exists u \in nei (II) (\{y\}) (u \times \{x\} \subseteq M \leftrightarrow u \times \{t\} \subseteq M) \to ⟨y, t⟩ \in M)$
25	24	ralimdv	$⊢ [0, 1] \times \{x\} \subseteq M \to (\forall y \in [0, 1] \exists u \in nei (II) (\{y\}) (u \times \{x\} \subseteq M \leftrightarrow u \times \{t\} \subseteq M) \to \forall y \in [0, 1] ⟨y, t⟩ \in M)$
26	25	com12	$⊢ \forall y \in [0, 1] \exists u \in nei (II) (\{y\}) (u \times \{x\} \subseteq M \leftrightarrow u \times \{t\} \subseteq M) \to ([0, 1] \times \{x\} \subseteq M \to \forall y \in [0, 1] ⟨y, t⟩ \in M)$
27		dfss3	$⊢ [0, 1] \times \{t\} \subseteq M \leftrightarrow \forall z \in ([0, 1] \times \{t\}) z \in M$
28		eleq1	$⊢ z = ⟨y, u⟩ \to (z \in M \leftrightarrow ⟨y, u⟩ \in M)$
29	28	ralxp	$⊢ \forall z \in ([0, 1] \times \{t\}) z \in M \leftrightarrow \forall y \in [0, 1] \forall u \in \{t\} ⟨y, u⟩ \in M$
30		vex	$⊢ t \in V$
31		opeq2	$⊢ u = t \to ⟨y, u⟩ = ⟨y, t⟩$
32	31	eleq1d	$⊢ u = t \to (⟨y, u⟩ \in M \leftrightarrow ⟨y, t⟩ \in M)$
33	30 32	ralsn	$⊢ \forall u \in \{t\} ⟨y, u⟩ \in M \leftrightarrow ⟨y, t⟩ \in M$
34	33	ralbii	$⊢ \forall y \in [0, 1] \forall u \in \{t\} ⟨y, u⟩ \in M \leftrightarrow \forall y \in [0, 1] ⟨y, t⟩ \in M$
35	27 29 34	3bitri	$⊢ [0, 1] \times \{t\} \subseteq M \leftrightarrow \forall y \in [0, 1] ⟨y, t⟩ \in M$
36	26 35	imbitrrdi	$⊢ \forall y \in [0, 1] \exists u \in nei (II) (\{y\}) (u \times \{x\} \subseteq M \leftrightarrow u \times \{t\} \subseteq M) \to ([0, 1] \times \{x\} \subseteq M \to [0, 1] \times \{t\} \subseteq M)$

Metamath Proof Explorer

Theorem cvmlift2lem1

Proof