ispconn

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	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))$

Step	Hyp	Ref	Expression
1		ispconn.1	$⊢ X = ⋃ J$
2		unieq	$⊢ j = J \to ⋃ j = ⋃ J$
3	2 1	eqtr4di	$⊢ j = J \to ⋃ j = X$
4		oveq2	$⊢ j = J \to II Cn j = II Cn J$
5	4	rexeqdv	$⊢ j = J \to (\exists f \in (II Cn j) (f (0) = x \land f (1) = y) \leftrightarrow \exists f \in (II Cn J) (f (0) = x \land f (1) = y))$
6	3 5	raleqbidv	$⊢ j = J \to (\forall y \in ⋃ j \exists f \in (II Cn j) (f (0) = x \land f (1) = y) \leftrightarrow \forall y \in X \exists f \in (II Cn J) (f (0) = x \land f (1) = y))$
7	3 6	raleqbidv	$⊢ j = J \to (\forall x \in ⋃ j \forall y \in ⋃ j \exists f \in (II Cn j) (f (0) = x \land f (1) = y) \leftrightarrow \forall x \in X \forall y \in X \exists f \in (II Cn J) (f (0) = x \land f (1) = y))$
8		df-pconn	$⊢ PConn = \{j \in Top \| \forall x \in ⋃ j \forall y \in ⋃ j \exists f \in (II Cn j) (f (0) = x \land f (1) = y)\}$
9	7 8	elrab2	$⊢ 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))$

Metamath Proof Explorer