txsconnlem

	Ref	Expression
Hypotheses	txsconn.1	$⊢ φ \to R \in Top$
	txsconn.2	$⊢ φ \to S \in Top$
	txsconn.3	$⊢ φ \to F \in (II Cn (R \times_{t} S))$
	txsconn.5	$⊢ A = ({1^{st} ↾}_{(⋃ R \times ⋃ S)}) \circ F$
	txsconn.6	$⊢ B = ({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) \circ F$
	txsconn.7	$⊢ φ \to G \in (A PHtpy (R) ([0, 1] \times \{A (0)\}))$
	txsconn.8	$⊢ φ \to H \in (B PHtpy (S) ([0, 1] \times \{B (0)\}))$
Assertion	txsconnlem	$⊢ φ \to F ≃_{ph} (R \times_{t} S) ([0, 1] \times \{F (0)\})$

Proof

Step	Hyp	Ref	Expression
1		txsconn.1	$⊢ φ \to R \in Top$
2		txsconn.2	$⊢ φ \to S \in Top$
3		txsconn.3	$⊢ φ \to F \in (II Cn (R \times_{t} S))$
4		txsconn.5	$⊢ A = ({1^{st} ↾}_{(⋃ R \times ⋃ S)}) \circ F$
5		txsconn.6	$⊢ B = ({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) \circ F$
6		txsconn.7	$⊢ φ \to G \in (A PHtpy (R) ([0, 1] \times \{A (0)\}))$
7		txsconn.8	$⊢ φ \to H \in (B PHtpy (S) ([0, 1] \times \{B (0)\}))$
8		fconstmpt	$⊢ [0, 1] \times \{F (0)\} = (x \in [0, 1] ⟼ F (0))$
9		iitopon	$⊢ II \in TopOn ([0, 1])$
10	9	a1i	$⊢ φ \to II \in TopOn ([0, 1])$
11		eqid	$⊢ ⋃ R = ⋃ R$
12	11	toptopon	$⊢ R \in Top \leftrightarrow R \in TopOn (⋃ R)$
13	1 12	sylib	$⊢ φ \to R \in TopOn (⋃ R)$
14		eqid	$⊢ ⋃ S = ⋃ S$
15	14	toptopon	$⊢ S \in Top \leftrightarrow S \in TopOn (⋃ S)$
16	2 15	sylib	$⊢ φ \to S \in TopOn (⋃ S)$
17		txtopon	$⊢ (R \in TopOn (⋃ R) \land S \in TopOn (⋃ S)) \to R \times_{t} S \in TopOn (⋃ R \times ⋃ S)$
18	13 16 17	syl2anc	$⊢ φ \to R \times_{t} S \in TopOn (⋃ R \times ⋃ S)$
19		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$
20	10 18 3 19	syl3anc	$⊢ φ \to F : [0, 1] ⟶ ⋃ R \times ⋃ S$
21		0elunit	$⊢ 0 \in [0, 1]$
22		ffvelrn	$⊢ (F : [0, 1] ⟶ ⋃ R \times ⋃ S \land 0 \in [0, 1]) \to F (0) \in (⋃ R \times ⋃ S)$
23	20 21 22	sylancl	$⊢ φ \to F (0) \in (⋃ R \times ⋃ S)$
24	10 18 23	cnmptc	$⊢ φ \to (x \in [0, 1] ⟼ F (0)) \in (II Cn (R \times_{t} S))$
25	8 24	eqeltrid	$⊢ φ \to [0, 1] \times \{F (0)\} \in (II Cn (R \times_{t} S))$
26		tx1cn	$⊢ (R \in TopOn (⋃ R) \land S \in TopOn (⋃ S)) \to {1^{st} ↾}_{(⋃ R \times ⋃ S)} \in ((R \times_{t} S) Cn R)$
27	13 16 26	syl2anc	$⊢ φ \to {1^{st} ↾}_{(⋃ R \times ⋃ S)} \in ((R \times_{t} S) Cn R)$
28		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)$
29	3 27 28	syl2anc	$⊢ φ \to ({1^{st} ↾}_{(⋃ R \times ⋃ S)}) \circ F \in (II Cn R)$
30	4 29	eqeltrid	$⊢ φ \to A \in (II Cn R)$
31		fconstmpt	$⊢ [0, 1] \times \{A (0)\} = (x \in [0, 1] ⟼ A (0))$
32		iiuni	$⊢ [0, 1] = ⋃ II$
33	32 11	cnf	$⊢ A \in (II Cn R) \to A : [0, 1] ⟶ ⋃ R$
34	30 33	syl	$⊢ φ \to A : [0, 1] ⟶ ⋃ R$
35		ffvelrn	$⊢ (A : [0, 1] ⟶ ⋃ R \land 0 \in [0, 1]) \to A (0) \in ⋃ R$
36	34 21 35	sylancl	$⊢ φ \to A (0) \in ⋃ R$
37	10 13 36	cnmptc	$⊢ φ \to (x \in [0, 1] ⟼ A (0)) \in (II Cn R)$
38	31 37	eqeltrid	$⊢ φ \to [0, 1] \times \{A (0)\} \in (II Cn R)$
39	30 38	phtpycn	$⊢ φ \to A PHtpy (R) ([0, 1] \times \{A (0)\}) \subseteq (II \times_{t} II) Cn R$
40	39 6	sseldd	$⊢ φ \to G \in ((II \times_{t} II) Cn R)$
41		iitop	$⊢ II \in Top$
42	41 41 32 32	txunii	$⊢ [0, 1] \times [0, 1] = ⋃ (II \times_{t} II)$
43	42 11	cnf	$⊢ G \in ((II \times_{t} II) Cn R) \to G : [0, 1] \times [0, 1] ⟶ ⋃ R$
44		ffn	$⊢ G : [0, 1] \times [0, 1] ⟶ ⋃ R \to G Fn ([0, 1] \times [0, 1])$
45	40 43 44	3syl	$⊢ φ \to G Fn ([0, 1] \times [0, 1])$
46		fnov	$⊢ G Fn ([0, 1] \times [0, 1]) \leftrightarrow G = (x \in [0, 1], y \in [0, 1] ⟼ x G y)$
47	45 46	sylib	$⊢ φ \to G = (x \in [0, 1], y \in [0, 1] ⟼ x G y)$
48	47 40	eqeltrrd	$⊢ φ \to (x \in [0, 1], y \in [0, 1] ⟼ x G y) \in ((II \times_{t} II) Cn R)$
49		tx2cn	$⊢ (R \in TopOn (⋃ R) \land S \in TopOn (⋃ S)) \to {2^{nd} ↾}_{(⋃ R \times ⋃ S)} \in ((R \times_{t} S) Cn S)$
50	13 16 49	syl2anc	$⊢ φ \to {2^{nd} ↾}_{(⋃ R \times ⋃ S)} \in ((R \times_{t} S) Cn S)$
51		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)$
52	3 50 51	syl2anc	$⊢ φ \to ({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) \circ F \in (II Cn S)$
53	5 52	eqeltrid	$⊢ φ \to B \in (II Cn S)$
54		fconstmpt	$⊢ [0, 1] \times \{B (0)\} = (x \in [0, 1] ⟼ B (0))$
55	32 14	cnf	$⊢ B \in (II Cn S) \to B : [0, 1] ⟶ ⋃ S$
56	53 55	syl	$⊢ φ \to B : [0, 1] ⟶ ⋃ S$
57		ffvelrn	$⊢ (B : [0, 1] ⟶ ⋃ S \land 0 \in [0, 1]) \to B (0) \in ⋃ S$
58	56 21 57	sylancl	$⊢ φ \to B (0) \in ⋃ S$
59	10 16 58	cnmptc	$⊢ φ \to (x \in [0, 1] ⟼ B (0)) \in (II Cn S)$
60	54 59	eqeltrid	$⊢ φ \to [0, 1] \times \{B (0)\} \in (II Cn S)$
61	53 60	phtpycn	$⊢ φ \to B PHtpy (S) ([0, 1] \times \{B (0)\}) \subseteq (II \times_{t} II) Cn S$
62	61 7	sseldd	$⊢ φ \to H \in ((II \times_{t} II) Cn S)$
63	42 14	cnf	$⊢ H \in ((II \times_{t} II) Cn S) \to H : [0, 1] \times [0, 1] ⟶ ⋃ S$
64		ffn	$⊢ H : [0, 1] \times [0, 1] ⟶ ⋃ S \to H Fn ([0, 1] \times [0, 1])$
65	62 63 64	3syl	$⊢ φ \to H Fn ([0, 1] \times [0, 1])$
66		fnov	$⊢ H Fn ([0, 1] \times [0, 1]) \leftrightarrow H = (x \in [0, 1], y \in [0, 1] ⟼ x H y)$
67	65 66	sylib	$⊢ φ \to H = (x \in [0, 1], y \in [0, 1] ⟼ x H y)$
68	67 62	eqeltrrd	$⊢ φ \to (x \in [0, 1], y \in [0, 1] ⟼ x H y) \in ((II \times_{t} II) Cn S)$
69	10 10 48 68	cnmpt2t	$⊢ φ \to (x \in [0, 1], y \in [0, 1] ⟼ ⟨x G y, x H y⟩) \in ((II \times_{t} II) Cn (R \times_{t} S))$
70	30 38	phtpyhtpy	$⊢ φ \to A PHtpy (R) ([0, 1] \times \{A (0)\}) \subseteq A (II Htpy R) ([0, 1] \times \{A (0)\})$
71	70 6	sseldd	$⊢ φ \to G \in (A (II Htpy R) ([0, 1] \times \{A (0)\}))$
72	10 30 38 71	htpyi	$⊢ (φ \land s \in [0, 1]) \to (s G 0 = A (s) \land s G 1 = ([0, 1] \times \{A (0)\}) (s))$
73	72	simpld	$⊢ (φ \land s \in [0, 1]) \to s G 0 = A (s)$
74	4	fveq1i	$⊢ A (s) = (({1^{st} ↾}_{(⋃ R \times ⋃ S)}) \circ F) (s)$
75		fvco3	$⊢ (F : [0, 1] ⟶ ⋃ R \times ⋃ S \land s \in [0, 1]) \to (({1^{st} ↾}_{(⋃ R \times ⋃ S)}) \circ F) (s) = ({1^{st} ↾}_{(⋃ R \times ⋃ S)}) (F (s))$
76	20 75	sylan	$⊢ (φ \land s \in [0, 1]) \to (({1^{st} ↾}_{(⋃ R \times ⋃ S)}) \circ F) (s) = ({1^{st} ↾}_{(⋃ R \times ⋃ S)}) (F (s))$
77	74 76	syl5eq	$⊢ (φ \land s \in [0, 1]) \to A (s) = ({1^{st} ↾}_{(⋃ R \times ⋃ S)}) (F (s))$
78		ffvelrn	$⊢ (F : [0, 1] ⟶ ⋃ R \times ⋃ S \land s \in [0, 1]) \to F (s) \in (⋃ R \times ⋃ S)$
79	20 78	sylan	$⊢ (φ \land s \in [0, 1]) \to F (s) \in (⋃ R \times ⋃ S)$
80		fvres	$⊢ F (s) \in (⋃ R \times ⋃ S) \to ({1^{st} ↾}_{(⋃ R \times ⋃ S)}) (F (s)) = 1^{st} (F (s))$
81	79 80	syl	$⊢ (φ \land s \in [0, 1]) \to ({1^{st} ↾}_{(⋃ R \times ⋃ S)}) (F (s)) = 1^{st} (F (s))$
82	73 77 81	3eqtrd	$⊢ (φ \land s \in [0, 1]) \to s G 0 = 1^{st} (F (s))$
83	53 60	phtpyhtpy	$⊢ φ \to B PHtpy (S) ([0, 1] \times \{B (0)\}) \subseteq B (II Htpy S) ([0, 1] \times \{B (0)\})$
84	83 7	sseldd	$⊢ φ \to H \in (B (II Htpy S) ([0, 1] \times \{B (0)\}))$
85	10 53 60 84	htpyi	$⊢ (φ \land s \in [0, 1]) \to (s H 0 = B (s) \land s H 1 = ([0, 1] \times \{B (0)\}) (s))$
86	85	simpld	$⊢ (φ \land s \in [0, 1]) \to s H 0 = B (s)$
87	5	fveq1i	$⊢ B (s) = (({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) \circ F) (s)$
88		fvco3	$⊢ (F : [0, 1] ⟶ ⋃ R \times ⋃ S \land s \in [0, 1]) \to (({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) \circ F) (s) = ({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) (F (s))$
89	20 88	sylan	$⊢ (φ \land s \in [0, 1]) \to (({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) \circ F) (s) = ({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) (F (s))$
90	87 89	syl5eq	$⊢ (φ \land s \in [0, 1]) \to B (s) = ({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) (F (s))$
91		fvres	$⊢ F (s) \in (⋃ R \times ⋃ S) \to ({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) (F (s)) = 2^{nd} (F (s))$
92	79 91	syl	$⊢ (φ \land s \in [0, 1]) \to ({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) (F (s)) = 2^{nd} (F (s))$
93	86 90 92	3eqtrd	$⊢ (φ \land s \in [0, 1]) \to s H 0 = 2^{nd} (F (s))$
94	82 93	opeq12d	$⊢ (φ \land s \in [0, 1]) \to ⟨s G 0, s H 0⟩ = ⟨1^{st} (F (s)), 2^{nd} (F (s))⟩$
95		simpr	$⊢ (φ \land s \in [0, 1]) \to s \in [0, 1]$
96		oveq12	$⊢ (x = s \land y = 0) \to x G y = s G 0$
97		oveq12	$⊢ (x = s \land y = 0) \to x H y = s H 0$
98	96 97	opeq12d	$⊢ (x = s \land y = 0) \to ⟨x G y, x H y⟩ = ⟨s G 0, s H 0⟩$
99		eqid	$⊢ (x \in [0, 1], y \in [0, 1] ⟼ ⟨x G y, x H y⟩) = (x \in [0, 1], y \in [0, 1] ⟼ ⟨x G y, x H y⟩)$
100		opex	$⊢ ⟨s G 0, s H 0⟩ \in V$
101	98 99 100	ovmpoa	$⊢ (s \in [0, 1] \land 0 \in [0, 1]) \to s (x \in [0, 1], y \in [0, 1] ⟼ ⟨x G y, x H y⟩) 0 = ⟨s G 0, s H 0⟩$
102	95 21 101	sylancl	$⊢ (φ \land s \in [0, 1]) \to s (x \in [0, 1], y \in [0, 1] ⟼ ⟨x G y, x H y⟩) 0 = ⟨s G 0, s H 0⟩$
103		1st2nd2	$⊢ F (s) \in (⋃ R \times ⋃ S) \to F (s) = ⟨1^{st} (F (s)), 2^{nd} (F (s))⟩$
104	79 103	syl	$⊢ (φ \land s \in [0, 1]) \to F (s) = ⟨1^{st} (F (s)), 2^{nd} (F (s))⟩$
105	94 102 104	3eqtr4d	$⊢ (φ \land s \in [0, 1]) \to s (x \in [0, 1], y \in [0, 1] ⟼ ⟨x G y, x H y⟩) 0 = F (s)$
106	72	simprd	$⊢ (φ \land s \in [0, 1]) \to s G 1 = ([0, 1] \times \{A (0)\}) (s)$
107		fvex	$⊢ A (0) \in V$
108	107	fvconst2	$⊢ s \in [0, 1] \to ([0, 1] \times \{A (0)\}) (s) = A (0)$
109	108	adantl	$⊢ (φ \land s \in [0, 1]) \to ([0, 1] \times \{A (0)\}) (s) = A (0)$
110	4	fveq1i	$⊢ A (0) = (({1^{st} ↾}_{(⋃ R \times ⋃ S)}) \circ F) (0)$
111		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))$
112	20 21 111	sylancl	$⊢ φ \to (({1^{st} ↾}_{(⋃ R \times ⋃ S)}) \circ F) (0) = ({1^{st} ↾}_{(⋃ R \times ⋃ S)}) (F (0))$
113		fvres	$⊢ F (0) \in (⋃ R \times ⋃ S) \to ({1^{st} ↾}_{(⋃ R \times ⋃ S)}) (F (0)) = 1^{st} (F (0))$
114	23 113	syl	$⊢ φ \to ({1^{st} ↾}_{(⋃ R \times ⋃ S)}) (F (0)) = 1^{st} (F (0))$
115	112 114	eqtrd	$⊢ φ \to (({1^{st} ↾}_{(⋃ R \times ⋃ S)}) \circ F) (0) = 1^{st} (F (0))$
116	110 115	syl5eq	$⊢ φ \to A (0) = 1^{st} (F (0))$
117	116	adantr	$⊢ (φ \land s \in [0, 1]) \to A (0) = 1^{st} (F (0))$
118	106 109 117	3eqtrd	$⊢ (φ \land s \in [0, 1]) \to s G 1 = 1^{st} (F (0))$
119	85	simprd	$⊢ (φ \land s \in [0, 1]) \to s H 1 = ([0, 1] \times \{B (0)\}) (s)$
120		fvex	$⊢ B (0) \in V$
121	120	fvconst2	$⊢ s \in [0, 1] \to ([0, 1] \times \{B (0)\}) (s) = B (0)$
122	121	adantl	$⊢ (φ \land s \in [0, 1]) \to ([0, 1] \times \{B (0)\}) (s) = B (0)$
123	5	fveq1i	$⊢ B (0) = (({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) \circ F) (0)$
124		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))$
125	20 21 124	sylancl	$⊢ φ \to (({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) \circ F) (0) = ({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) (F (0))$
126		fvres	$⊢ F (0) \in (⋃ R \times ⋃ S) \to ({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) (F (0)) = 2^{nd} (F (0))$
127	23 126	syl	$⊢ φ \to ({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) (F (0)) = 2^{nd} (F (0))$
128	125 127	eqtrd	$⊢ φ \to (({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) \circ F) (0) = 2^{nd} (F (0))$
129	123 128	syl5eq	$⊢ φ \to B (0) = 2^{nd} (F (0))$
130	129	adantr	$⊢ (φ \land s \in [0, 1]) \to B (0) = 2^{nd} (F (0))$
131	119 122 130	3eqtrd	$⊢ (φ \land s \in [0, 1]) \to s H 1 = 2^{nd} (F (0))$
132	118 131	opeq12d	$⊢ (φ \land s \in [0, 1]) \to ⟨s G 1, s H 1⟩ = ⟨1^{st} (F (0)), 2^{nd} (F (0))⟩$
133		1elunit	$⊢ 1 \in [0, 1]$
134		oveq12	$⊢ (x = s \land y = 1) \to x G y = s G 1$
135		oveq12	$⊢ (x = s \land y = 1) \to x H y = s H 1$
136	134 135	opeq12d	$⊢ (x = s \land y = 1) \to ⟨x G y, x H y⟩ = ⟨s G 1, s H 1⟩$
137		opex	$⊢ ⟨s G 1, s H 1⟩ \in V$
138	136 99 137	ovmpoa	$⊢ (s \in [0, 1] \land 1 \in [0, 1]) \to s (x \in [0, 1], y \in [0, 1] ⟼ ⟨x G y, x H y⟩) 1 = ⟨s G 1, s H 1⟩$
139	95 133 138	sylancl	$⊢ (φ \land s \in [0, 1]) \to s (x \in [0, 1], y \in [0, 1] ⟼ ⟨x G y, x H y⟩) 1 = ⟨s G 1, s H 1⟩$
140		fvex	$⊢ F (0) \in V$
141	140	fvconst2	$⊢ s \in [0, 1] \to ([0, 1] \times \{F (0)\}) (s) = F (0)$
142	141	adantl	$⊢ (φ \land s \in [0, 1]) \to ([0, 1] \times \{F (0)\}) (s) = F (0)$
143	23	adantr	$⊢ (φ \land s \in [0, 1]) \to F (0) \in (⋃ R \times ⋃ S)$
144		1st2nd2	$⊢ F (0) \in (⋃ R \times ⋃ S) \to F (0) = ⟨1^{st} (F (0)), 2^{nd} (F (0))⟩$
145	143 144	syl	$⊢ (φ \land s \in [0, 1]) \to F (0) = ⟨1^{st} (F (0)), 2^{nd} (F (0))⟩$
146	142 145	eqtrd	$⊢ (φ \land s \in [0, 1]) \to ([0, 1] \times \{F (0)\}) (s) = ⟨1^{st} (F (0)), 2^{nd} (F (0))⟩$
147	132 139 146	3eqtr4d	$⊢ (φ \land s \in [0, 1]) \to s (x \in [0, 1], y \in [0, 1] ⟼ ⟨x G y, x H y⟩) 1 = ([0, 1] \times \{F (0)\}) (s)$
148	30 38 6	phtpyi	$⊢ (φ \land s \in [0, 1]) \to (0 G s = A (0) \land 1 G s = A (1))$
149	148	simpld	$⊢ (φ \land s \in [0, 1]) \to 0 G s = A (0)$
150	149 117	eqtrd	$⊢ (φ \land s \in [0, 1]) \to 0 G s = 1^{st} (F (0))$
151	53 60 7	phtpyi	$⊢ (φ \land s \in [0, 1]) \to (0 H s = B (0) \land 1 H s = B (1))$
152	151	simpld	$⊢ (φ \land s \in [0, 1]) \to 0 H s = B (0)$
153	152 130	eqtrd	$⊢ (φ \land s \in [0, 1]) \to 0 H s = 2^{nd} (F (0))$
154	150 153	opeq12d	$⊢ (φ \land s \in [0, 1]) \to ⟨0 G s, 0 H s⟩ = ⟨1^{st} (F (0)), 2^{nd} (F (0))⟩$
155		oveq12	$⊢ (x = 0 \land y = s) \to x G y = 0 G s$
156		oveq12	$⊢ (x = 0 \land y = s) \to x H y = 0 H s$
157	155 156	opeq12d	$⊢ (x = 0 \land y = s) \to ⟨x G y, x H y⟩ = ⟨0 G s, 0 H s⟩$
158		opex	$⊢ ⟨0 G s, 0 H s⟩ \in V$
159	157 99 158	ovmpoa	$⊢ (0 \in [0, 1] \land s \in [0, 1]) \to 0 (x \in [0, 1], y \in [0, 1] ⟼ ⟨x G y, x H y⟩) s = ⟨0 G s, 0 H s⟩$
160	21 95 159	sylancr	$⊢ (φ \land s \in [0, 1]) \to 0 (x \in [0, 1], y \in [0, 1] ⟼ ⟨x G y, x H y⟩) s = ⟨0 G s, 0 H s⟩$
161	154 160 145	3eqtr4d	$⊢ (φ \land s \in [0, 1]) \to 0 (x \in [0, 1], y \in [0, 1] ⟼ ⟨x G y, x H y⟩) s = F (0)$
162	148	simprd	$⊢ (φ \land s \in [0, 1]) \to 1 G s = A (1)$
163	4	fveq1i	$⊢ A (1) = (({1^{st} ↾}_{(⋃ R \times ⋃ S)}) \circ F) (1)$
164		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))$
165	20 133 164	sylancl	$⊢ φ \to (({1^{st} ↾}_{(⋃ R \times ⋃ S)}) \circ F) (1) = ({1^{st} ↾}_{(⋃ R \times ⋃ S)}) (F (1))$
166	163 165	syl5eq	$⊢ φ \to A (1) = ({1^{st} ↾}_{(⋃ R \times ⋃ S)}) (F (1))$
167		ffvelrn	$⊢ (F : [0, 1] ⟶ ⋃ R \times ⋃ S \land 1 \in [0, 1]) \to F (1) \in (⋃ R \times ⋃ S)$
168	20 133 167	sylancl	$⊢ φ \to F (1) \in (⋃ R \times ⋃ S)$
169		fvres	$⊢ F (1) \in (⋃ R \times ⋃ S) \to ({1^{st} ↾}_{(⋃ R \times ⋃ S)}) (F (1)) = 1^{st} (F (1))$
170	168 169	syl	$⊢ φ \to ({1^{st} ↾}_{(⋃ R \times ⋃ S)}) (F (1)) = 1^{st} (F (1))$
171	166 170	eqtrd	$⊢ φ \to A (1) = 1^{st} (F (1))$
172	171	adantr	$⊢ (φ \land s \in [0, 1]) \to A (1) = 1^{st} (F (1))$
173	162 172	eqtrd	$⊢ (φ \land s \in [0, 1]) \to 1 G s = 1^{st} (F (1))$
174	151	simprd	$⊢ (φ \land s \in [0, 1]) \to 1 H s = B (1)$
175	5	fveq1i	$⊢ B (1) = (({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) \circ F) (1)$
176		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))$
177	20 133 176	sylancl	$⊢ φ \to (({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) \circ F) (1) = ({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) (F (1))$
178	175 177	syl5eq	$⊢ φ \to B (1) = ({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) (F (1))$
179		fvres	$⊢ F (1) \in (⋃ R \times ⋃ S) \to ({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) (F (1)) = 2^{nd} (F (1))$
180	168 179	syl	$⊢ φ \to ({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) (F (1)) = 2^{nd} (F (1))$
181	178 180	eqtrd	$⊢ φ \to B (1) = 2^{nd} (F (1))$
182	181	adantr	$⊢ (φ \land s \in [0, 1]) \to B (1) = 2^{nd} (F (1))$
183	174 182	eqtrd	$⊢ (φ \land s \in [0, 1]) \to 1 H s = 2^{nd} (F (1))$
184	173 183	opeq12d	$⊢ (φ \land s \in [0, 1]) \to ⟨1 G s, 1 H s⟩ = ⟨1^{st} (F (1)), 2^{nd} (F (1))⟩$
185		oveq12	$⊢ (x = 1 \land y = s) \to x G y = 1 G s$
186		oveq12	$⊢ (x = 1 \land y = s) \to x H y = 1 H s$
187	185 186	opeq12d	$⊢ (x = 1 \land y = s) \to ⟨x G y, x H y⟩ = ⟨1 G s, 1 H s⟩$
188		opex	$⊢ ⟨1 G s, 1 H s⟩ \in V$
189	187 99 188	ovmpoa	$⊢ (1 \in [0, 1] \land s \in [0, 1]) \to 1 (x \in [0, 1], y \in [0, 1] ⟼ ⟨x G y, x H y⟩) s = ⟨1 G s, 1 H s⟩$
190	133 95 189	sylancr	$⊢ (φ \land s \in [0, 1]) \to 1 (x \in [0, 1], y \in [0, 1] ⟼ ⟨x G y, x H y⟩) s = ⟨1 G s, 1 H s⟩$
191	168	adantr	$⊢ (φ \land s \in [0, 1]) \to F (1) \in (⋃ R \times ⋃ S)$
192		1st2nd2	$⊢ F (1) \in (⋃ R \times ⋃ S) \to F (1) = ⟨1^{st} (F (1)), 2^{nd} (F (1))⟩$
193	191 192	syl	$⊢ (φ \land s \in [0, 1]) \to F (1) = ⟨1^{st} (F (1)), 2^{nd} (F (1))⟩$
194	184 190 193	3eqtr4d	$⊢ (φ \land s \in [0, 1]) \to 1 (x \in [0, 1], y \in [0, 1] ⟼ ⟨x G y, x H y⟩) s = F (1)$
195	3 25 69 105 147 161 194	isphtpy2d	$⊢ φ \to (x \in [0, 1], y \in [0, 1] ⟼ ⟨x G y, x H y⟩) \in (F PHtpy (R \times_{t} S) ([0, 1] \times \{F (0)\}))$
196	195	ne0d	$⊢ φ \to F PHtpy (R \times_{t} S) ([0, 1] \times \{F (0)\}) \neq \emptyset$
197		isphtpc	$⊢ F ≃_{ph} (R \times_{t} S) ([0, 1] \times \{F (0)\}) \leftrightarrow (F \in (II Cn (R \times_{t} S)) \land [0, 1] \times \{F (0)\} \in (II Cn (R \times_{t} S)) \land F PHtpy (R \times_{t} S) ([0, 1] \times \{F (0)\}) \neq \emptyset)$
198	3 25 196 197	syl3anbrc	$⊢ φ \to F ≃_{ph} (R \times_{t} S) ([0, 1] \times \{F (0)\})$

Metamath Proof Explorer

Theorem txsconnlem

Proof