pconncn

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

		Ref	Expression
	Hypothesis	ispconn.1	$⊢ X = ⋃ J$
	Assertion	pconncn	$⊢ (J \in PConn \land A \in X \land B \in X) \to \exists f \in (II Cn J) (f (0) = A \land f (1) = B)$

Step	Hyp	Ref	Expression
1		ispconn.1	$⊢ X = ⋃ J$
2	1	ispconn	$⊢ J \in PConn \leftrightarrow (J \in Top \land \forall x \in X \forall y \in X \exists f \in (II Cn J) (f (0) = x \land f (1) = y))$
3	2	simprbi	$⊢ J \in PConn \to \forall x \in X \forall y \in X \exists f \in (II Cn J) (f (0) = x \land f (1) = y)$
4		eqeq2	$⊢ x = A \to (f (0) = x \leftrightarrow f (0) = A)$
5	4	anbi1d	$⊢ x = A \to ((f (0) = x \land f (1) = y) \leftrightarrow (f (0) = A \land f (1) = y))$
6	5	rexbidv	$⊢ x = A \to (\exists f \in (II Cn J) (f (0) = x \land f (1) = y) \leftrightarrow \exists f \in (II Cn J) (f (0) = A \land f (1) = y))$
7		eqeq2	$⊢ y = B \to (f (1) = y \leftrightarrow f (1) = B)$
8	7	anbi2d	$⊢ y = B \to ((f (0) = A \land f (1) = y) \leftrightarrow (f (0) = A \land f (1) = B))$
9	8	rexbidv	$⊢ y = B \to (\exists f \in (II Cn J) (f (0) = A \land f (1) = y) \leftrightarrow \exists f \in (II Cn J) (f (0) = A \land f (1) = B))$
10	6 9	rspc2v	$⊢ (A \in X \land B \in X) \to (\forall x \in X \forall y \in X \exists f \in (II Cn J) (f (0) = x \land f (1) = y) \to \exists f \in (II Cn J) (f (0) = A \land f (1) = B))$
11	3 10	syl5com	$⊢ J \in PConn \to ((A \in X \land B \in X) \to \exists f \in (II Cn J) (f (0) = A \land f (1) = B))$
12	11	3impib	$⊢ (J \in PConn \land A \in X \land B \in X) \to \exists f \in (II Cn J) (f (0) = A \land f (1) = B)$

Metamath Proof Explorer