Theorem txsconnlem

Description: Lemma for txsconn . (Contributed by Mario Carneiro, 9-Mar-2015)

	Ref	Expression
Hypotheses	txsconn.1	|- ( ph -> R e. Top )
	txsconn.2	|- ( ph -> S e. Top )
	txsconn.3	|- ( ph -> F e. ( II Cn ( R tX S ) ) )
	txsconn.5	|- A = ( ( 1st |` ( U. R X. U. S ) ) o. F )
	txsconn.6	|- B = ( ( 2nd |` ( U. R X. U. S ) ) o. F )
	txsconn.7	|- ( ph -> G e. ( A ( PHtpy ` R ) ( ( 0 [,] 1 ) X. { ( A ` 0 ) } ) ) )
	txsconn.8	|- ( ph -> H e. ( B ( PHtpy ` S ) ( ( 0 [,] 1 ) X. { ( B ` 0 ) } ) ) )
Assertion	txsconnlem	|- ( ph -> F ( ~=ph ` ( R tX S ) ) ( ( 0 [,] 1 ) X. { ( F ` 0 ) } ) )

Proof

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