Metamath Proof Explorer

Theorem disjun0

Description: Adding the empty element preserves disjointness. (Contributed by Thierry Arnoux, 30-May-2020)

		Ref	Expression
	Assertion	disjun0	$⊢ \underset{x \in A}{Disj} x \to \underset{x \in A \cup \{\emptyset\}}{Disj} x$

Proof

Step	Hyp	Ref	Expression
1		snssi	$⊢ \emptyset \in A \to \{\emptyset\} \subseteq A$
2		ssequn2	$⊢ \{\emptyset\} \subseteq A \leftrightarrow A \cup \{\emptyset\} = A$
3	1 2	sylib	$⊢ \emptyset \in A \to A \cup \{\emptyset\} = A$
4	3	disjeq1d	$⊢ \emptyset \in A \to (\underset{x \in A \cup \{\emptyset\}}{Disj} x \leftrightarrow \underset{x \in A}{Disj} x)$
5	4	biimparc	$⊢ (\underset{x \in A}{Disj} x \land \emptyset \in A) \to \underset{x \in A \cup \{\emptyset\}}{Disj} x$
6		simpl	$⊢ (\underset{x \in A}{Disj} x \land \neg \emptyset \in A) \to \underset{x \in A}{Disj} x$
7		in0	$⊢ ⋃_{x \in A} x \cap \emptyset = \emptyset$
8	7	a1i	$⊢ (\underset{x \in A}{Disj} x \land \neg \emptyset \in A) \to ⋃_{x \in A} x \cap \emptyset = \emptyset$
9		0ex	$⊢ \emptyset \in V$
10		id	$⊢ x = \emptyset \to x = \emptyset$
11	10	disjunsn	$⊢ (\emptyset \in V \land \neg \emptyset \in A) \to (\underset{x \in A \cup \{\emptyset\}}{Disj} x \leftrightarrow (\underset{x \in A}{Disj} x \land ⋃_{x \in A} x \cap \emptyset = \emptyset))$
12	9 11	mpan	$⊢ \neg \emptyset \in A \to (\underset{x \in A \cup \{\emptyset\}}{Disj} x \leftrightarrow (\underset{x \in A}{Disj} x \land ⋃_{x \in A} x \cap \emptyset = \emptyset))$
13	12	adantl	$⊢ (\underset{x \in A}{Disj} x \land \neg \emptyset \in A) \to (\underset{x \in A \cup \{\emptyset\}}{Disj} x \leftrightarrow (\underset{x \in A}{Disj} x \land ⋃_{x \in A} x \cap \emptyset = \emptyset))$
14	6 8 13	mpbir2and	$⊢ (\underset{x \in A}{Disj} x \land \neg \emptyset \in A) \to \underset{x \in A \cup \{\emptyset\}}{Disj} x$
15	5 14	pm2.61dan	$⊢ \underset{x \in A}{Disj} x \to \underset{x \in A \cup \{\emptyset\}}{Disj} x$