Metamath Proof Explorer


Theorem ispconn

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

Ref Expression
Hypothesis ispconn.1 𝑋 = 𝐽
Assertion ispconn ( 𝐽 ∈ PConn ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑥𝑋𝑦𝑋𝑓 ∈ ( II Cn 𝐽 ) ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) ) )

Proof

Step Hyp Ref Expression
1 ispconn.1 𝑋 = 𝐽
2 unieq ( 𝑗 = 𝐽 𝑗 = 𝐽 )
3 2 1 eqtr4di ( 𝑗 = 𝐽 𝑗 = 𝑋 )
4 oveq2 ( 𝑗 = 𝐽 → ( II Cn 𝑗 ) = ( II Cn 𝐽 ) )
5 4 rexeqdv ( 𝑗 = 𝐽 → ( ∃ 𝑓 ∈ ( II Cn 𝑗 ) ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) ↔ ∃ 𝑓 ∈ ( II Cn 𝐽 ) ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) ) )
6 3 5 raleqbidv ( 𝑗 = 𝐽 → ( ∀ 𝑦 𝑗𝑓 ∈ ( II Cn 𝑗 ) ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) ↔ ∀ 𝑦𝑋𝑓 ∈ ( II Cn 𝐽 ) ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) ) )
7 3 6 raleqbidv ( 𝑗 = 𝐽 → ( ∀ 𝑥 𝑗𝑦 𝑗𝑓 ∈ ( II Cn 𝑗 ) ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) ↔ ∀ 𝑥𝑋𝑦𝑋𝑓 ∈ ( II Cn 𝐽 ) ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) ) )
8 df-pconn PConn = { 𝑗 ∈ Top ∣ ∀ 𝑥 𝑗𝑦 𝑗𝑓 ∈ ( II Cn 𝑗 ) ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) }
9 7 8 elrab2 ( 𝐽 ∈ PConn ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑥𝑋𝑦𝑋𝑓 ∈ ( II Cn 𝐽 ) ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) ) )