Theorem issconn

Description: The property of being a simply connected topological space. (Contributed by Mario Carneiro, 11-Feb-2015)

	Ref	Expression
Assertion	issconn	⊢ ( 𝐽 ∈ SConn ↔ ( 𝐽 ∈ PConn ∧ ∀ 𝑓 ∈ ( II Cn 𝐽 ) ( ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) → 𝑓 ( ≃ph ‘ 𝐽 ) ( ( 0 [,] 1 ) × { ( 𝑓 ‘ 0 ) } ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		oveq2	⊢ ( 𝑗 = 𝐽 → ( II Cn 𝑗 ) = ( II Cn 𝐽 ) )
2		fveq2	⊢ ( 𝑗 = 𝐽 → ( ≃ph ‘ 𝑗 ) = ( ≃ph ‘ 𝐽 ) )
3	2	breqd	⊢ ( 𝑗 = 𝐽 → ( 𝑓 ( ≃ph ‘ 𝑗 ) ( ( 0 [,] 1 ) × { ( 𝑓 ‘ 0 ) } ) ↔ 𝑓 ( ≃ph ‘ 𝐽 ) ( ( 0 [,] 1 ) × { ( 𝑓 ‘ 0 ) } ) ) )
4	3	imbi2d	⊢ ( 𝑗 = 𝐽 → ( ( ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) → 𝑓 ( ≃ph ‘ 𝑗 ) ( ( 0 [,] 1 ) × { ( 𝑓 ‘ 0 ) } ) ) ↔ ( ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) → 𝑓 ( ≃ph ‘ 𝐽 ) ( ( 0 [,] 1 ) × { ( 𝑓 ‘ 0 ) } ) ) ) )
5	1 4	raleqbidv	⊢ ( 𝑗 = 𝐽 → ( ∀ 𝑓 ∈ ( II Cn 𝑗 ) ( ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) → 𝑓 ( ≃ph ‘ 𝑗 ) ( ( 0 [,] 1 ) × { ( 𝑓 ‘ 0 ) } ) ) ↔ ∀ 𝑓 ∈ ( II Cn 𝐽 ) ( ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) → 𝑓 ( ≃ph ‘ 𝐽 ) ( ( 0 [,] 1 ) × { ( 𝑓 ‘ 0 ) } ) ) ) )
6		df-sconn	⊢ SConn = { 𝑗 ∈ PConn ∣ ∀ 𝑓 ∈ ( II Cn 𝑗 ) ( ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) → 𝑓 ( ≃ph ‘ 𝑗 ) ( ( 0 [,] 1 ) × { ( 𝑓 ‘ 0 ) } ) ) }
7	5 6	elrab2	⊢ ( 𝐽 ∈ SConn ↔ ( 𝐽 ∈ PConn ∧ ∀ 𝑓 ∈ ( II Cn 𝐽 ) ( ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) → 𝑓 ( ≃ph ‘ 𝐽 ) ( ( 0 [,] 1 ) × { ( 𝑓 ‘ 0 ) } ) ) ) )