Metamath Proof Explorer

Theorem connsub

Description: Two equivalent ways of saying that a subspace topology is connected. (Contributed by Jeff Hankins, 9-Jul-2009) (Proof shortened by Mario Carneiro, 10-Mar-2015)

		Ref	Expression
	Assertion	connsub	$⊢ (J \in TopOn (X) \land S \subseteq X) \to (J ↾_{𝑡} S \in Conn \leftrightarrow \forall x \in J \forall y \in J ((x \cap S \neq \emptyset \land y \cap S \neq \emptyset \land x \cap y \subseteq X ∖ S) \to \neg S \subseteq x \cup y))$

Proof

Step	Hyp	Ref	Expression
1		connsuba	$⊢ (J \in TopOn (X) \land S \subseteq X) \to (J ↾_{𝑡} S \in Conn \leftrightarrow \forall x \in J \forall y \in J ((x \cap S \neq \emptyset \land y \cap S \neq \emptyset \land (x \cap y) \cap S = \emptyset) \to (x \cup y) \cap S \neq S))$
2		inss1	$⊢ x \cap y \subseteq x$
3		toponss	$⊢ (J \in TopOn (X) \land x \in J) \to x \subseteq X$
4	3	ad2ant2r	$⊢ ((J \in TopOn (X) \land S \subseteq X) \land (x \in J \land y \in J)) \to x \subseteq X$
5	2 4	sstrid	$⊢ ((J \in TopOn (X) \land S \subseteq X) \land (x \in J \land y \in J)) \to x \cap y \subseteq X$
6		reldisj	$⊢ x \cap y \subseteq X \to ((x \cap y) \cap S = \emptyset \leftrightarrow x \cap y \subseteq X ∖ S)$
7	5 6	syl	$⊢ ((J \in TopOn (X) \land S \subseteq X) \land (x \in J \land y \in J)) \to ((x \cap y) \cap S = \emptyset \leftrightarrow x \cap y \subseteq X ∖ S)$
8	7	3anbi3d	$⊢ ((J \in TopOn (X) \land S \subseteq X) \land (x \in J \land y \in J)) \to ((x \cap S \neq \emptyset \land y \cap S \neq \emptyset \land (x \cap y) \cap S = \emptyset) \leftrightarrow (x \cap S \neq \emptyset \land y \cap S \neq \emptyset \land x \cap y \subseteq X ∖ S))$
9		sseqin2	$⊢ S \subseteq x \cup y \leftrightarrow (x \cup y) \cap S = S$
10	9	a1i	$⊢ ((J \in TopOn (X) \land S \subseteq X) \land (x \in J \land y \in J)) \to (S \subseteq x \cup y \leftrightarrow (x \cup y) \cap S = S)$
11	10	bicomd	$⊢ ((J \in TopOn (X) \land S \subseteq X) \land (x \in J \land y \in J)) \to ((x \cup y) \cap S = S \leftrightarrow S \subseteq x \cup y)$
12	11	necon3abid	$⊢ ((J \in TopOn (X) \land S \subseteq X) \land (x \in J \land y \in J)) \to ((x \cup y) \cap S \neq S \leftrightarrow \neg S \subseteq x \cup y)$
13	8 12	imbi12d	$⊢ ((J \in TopOn (X) \land S \subseteq X) \land (x \in J \land y \in J)) \to (((x \cap S \neq \emptyset \land y \cap S \neq \emptyset \land (x \cap y) \cap S = \emptyset) \to (x \cup y) \cap S \neq S) \leftrightarrow ((x \cap S \neq \emptyset \land y \cap S \neq \emptyset \land x \cap y \subseteq X ∖ S) \to \neg S \subseteq x \cup y))$
14	13	2ralbidva	$⊢ (J \in TopOn (X) \land S \subseteq X) \to (\forall x \in J \forall y \in J ((x \cap S \neq \emptyset \land y \cap S \neq \emptyset \land (x \cap y) \cap S = \emptyset) \to (x \cup y) \cap S \neq S) \leftrightarrow \forall x \in J \forall y \in J ((x \cap S \neq \emptyset \land y \cap S \neq \emptyset \land x \cap y \subseteq X ∖ S) \to \neg S \subseteq x \cup y))$
15	1 14	bitrd	$⊢ (J \in TopOn (X) \land S \subseteq X) \to (J ↾_{𝑡} S \in Conn \leftrightarrow \forall x \in J \forall y \in J ((x \cap S \neq \emptyset \land y \cap S \neq \emptyset \land x \cap y \subseteq X ∖ S) \to \neg S \subseteq x \cup y))$