disjpss

Description: A class is a proper subset of its union with a disjoint nonempty class. (Contributed by NM, 15-Sep-2004)

		Ref	Expression
	Assertion	disjpss	$⊢ (A \cap B = \emptyset \land B \neq \emptyset) \to A \subset A \cup B$

Step	Hyp	Ref	Expression
1		ssid	$⊢ B \subseteq B$
2	1	biantru	$⊢ B \subseteq A \leftrightarrow (B \subseteq A \land B \subseteq B)$
3		ssin	$⊢ (B \subseteq A \land B \subseteq B) \leftrightarrow B \subseteq A \cap B$
4	2 3	bitri	$⊢ B \subseteq A \leftrightarrow B \subseteq A \cap B$
5		sseq2	$⊢ A \cap B = \emptyset \to (B \subseteq A \cap B \leftrightarrow B \subseteq \emptyset)$
6	4 5	bitrid	$⊢ A \cap B = \emptyset \to (B \subseteq A \leftrightarrow B \subseteq \emptyset)$
7		ss0	$⊢ B \subseteq \emptyset \to B = \emptyset$
8	6 7	biimtrdi	$⊢ A \cap B = \emptyset \to (B \subseteq A \to B = \emptyset)$
9	8	necon3ad	$⊢ A \cap B = \emptyset \to (B \neq \emptyset \to \neg B \subseteq A)$
10	9	imp	$⊢ (A \cap B = \emptyset \land B \neq \emptyset) \to \neg B \subseteq A$
11		nsspssun	$⊢ \neg B \subseteq A \leftrightarrow A \subset B \cup A$
12		uncom	$⊢ B \cup A = A \cup B$
13	12	psseq2i	$⊢ A \subset B \cup A \leftrightarrow A \subset A \cup B$
14	11 13	bitri	$⊢ \neg B \subseteq A \leftrightarrow A \subset A \cup B$
15	10 14	sylib	$⊢ (A \cap B = \emptyset \land B \neq \emptyset) \to A \subset A \cup B$

Metamath Proof Explorer