Theorem pconncn

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

	Ref	Expression
Hypothesis	ispconn.1	⊢ 𝑋 = ∪ 𝐽
Assertion	pconncn	⊢ ( ( 𝐽 ∈ PConn ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ∃ 𝑓 ∈ ( II Cn 𝐽 ) ( ( 𝑓 ‘ 0 ) = 𝐴 ∧ ( 𝑓 ‘ 1 ) = 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		ispconn.1	⊢ 𝑋 = ∪ 𝐽
2	1	ispconn	⊢ ( 𝐽 ∈ PConn ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ∃ 𝑓 ∈ ( II Cn 𝐽 ) ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) ) )
3	2	simprbi	⊢ ( 𝐽 ∈ PConn → ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ∃ 𝑓 ∈ ( II Cn 𝐽 ) ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) )
4		eqeq2	⊢ ( 𝑥 = 𝐴 → ( ( 𝑓 ‘ 0 ) = 𝑥 ↔ ( 𝑓 ‘ 0 ) = 𝐴 ) )
5	4	anbi1d	⊢ ( 𝑥 = 𝐴 → ( ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) ↔ ( ( 𝑓 ‘ 0 ) = 𝐴 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) ) )
6	5	rexbidv	⊢ ( 𝑥 = 𝐴 → ( ∃ 𝑓 ∈ ( II Cn 𝐽 ) ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) ↔ ∃ 𝑓 ∈ ( II Cn 𝐽 ) ( ( 𝑓 ‘ 0 ) = 𝐴 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) ) )
7		eqeq2	⊢ ( 𝑦 = 𝐵 → ( ( 𝑓 ‘ 1 ) = 𝑦 ↔ ( 𝑓 ‘ 1 ) = 𝐵 ) )
8	7	anbi2d	⊢ ( 𝑦 = 𝐵 → ( ( ( 𝑓 ‘ 0 ) = 𝐴 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) ↔ ( ( 𝑓 ‘ 0 ) = 𝐴 ∧ ( 𝑓 ‘ 1 ) = 𝐵 ) ) )
9	8	rexbidv	⊢ ( 𝑦 = 𝐵 → ( ∃ 𝑓 ∈ ( II Cn 𝐽 ) ( ( 𝑓 ‘ 0 ) = 𝐴 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) ↔ ∃ 𝑓 ∈ ( II Cn 𝐽 ) ( ( 𝑓 ‘ 0 ) = 𝐴 ∧ ( 𝑓 ‘ 1 ) = 𝐵 ) ) )
10	6 9	rspc2v	⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ∃ 𝑓 ∈ ( II Cn 𝐽 ) ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) → ∃ 𝑓 ∈ ( II Cn 𝐽 ) ( ( 𝑓 ‘ 0 ) = 𝐴 ∧ ( 𝑓 ‘ 1 ) = 𝐵 ) ) )
11	3 10	syl5com	⊢ ( 𝐽 ∈ PConn → ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ∃ 𝑓 ∈ ( II Cn 𝐽 ) ( ( 𝑓 ‘ 0 ) = 𝐴 ∧ ( 𝑓 ‘ 1 ) = 𝐵 ) ) )
12	11	3impib	⊢ ( ( 𝐽 ∈ PConn ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ∃ 𝑓 ∈ ( II Cn 𝐽 ) ( ( 𝑓 ‘ 0 ) = 𝐴 ∧ ( 𝑓 ‘ 1 ) = 𝐵 ) )