txpconn

Description: The topological product of two path-connected spaces is path-connected. (Contributed by Mario Carneiro, 12-Feb-2015)

		Ref	Expression
	Assertion	txpconn	$⊢ (R \in PConn \land S \in PConn) \to R \times_{t} S \in PConn$

Proof

Step	Hyp	Ref	Expression
1		pconntop	$⊢ R \in PConn \to R \in Top$
2		pconntop	$⊢ S \in PConn \to S \in Top$
3		txtop	$⊢ (R \in Top \land S \in Top) \to R \times_{t} S \in Top$
4	1 2 3	syl2an	$⊢ (R \in PConn \land S \in PConn) \to R \times_{t} S \in Top$
5		an6	$⊢ ((R \in PConn \land x \in ⋃ R \land z \in ⋃ R) \land (S \in PConn \land y \in ⋃ S \land w \in ⋃ S)) \leftrightarrow ((R \in PConn \land S \in PConn) \land (x \in ⋃ R \land y \in ⋃ S) \land (z \in ⋃ R \land w \in ⋃ S))$
6		eqid	$⊢ ⋃ R = ⋃ R$
7	6	pconncn	$⊢ (R \in PConn \land x \in ⋃ R \land z \in ⋃ R) \to \exists g \in (II Cn R) (g (0) = x \land g (1) = z)$
8		eqid	$⊢ ⋃ S = ⋃ S$
9	8	pconncn	$⊢ (S \in PConn \land y \in ⋃ S \land w \in ⋃ S) \to \exists h \in (II Cn S) (h (0) = y \land h (1) = w)$
10	7 9	anim12i	$⊢ ((R \in PConn \land x \in ⋃ R \land z \in ⋃ R) \land (S \in PConn \land y \in ⋃ S \land w \in ⋃ S)) \to (\exists g \in (II Cn R) (g (0) = x \land g (1) = z) \land \exists h \in (II Cn S) (h (0) = y \land h (1) = w))$
11	5 10	sylbir	$⊢ ((R \in PConn \land S \in PConn) \land (x \in ⋃ R \land y \in ⋃ S) \land (z \in ⋃ R \land w \in ⋃ S)) \to (\exists g \in (II Cn R) (g (0) = x \land g (1) = z) \land \exists h \in (II Cn S) (h (0) = y \land h (1) = w))$
12		reeanv	$⊢ \exists g \in (II Cn R) \exists h \in (II Cn S) ((g (0) = x \land g (1) = z) \land (h (0) = y \land h (1) = w)) \leftrightarrow (\exists g \in (II Cn R) (g (0) = x \land g (1) = z) \land \exists h \in (II Cn S) (h (0) = y \land h (1) = w))$
13	11 12	sylibr	$⊢ ((R \in PConn \land S \in PConn) \land (x \in ⋃ R \land y \in ⋃ S) \land (z \in ⋃ R \land w \in ⋃ S)) \to \exists g \in (II Cn R) \exists h \in (II Cn S) ((g (0) = x \land g (1) = z) \land (h (0) = y \land h (1) = w))$
14		iiuni	$⊢ [0, 1] = ⋃ II$
15		eqid	$⊢ (t \in [0, 1] ⟼ ⟨g (t), h (t)⟩) = (t \in [0, 1] ⟼ ⟨g (t), h (t)⟩)$
16	14 15	txcnmpt	$⊢ (g \in (II Cn R) \land h \in (II Cn S)) \to (t \in [0, 1] ⟼ ⟨g (t), h (t)⟩) \in (II Cn (R \times_{t} S))$
17	16	ad2antrl	$⊢ (((R \in PConn \land S \in PConn) \land (x \in ⋃ R \land y \in ⋃ S) \land (z \in ⋃ R \land w \in ⋃ S)) \land ((g \in (II Cn R) \land h \in (II Cn S)) \land ((g (0) = x \land g (1) = z) \land (h (0) = y \land h (1) = w)))) \to (t \in [0, 1] ⟼ ⟨g (t), h (t)⟩) \in (II Cn (R \times_{t} S))$
18		0elunit	$⊢ 0 \in [0, 1]$
19		fveq2	$⊢ t = 0 \to g (t) = g (0)$
20		fveq2	$⊢ t = 0 \to h (t) = h (0)$
21	19 20	opeq12d	$⊢ t = 0 \to ⟨g (t), h (t)⟩ = ⟨g (0), h (0)⟩$
22		opex	$⊢ ⟨g (0), h (0)⟩ \in V$
23	21 15 22	fvmpt	$⊢ 0 \in [0, 1] \to (t \in [0, 1] ⟼ ⟨g (t), h (t)⟩) (0) = ⟨g (0), h (0)⟩$
24	18 23	ax-mp	$⊢ (t \in [0, 1] ⟼ ⟨g (t), h (t)⟩) (0) = ⟨g (0), h (0)⟩$
25		simprrl	$⊢ (((R \in PConn \land S \in PConn) \land (x \in ⋃ R \land y \in ⋃ S) \land (z \in ⋃ R \land w \in ⋃ S)) \land ((g \in (II Cn R) \land h \in (II Cn S)) \land ((g (0) = x \land g (1) = z) \land (h (0) = y \land h (1) = w)))) \to (g (0) = x \land g (1) = z)$
26	25	simpld	$⊢ (((R \in PConn \land S \in PConn) \land (x \in ⋃ R \land y \in ⋃ S) \land (z \in ⋃ R \land w \in ⋃ S)) \land ((g \in (II Cn R) \land h \in (II Cn S)) \land ((g (0) = x \land g (1) = z) \land (h (0) = y \land h (1) = w)))) \to g (0) = x$
27		simprrr	$⊢ (((R \in PConn \land S \in PConn) \land (x \in ⋃ R \land y \in ⋃ S) \land (z \in ⋃ R \land w \in ⋃ S)) \land ((g \in (II Cn R) \land h \in (II Cn S)) \land ((g (0) = x \land g (1) = z) \land (h (0) = y \land h (1) = w)))) \to (h (0) = y \land h (1) = w)$
28	27	simpld	$⊢ (((R \in PConn \land S \in PConn) \land (x \in ⋃ R \land y \in ⋃ S) \land (z \in ⋃ R \land w \in ⋃ S)) \land ((g \in (II Cn R) \land h \in (II Cn S)) \land ((g (0) = x \land g (1) = z) \land (h (0) = y \land h (1) = w)))) \to h (0) = y$
29	26 28	opeq12d	$⊢ (((R \in PConn \land S \in PConn) \land (x \in ⋃ R \land y \in ⋃ S) \land (z \in ⋃ R \land w \in ⋃ S)) \land ((g \in (II Cn R) \land h \in (II Cn S)) \land ((g (0) = x \land g (1) = z) \land (h (0) = y \land h (1) = w)))) \to ⟨g (0), h (0)⟩ = ⟨x, y⟩$
30	24 29	eqtrid	$⊢ (((R \in PConn \land S \in PConn) \land (x \in ⋃ R \land y \in ⋃ S) \land (z \in ⋃ R \land w \in ⋃ S)) \land ((g \in (II Cn R) \land h \in (II Cn S)) \land ((g (0) = x \land g (1) = z) \land (h (0) = y \land h (1) = w)))) \to (t \in [0, 1] ⟼ ⟨g (t), h (t)⟩) (0) = ⟨x, y⟩$
31		1elunit	$⊢ 1 \in [0, 1]$
32		fveq2	$⊢ t = 1 \to g (t) = g (1)$
33		fveq2	$⊢ t = 1 \to h (t) = h (1)$
34	32 33	opeq12d	$⊢ t = 1 \to ⟨g (t), h (t)⟩ = ⟨g (1), h (1)⟩$
35		opex	$⊢ ⟨g (1), h (1)⟩ \in V$
36	34 15 35	fvmpt	$⊢ 1 \in [0, 1] \to (t \in [0, 1] ⟼ ⟨g (t), h (t)⟩) (1) = ⟨g (1), h (1)⟩$
37	31 36	ax-mp	$⊢ (t \in [0, 1] ⟼ ⟨g (t), h (t)⟩) (1) = ⟨g (1), h (1)⟩$
38	25	simprd	$⊢ (((R \in PConn \land S \in PConn) \land (x \in ⋃ R \land y \in ⋃ S) \land (z \in ⋃ R \land w \in ⋃ S)) \land ((g \in (II Cn R) \land h \in (II Cn S)) \land ((g (0) = x \land g (1) = z) \land (h (0) = y \land h (1) = w)))) \to g (1) = z$
39	27	simprd	$⊢ (((R \in PConn \land S \in PConn) \land (x \in ⋃ R \land y \in ⋃ S) \land (z \in ⋃ R \land w \in ⋃ S)) \land ((g \in (II Cn R) \land h \in (II Cn S)) \land ((g (0) = x \land g (1) = z) \land (h (0) = y \land h (1) = w)))) \to h (1) = w$
40	38 39	opeq12d	$⊢ (((R \in PConn \land S \in PConn) \land (x \in ⋃ R \land y \in ⋃ S) \land (z \in ⋃ R \land w \in ⋃ S)) \land ((g \in (II Cn R) \land h \in (II Cn S)) \land ((g (0) = x \land g (1) = z) \land (h (0) = y \land h (1) = w)))) \to ⟨g (1), h (1)⟩ = ⟨z, w⟩$
41	37 40	eqtrid	$⊢ (((R \in PConn \land S \in PConn) \land (x \in ⋃ R \land y \in ⋃ S) \land (z \in ⋃ R \land w \in ⋃ S)) \land ((g \in (II Cn R) \land h \in (II Cn S)) \land ((g (0) = x \land g (1) = z) \land (h (0) = y \land h (1) = w)))) \to (t \in [0, 1] ⟼ ⟨g (t), h (t)⟩) (1) = ⟨z, w⟩$
42		fveq1	$⊢ f = (t \in [0, 1] ⟼ ⟨g (t), h (t)⟩) \to f (0) = (t \in [0, 1] ⟼ ⟨g (t), h (t)⟩) (0)$
43	42	eqeq1d	$⊢ f = (t \in [0, 1] ⟼ ⟨g (t), h (t)⟩) \to (f (0) = ⟨x, y⟩ \leftrightarrow (t \in [0, 1] ⟼ ⟨g (t), h (t)⟩) (0) = ⟨x, y⟩)$
44		fveq1	$⊢ f = (t \in [0, 1] ⟼ ⟨g (t), h (t)⟩) \to f (1) = (t \in [0, 1] ⟼ ⟨g (t), h (t)⟩) (1)$
45	44	eqeq1d	$⊢ f = (t \in [0, 1] ⟼ ⟨g (t), h (t)⟩) \to (f (1) = ⟨z, w⟩ \leftrightarrow (t \in [0, 1] ⟼ ⟨g (t), h (t)⟩) (1) = ⟨z, w⟩)$
46	43 45	anbi12d	$⊢ f = (t \in [0, 1] ⟼ ⟨g (t), h (t)⟩) \to ((f (0) = ⟨x, y⟩ \land f (1) = ⟨z, w⟩) \leftrightarrow ((t \in [0, 1] ⟼ ⟨g (t), h (t)⟩) (0) = ⟨x, y⟩ \land (t \in [0, 1] ⟼ ⟨g (t), h (t)⟩) (1) = ⟨z, w⟩))$
47	46	rspcev	$⊢ ((t \in [0, 1] ⟼ ⟨g (t), h (t)⟩) \in (II Cn (R \times_{t} S)) \land ((t \in [0, 1] ⟼ ⟨g (t), h (t)⟩) (0) = ⟨x, y⟩ \land (t \in [0, 1] ⟼ ⟨g (t), h (t)⟩) (1) = ⟨z, w⟩)) \to \exists f \in (II Cn (R \times_{t} S)) (f (0) = ⟨x, y⟩ \land f (1) = ⟨z, w⟩)$
48	17 30 41 47	syl12anc	$⊢ (((R \in PConn \land S \in PConn) \land (x \in ⋃ R \land y \in ⋃ S) \land (z \in ⋃ R \land w \in ⋃ S)) \land ((g \in (II Cn R) \land h \in (II Cn S)) \land ((g (0) = x \land g (1) = z) \land (h (0) = y \land h (1) = w)))) \to \exists f \in (II Cn (R \times_{t} S)) (f (0) = ⟨x, y⟩ \land f (1) = ⟨z, w⟩)$
49	48	expr	$⊢ (((R \in PConn \land S \in PConn) \land (x \in ⋃ R \land y \in ⋃ S) \land (z \in ⋃ R \land w \in ⋃ S)) \land (g \in (II Cn R) \land h \in (II Cn S))) \to (((g (0) = x \land g (1) = z) \land (h (0) = y \land h (1) = w)) \to \exists f \in (II Cn (R \times_{t} S)) (f (0) = ⟨x, y⟩ \land f (1) = ⟨z, w⟩))$
50	49	rexlimdvva	$⊢ ((R \in PConn \land S \in PConn) \land (x \in ⋃ R \land y \in ⋃ S) \land (z \in ⋃ R \land w \in ⋃ S)) \to (\exists g \in (II Cn R) \exists h \in (II Cn S) ((g (0) = x \land g (1) = z) \land (h (0) = y \land h (1) = w)) \to \exists f \in (II Cn (R \times_{t} S)) (f (0) = ⟨x, y⟩ \land f (1) = ⟨z, w⟩))$
51	13 50	mpd	$⊢ ((R \in PConn \land S \in PConn) \land (x \in ⋃ R \land y \in ⋃ S) \land (z \in ⋃ R \land w \in ⋃ S)) \to \exists f \in (II Cn (R \times_{t} S)) (f (0) = ⟨x, y⟩ \land f (1) = ⟨z, w⟩)$
52	51	3expa	$⊢ (((R \in PConn \land S \in PConn) \land (x \in ⋃ R \land y \in ⋃ S)) \land (z \in ⋃ R \land w \in ⋃ S)) \to \exists f \in (II Cn (R \times_{t} S)) (f (0) = ⟨x, y⟩ \land f (1) = ⟨z, w⟩)$
53	52	ralrimivva	$⊢ ((R \in PConn \land S \in PConn) \land (x \in ⋃ R \land y \in ⋃ S)) \to \forall z \in ⋃ R \forall w \in ⋃ S \exists f \in (II Cn (R \times_{t} S)) (f (0) = ⟨x, y⟩ \land f (1) = ⟨z, w⟩)$
54	53	ralrimivva	$⊢ (R \in PConn \land S \in PConn) \to \forall x \in ⋃ R \forall y \in ⋃ S \forall z \in ⋃ R \forall w \in ⋃ S \exists f \in (II Cn (R \times_{t} S)) (f (0) = ⟨x, y⟩ \land f (1) = ⟨z, w⟩)$
55		eqeq2	$⊢ v = ⟨z, w⟩ \to (f (1) = v \leftrightarrow f (1) = ⟨z, w⟩)$
56	55	anbi2d	$⊢ v = ⟨z, w⟩ \to ((f (0) = u \land f (1) = v) \leftrightarrow (f (0) = u \land f (1) = ⟨z, w⟩))$
57	56	rexbidv	$⊢ v = ⟨z, w⟩ \to (\exists f \in (II Cn (R \times_{t} S)) (f (0) = u \land f (1) = v) \leftrightarrow \exists f \in (II Cn (R \times_{t} S)) (f (0) = u \land f (1) = ⟨z, w⟩))$
58	57	ralxp	$⊢ \forall v \in (⋃ R \times ⋃ S) \exists f \in (II Cn (R \times_{t} S)) (f (0) = u \land f (1) = v) \leftrightarrow \forall z \in ⋃ R \forall w \in ⋃ S \exists f \in (II Cn (R \times_{t} S)) (f (0) = u \land f (1) = ⟨z, w⟩)$
59		eqeq2	$⊢ u = ⟨x, y⟩ \to (f (0) = u \leftrightarrow f (0) = ⟨x, y⟩)$
60	59	anbi1d	$⊢ u = ⟨x, y⟩ \to ((f (0) = u \land f (1) = ⟨z, w⟩) \leftrightarrow (f (0) = ⟨x, y⟩ \land f (1) = ⟨z, w⟩))$
61	60	rexbidv	$⊢ u = ⟨x, y⟩ \to (\exists f \in (II Cn (R \times_{t} S)) (f (0) = u \land f (1) = ⟨z, w⟩) \leftrightarrow \exists f \in (II Cn (R \times_{t} S)) (f (0) = ⟨x, y⟩ \land f (1) = ⟨z, w⟩))$
62	61	2ralbidv	$⊢ u = ⟨x, y⟩ \to (\forall z \in ⋃ R \forall w \in ⋃ S \exists f \in (II Cn (R \times_{t} S)) (f (0) = u \land f (1) = ⟨z, w⟩) \leftrightarrow \forall z \in ⋃ R \forall w \in ⋃ S \exists f \in (II Cn (R \times_{t} S)) (f (0) = ⟨x, y⟩ \land f (1) = ⟨z, w⟩))$
63	58 62	bitrid	$⊢ u = ⟨x, y⟩ \to (\forall v \in (⋃ R \times ⋃ S) \exists f \in (II Cn (R \times_{t} S)) (f (0) = u \land f (1) = v) \leftrightarrow \forall z \in ⋃ R \forall w \in ⋃ S \exists f \in (II Cn (R \times_{t} S)) (f (0) = ⟨x, y⟩ \land f (1) = ⟨z, w⟩))$
64	63	ralxp	$⊢ \forall u \in (⋃ R \times ⋃ S) \forall v \in (⋃ R \times ⋃ S) \exists f \in (II Cn (R \times_{t} S)) (f (0) = u \land f (1) = v) \leftrightarrow \forall x \in ⋃ R \forall y \in ⋃ S \forall z \in ⋃ R \forall w \in ⋃ S \exists f \in (II Cn (R \times_{t} S)) (f (0) = ⟨x, y⟩ \land f (1) = ⟨z, w⟩)$
65	54 64	sylibr	$⊢ (R \in PConn \land S \in PConn) \to \forall u \in (⋃ R \times ⋃ S) \forall v \in (⋃ R \times ⋃ S) \exists f \in (II Cn (R \times_{t} S)) (f (0) = u \land f (1) = v)$
66	6 8	txuni	$⊢ (R \in Top \land S \in Top) \to ⋃ R \times ⋃ S = ⋃ (R \times_{t} S)$
67	1 2 66	syl2an	$⊢ (R \in PConn \land S \in PConn) \to ⋃ R \times ⋃ S = ⋃ (R \times_{t} S)$
68	67	raleqdv	$⊢ (R \in PConn \land S \in PConn) \to (\forall v \in (⋃ R \times ⋃ S) \exists f \in (II Cn (R \times_{t} S)) (f (0) = u \land f (1) = v) \leftrightarrow \forall v \in ⋃ (R \times_{t} S) \exists f \in (II Cn (R \times_{t} S)) (f (0) = u \land f (1) = v))$
69	67 68	raleqbidv	$⊢ (R \in PConn \land S \in PConn) \to (\forall u \in (⋃ R \times ⋃ S) \forall v \in (⋃ R \times ⋃ S) \exists f \in (II Cn (R \times_{t} S)) (f (0) = u \land f (1) = v) \leftrightarrow \forall u \in ⋃ (R \times_{t} S) \forall v \in ⋃ (R \times_{t} S) \exists f \in (II Cn (R \times_{t} S)) (f (0) = u \land f (1) = v))$
70	65 69	mpbid	$⊢ (R \in PConn \land S \in PConn) \to \forall u \in ⋃ (R \times_{t} S) \forall v \in ⋃ (R \times_{t} S) \exists f \in (II Cn (R \times_{t} S)) (f (0) = u \land f (1) = v)$
71		eqid	$⊢ ⋃ (R \times_{t} S) = ⋃ (R \times_{t} S)$
72	71	ispconn	$⊢ R \times_{t} S \in PConn \leftrightarrow (R \times_{t} S \in Top \land \forall u \in ⋃ (R \times_{t} S) \forall v \in ⋃ (R \times_{t} S) \exists f \in (II Cn (R \times_{t} S)) (f (0) = u \land f (1) = v))$
73	4 70 72	sylanbrc	$⊢ (R \in PConn \land S \in PConn) \to R \times_{t} S \in PConn$

Metamath Proof Explorer

Theorem txpconn

Proof