Metamath Proof Explorer


Theorem txsconn

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

Ref Expression
Assertion txsconn ( ( 𝑅 ∈ SConn ∧ 𝑆 ∈ SConn ) → ( 𝑅 ×t 𝑆 ) ∈ SConn )

Proof

Step Hyp Ref Expression
1 sconnpconn ( 𝑅 ∈ SConn → 𝑅 ∈ PConn )
2 sconnpconn ( 𝑆 ∈ SConn → 𝑆 ∈ PConn )
3 txpconn ( ( 𝑅 ∈ PConn ∧ 𝑆 ∈ PConn ) → ( 𝑅 ×t 𝑆 ) ∈ PConn )
4 1 2 3 syl2an ( ( 𝑅 ∈ SConn ∧ 𝑆 ∈ SConn ) → ( 𝑅 ×t 𝑆 ) ∈ PConn )
5 simpll ( ( ( 𝑅 ∈ SConn ∧ 𝑆 ∈ SConn ) ∧ ( 𝑓 ∈ ( II Cn ( 𝑅 ×t 𝑆 ) ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) → 𝑅 ∈ SConn )
6 simprl ( ( ( 𝑅 ∈ SConn ∧ 𝑆 ∈ SConn ) ∧ ( 𝑓 ∈ ( II Cn ( 𝑅 ×t 𝑆 ) ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) → 𝑓 ∈ ( II Cn ( 𝑅 ×t 𝑆 ) ) )
7 sconntop ( 𝑅 ∈ SConn → 𝑅 ∈ Top )
8 7 ad2antrr ( ( ( 𝑅 ∈ SConn ∧ 𝑆 ∈ SConn ) ∧ ( 𝑓 ∈ ( II Cn ( 𝑅 ×t 𝑆 ) ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) → 𝑅 ∈ Top )
9 eqid 𝑅 = 𝑅
10 9 toptopon ( 𝑅 ∈ Top ↔ 𝑅 ∈ ( TopOn ‘ 𝑅 ) )
11 8 10 sylib ( ( ( 𝑅 ∈ SConn ∧ 𝑆 ∈ SConn ) ∧ ( 𝑓 ∈ ( II Cn ( 𝑅 ×t 𝑆 ) ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) → 𝑅 ∈ ( TopOn ‘ 𝑅 ) )
12 sconntop ( 𝑆 ∈ SConn → 𝑆 ∈ Top )
13 12 ad2antlr ( ( ( 𝑅 ∈ SConn ∧ 𝑆 ∈ SConn ) ∧ ( 𝑓 ∈ ( II Cn ( 𝑅 ×t 𝑆 ) ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) → 𝑆 ∈ Top )
14 eqid 𝑆 = 𝑆
15 14 toptopon ( 𝑆 ∈ Top ↔ 𝑆 ∈ ( TopOn ‘ 𝑆 ) )
16 13 15 sylib ( ( ( 𝑅 ∈ SConn ∧ 𝑆 ∈ SConn ) ∧ ( 𝑓 ∈ ( II Cn ( 𝑅 ×t 𝑆 ) ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) → 𝑆 ∈ ( TopOn ‘ 𝑆 ) )
17 tx1cn ( ( 𝑅 ∈ ( TopOn ‘ 𝑅 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑆 ) ) → ( 1st ↾ ( 𝑅 × 𝑆 ) ) ∈ ( ( 𝑅 ×t 𝑆 ) Cn 𝑅 ) )
18 11 16 17 syl2anc ( ( ( 𝑅 ∈ SConn ∧ 𝑆 ∈ SConn ) ∧ ( 𝑓 ∈ ( II Cn ( 𝑅 ×t 𝑆 ) ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) → ( 1st ↾ ( 𝑅 × 𝑆 ) ) ∈ ( ( 𝑅 ×t 𝑆 ) Cn 𝑅 ) )
19 cnco ( ( 𝑓 ∈ ( II Cn ( 𝑅 ×t 𝑆 ) ) ∧ ( 1st ↾ ( 𝑅 × 𝑆 ) ) ∈ ( ( 𝑅 ×t 𝑆 ) Cn 𝑅 ) ) → ( ( 1st ↾ ( 𝑅 × 𝑆 ) ) ∘ 𝑓 ) ∈ ( II Cn 𝑅 ) )
20 6 18 19 syl2anc ( ( ( 𝑅 ∈ SConn ∧ 𝑆 ∈ SConn ) ∧ ( 𝑓 ∈ ( II Cn ( 𝑅 ×t 𝑆 ) ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) → ( ( 1st ↾ ( 𝑅 × 𝑆 ) ) ∘ 𝑓 ) ∈ ( II Cn 𝑅 ) )
21 simprr ( ( ( 𝑅 ∈ SConn ∧ 𝑆 ∈ SConn ) ∧ ( 𝑓 ∈ ( II Cn ( 𝑅 ×t 𝑆 ) ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) → ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) )
22 21 fveq2d ( ( ( 𝑅 ∈ SConn ∧ 𝑆 ∈ SConn ) ∧ ( 𝑓 ∈ ( II Cn ( 𝑅 ×t 𝑆 ) ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) → ( ( 1st ↾ ( 𝑅 × 𝑆 ) ) ‘ ( 𝑓 ‘ 0 ) ) = ( ( 1st ↾ ( 𝑅 × 𝑆 ) ) ‘ ( 𝑓 ‘ 1 ) ) )
23 iitopon II ∈ ( TopOn ‘ ( 0 [,] 1 ) )
24 23 a1i ( ( ( 𝑅 ∈ SConn ∧ 𝑆 ∈ SConn ) ∧ ( 𝑓 ∈ ( II Cn ( 𝑅 ×t 𝑆 ) ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) → II ∈ ( TopOn ‘ ( 0 [,] 1 ) ) )
25 txtopon ( ( 𝑅 ∈ ( TopOn ‘ 𝑅 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑆 ) ) → ( 𝑅 ×t 𝑆 ) ∈ ( TopOn ‘ ( 𝑅 × 𝑆 ) ) )
26 11 16 25 syl2anc ( ( ( 𝑅 ∈ SConn ∧ 𝑆 ∈ SConn ) ∧ ( 𝑓 ∈ ( II Cn ( 𝑅 ×t 𝑆 ) ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) → ( 𝑅 ×t 𝑆 ) ∈ ( TopOn ‘ ( 𝑅 × 𝑆 ) ) )
27 cnf2 ( ( II ∈ ( TopOn ‘ ( 0 [,] 1 ) ) ∧ ( 𝑅 ×t 𝑆 ) ∈ ( TopOn ‘ ( 𝑅 × 𝑆 ) ) ∧ 𝑓 ∈ ( II Cn ( 𝑅 ×t 𝑆 ) ) ) → 𝑓 : ( 0 [,] 1 ) ⟶ ( 𝑅 × 𝑆 ) )
28 24 26 6 27 syl3anc ( ( ( 𝑅 ∈ SConn ∧ 𝑆 ∈ SConn ) ∧ ( 𝑓 ∈ ( II Cn ( 𝑅 ×t 𝑆 ) ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) → 𝑓 : ( 0 [,] 1 ) ⟶ ( 𝑅 × 𝑆 ) )
29 0elunit 0 ∈ ( 0 [,] 1 )
30 fvco3 ( ( 𝑓 : ( 0 [,] 1 ) ⟶ ( 𝑅 × 𝑆 ) ∧ 0 ∈ ( 0 [,] 1 ) ) → ( ( ( 1st ↾ ( 𝑅 × 𝑆 ) ) ∘ 𝑓 ) ‘ 0 ) = ( ( 1st ↾ ( 𝑅 × 𝑆 ) ) ‘ ( 𝑓 ‘ 0 ) ) )
31 28 29 30 sylancl ( ( ( 𝑅 ∈ SConn ∧ 𝑆 ∈ SConn ) ∧ ( 𝑓 ∈ ( II Cn ( 𝑅 ×t 𝑆 ) ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) → ( ( ( 1st ↾ ( 𝑅 × 𝑆 ) ) ∘ 𝑓 ) ‘ 0 ) = ( ( 1st ↾ ( 𝑅 × 𝑆 ) ) ‘ ( 𝑓 ‘ 0 ) ) )
32 1elunit 1 ∈ ( 0 [,] 1 )
33 fvco3 ( ( 𝑓 : ( 0 [,] 1 ) ⟶ ( 𝑅 × 𝑆 ) ∧ 1 ∈ ( 0 [,] 1 ) ) → ( ( ( 1st ↾ ( 𝑅 × 𝑆 ) ) ∘ 𝑓 ) ‘ 1 ) = ( ( 1st ↾ ( 𝑅 × 𝑆 ) ) ‘ ( 𝑓 ‘ 1 ) ) )
34 28 32 33 sylancl ( ( ( 𝑅 ∈ SConn ∧ 𝑆 ∈ SConn ) ∧ ( 𝑓 ∈ ( II Cn ( 𝑅 ×t 𝑆 ) ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) → ( ( ( 1st ↾ ( 𝑅 × 𝑆 ) ) ∘ 𝑓 ) ‘ 1 ) = ( ( 1st ↾ ( 𝑅 × 𝑆 ) ) ‘ ( 𝑓 ‘ 1 ) ) )
35 22 31 34 3eqtr4d ( ( ( 𝑅 ∈ SConn ∧ 𝑆 ∈ SConn ) ∧ ( 𝑓 ∈ ( II Cn ( 𝑅 ×t 𝑆 ) ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) → ( ( ( 1st ↾ ( 𝑅 × 𝑆 ) ) ∘ 𝑓 ) ‘ 0 ) = ( ( ( 1st ↾ ( 𝑅 × 𝑆 ) ) ∘ 𝑓 ) ‘ 1 ) )
36 sconnpht ( ( 𝑅 ∈ SConn ∧ ( ( 1st ↾ ( 𝑅 × 𝑆 ) ) ∘ 𝑓 ) ∈ ( II Cn 𝑅 ) ∧ ( ( ( 1st ↾ ( 𝑅 × 𝑆 ) ) ∘ 𝑓 ) ‘ 0 ) = ( ( ( 1st ↾ ( 𝑅 × 𝑆 ) ) ∘ 𝑓 ) ‘ 1 ) ) → ( ( 1st ↾ ( 𝑅 × 𝑆 ) ) ∘ 𝑓 ) ( ≃ph𝑅 ) ( ( 0 [,] 1 ) × { ( ( ( 1st ↾ ( 𝑅 × 𝑆 ) ) ∘ 𝑓 ) ‘ 0 ) } ) )
37 5 20 35 36 syl3anc ( ( ( 𝑅 ∈ SConn ∧ 𝑆 ∈ SConn ) ∧ ( 𝑓 ∈ ( II Cn ( 𝑅 ×t 𝑆 ) ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) → ( ( 1st ↾ ( 𝑅 × 𝑆 ) ) ∘ 𝑓 ) ( ≃ph𝑅 ) ( ( 0 [,] 1 ) × { ( ( ( 1st ↾ ( 𝑅 × 𝑆 ) ) ∘ 𝑓 ) ‘ 0 ) } ) )
38 isphtpc ( ( ( 1st ↾ ( 𝑅 × 𝑆 ) ) ∘ 𝑓 ) ( ≃ph𝑅 ) ( ( 0 [,] 1 ) × { ( ( ( 1st ↾ ( 𝑅 × 𝑆 ) ) ∘ 𝑓 ) ‘ 0 ) } ) ↔ ( ( ( 1st ↾ ( 𝑅 × 𝑆 ) ) ∘ 𝑓 ) ∈ ( II Cn 𝑅 ) ∧ ( ( 0 [,] 1 ) × { ( ( ( 1st ↾ ( 𝑅 × 𝑆 ) ) ∘ 𝑓 ) ‘ 0 ) } ) ∈ ( II Cn 𝑅 ) ∧ ( ( ( 1st ↾ ( 𝑅 × 𝑆 ) ) ∘ 𝑓 ) ( PHtpy ‘ 𝑅 ) ( ( 0 [,] 1 ) × { ( ( ( 1st ↾ ( 𝑅 × 𝑆 ) ) ∘ 𝑓 ) ‘ 0 ) } ) ) ≠ ∅ ) )
39 37 38 sylib ( ( ( 𝑅 ∈ SConn ∧ 𝑆 ∈ SConn ) ∧ ( 𝑓 ∈ ( II Cn ( 𝑅 ×t 𝑆 ) ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) → ( ( ( 1st ↾ ( 𝑅 × 𝑆 ) ) ∘ 𝑓 ) ∈ ( II Cn 𝑅 ) ∧ ( ( 0 [,] 1 ) × { ( ( ( 1st ↾ ( 𝑅 × 𝑆 ) ) ∘ 𝑓 ) ‘ 0 ) } ) ∈ ( II Cn 𝑅 ) ∧ ( ( ( 1st ↾ ( 𝑅 × 𝑆 ) ) ∘ 𝑓 ) ( PHtpy ‘ 𝑅 ) ( ( 0 [,] 1 ) × { ( ( ( 1st ↾ ( 𝑅 × 𝑆 ) ) ∘ 𝑓 ) ‘ 0 ) } ) ) ≠ ∅ ) )
40 39 simp3d ( ( ( 𝑅 ∈ SConn ∧ 𝑆 ∈ SConn ) ∧ ( 𝑓 ∈ ( II Cn ( 𝑅 ×t 𝑆 ) ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) → ( ( ( 1st ↾ ( 𝑅 × 𝑆 ) ) ∘ 𝑓 ) ( PHtpy ‘ 𝑅 ) ( ( 0 [,] 1 ) × { ( ( ( 1st ↾ ( 𝑅 × 𝑆 ) ) ∘ 𝑓 ) ‘ 0 ) } ) ) ≠ ∅ )
41 n0 ( ( ( ( 1st ↾ ( 𝑅 × 𝑆 ) ) ∘ 𝑓 ) ( PHtpy ‘ 𝑅 ) ( ( 0 [,] 1 ) × { ( ( ( 1st ↾ ( 𝑅 × 𝑆 ) ) ∘ 𝑓 ) ‘ 0 ) } ) ) ≠ ∅ ↔ ∃ 𝑔 𝑔 ∈ ( ( ( 1st ↾ ( 𝑅 × 𝑆 ) ) ∘ 𝑓 ) ( PHtpy ‘ 𝑅 ) ( ( 0 [,] 1 ) × { ( ( ( 1st ↾ ( 𝑅 × 𝑆 ) ) ∘ 𝑓 ) ‘ 0 ) } ) ) )
42 40 41 sylib ( ( ( 𝑅 ∈ SConn ∧ 𝑆 ∈ SConn ) ∧ ( 𝑓 ∈ ( II Cn ( 𝑅 ×t 𝑆 ) ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) → ∃ 𝑔 𝑔 ∈ ( ( ( 1st ↾ ( 𝑅 × 𝑆 ) ) ∘ 𝑓 ) ( PHtpy ‘ 𝑅 ) ( ( 0 [,] 1 ) × { ( ( ( 1st ↾ ( 𝑅 × 𝑆 ) ) ∘ 𝑓 ) ‘ 0 ) } ) ) )
43 simplr ( ( ( 𝑅 ∈ SConn ∧ 𝑆 ∈ SConn ) ∧ ( 𝑓 ∈ ( II Cn ( 𝑅 ×t 𝑆 ) ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) → 𝑆 ∈ SConn )
44 tx2cn ( ( 𝑅 ∈ ( TopOn ‘ 𝑅 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑆 ) ) → ( 2nd ↾ ( 𝑅 × 𝑆 ) ) ∈ ( ( 𝑅 ×t 𝑆 ) Cn 𝑆 ) )
45 11 16 44 syl2anc ( ( ( 𝑅 ∈ SConn ∧ 𝑆 ∈ SConn ) ∧ ( 𝑓 ∈ ( II Cn ( 𝑅 ×t 𝑆 ) ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) → ( 2nd ↾ ( 𝑅 × 𝑆 ) ) ∈ ( ( 𝑅 ×t 𝑆 ) Cn 𝑆 ) )
46 cnco ( ( 𝑓 ∈ ( II Cn ( 𝑅 ×t 𝑆 ) ) ∧ ( 2nd ↾ ( 𝑅 × 𝑆 ) ) ∈ ( ( 𝑅 ×t 𝑆 ) Cn 𝑆 ) ) → ( ( 2nd ↾ ( 𝑅 × 𝑆 ) ) ∘ 𝑓 ) ∈ ( II Cn 𝑆 ) )
47 6 45 46 syl2anc ( ( ( 𝑅 ∈ SConn ∧ 𝑆 ∈ SConn ) ∧ ( 𝑓 ∈ ( II Cn ( 𝑅 ×t 𝑆 ) ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) → ( ( 2nd ↾ ( 𝑅 × 𝑆 ) ) ∘ 𝑓 ) ∈ ( II Cn 𝑆 ) )
48 21 fveq2d ( ( ( 𝑅 ∈ SConn ∧ 𝑆 ∈ SConn ) ∧ ( 𝑓 ∈ ( II Cn ( 𝑅 ×t 𝑆 ) ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) → ( ( 2nd ↾ ( 𝑅 × 𝑆 ) ) ‘ ( 𝑓 ‘ 0 ) ) = ( ( 2nd ↾ ( 𝑅 × 𝑆 ) ) ‘ ( 𝑓 ‘ 1 ) ) )
49 fvco3 ( ( 𝑓 : ( 0 [,] 1 ) ⟶ ( 𝑅 × 𝑆 ) ∧ 0 ∈ ( 0 [,] 1 ) ) → ( ( ( 2nd ↾ ( 𝑅 × 𝑆 ) ) ∘ 𝑓 ) ‘ 0 ) = ( ( 2nd ↾ ( 𝑅 × 𝑆 ) ) ‘ ( 𝑓 ‘ 0 ) ) )
50 28 29 49 sylancl ( ( ( 𝑅 ∈ SConn ∧ 𝑆 ∈ SConn ) ∧ ( 𝑓 ∈ ( II Cn ( 𝑅 ×t 𝑆 ) ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) → ( ( ( 2nd ↾ ( 𝑅 × 𝑆 ) ) ∘ 𝑓 ) ‘ 0 ) = ( ( 2nd ↾ ( 𝑅 × 𝑆 ) ) ‘ ( 𝑓 ‘ 0 ) ) )
51 fvco3 ( ( 𝑓 : ( 0 [,] 1 ) ⟶ ( 𝑅 × 𝑆 ) ∧ 1 ∈ ( 0 [,] 1 ) ) → ( ( ( 2nd ↾ ( 𝑅 × 𝑆 ) ) ∘ 𝑓 ) ‘ 1 ) = ( ( 2nd ↾ ( 𝑅 × 𝑆 ) ) ‘ ( 𝑓 ‘ 1 ) ) )
52 28 32 51 sylancl ( ( ( 𝑅 ∈ SConn ∧ 𝑆 ∈ SConn ) ∧ ( 𝑓 ∈ ( II Cn ( 𝑅 ×t 𝑆 ) ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) → ( ( ( 2nd ↾ ( 𝑅 × 𝑆 ) ) ∘ 𝑓 ) ‘ 1 ) = ( ( 2nd ↾ ( 𝑅 × 𝑆 ) ) ‘ ( 𝑓 ‘ 1 ) ) )
53 48 50 52 3eqtr4d ( ( ( 𝑅 ∈ SConn ∧ 𝑆 ∈ SConn ) ∧ ( 𝑓 ∈ ( II Cn ( 𝑅 ×t 𝑆 ) ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) → ( ( ( 2nd ↾ ( 𝑅 × 𝑆 ) ) ∘ 𝑓 ) ‘ 0 ) = ( ( ( 2nd ↾ ( 𝑅 × 𝑆 ) ) ∘ 𝑓 ) ‘ 1 ) )
54 sconnpht ( ( 𝑆 ∈ SConn ∧ ( ( 2nd ↾ ( 𝑅 × 𝑆 ) ) ∘ 𝑓 ) ∈ ( II Cn 𝑆 ) ∧ ( ( ( 2nd ↾ ( 𝑅 × 𝑆 ) ) ∘ 𝑓 ) ‘ 0 ) = ( ( ( 2nd ↾ ( 𝑅 × 𝑆 ) ) ∘ 𝑓 ) ‘ 1 ) ) → ( ( 2nd ↾ ( 𝑅 × 𝑆 ) ) ∘ 𝑓 ) ( ≃ph𝑆 ) ( ( 0 [,] 1 ) × { ( ( ( 2nd ↾ ( 𝑅 × 𝑆 ) ) ∘ 𝑓 ) ‘ 0 ) } ) )
55 43 47 53 54 syl3anc ( ( ( 𝑅 ∈ SConn ∧ 𝑆 ∈ SConn ) ∧ ( 𝑓 ∈ ( II Cn ( 𝑅 ×t 𝑆 ) ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) → ( ( 2nd ↾ ( 𝑅 × 𝑆 ) ) ∘ 𝑓 ) ( ≃ph𝑆 ) ( ( 0 [,] 1 ) × { ( ( ( 2nd ↾ ( 𝑅 × 𝑆 ) ) ∘ 𝑓 ) ‘ 0 ) } ) )
56 isphtpc ( ( ( 2nd ↾ ( 𝑅 × 𝑆 ) ) ∘ 𝑓 ) ( ≃ph𝑆 ) ( ( 0 [,] 1 ) × { ( ( ( 2nd ↾ ( 𝑅 × 𝑆 ) ) ∘ 𝑓 ) ‘ 0 ) } ) ↔ ( ( ( 2nd ↾ ( 𝑅 × 𝑆 ) ) ∘ 𝑓 ) ∈ ( II Cn 𝑆 ) ∧ ( ( 0 [,] 1 ) × { ( ( ( 2nd ↾ ( 𝑅 × 𝑆 ) ) ∘ 𝑓 ) ‘ 0 ) } ) ∈ ( II Cn 𝑆 ) ∧ ( ( ( 2nd ↾ ( 𝑅 × 𝑆 ) ) ∘ 𝑓 ) ( PHtpy ‘ 𝑆 ) ( ( 0 [,] 1 ) × { ( ( ( 2nd ↾ ( 𝑅 × 𝑆 ) ) ∘ 𝑓 ) ‘ 0 ) } ) ) ≠ ∅ ) )
57 55 56 sylib ( ( ( 𝑅 ∈ SConn ∧ 𝑆 ∈ SConn ) ∧ ( 𝑓 ∈ ( II Cn ( 𝑅 ×t 𝑆 ) ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) → ( ( ( 2nd ↾ ( 𝑅 × 𝑆 ) ) ∘ 𝑓 ) ∈ ( II Cn 𝑆 ) ∧ ( ( 0 [,] 1 ) × { ( ( ( 2nd ↾ ( 𝑅 × 𝑆 ) ) ∘ 𝑓 ) ‘ 0 ) } ) ∈ ( II Cn 𝑆 ) ∧ ( ( ( 2nd ↾ ( 𝑅 × 𝑆 ) ) ∘ 𝑓 ) ( PHtpy ‘ 𝑆 ) ( ( 0 [,] 1 ) × { ( ( ( 2nd ↾ ( 𝑅 × 𝑆 ) ) ∘ 𝑓 ) ‘ 0 ) } ) ) ≠ ∅ ) )
58 57 simp3d ( ( ( 𝑅 ∈ SConn ∧ 𝑆 ∈ SConn ) ∧ ( 𝑓 ∈ ( II Cn ( 𝑅 ×t 𝑆 ) ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) → ( ( ( 2nd ↾ ( 𝑅 × 𝑆 ) ) ∘ 𝑓 ) ( PHtpy ‘ 𝑆 ) ( ( 0 [,] 1 ) × { ( ( ( 2nd ↾ ( 𝑅 × 𝑆 ) ) ∘ 𝑓 ) ‘ 0 ) } ) ) ≠ ∅ )
59 n0 ( ( ( ( 2nd ↾ ( 𝑅 × 𝑆 ) ) ∘ 𝑓 ) ( PHtpy ‘ 𝑆 ) ( ( 0 [,] 1 ) × { ( ( ( 2nd ↾ ( 𝑅 × 𝑆 ) ) ∘ 𝑓 ) ‘ 0 ) } ) ) ≠ ∅ ↔ ∃ ∈ ( ( ( 2nd ↾ ( 𝑅 × 𝑆 ) ) ∘ 𝑓 ) ( PHtpy ‘ 𝑆 ) ( ( 0 [,] 1 ) × { ( ( ( 2nd ↾ ( 𝑅 × 𝑆 ) ) ∘ 𝑓 ) ‘ 0 ) } ) ) )
60 58 59 sylib ( ( ( 𝑅 ∈ SConn ∧ 𝑆 ∈ SConn ) ∧ ( 𝑓 ∈ ( II Cn ( 𝑅 ×t 𝑆 ) ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) → ∃ ∈ ( ( ( 2nd ↾ ( 𝑅 × 𝑆 ) ) ∘ 𝑓 ) ( PHtpy ‘ 𝑆 ) ( ( 0 [,] 1 ) × { ( ( ( 2nd ↾ ( 𝑅 × 𝑆 ) ) ∘ 𝑓 ) ‘ 0 ) } ) ) )
61 exdistrv ( ∃ 𝑔 ( 𝑔 ∈ ( ( ( 1st ↾ ( 𝑅 × 𝑆 ) ) ∘ 𝑓 ) ( PHtpy ‘ 𝑅 ) ( ( 0 [,] 1 ) × { ( ( ( 1st ↾ ( 𝑅 × 𝑆 ) ) ∘ 𝑓 ) ‘ 0 ) } ) ) ∧ ∈ ( ( ( 2nd ↾ ( 𝑅 × 𝑆 ) ) ∘ 𝑓 ) ( PHtpy ‘ 𝑆 ) ( ( 0 [,] 1 ) × { ( ( ( 2nd ↾ ( 𝑅 × 𝑆 ) ) ∘ 𝑓 ) ‘ 0 ) } ) ) ) ↔ ( ∃ 𝑔 𝑔 ∈ ( ( ( 1st ↾ ( 𝑅 × 𝑆 ) ) ∘ 𝑓 ) ( PHtpy ‘ 𝑅 ) ( ( 0 [,] 1 ) × { ( ( ( 1st ↾ ( 𝑅 × 𝑆 ) ) ∘ 𝑓 ) ‘ 0 ) } ) ) ∧ ∃ ∈ ( ( ( 2nd ↾ ( 𝑅 × 𝑆 ) ) ∘ 𝑓 ) ( PHtpy ‘ 𝑆 ) ( ( 0 [,] 1 ) × { ( ( ( 2nd ↾ ( 𝑅 × 𝑆 ) ) ∘ 𝑓 ) ‘ 0 ) } ) ) ) )
62 8 adantr ( ( ( ( 𝑅 ∈ SConn ∧ 𝑆 ∈ SConn ) ∧ ( 𝑓 ∈ ( II Cn ( 𝑅 ×t 𝑆 ) ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) ∧ ( 𝑔 ∈ ( ( ( 1st ↾ ( 𝑅 × 𝑆 ) ) ∘ 𝑓 ) ( PHtpy ‘ 𝑅 ) ( ( 0 [,] 1 ) × { ( ( ( 1st ↾ ( 𝑅 × 𝑆 ) ) ∘ 𝑓 ) ‘ 0 ) } ) ) ∧ ∈ ( ( ( 2nd ↾ ( 𝑅 × 𝑆 ) ) ∘ 𝑓 ) ( PHtpy ‘ 𝑆 ) ( ( 0 [,] 1 ) × { ( ( ( 2nd ↾ ( 𝑅 × 𝑆 ) ) ∘ 𝑓 ) ‘ 0 ) } ) ) ) ) → 𝑅 ∈ Top )
63 13 adantr ( ( ( ( 𝑅 ∈ SConn ∧ 𝑆 ∈ SConn ) ∧ ( 𝑓 ∈ ( II Cn ( 𝑅 ×t 𝑆 ) ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) ∧ ( 𝑔 ∈ ( ( ( 1st ↾ ( 𝑅 × 𝑆 ) ) ∘ 𝑓 ) ( PHtpy ‘ 𝑅 ) ( ( 0 [,] 1 ) × { ( ( ( 1st ↾ ( 𝑅 × 𝑆 ) ) ∘ 𝑓 ) ‘ 0 ) } ) ) ∧ ∈ ( ( ( 2nd ↾ ( 𝑅 × 𝑆 ) ) ∘ 𝑓 ) ( PHtpy ‘ 𝑆 ) ( ( 0 [,] 1 ) × { ( ( ( 2nd ↾ ( 𝑅 × 𝑆 ) ) ∘ 𝑓 ) ‘ 0 ) } ) ) ) ) → 𝑆 ∈ Top )
64 6 adantr ( ( ( ( 𝑅 ∈ SConn ∧ 𝑆 ∈ SConn ) ∧ ( 𝑓 ∈ ( II Cn ( 𝑅 ×t 𝑆 ) ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) ∧ ( 𝑔 ∈ ( ( ( 1st ↾ ( 𝑅 × 𝑆 ) ) ∘ 𝑓 ) ( PHtpy ‘ 𝑅 ) ( ( 0 [,] 1 ) × { ( ( ( 1st ↾ ( 𝑅 × 𝑆 ) ) ∘ 𝑓 ) ‘ 0 ) } ) ) ∧ ∈ ( ( ( 2nd ↾ ( 𝑅 × 𝑆 ) ) ∘ 𝑓 ) ( PHtpy ‘ 𝑆 ) ( ( 0 [,] 1 ) × { ( ( ( 2nd ↾ ( 𝑅 × 𝑆 ) ) ∘ 𝑓 ) ‘ 0 ) } ) ) ) ) → 𝑓 ∈ ( II Cn ( 𝑅 ×t 𝑆 ) ) )
65 eqid ( ( 1st ↾ ( 𝑅 × 𝑆 ) ) ∘ 𝑓 ) = ( ( 1st ↾ ( 𝑅 × 𝑆 ) ) ∘ 𝑓 )
66 eqid ( ( 2nd ↾ ( 𝑅 × 𝑆 ) ) ∘ 𝑓 ) = ( ( 2nd ↾ ( 𝑅 × 𝑆 ) ) ∘ 𝑓 )
67 simprl ( ( ( ( 𝑅 ∈ SConn ∧ 𝑆 ∈ SConn ) ∧ ( 𝑓 ∈ ( II Cn ( 𝑅 ×t 𝑆 ) ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) ∧ ( 𝑔 ∈ ( ( ( 1st ↾ ( 𝑅 × 𝑆 ) ) ∘ 𝑓 ) ( PHtpy ‘ 𝑅 ) ( ( 0 [,] 1 ) × { ( ( ( 1st ↾ ( 𝑅 × 𝑆 ) ) ∘ 𝑓 ) ‘ 0 ) } ) ) ∧ ∈ ( ( ( 2nd ↾ ( 𝑅 × 𝑆 ) ) ∘ 𝑓 ) ( PHtpy ‘ 𝑆 ) ( ( 0 [,] 1 ) × { ( ( ( 2nd ↾ ( 𝑅 × 𝑆 ) ) ∘ 𝑓 ) ‘ 0 ) } ) ) ) ) → 𝑔 ∈ ( ( ( 1st ↾ ( 𝑅 × 𝑆 ) ) ∘ 𝑓 ) ( PHtpy ‘ 𝑅 ) ( ( 0 [,] 1 ) × { ( ( ( 1st ↾ ( 𝑅 × 𝑆 ) ) ∘ 𝑓 ) ‘ 0 ) } ) ) )
68 simprr ( ( ( ( 𝑅 ∈ SConn ∧ 𝑆 ∈ SConn ) ∧ ( 𝑓 ∈ ( II Cn ( 𝑅 ×t 𝑆 ) ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) ∧ ( 𝑔 ∈ ( ( ( 1st ↾ ( 𝑅 × 𝑆 ) ) ∘ 𝑓 ) ( PHtpy ‘ 𝑅 ) ( ( 0 [,] 1 ) × { ( ( ( 1st ↾ ( 𝑅 × 𝑆 ) ) ∘ 𝑓 ) ‘ 0 ) } ) ) ∧ ∈ ( ( ( 2nd ↾ ( 𝑅 × 𝑆 ) ) ∘ 𝑓 ) ( PHtpy ‘ 𝑆 ) ( ( 0 [,] 1 ) × { ( ( ( 2nd ↾ ( 𝑅 × 𝑆 ) ) ∘ 𝑓 ) ‘ 0 ) } ) ) ) ) → ∈ ( ( ( 2nd ↾ ( 𝑅 × 𝑆 ) ) ∘ 𝑓 ) ( PHtpy ‘ 𝑆 ) ( ( 0 [,] 1 ) × { ( ( ( 2nd ↾ ( 𝑅 × 𝑆 ) ) ∘ 𝑓 ) ‘ 0 ) } ) ) )
69 62 63 64 65 66 67 68 txsconnlem ( ( ( ( 𝑅 ∈ SConn ∧ 𝑆 ∈ SConn ) ∧ ( 𝑓 ∈ ( II Cn ( 𝑅 ×t 𝑆 ) ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) ∧ ( 𝑔 ∈ ( ( ( 1st ↾ ( 𝑅 × 𝑆 ) ) ∘ 𝑓 ) ( PHtpy ‘ 𝑅 ) ( ( 0 [,] 1 ) × { ( ( ( 1st ↾ ( 𝑅 × 𝑆 ) ) ∘ 𝑓 ) ‘ 0 ) } ) ) ∧ ∈ ( ( ( 2nd ↾ ( 𝑅 × 𝑆 ) ) ∘ 𝑓 ) ( PHtpy ‘ 𝑆 ) ( ( 0 [,] 1 ) × { ( ( ( 2nd ↾ ( 𝑅 × 𝑆 ) ) ∘ 𝑓 ) ‘ 0 ) } ) ) ) ) → 𝑓 ( ≃ph ‘ ( 𝑅 ×t 𝑆 ) ) ( ( 0 [,] 1 ) × { ( 𝑓 ‘ 0 ) } ) )
70 69 ex ( ( ( 𝑅 ∈ SConn ∧ 𝑆 ∈ SConn ) ∧ ( 𝑓 ∈ ( II Cn ( 𝑅 ×t 𝑆 ) ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) → ( ( 𝑔 ∈ ( ( ( 1st ↾ ( 𝑅 × 𝑆 ) ) ∘ 𝑓 ) ( PHtpy ‘ 𝑅 ) ( ( 0 [,] 1 ) × { ( ( ( 1st ↾ ( 𝑅 × 𝑆 ) ) ∘ 𝑓 ) ‘ 0 ) } ) ) ∧ ∈ ( ( ( 2nd ↾ ( 𝑅 × 𝑆 ) ) ∘ 𝑓 ) ( PHtpy ‘ 𝑆 ) ( ( 0 [,] 1 ) × { ( ( ( 2nd ↾ ( 𝑅 × 𝑆 ) ) ∘ 𝑓 ) ‘ 0 ) } ) ) ) → 𝑓 ( ≃ph ‘ ( 𝑅 ×t 𝑆 ) ) ( ( 0 [,] 1 ) × { ( 𝑓 ‘ 0 ) } ) ) )
71 70 exlimdvv ( ( ( 𝑅 ∈ SConn ∧ 𝑆 ∈ SConn ) ∧ ( 𝑓 ∈ ( II Cn ( 𝑅 ×t 𝑆 ) ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) → ( ∃ 𝑔 ( 𝑔 ∈ ( ( ( 1st ↾ ( 𝑅 × 𝑆 ) ) ∘ 𝑓 ) ( PHtpy ‘ 𝑅 ) ( ( 0 [,] 1 ) × { ( ( ( 1st ↾ ( 𝑅 × 𝑆 ) ) ∘ 𝑓 ) ‘ 0 ) } ) ) ∧ ∈ ( ( ( 2nd ↾ ( 𝑅 × 𝑆 ) ) ∘ 𝑓 ) ( PHtpy ‘ 𝑆 ) ( ( 0 [,] 1 ) × { ( ( ( 2nd ↾ ( 𝑅 × 𝑆 ) ) ∘ 𝑓 ) ‘ 0 ) } ) ) ) → 𝑓 ( ≃ph ‘ ( 𝑅 ×t 𝑆 ) ) ( ( 0 [,] 1 ) × { ( 𝑓 ‘ 0 ) } ) ) )
72 61 71 syl5bir ( ( ( 𝑅 ∈ SConn ∧ 𝑆 ∈ SConn ) ∧ ( 𝑓 ∈ ( II Cn ( 𝑅 ×t 𝑆 ) ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) → ( ( ∃ 𝑔 𝑔 ∈ ( ( ( 1st ↾ ( 𝑅 × 𝑆 ) ) ∘ 𝑓 ) ( PHtpy ‘ 𝑅 ) ( ( 0 [,] 1 ) × { ( ( ( 1st ↾ ( 𝑅 × 𝑆 ) ) ∘ 𝑓 ) ‘ 0 ) } ) ) ∧ ∃ ∈ ( ( ( 2nd ↾ ( 𝑅 × 𝑆 ) ) ∘ 𝑓 ) ( PHtpy ‘ 𝑆 ) ( ( 0 [,] 1 ) × { ( ( ( 2nd ↾ ( 𝑅 × 𝑆 ) ) ∘ 𝑓 ) ‘ 0 ) } ) ) ) → 𝑓 ( ≃ph ‘ ( 𝑅 ×t 𝑆 ) ) ( ( 0 [,] 1 ) × { ( 𝑓 ‘ 0 ) } ) ) )
73 42 60 72 mp2and ( ( ( 𝑅 ∈ SConn ∧ 𝑆 ∈ SConn ) ∧ ( 𝑓 ∈ ( II Cn ( 𝑅 ×t 𝑆 ) ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) → 𝑓 ( ≃ph ‘ ( 𝑅 ×t 𝑆 ) ) ( ( 0 [,] 1 ) × { ( 𝑓 ‘ 0 ) } ) )
74 73 expr ( ( ( 𝑅 ∈ SConn ∧ 𝑆 ∈ SConn ) ∧ 𝑓 ∈ ( II Cn ( 𝑅 ×t 𝑆 ) ) ) → ( ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) → 𝑓 ( ≃ph ‘ ( 𝑅 ×t 𝑆 ) ) ( ( 0 [,] 1 ) × { ( 𝑓 ‘ 0 ) } ) ) )
75 74 ralrimiva ( ( 𝑅 ∈ SConn ∧ 𝑆 ∈ SConn ) → ∀ 𝑓 ∈ ( II Cn ( 𝑅 ×t 𝑆 ) ) ( ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) → 𝑓 ( ≃ph ‘ ( 𝑅 ×t 𝑆 ) ) ( ( 0 [,] 1 ) × { ( 𝑓 ‘ 0 ) } ) ) )
76 issconn ( ( 𝑅 ×t 𝑆 ) ∈ SConn ↔ ( ( 𝑅 ×t 𝑆 ) ∈ PConn ∧ ∀ 𝑓 ∈ ( II Cn ( 𝑅 ×t 𝑆 ) ) ( ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) → 𝑓 ( ≃ph ‘ ( 𝑅 ×t 𝑆 ) ) ( ( 0 [,] 1 ) × { ( 𝑓 ‘ 0 ) } ) ) ) )
77 4 75 76 sylanbrc ( ( 𝑅 ∈ SConn ∧ 𝑆 ∈ SConn ) → ( 𝑅 ×t 𝑆 ) ∈ SConn )