Metamath Proof Explorer

Theorem sconnpi1

Description: A path-connected topological space is simply connected iff its fundamental group is trivial. (Contributed by Mario Carneiro, 12-Feb-2015)

Ref Expression
Hypothesis sconnpi1.1 ⊢ 𝑋 = ∪ 𝐽
Assertion sconnpi1 ( ( 𝐽 ∈ PConn ∧ 𝑌 ∈ 𝑋 ) → ( 𝐽 ∈ SConn ↔ ( Base ‘ ( 𝐽 π1 𝑌 ) ) ≈ 1o ) )

Proof

Step Hyp Ref Expression
1 sconnpi1.1 ⊢ 𝑋 = ∪ 𝐽
2 sconntop ⊢ ( 𝐽 ∈ SConn → 𝐽 ∈ Top )
3 2 adantl ⊢ ( ( 𝑌 ∈ 𝑋 ∧ 𝐽 ∈ SConn ) → 𝐽 ∈ Top )
4 simpl ⊢ ( ( 𝑌 ∈ 𝑋 ∧ 𝐽 ∈ SConn ) → 𝑌 ∈ 𝑋 )
5 eqid ⊢ ( 𝐽 π1 𝑌 ) = ( 𝐽 π1 𝑌 )
6 eqid ⊢ ( Base ‘ ( 𝐽 π1 𝑌 ) ) = ( Base ‘ ( 𝐽 π1 𝑌 ) )
7 simpl ⊢ ( ( 𝐽 ∈ Top ∧ 𝑌 ∈ 𝑋 ) → 𝐽 ∈ Top )
8 1 toptopon ⊢ ( 𝐽 ∈ Top ↔ 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
9 7 8 sylib ⊢ ( ( 𝐽 ∈ Top ∧ 𝑌 ∈ 𝑋 ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
10 simpr ⊢ ( ( 𝐽 ∈ Top ∧ 𝑌 ∈ 𝑋 ) → 𝑌 ∈ 𝑋 )
11 5 6 9 10 elpi1 ⊢ ( ( 𝐽 ∈ Top ∧ 𝑌 ∈ 𝑋 ) → ( 𝑥 ∈ ( Base ‘ ( 𝐽 π1 𝑌 ) ) ↔ ∃ 𝑓 ∈ ( II Cn 𝐽 ) ( ( ( 𝑓 ‘ 0 ) = 𝑌 ∧ ( 𝑓 ‘ 1 ) = 𝑌 ) ∧ 𝑥 = [ 𝑓 ] ( ≃ph ‘ 𝐽 ) ) ) )
12 3 4 11 syl2anc ⊢ ( ( 𝑌 ∈ 𝑋 ∧ 𝐽 ∈ SConn ) → ( 𝑥 ∈ ( Base ‘ ( 𝐽 π1 𝑌 ) ) ↔ ∃ 𝑓 ∈ ( II Cn 𝐽 ) ( ( ( 𝑓 ‘ 0 ) = 𝑌 ∧ ( 𝑓 ‘ 1 ) = 𝑌 ) ∧ 𝑥 = [ 𝑓 ] ( ≃ph ‘ 𝐽 ) ) ) )
13 phtpcer ⊢ ( ≃ph ‘ 𝐽 ) Er ( II Cn 𝐽 )
14 13 a1i ⊢ ( ( ( ( 𝑌 ∈ 𝑋 ∧ 𝐽 ∈ SConn ) ∧ 𝑓 ∈ ( II Cn 𝐽 ) ) ∧ ( ( 𝑓 ‘ 0 ) = 𝑌 ∧ ( 𝑓 ‘ 1 ) = 𝑌 ) ) → ( ≃ph ‘ 𝐽 ) Er ( II Cn 𝐽 ) )
15 simpllr ⊢ ( ( ( ( 𝑌 ∈ 𝑋 ∧ 𝐽 ∈ SConn ) ∧ 𝑓 ∈ ( II Cn 𝐽 ) ) ∧ ( ( 𝑓 ‘ 0 ) = 𝑌 ∧ ( 𝑓 ‘ 1 ) = 𝑌 ) ) → 𝐽 ∈ SConn )
16 simplr ⊢ ( ( ( ( 𝑌 ∈ 𝑋 ∧ 𝐽 ∈ SConn ) ∧ 𝑓 ∈ ( II Cn 𝐽 ) ) ∧ ( ( 𝑓 ‘ 0 ) = 𝑌 ∧ ( 𝑓 ‘ 1 ) = 𝑌 ) ) → 𝑓 ∈ ( II Cn 𝐽 ) )
17 simprl ⊢ ( ( ( ( 𝑌 ∈ 𝑋 ∧ 𝐽 ∈ SConn ) ∧ 𝑓 ∈ ( II Cn 𝐽 ) ) ∧ ( ( 𝑓 ‘ 0 ) = 𝑌 ∧ ( 𝑓 ‘ 1 ) = 𝑌 ) ) → ( 𝑓 ‘ 0 ) = 𝑌 )
18 simprr ⊢ ( ( ( ( 𝑌 ∈ 𝑋 ∧ 𝐽 ∈ SConn ) ∧ 𝑓 ∈ ( II Cn 𝐽 ) ) ∧ ( ( 𝑓 ‘ 0 ) = 𝑌 ∧ ( 𝑓 ‘ 1 ) = 𝑌 ) ) → ( 𝑓 ‘ 1 ) = 𝑌 )
19 17 18 eqtr4d ⊢ ( ( ( ( 𝑌 ∈ 𝑋 ∧ 𝐽 ∈ SConn ) ∧ 𝑓 ∈ ( II Cn 𝐽 ) ) ∧ ( ( 𝑓 ‘ 0 ) = 𝑌 ∧ ( 𝑓 ‘ 1 ) = 𝑌 ) ) → ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) )
20 sconnpht ⊢ ( ( 𝐽 ∈ SConn ∧ 𝑓 ∈ ( II Cn 𝐽 ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) → 𝑓 ( ≃ph ‘ 𝐽 ) ( ( 0 [,] 1 ) × { ( 𝑓 ‘ 0 ) } ) )
21 15 16 19 20 syl3anc ⊢ ( ( ( ( 𝑌 ∈ 𝑋 ∧ 𝐽 ∈ SConn ) ∧ 𝑓 ∈ ( II Cn 𝐽 ) ) ∧ ( ( 𝑓 ‘ 0 ) = 𝑌 ∧ ( 𝑓 ‘ 1 ) = 𝑌 ) ) → 𝑓 ( ≃ph ‘ 𝐽 ) ( ( 0 [,] 1 ) × { ( 𝑓 ‘ 0 ) } ) )
22 17 sneqd ⊢ ( ( ( ( 𝑌 ∈ 𝑋 ∧ 𝐽 ∈ SConn ) ∧ 𝑓 ∈ ( II Cn 𝐽 ) ) ∧ ( ( 𝑓 ‘ 0 ) = 𝑌 ∧ ( 𝑓 ‘ 1 ) = 𝑌 ) ) → { ( 𝑓 ‘ 0 ) } = { 𝑌 } )
23 22 xpeq2d ⊢ ( ( ( ( 𝑌 ∈ 𝑋 ∧ 𝐽 ∈ SConn ) ∧ 𝑓 ∈ ( II Cn 𝐽 ) ) ∧ ( ( 𝑓 ‘ 0 ) = 𝑌 ∧ ( 𝑓 ‘ 1 ) = 𝑌 ) ) → ( ( 0 [,] 1 ) × { ( 𝑓 ‘ 0 ) } ) = ( ( 0 [,] 1 ) × { 𝑌 } ) )
24 21 23 breqtrd ⊢ ( ( ( ( 𝑌 ∈ 𝑋 ∧ 𝐽 ∈ SConn ) ∧ 𝑓 ∈ ( II Cn 𝐽 ) ) ∧ ( ( 𝑓 ‘ 0 ) = 𝑌 ∧ ( 𝑓 ‘ 1 ) = 𝑌 ) ) → 𝑓 ( ≃ph ‘ 𝐽 ) ( ( 0 [,] 1 ) × { 𝑌 } ) )
25 14 24 erthi ⊢ ( ( ( ( 𝑌 ∈ 𝑋 ∧ 𝐽 ∈ SConn ) ∧ 𝑓 ∈ ( II Cn 𝐽 ) ) ∧ ( ( 𝑓 ‘ 0 ) = 𝑌 ∧ ( 𝑓 ‘ 1 ) = 𝑌 ) ) → [ 𝑓 ] ( ≃ph ‘ 𝐽 ) = [ ( ( 0 [,] 1 ) × { 𝑌 } ) ] ( ≃ph ‘ 𝐽 ) )
26 3 8 sylib ⊢ ( ( 𝑌 ∈ 𝑋 ∧ 𝐽 ∈ SConn ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
27 eqid ⊢ ( ( 0 [,] 1 ) × { 𝑌 } ) = ( ( 0 [,] 1 ) × { 𝑌 } )
28 5 27 pi1id ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑌 ∈ 𝑋 ) → [ ( ( 0 [,] 1 ) × { 𝑌 } ) ] ( ≃ph ‘ 𝐽 ) = ( 0g ‘ ( 𝐽 π1 𝑌 ) ) )
29 26 4 28 syl2anc ⊢ ( ( 𝑌 ∈ 𝑋 ∧ 𝐽 ∈ SConn ) → [ ( ( 0 [,] 1 ) × { 𝑌 } ) ] ( ≃ph ‘ 𝐽 ) = ( 0g ‘ ( 𝐽 π1 𝑌 ) ) )
30 29 ad2antrr ⊢ ( ( ( ( 𝑌 ∈ 𝑋 ∧ 𝐽 ∈ SConn ) ∧ 𝑓 ∈ ( II Cn 𝐽 ) ) ∧ ( ( 𝑓 ‘ 0 ) = 𝑌 ∧ ( 𝑓 ‘ 1 ) = 𝑌 ) ) → [ ( ( 0 [,] 1 ) × { 𝑌 } ) ] ( ≃ph ‘ 𝐽 ) = ( 0g ‘ ( 𝐽 π1 𝑌 ) ) )
31 25 30 eqtrd ⊢ ( ( ( ( 𝑌 ∈ 𝑋 ∧ 𝐽 ∈ SConn ) ∧ 𝑓 ∈ ( II Cn 𝐽 ) ) ∧ ( ( 𝑓 ‘ 0 ) = 𝑌 ∧ ( 𝑓 ‘ 1 ) = 𝑌 ) ) → [ 𝑓 ] ( ≃ph ‘ 𝐽 ) = ( 0g ‘ ( 𝐽 π1 𝑌 ) ) )
32 velsn ⊢ ( 𝑥 ∈ { ( 0g ‘ ( 𝐽 π1 𝑌 ) ) } ↔ 𝑥 = ( 0g ‘ ( 𝐽 π1 𝑌 ) ) )
33 eqeq1 ⊢ ( 𝑥 = [ 𝑓 ] ( ≃ph ‘ 𝐽 ) → ( 𝑥 = ( 0g ‘ ( 𝐽 π1 𝑌 ) ) ↔ [ 𝑓 ] ( ≃ph ‘ 𝐽 ) = ( 0g ‘ ( 𝐽 π1 𝑌 ) ) ) )
34 32 33 syl5bb ⊢ ( 𝑥 = [ 𝑓 ] ( ≃ph ‘ 𝐽 ) → ( 𝑥 ∈ { ( 0g ‘ ( 𝐽 π1 𝑌 ) ) } ↔ [ 𝑓 ] ( ≃ph ‘ 𝐽 ) = ( 0g ‘ ( 𝐽 π1 𝑌 ) ) ) )
35 31 34 syl5ibrcom ⊢ ( ( ( ( 𝑌 ∈ 𝑋 ∧ 𝐽 ∈ SConn ) ∧ 𝑓 ∈ ( II Cn 𝐽 ) ) ∧ ( ( 𝑓 ‘ 0 ) = 𝑌 ∧ ( 𝑓 ‘ 1 ) = 𝑌 ) ) → ( 𝑥 = [ 𝑓 ] ( ≃ph ‘ 𝐽 ) → 𝑥 ∈ { ( 0g ‘ ( 𝐽 π1 𝑌 ) ) } ) )
36 35 expimpd ⊢ ( ( ( 𝑌 ∈ 𝑋 ∧ 𝐽 ∈ SConn ) ∧ 𝑓 ∈ ( II Cn 𝐽 ) ) → ( ( ( ( 𝑓 ‘ 0 ) = 𝑌 ∧ ( 𝑓 ‘ 1 ) = 𝑌 ) ∧ 𝑥 = [ 𝑓 ] ( ≃ph ‘ 𝐽 ) ) → 𝑥 ∈ { ( 0g ‘ ( 𝐽 π1 𝑌 ) ) } ) )
37 36 rexlimdva ⊢ ( ( 𝑌 ∈ 𝑋 ∧ 𝐽 ∈ SConn ) → ( ∃ 𝑓 ∈ ( II Cn 𝐽 ) ( ( ( 𝑓 ‘ 0 ) = 𝑌 ∧ ( 𝑓 ‘ 1 ) = 𝑌 ) ∧ 𝑥 = [ 𝑓 ] ( ≃ph ‘ 𝐽 ) ) → 𝑥 ∈ { ( 0g ‘ ( 𝐽 π1 𝑌 ) ) } ) )
38 12 37 sylbid ⊢ ( ( 𝑌 ∈ 𝑋 ∧ 𝐽 ∈ SConn ) → ( 𝑥 ∈ ( Base ‘ ( 𝐽 π1 𝑌 ) ) → 𝑥 ∈ { ( 0g ‘ ( 𝐽 π1 𝑌 ) ) } ) )
39 38 ssrdv ⊢ ( ( 𝑌 ∈ 𝑋 ∧ 𝐽 ∈ SConn ) → ( Base ‘ ( 𝐽 π1 𝑌 ) ) ⊆ { ( 0g ‘ ( 𝐽 π1 𝑌 ) ) } )
40 5 pi1grp ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑌 ∈ 𝑋 ) → ( 𝐽 π1 𝑌 ) ∈ Grp )
41 26 4 40 syl2anc ⊢ ( ( 𝑌 ∈ 𝑋 ∧ 𝐽 ∈ SConn ) → ( 𝐽 π1 𝑌 ) ∈ Grp )
42 eqid ⊢ ( 0g ‘ ( 𝐽 π1 𝑌 ) ) = ( 0g ‘ ( 𝐽 π1 𝑌 ) )
43 6 42 grpidcl ⊢ ( ( 𝐽 π1 𝑌 ) ∈ Grp → ( 0g ‘ ( 𝐽 π1 𝑌 ) ) ∈ ( Base ‘ ( 𝐽 π1 𝑌 ) ) )
44 41 43 syl ⊢ ( ( 𝑌 ∈ 𝑋 ∧ 𝐽 ∈ SConn ) → ( 0g ‘ ( 𝐽 π1 𝑌 ) ) ∈ ( Base ‘ ( 𝐽 π1 𝑌 ) ) )
45 44 snssd ⊢ ( ( 𝑌 ∈ 𝑋 ∧ 𝐽 ∈ SConn ) → { ( 0g ‘ ( 𝐽 π1 𝑌 ) ) } ⊆ ( Base ‘ ( 𝐽 π1 𝑌 ) ) )
46 39 45 eqssd ⊢ ( ( 𝑌 ∈ 𝑋 ∧ 𝐽 ∈ SConn ) → ( Base ‘ ( 𝐽 π1 𝑌 ) ) = { ( 0g ‘ ( 𝐽 π1 𝑌 ) ) } )
47 fvex ⊢ ( 0g ‘ ( 𝐽 π1 𝑌 ) ) ∈ V
48 47 ensn1 ⊢ { ( 0g ‘ ( 𝐽 π1 𝑌 ) ) } ≈ 1o
49 46 48 eqbrtrdi ⊢ ( ( 𝑌 ∈ 𝑋 ∧ 𝐽 ∈ SConn ) → ( Base ‘ ( 𝐽 π1 𝑌 ) ) ≈ 1o )
50 49 adantll ⊢ ( ( ( 𝐽 ∈ PConn ∧ 𝑌 ∈ 𝑋 ) ∧ 𝐽 ∈ SConn ) → ( Base ‘ ( 𝐽 π1 𝑌 ) ) ≈ 1o )
51 simpll ⊢ ( ( ( 𝐽 ∈ PConn ∧ 𝑌 ∈ 𝑋 ) ∧ ( Base ‘ ( 𝐽 π1 𝑌 ) ) ≈ 1o ) → 𝐽 ∈ PConn )
52 eqid ⊢ ( 𝐽 π1 ( 𝑓 ‘ 0 ) ) = ( 𝐽 π1 ( 𝑓 ‘ 0 ) )
53 eqid ⊢ ( Base ‘ ( 𝐽 π1 ( 𝑓 ‘ 0 ) ) ) = ( Base ‘ ( 𝐽 π1 ( 𝑓 ‘ 0 ) ) )
54 simplll ⊢ ( ( ( ( 𝐽 ∈ PConn ∧ 𝑌 ∈ 𝑋 ) ∧ ( Base ‘ ( 𝐽 π1 𝑌 ) ) ≈ 1o ) ∧ ( 𝑓 ∈ ( II Cn 𝐽 ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) → 𝐽 ∈ PConn )
55 pconntop ⊢ ( 𝐽 ∈ PConn → 𝐽 ∈ Top )
56 54 55 syl ⊢ ( ( ( ( 𝐽 ∈ PConn ∧ 𝑌 ∈ 𝑋 ) ∧ ( Base ‘ ( 𝐽 π1 𝑌 ) ) ≈ 1o ) ∧ ( 𝑓 ∈ ( II Cn 𝐽 ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) → 𝐽 ∈ Top )
57 56 8 sylib ⊢ ( ( ( ( 𝐽 ∈ PConn ∧ 𝑌 ∈ 𝑋 ) ∧ ( Base ‘ ( 𝐽 π1 𝑌 ) ) ≈ 1o ) ∧ ( 𝑓 ∈ ( II Cn 𝐽 ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
58 simprl ⊢ ( ( ( ( 𝐽 ∈ PConn ∧ 𝑌 ∈ 𝑋 ) ∧ ( Base ‘ ( 𝐽 π1 𝑌 ) ) ≈ 1o ) ∧ ( 𝑓 ∈ ( II Cn 𝐽 ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) → 𝑓 ∈ ( II Cn 𝐽 ) )
59 iiuni ⊢ ( 0 [,] 1 ) = ∪ II
60 59 1 cnf ⊢ ( 𝑓 ∈ ( II Cn 𝐽 ) → 𝑓 : ( 0 [,] 1 ) ⟶ 𝑋 )
61 58 60 syl ⊢ ( ( ( ( 𝐽 ∈ PConn ∧ 𝑌 ∈ 𝑋 ) ∧ ( Base ‘ ( 𝐽 π1 𝑌 ) ) ≈ 1o ) ∧ ( 𝑓 ∈ ( II Cn 𝐽 ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) → 𝑓 : ( 0 [,] 1 ) ⟶ 𝑋 )
62 0elunit ⊢ 0 ∈ ( 0 [,] 1 )
63 ffvelrn ⊢ ( ( 𝑓 : ( 0 [,] 1 ) ⟶ 𝑋 ∧ 0 ∈ ( 0 [,] 1 ) ) → ( 𝑓 ‘ 0 ) ∈ 𝑋 )
64 61 62 63 sylancl ⊢ ( ( ( ( 𝐽 ∈ PConn ∧ 𝑌 ∈ 𝑋 ) ∧ ( Base ‘ ( 𝐽 π1 𝑌 ) ) ≈ 1o ) ∧ ( 𝑓 ∈ ( II Cn 𝐽 ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) → ( 𝑓 ‘ 0 ) ∈ 𝑋 )
65 eqidd ⊢ ( ( ( ( 𝐽 ∈ PConn ∧ 𝑌 ∈ 𝑋 ) ∧ ( Base ‘ ( 𝐽 π1 𝑌 ) ) ≈ 1o ) ∧ ( 𝑓 ∈ ( II Cn 𝐽 ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) → ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 0 ) )
66 simprr ⊢ ( ( ( ( 𝐽 ∈ PConn ∧ 𝑌 ∈ 𝑋 ) ∧ ( Base ‘ ( 𝐽 π1 𝑌 ) ) ≈ 1o ) ∧ ( 𝑓 ∈ ( II Cn 𝐽 ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) → ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) )
67 66 eqcomd ⊢ ( ( ( ( 𝐽 ∈ PConn ∧ 𝑌 ∈ 𝑋 ) ∧ ( Base ‘ ( 𝐽 π1 𝑌 ) ) ≈ 1o ) ∧ ( 𝑓 ∈ ( II Cn 𝐽 ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) → ( 𝑓 ‘ 1 ) = ( 𝑓 ‘ 0 ) )
68 52 53 57 64 58 65 67 elpi1i ⊢ ( ( ( ( 𝐽 ∈ PConn ∧ 𝑌 ∈ 𝑋 ) ∧ ( Base ‘ ( 𝐽 π1 𝑌 ) ) ≈ 1o ) ∧ ( 𝑓 ∈ ( II Cn 𝐽 ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) → [ 𝑓 ] ( ≃ph ‘ 𝐽 ) ∈ ( Base ‘ ( 𝐽 π1 ( 𝑓 ‘ 0 ) ) ) )
69 eqid ⊢ ( ( 0 [,] 1 ) × { ( 𝑓 ‘ 0 ) } ) = ( ( 0 [,] 1 ) × { ( 𝑓 ‘ 0 ) } )
70 69 pcoptcl ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( 𝑓 ‘ 0 ) ∈ 𝑋 ) → ( ( ( 0 [,] 1 ) × { ( 𝑓 ‘ 0 ) } ) ∈ ( II Cn 𝐽 ) ∧ ( ( ( 0 [,] 1 ) × { ( 𝑓 ‘ 0 ) } ) ‘ 0 ) = ( 𝑓 ‘ 0 ) ∧ ( ( ( 0 [,] 1 ) × { ( 𝑓 ‘ 0 ) } ) ‘ 1 ) = ( 𝑓 ‘ 0 ) ) )
71 57 64 70 syl2anc ⊢ ( ( ( ( 𝐽 ∈ PConn ∧ 𝑌 ∈ 𝑋 ) ∧ ( Base ‘ ( 𝐽 π1 𝑌 ) ) ≈ 1o ) ∧ ( 𝑓 ∈ ( II Cn 𝐽 ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) → ( ( ( 0 [,] 1 ) × { ( 𝑓 ‘ 0 ) } ) ∈ ( II Cn 𝐽 ) ∧ ( ( ( 0 [,] 1 ) × { ( 𝑓 ‘ 0 ) } ) ‘ 0 ) = ( 𝑓 ‘ 0 ) ∧ ( ( ( 0 [,] 1 ) × { ( 𝑓 ‘ 0 ) } ) ‘ 1 ) = ( 𝑓 ‘ 0 ) ) )
72 71 simp1d ⊢ ( ( ( ( 𝐽 ∈ PConn ∧ 𝑌 ∈ 𝑋 ) ∧ ( Base ‘ ( 𝐽 π1 𝑌 ) ) ≈ 1o ) ∧ ( 𝑓 ∈ ( II Cn 𝐽 ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) → ( ( 0 [,] 1 ) × { ( 𝑓 ‘ 0 ) } ) ∈ ( II Cn 𝐽 ) )
73 71 simp2d ⊢ ( ( ( ( 𝐽 ∈ PConn ∧ 𝑌 ∈ 𝑋 ) ∧ ( Base ‘ ( 𝐽 π1 𝑌 ) ) ≈ 1o ) ∧ ( 𝑓 ∈ ( II Cn 𝐽 ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) → ( ( ( 0 [,] 1 ) × { ( 𝑓 ‘ 0 ) } ) ‘ 0 ) = ( 𝑓 ‘ 0 ) )
74 71 simp3d ⊢ ( ( ( ( 𝐽 ∈ PConn ∧ 𝑌 ∈ 𝑋 ) ∧ ( Base ‘ ( 𝐽 π1 𝑌 ) ) ≈ 1o ) ∧ ( 𝑓 ∈ ( II Cn 𝐽 ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) → ( ( ( 0 [,] 1 ) × { ( 𝑓 ‘ 0 ) } ) ‘ 1 ) = ( 𝑓 ‘ 0 ) )
75 52 53 57 64 72 73 74 elpi1i ⊢ ( ( ( ( 𝐽 ∈ PConn ∧ 𝑌 ∈ 𝑋 ) ∧ ( Base ‘ ( 𝐽 π1 𝑌 ) ) ≈ 1o ) ∧ ( 𝑓 ∈ ( II Cn 𝐽 ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) → [ ( ( 0 [,] 1 ) × { ( 𝑓 ‘ 0 ) } ) ] ( ≃ph ‘ 𝐽 ) ∈ ( Base ‘ ( 𝐽 π1 ( 𝑓 ‘ 0 ) ) ) )
76 simpllr ⊢ ( ( ( ( 𝐽 ∈ PConn ∧ 𝑌 ∈ 𝑋 ) ∧ ( Base ‘ ( 𝐽 π1 𝑌 ) ) ≈ 1o ) ∧ ( 𝑓 ∈ ( II Cn 𝐽 ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) → 𝑌 ∈ 𝑋 )
77 1 52 5 53 6 pconnpi1 ⊢ ( ( 𝐽 ∈ PConn ∧ ( 𝑓 ‘ 0 ) ∈ 𝑋 ∧ 𝑌 ∈ 𝑋 ) → ( 𝐽 π1 ( 𝑓 ‘ 0 ) ) ≃𝑔 ( 𝐽 π1 𝑌 ) )
78 54 64 76 77 syl3anc ⊢ ( ( ( ( 𝐽 ∈ PConn ∧ 𝑌 ∈ 𝑋 ) ∧ ( Base ‘ ( 𝐽 π1 𝑌 ) ) ≈ 1o ) ∧ ( 𝑓 ∈ ( II Cn 𝐽 ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) → ( 𝐽 π1 ( 𝑓 ‘ 0 ) ) ≃𝑔 ( 𝐽 π1 𝑌 ) )
79 53 6 gicen ⊢ ( ( 𝐽 π1 ( 𝑓 ‘ 0 ) ) ≃𝑔 ( 𝐽 π1 𝑌 ) → ( Base ‘ ( 𝐽 π1 ( 𝑓 ‘ 0 ) ) ) ≈ ( Base ‘ ( 𝐽 π1 𝑌 ) ) )
80 78 79 syl ⊢ ( ( ( ( 𝐽 ∈ PConn ∧ 𝑌 ∈ 𝑋 ) ∧ ( Base ‘ ( 𝐽 π1 𝑌 ) ) ≈ 1o ) ∧ ( 𝑓 ∈ ( II Cn 𝐽 ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) → ( Base ‘ ( 𝐽 π1 ( 𝑓 ‘ 0 ) ) ) ≈ ( Base ‘ ( 𝐽 π1 𝑌 ) ) )
81 simplr ⊢ ( ( ( ( 𝐽 ∈ PConn ∧ 𝑌 ∈ 𝑋 ) ∧ ( Base ‘ ( 𝐽 π1 𝑌 ) ) ≈ 1o ) ∧ ( 𝑓 ∈ ( II Cn 𝐽 ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) → ( Base ‘ ( 𝐽 π1 𝑌 ) ) ≈ 1o )
82 entr ⊢ ( ( ( Base ‘ ( 𝐽 π1 ( 𝑓 ‘ 0 ) ) ) ≈ ( Base ‘ ( 𝐽 π1 𝑌 ) ) ∧ ( Base ‘ ( 𝐽 π1 𝑌 ) ) ≈ 1o ) → ( Base ‘ ( 𝐽 π1 ( 𝑓 ‘ 0 ) ) ) ≈ 1o )
83 80 81 82 syl2anc ⊢ ( ( ( ( 𝐽 ∈ PConn ∧ 𝑌 ∈ 𝑋 ) ∧ ( Base ‘ ( 𝐽 π1 𝑌 ) ) ≈ 1o ) ∧ ( 𝑓 ∈ ( II Cn 𝐽 ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) → ( Base ‘ ( 𝐽 π1 ( 𝑓 ‘ 0 ) ) ) ≈ 1o )
84 en1eqsn ⊢ ( ( [ ( ( 0 [,] 1 ) × { ( 𝑓 ‘ 0 ) } ) ] ( ≃ph ‘ 𝐽 ) ∈ ( Base ‘ ( 𝐽 π1 ( 𝑓 ‘ 0 ) ) ) ∧ ( Base ‘ ( 𝐽 π1 ( 𝑓 ‘ 0 ) ) ) ≈ 1o ) → ( Base ‘ ( 𝐽 π1 ( 𝑓 ‘ 0 ) ) ) = { [ ( ( 0 [,] 1 ) × { ( 𝑓 ‘ 0 ) } ) ] ( ≃ph ‘ 𝐽 ) } )
85 75 83 84 syl2anc ⊢ ( ( ( ( 𝐽 ∈ PConn ∧ 𝑌 ∈ 𝑋 ) ∧ ( Base ‘ ( 𝐽 π1 𝑌 ) ) ≈ 1o ) ∧ ( 𝑓 ∈ ( II Cn 𝐽 ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) → ( Base ‘ ( 𝐽 π1 ( 𝑓 ‘ 0 ) ) ) = { [ ( ( 0 [,] 1 ) × { ( 𝑓 ‘ 0 ) } ) ] ( ≃ph ‘ 𝐽 ) } )
86 68 85 eleqtrd ⊢ ( ( ( ( 𝐽 ∈ PConn ∧ 𝑌 ∈ 𝑋 ) ∧ ( Base ‘ ( 𝐽 π1 𝑌 ) ) ≈ 1o ) ∧ ( 𝑓 ∈ ( II Cn 𝐽 ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) → [ 𝑓 ] ( ≃ph ‘ 𝐽 ) ∈ { [ ( ( 0 [,] 1 ) × { ( 𝑓 ‘ 0 ) } ) ] ( ≃ph ‘ 𝐽 ) } )
87 elsni ⊢ ( [ 𝑓 ] ( ≃ph ‘ 𝐽 ) ∈ { [ ( ( 0 [,] 1 ) × { ( 𝑓 ‘ 0 ) } ) ] ( ≃ph ‘ 𝐽 ) } → [ 𝑓 ] ( ≃ph ‘ 𝐽 ) = [ ( ( 0 [,] 1 ) × { ( 𝑓 ‘ 0 ) } ) ] ( ≃ph ‘ 𝐽 ) )
88 86 87 syl ⊢ ( ( ( ( 𝐽 ∈ PConn ∧ 𝑌 ∈ 𝑋 ) ∧ ( Base ‘ ( 𝐽 π1 𝑌 ) ) ≈ 1o ) ∧ ( 𝑓 ∈ ( II Cn 𝐽 ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) → [ 𝑓 ] ( ≃ph ‘ 𝐽 ) = [ ( ( 0 [,] 1 ) × { ( 𝑓 ‘ 0 ) } ) ] ( ≃ph ‘ 𝐽 ) )
89 13 a1i ⊢ ( ( ( ( 𝐽 ∈ PConn ∧ 𝑌 ∈ 𝑋 ) ∧ ( Base ‘ ( 𝐽 π1 𝑌 ) ) ≈ 1o ) ∧ ( 𝑓 ∈ ( II Cn 𝐽 ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) → ( ≃ph ‘ 𝐽 ) Er ( II Cn 𝐽 ) )
90 89 58 erth ⊢ ( ( ( ( 𝐽 ∈ PConn ∧ 𝑌 ∈ 𝑋 ) ∧ ( Base ‘ ( 𝐽 π1 𝑌 ) ) ≈ 1o ) ∧ ( 𝑓 ∈ ( II Cn 𝐽 ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) → ( 𝑓 ( ≃ph ‘ 𝐽 ) ( ( 0 [,] 1 ) × { ( 𝑓 ‘ 0 ) } ) ↔ [ 𝑓 ] ( ≃ph ‘ 𝐽 ) = [ ( ( 0 [,] 1 ) × { ( 𝑓 ‘ 0 ) } ) ] ( ≃ph ‘ 𝐽 ) ) )
91 88 90 mpbird ⊢ ( ( ( ( 𝐽 ∈ PConn ∧ 𝑌 ∈ 𝑋 ) ∧ ( Base ‘ ( 𝐽 π1 𝑌 ) ) ≈ 1o ) ∧ ( 𝑓 ∈ ( II Cn 𝐽 ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) → 𝑓 ( ≃ph ‘ 𝐽 ) ( ( 0 [,] 1 ) × { ( 𝑓 ‘ 0 ) } ) )
92 91 expr ⊢ ( ( ( ( 𝐽 ∈ PConn ∧ 𝑌 ∈ 𝑋 ) ∧ ( Base ‘ ( 𝐽 π1 𝑌 ) ) ≈ 1o ) ∧ 𝑓 ∈ ( II Cn 𝐽 ) ) → ( ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) → 𝑓 ( ≃ph ‘ 𝐽 ) ( ( 0 [,] 1 ) × { ( 𝑓 ‘ 0 ) } ) ) )
93 92 ralrimiva ⊢ ( ( ( 𝐽 ∈ PConn ∧ 𝑌 ∈ 𝑋 ) ∧ ( Base ‘ ( 𝐽 π1 𝑌 ) ) ≈ 1o ) → ∀ 𝑓 ∈ ( II Cn 𝐽 ) ( ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) → 𝑓 ( ≃ph ‘ 𝐽 ) ( ( 0 [,] 1 ) × { ( 𝑓 ‘ 0 ) } ) ) )
94 issconn ⊢ ( 𝐽 ∈ SConn ↔ ( 𝐽 ∈ PConn ∧ ∀ 𝑓 ∈ ( II Cn 𝐽 ) ( ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) → 𝑓 ( ≃ph ‘ 𝐽 ) ( ( 0 [,] 1 ) × { ( 𝑓 ‘ 0 ) } ) ) ) )
95 51 93 94 sylanbrc ⊢ ( ( ( 𝐽 ∈ PConn ∧ 𝑌 ∈ 𝑋 ) ∧ ( Base ‘ ( 𝐽 π1 𝑌 ) ) ≈ 1o ) → 𝐽 ∈ SConn )
96 50 95 impbida ⊢ ( ( 𝐽 ∈ PConn ∧ 𝑌 ∈ 𝑋 ) → ( 𝐽 ∈ SConn ↔ ( Base ‘ ( 𝐽 π1 𝑌 ) ) ≈ 1o ) )