sorpss

Description: Express strict ordering under proper subsets, i.e. the notion of a chain of sets. (Contributed by Stefan O'Rear, 2-Nov-2014)

		Ref	Expression
	Assertion	sorpss	$⊢ [\subset] Or A \leftrightarrow \forall x \in A \forall y \in A (x \subseteq y \lor y \subseteq x)$

Step	Hyp	Ref	Expression
1		porpss	$⊢ [\subset] Po A$
2	1	biantrur	$⊢ \forall x \in A \forall y \in A (x [\subset] y \lor x = y \lor y [\subset] x) \leftrightarrow ([\subset] Po A \land \forall x \in A \forall y \in A (x [\subset] y \lor x = y \lor y [\subset] x))$
3		sspsstri	$⊢ (x \subseteq y \lor y \subseteq x) \leftrightarrow (x \subset y \lor x = y \lor y \subset x)$
4		vex	$⊢ y \in V$
5	4	brrpss	$⊢ x [\subset] y \leftrightarrow x \subset y$
6		biid	$⊢ x = y \leftrightarrow x = y$
7		vex	$⊢ x \in V$
8	7	brrpss	$⊢ y [\subset] x \leftrightarrow y \subset x$
9	5 6 8	3orbi123i	$⊢ (x [\subset] y \lor x = y \lor y [\subset] x) \leftrightarrow (x \subset y \lor x = y \lor y \subset x)$
10	3 9	bitr4i	$⊢ (x \subseteq y \lor y \subseteq x) \leftrightarrow (x [\subset] y \lor x = y \lor y [\subset] x)$
11	10	2ralbii	$⊢ \forall x \in A \forall y \in A (x \subseteq y \lor y \subseteq x) \leftrightarrow \forall x \in A \forall y \in A (x [\subset] y \lor x = y \lor y [\subset] x)$
12		df-so	$⊢ [\subset] Or A \leftrightarrow ([\subset] Po A \land \forall x \in A \forall y \in A (x [\subset] y \lor x = y \lor y [\subset] x))$
13	2 11 12	3bitr4ri	$⊢ [\subset] Or A \leftrightarrow \forall x \in A \forall y \in A (x \subseteq y \lor y \subseteq x)$

Metamath Proof Explorer