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 
|- X = U. J
Assertion sconnpi1 
|- ( ( J e. PConn /\ Y e. X ) -> ( J e. SConn <-> ( Base ` ( J pi1 Y ) ) ~~ 1o ) )

Proof

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