txsconn

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

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

Proof

Step	Hyp	Ref	Expression
1		sconnpconn	$⊢ R \in SConn \to R \in PConn$
2		sconnpconn	$⊢ S \in SConn \to S \in PConn$
3		txpconn	$⊢ (R \in PConn \land S \in PConn) \to R \times_{t} S \in PConn$
4	1 2 3	syl2an	$⊢ (R \in SConn \land S \in SConn) \to R \times_{t} S \in PConn$
5		simpll	$⊢ ((R \in SConn \land S \in SConn) \land (f \in (II Cn (R \times_{t} S)) \land f (0) = f (1))) \to R \in SConn$
6		simprl	$⊢ ((R \in SConn \land S \in SConn) \land (f \in (II Cn (R \times_{t} S)) \land f (0) = f (1))) \to f \in (II Cn (R \times_{t} S))$
7		sconntop	$⊢ R \in SConn \to R \in Top$
8	7	ad2antrr	$⊢ ((R \in SConn \land S \in SConn) \land (f \in (II Cn (R \times_{t} S)) \land f (0) = f (1))) \to R \in Top$
9		eqid	$⊢ ⋃ R = ⋃ R$
10	9	toptopon	$⊢ R \in Top \leftrightarrow R \in TopOn (⋃ R)$
11	8 10	sylib	$⊢ ((R \in SConn \land S \in SConn) \land (f \in (II Cn (R \times_{t} S)) \land f (0) = f (1))) \to R \in TopOn (⋃ R)$
12		sconntop	$⊢ S \in SConn \to S \in Top$
13	12	ad2antlr	$⊢ ((R \in SConn \land S \in SConn) \land (f \in (II Cn (R \times_{t} S)) \land f (0) = f (1))) \to S \in Top$
14		eqid	$⊢ ⋃ S = ⋃ S$
15	14	toptopon	$⊢ S \in Top \leftrightarrow S \in TopOn (⋃ S)$
16	13 15	sylib	$⊢ ((R \in SConn \land S \in SConn) \land (f \in (II Cn (R \times_{t} S)) \land f (0) = f (1))) \to S \in TopOn (⋃ S)$
17		tx1cn	$⊢ (R \in TopOn (⋃ R) \land S \in TopOn (⋃ S)) \to {1^{st} ↾}_{(⋃ R \times ⋃ S)} \in ((R \times_{t} S) Cn R)$
18	11 16 17	syl2anc	$⊢ ((R \in SConn \land S \in SConn) \land (f \in (II Cn (R \times_{t} S)) \land f (0) = f (1))) \to {1^{st} ↾}_{(⋃ R \times ⋃ S)} \in ((R \times_{t} S) Cn R)$
19		cnco	$⊢ (f \in (II Cn (R \times_{t} S)) \land {1^{st} ↾}_{(⋃ R \times ⋃ S)} \in ((R \times_{t} S) Cn R)) \to ({1^{st} ↾}_{(⋃ R \times ⋃ S)}) \circ f \in (II Cn R)$
20	6 18 19	syl2anc	$⊢ ((R \in SConn \land S \in SConn) \land (f \in (II Cn (R \times_{t} S)) \land f (0) = f (1))) \to ({1^{st} ↾}_{(⋃ R \times ⋃ S)}) \circ f \in (II Cn R)$
21		simprr	$⊢ ((R \in SConn \land S \in SConn) \land (f \in (II Cn (R \times_{t} S)) \land f (0) = f (1))) \to f (0) = f (1)$
22	21	fveq2d	$⊢ ((R \in SConn \land S \in SConn) \land (f \in (II Cn (R \times_{t} S)) \land f (0) = f (1))) \to ({1^{st} ↾}_{(⋃ R \times ⋃ S)}) (f (0)) = ({1^{st} ↾}_{(⋃ R \times ⋃ S)}) (f (1))$
23		iitopon	$⊢ II \in TopOn ([0, 1])$
24	23	a1i	$⊢ ((R \in SConn \land S \in SConn) \land (f \in (II Cn (R \times_{t} S)) \land f (0) = f (1))) \to II \in TopOn ([0, 1])$
25		txtopon	$⊢ (R \in TopOn (⋃ R) \land S \in TopOn (⋃ S)) \to R \times_{t} S \in TopOn (⋃ R \times ⋃ S)$
26	11 16 25	syl2anc	$⊢ ((R \in SConn \land S \in SConn) \land (f \in (II Cn (R \times_{t} S)) \land f (0) = f (1))) \to R \times_{t} S \in TopOn (⋃ R \times ⋃ S)$
27		cnf2	$⊢ (II \in TopOn ([0, 1]) \land R \times_{t} S \in TopOn (⋃ R \times ⋃ S) \land f \in (II Cn (R \times_{t} S))) \to f : [0, 1] ⟶ ⋃ R \times ⋃ S$
28	24 26 6 27	syl3anc	$⊢ ((R \in SConn \land S \in SConn) \land (f \in (II Cn (R \times_{t} S)) \land f (0) = f (1))) \to f : [0, 1] ⟶ ⋃ R \times ⋃ S$
29		0elunit	$⊢ 0 \in [0, 1]$
30		fvco3	$⊢ (f : [0, 1] ⟶ ⋃ R \times ⋃ S \land 0 \in [0, 1]) \to (({1^{st} ↾}_{(⋃ R \times ⋃ S)}) \circ f) (0) = ({1^{st} ↾}_{(⋃ R \times ⋃ S)}) (f (0))$
31	28 29 30	sylancl	$⊢ ((R \in SConn \land S \in SConn) \land (f \in (II Cn (R \times_{t} S)) \land f (0) = f (1))) \to (({1^{st} ↾}_{(⋃ R \times ⋃ S)}) \circ f) (0) = ({1^{st} ↾}_{(⋃ R \times ⋃ S)}) (f (0))$
32		1elunit	$⊢ 1 \in [0, 1]$
33		fvco3	$⊢ (f : [0, 1] ⟶ ⋃ R \times ⋃ S \land 1 \in [0, 1]) \to (({1^{st} ↾}_{(⋃ R \times ⋃ S)}) \circ f) (1) = ({1^{st} ↾}_{(⋃ R \times ⋃ S)}) (f (1))$
34	28 32 33	sylancl	$⊢ ((R \in SConn \land S \in SConn) \land (f \in (II Cn (R \times_{t} S)) \land f (0) = f (1))) \to (({1^{st} ↾}_{(⋃ R \times ⋃ S)}) \circ f) (1) = ({1^{st} ↾}_{(⋃ R \times ⋃ S)}) (f (1))$
35	22 31 34	3eqtr4d	$⊢ ((R \in SConn \land S \in SConn) \land (f \in (II Cn (R \times_{t} S)) \land f (0) = f (1))) \to (({1^{st} ↾}_{(⋃ R \times ⋃ S)}) \circ f) (0) = (({1^{st} ↾}_{(⋃ R \times ⋃ S)}) \circ f) (1)$
36		sconnpht	$⊢ (R \in SConn \land ({1^{st} ↾}_{(⋃ R \times ⋃ S)}) \circ f \in (II Cn R) \land (({1^{st} ↾}_{(⋃ R \times ⋃ S)}) \circ f) (0) = (({1^{st} ↾}_{(⋃ R \times ⋃ S)}) \circ f) (1)) \to (({1^{st} ↾}_{(⋃ R \times ⋃ S)}) \circ f) ≃_{ph} (R) ([0, 1] \times \{(({1^{st} ↾}_{(⋃ R \times ⋃ S)}) \circ f) (0)\})$
37	5 20 35 36	syl3anc	$⊢ ((R \in SConn \land S \in SConn) \land (f \in (II Cn (R \times_{t} S)) \land f (0) = f (1))) \to (({1^{st} ↾}_{(⋃ R \times ⋃ S)}) \circ f) ≃_{ph} (R) ([0, 1] \times \{(({1^{st} ↾}_{(⋃ R \times ⋃ S)}) \circ f) (0)\})$
38		isphtpc	$⊢ (({1^{st} ↾}_{(⋃ R \times ⋃ S)}) \circ f) ≃_{ph} (R) ([0, 1] \times \{(({1^{st} ↾}_{(⋃ R \times ⋃ S)}) \circ f) (0)\}) \leftrightarrow (({1^{st} ↾}_{(⋃ R \times ⋃ S)}) \circ f \in (II Cn R) \land [0, 1] \times \{(({1^{st} ↾}_{(⋃ R \times ⋃ S)}) \circ f) (0)\} \in (II Cn R) \land (({1^{st} ↾}_{(⋃ R \times ⋃ S)}) \circ f) PHtpy (R) ([0, 1] \times \{(({1^{st} ↾}_{(⋃ R \times ⋃ S)}) \circ f) (0)\}) \neq \emptyset)$
39	37 38	sylib	$⊢ ((R \in SConn \land S \in SConn) \land (f \in (II Cn (R \times_{t} S)) \land f (0) = f (1))) \to (({1^{st} ↾}_{(⋃ R \times ⋃ S)}) \circ f \in (II Cn R) \land [0, 1] \times \{(({1^{st} ↾}_{(⋃ R \times ⋃ S)}) \circ f) (0)\} \in (II Cn R) \land (({1^{st} ↾}_{(⋃ R \times ⋃ S)}) \circ f) PHtpy (R) ([0, 1] \times \{(({1^{st} ↾}_{(⋃ R \times ⋃ S)}) \circ f) (0)\}) \neq \emptyset)$
40	39	simp3d	$⊢ ((R \in SConn \land S \in SConn) \land (f \in (II Cn (R \times_{t} S)) \land f (0) = f (1))) \to (({1^{st} ↾}_{(⋃ R \times ⋃ S)}) \circ f) PHtpy (R) ([0, 1] \times \{(({1^{st} ↾}_{(⋃ R \times ⋃ S)}) \circ f) (0)\}) \neq \emptyset$
41		n0	$⊢ (({1^{st} ↾}_{(⋃ R \times ⋃ S)}) \circ f) PHtpy (R) ([0, 1] \times \{(({1^{st} ↾}_{(⋃ R \times ⋃ S)}) \circ f) (0)\}) \neq \emptyset \leftrightarrow \exists g g \in ((({1^{st} ↾}_{(⋃ R \times ⋃ S)}) \circ f) PHtpy (R) ([0, 1] \times \{(({1^{st} ↾}_{(⋃ R \times ⋃ S)}) \circ f) (0)\}))$
42	40 41	sylib	$⊢ ((R \in SConn \land S \in SConn) \land (f \in (II Cn (R \times_{t} S)) \land f (0) = f (1))) \to \exists g g \in ((({1^{st} ↾}_{(⋃ R \times ⋃ S)}) \circ f) PHtpy (R) ([0, 1] \times \{(({1^{st} ↾}_{(⋃ R \times ⋃ S)}) \circ f) (0)\}))$
43		simplr	$⊢ ((R \in SConn \land S \in SConn) \land (f \in (II Cn (R \times_{t} S)) \land f (0) = f (1))) \to S \in SConn$
44		tx2cn	$⊢ (R \in TopOn (⋃ R) \land S \in TopOn (⋃ S)) \to {2^{nd} ↾}_{(⋃ R \times ⋃ S)} \in ((R \times_{t} S) Cn S)$
45	11 16 44	syl2anc	$⊢ ((R \in SConn \land S \in SConn) \land (f \in (II Cn (R \times_{t} S)) \land f (0) = f (1))) \to {2^{nd} ↾}_{(⋃ R \times ⋃ S)} \in ((R \times_{t} S) Cn S)$
46		cnco	$⊢ (f \in (II Cn (R \times_{t} S)) \land {2^{nd} ↾}_{(⋃ R \times ⋃ S)} \in ((R \times_{t} S) Cn S)) \to ({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) \circ f \in (II Cn S)$
47	6 45 46	syl2anc	$⊢ ((R \in SConn \land S \in SConn) \land (f \in (II Cn (R \times_{t} S)) \land f (0) = f (1))) \to ({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) \circ f \in (II Cn S)$
48	21	fveq2d	$⊢ ((R \in SConn \land S \in SConn) \land (f \in (II Cn (R \times_{t} S)) \land f (0) = f (1))) \to ({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) (f (0)) = ({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) (f (1))$
49		fvco3	$⊢ (f : [0, 1] ⟶ ⋃ R \times ⋃ S \land 0 \in [0, 1]) \to (({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) \circ f) (0) = ({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) (f (0))$
50	28 29 49	sylancl	$⊢ ((R \in SConn \land S \in SConn) \land (f \in (II Cn (R \times_{t} S)) \land f (0) = f (1))) \to (({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) \circ f) (0) = ({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) (f (0))$
51		fvco3	$⊢ (f : [0, 1] ⟶ ⋃ R \times ⋃ S \land 1 \in [0, 1]) \to (({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) \circ f) (1) = ({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) (f (1))$
52	28 32 51	sylancl	$⊢ ((R \in SConn \land S \in SConn) \land (f \in (II Cn (R \times_{t} S)) \land f (0) = f (1))) \to (({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) \circ f) (1) = ({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) (f (1))$
53	48 50 52	3eqtr4d	$⊢ ((R \in SConn \land S \in SConn) \land (f \in (II Cn (R \times_{t} S)) \land f (0) = f (1))) \to (({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) \circ f) (0) = (({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) \circ f) (1)$
54		sconnpht	$⊢ (S \in SConn \land ({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) \circ f \in (II Cn S) \land (({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) \circ f) (0) = (({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) \circ f) (1)) \to (({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) \circ f) ≃_{ph} (S) ([0, 1] \times \{(({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) \circ f) (0)\})$
55	43 47 53 54	syl3anc	$⊢ ((R \in SConn \land S \in SConn) \land (f \in (II Cn (R \times_{t} S)) \land f (0) = f (1))) \to (({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) \circ f) ≃_{ph} (S) ([0, 1] \times \{(({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) \circ f) (0)\})$
56		isphtpc	$⊢ (({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) \circ f) ≃_{ph} (S) ([0, 1] \times \{(({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) \circ f) (0)\}) \leftrightarrow (({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) \circ f \in (II Cn S) \land [0, 1] \times \{(({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) \circ f) (0)\} \in (II Cn S) \land (({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) \circ f) PHtpy (S) ([0, 1] \times \{(({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) \circ f) (0)\}) \neq \emptyset)$
57	55 56	sylib	$⊢ ((R \in SConn \land S \in SConn) \land (f \in (II Cn (R \times_{t} S)) \land f (0) = f (1))) \to (({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) \circ f \in (II Cn S) \land [0, 1] \times \{(({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) \circ f) (0)\} \in (II Cn S) \land (({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) \circ f) PHtpy (S) ([0, 1] \times \{(({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) \circ f) (0)\}) \neq \emptyset)$
58	57	simp3d	$⊢ ((R \in SConn \land S \in SConn) \land (f \in (II Cn (R \times_{t} S)) \land f (0) = f (1))) \to (({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) \circ f) PHtpy (S) ([0, 1] \times \{(({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) \circ f) (0)\}) \neq \emptyset$
59		n0	$⊢ (({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) \circ f) PHtpy (S) ([0, 1] \times \{(({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) \circ f) (0)\}) \neq \emptyset \leftrightarrow \exists h h \in ((({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) \circ f) PHtpy (S) ([0, 1] \times \{(({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) \circ f) (0)\}))$
60	58 59	sylib	$⊢ ((R \in SConn \land S \in SConn) \land (f \in (II Cn (R \times_{t} S)) \land f (0) = f (1))) \to \exists h h \in ((({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) \circ f) PHtpy (S) ([0, 1] \times \{(({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) \circ f) (0)\}))$
61		exdistrv	$⊢ \exists g \exists h (g \in ((({1^{st} ↾}_{(⋃ R \times ⋃ S)}) \circ f) PHtpy (R) ([0, 1] \times \{(({1^{st} ↾}_{(⋃ R \times ⋃ S)}) \circ f) (0)\})) \land h \in ((({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) \circ f) PHtpy (S) ([0, 1] \times \{(({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) \circ f) (0)\}))) \leftrightarrow (\exists g g \in ((({1^{st} ↾}_{(⋃ R \times ⋃ S)}) \circ f) PHtpy (R) ([0, 1] \times \{(({1^{st} ↾}_{(⋃ R \times ⋃ S)}) \circ f) (0)\})) \land \exists h h \in ((({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) \circ f) PHtpy (S) ([0, 1] \times \{(({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) \circ f) (0)\})))$
62	8	adantr	$⊢ (((R \in SConn \land S \in SConn) \land (f \in (II Cn (R \times_{t} S)) \land f (0) = f (1))) \land (g \in ((({1^{st} ↾}_{(⋃ R \times ⋃ S)}) \circ f) PHtpy (R) ([0, 1] \times \{(({1^{st} ↾}_{(⋃ R \times ⋃ S)}) \circ f) (0)\})) \land h \in ((({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) \circ f) PHtpy (S) ([0, 1] \times \{(({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) \circ f) (0)\})))) \to R \in Top$
63	13	adantr	$⊢ (((R \in SConn \land S \in SConn) \land (f \in (II Cn (R \times_{t} S)) \land f (0) = f (1))) \land (g \in ((({1^{st} ↾}_{(⋃ R \times ⋃ S)}) \circ f) PHtpy (R) ([0, 1] \times \{(({1^{st} ↾}_{(⋃ R \times ⋃ S)}) \circ f) (0)\})) \land h \in ((({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) \circ f) PHtpy (S) ([0, 1] \times \{(({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) \circ f) (0)\})))) \to S \in Top$
64	6	adantr	$⊢ (((R \in SConn \land S \in SConn) \land (f \in (II Cn (R \times_{t} S)) \land f (0) = f (1))) \land (g \in ((({1^{st} ↾}_{(⋃ R \times ⋃ S)}) \circ f) PHtpy (R) ([0, 1] \times \{(({1^{st} ↾}_{(⋃ R \times ⋃ S)}) \circ f) (0)\})) \land h \in ((({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) \circ f) PHtpy (S) ([0, 1] \times \{(({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) \circ f) (0)\})))) \to f \in (II Cn (R \times_{t} S))$
65		eqid	$⊢ ({1^{st} ↾}_{(⋃ R \times ⋃ S)}) \circ f = ({1^{st} ↾}_{(⋃ R \times ⋃ S)}) \circ f$
66		eqid	$⊢ ({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) \circ f = ({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) \circ f$
67		simprl	$⊢ (((R \in SConn \land S \in SConn) \land (f \in (II Cn (R \times_{t} S)) \land f (0) = f (1))) \land (g \in ((({1^{st} ↾}_{(⋃ R \times ⋃ S)}) \circ f) PHtpy (R) ([0, 1] \times \{(({1^{st} ↾}_{(⋃ R \times ⋃ S)}) \circ f) (0)\})) \land h \in ((({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) \circ f) PHtpy (S) ([0, 1] \times \{(({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) \circ f) (0)\})))) \to g \in ((({1^{st} ↾}_{(⋃ R \times ⋃ S)}) \circ f) PHtpy (R) ([0, 1] \times \{(({1^{st} ↾}_{(⋃ R \times ⋃ S)}) \circ f) (0)\}))$
68		simprr	$⊢ (((R \in SConn \land S \in SConn) \land (f \in (II Cn (R \times_{t} S)) \land f (0) = f (1))) \land (g \in ((({1^{st} ↾}_{(⋃ R \times ⋃ S)}) \circ f) PHtpy (R) ([0, 1] \times \{(({1^{st} ↾}_{(⋃ R \times ⋃ S)}) \circ f) (0)\})) \land h \in ((({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) \circ f) PHtpy (S) ([0, 1] \times \{(({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) \circ f) (0)\})))) \to h \in ((({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) \circ f) PHtpy (S) ([0, 1] \times \{(({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) \circ f) (0)\}))$
69	62 63 64 65 66 67 68	txsconnlem	$⊢ (((R \in SConn \land S \in SConn) \land (f \in (II Cn (R \times_{t} S)) \land f (0) = f (1))) \land (g \in ((({1^{st} ↾}_{(⋃ R \times ⋃ S)}) \circ f) PHtpy (R) ([0, 1] \times \{(({1^{st} ↾}_{(⋃ R \times ⋃ S)}) \circ f) (0)\})) \land h \in ((({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) \circ f) PHtpy (S) ([0, 1] \times \{(({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) \circ f) (0)\})))) \to f ≃_{ph} (R \times_{t} S) ([0, 1] \times \{f (0)\})$
70	69	ex	$⊢ ((R \in SConn \land S \in SConn) \land (f \in (II Cn (R \times_{t} S)) \land f (0) = f (1))) \to ((g \in ((({1^{st} ↾}_{(⋃ R \times ⋃ S)}) \circ f) PHtpy (R) ([0, 1] \times \{(({1^{st} ↾}_{(⋃ R \times ⋃ S)}) \circ f) (0)\})) \land h \in ((({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) \circ f) PHtpy (S) ([0, 1] \times \{(({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) \circ f) (0)\}))) \to f ≃_{ph} (R \times_{t} S) ([0, 1] \times \{f (0)\}))$
71	70	exlimdvv	$⊢ ((R \in SConn \land S \in SConn) \land (f \in (II Cn (R \times_{t} S)) \land f (0) = f (1))) \to (\exists g \exists h (g \in ((({1^{st} ↾}_{(⋃ R \times ⋃ S)}) \circ f) PHtpy (R) ([0, 1] \times \{(({1^{st} ↾}_{(⋃ R \times ⋃ S)}) \circ f) (0)\})) \land h \in ((({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) \circ f) PHtpy (S) ([0, 1] \times \{(({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) \circ f) (0)\}))) \to f ≃_{ph} (R \times_{t} S) ([0, 1] \times \{f (0)\}))$
72	61 71	biimtrrid	$⊢ ((R \in SConn \land S \in SConn) \land (f \in (II Cn (R \times_{t} S)) \land f (0) = f (1))) \to ((\exists g g \in ((({1^{st} ↾}_{(⋃ R \times ⋃ S)}) \circ f) PHtpy (R) ([0, 1] \times \{(({1^{st} ↾}_{(⋃ R \times ⋃ S)}) \circ f) (0)\})) \land \exists h h \in ((({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) \circ f) PHtpy (S) ([0, 1] \times \{(({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) \circ f) (0)\}))) \to f ≃_{ph} (R \times_{t} S) ([0, 1] \times \{f (0)\}))$
73	42 60 72	mp2and	$⊢ ((R \in SConn \land S \in SConn) \land (f \in (II Cn (R \times_{t} S)) \land f (0) = f (1))) \to f ≃_{ph} (R \times_{t} S) ([0, 1] \times \{f (0)\})$
74	73	expr	$⊢ ((R \in SConn \land S \in SConn) \land f \in (II Cn (R \times_{t} S))) \to (f (0) = f (1) \to f ≃_{ph} (R \times_{t} S) ([0, 1] \times \{f (0)\}))$
75	74	ralrimiva	$⊢ (R \in SConn \land S \in SConn) \to \forall f \in (II Cn (R \times_{t} S)) (f (0) = f (1) \to f ≃_{ph} (R \times_{t} S) ([0, 1] \times \{f (0)\}))$
76		issconn	$⊢ R \times_{t} S \in SConn \leftrightarrow (R \times_{t} S \in PConn \land \forall f \in (II Cn (R \times_{t} S)) (f (0) = f (1) \to f ≃_{ph} (R \times_{t} S) ([0, 1] \times \{f (0)\})))$
77	4 75 76	sylanbrc	$⊢ (R \in SConn \land S \in SConn) \to R \times_{t} S \in SConn$

Metamath Proof Explorer

Theorem txsconn

Proof