porpss

Description: Every class is partially ordered by proper subsets. (Contributed by Stefan O'Rear, 2-Nov-2014)

		Ref	Expression
	Assertion	porpss	$⊢ [\subset] Po A$

Step	Hyp	Ref	Expression
1		pssirr	$⊢ \neg x \subset x$
2		psstr	$⊢ (x \subset y \land y \subset z) \to x \subset z$
3		vex	$⊢ x \in V$
4	3	brrpss	$⊢ x [\subset] x \leftrightarrow x \subset x$
5	4	notbii	$⊢ \neg x [\subset] x \leftrightarrow \neg x \subset x$
6		vex	$⊢ y \in V$
7	6	brrpss	$⊢ x [\subset] y \leftrightarrow x \subset y$
8		vex	$⊢ z \in V$
9	8	brrpss	$⊢ y [\subset] z \leftrightarrow y \subset z$
10	7 9	anbi12i	$⊢ (x [\subset] y \land y [\subset] z) \leftrightarrow (x \subset y \land y \subset z)$
11	8	brrpss	$⊢ x [\subset] z \leftrightarrow x \subset z$
12	10 11	imbi12i	$⊢ ((x [\subset] y \land y [\subset] z) \to x [\subset] z) \leftrightarrow ((x \subset y \land y \subset z) \to x \subset z)$
13	5 12	anbi12i	$⊢ (\neg x [\subset] x \land ((x [\subset] y \land y [\subset] z) \to x [\subset] z)) \leftrightarrow (\neg x \subset x \land ((x \subset y \land y \subset z) \to x \subset z))$
14	1 2 13	mpbir2an	$⊢ (\neg x [\subset] x \land ((x [\subset] y \land y [\subset] z) \to x [\subset] z))$
15	14	rgenw	$⊢ \forall z \in A (\neg x [\subset] x \land ((x [\subset] y \land y [\subset] z) \to x [\subset] z))$
16	15	rgen2w	$⊢ \forall x \in A \forall y \in A \forall z \in A (\neg x [\subset] x \land ((x [\subset] y \land y [\subset] z) \to x [\subset] z))$
17		df-po	$⊢ [\subset] Po A \leftrightarrow \forall x \in A \forall y \in A \forall z \in A (\neg x [\subset] x \land ((x [\subset] y \land y [\subset] z) \to x [\subset] z))$
18	16 17	mpbir	$⊢ [\subset] Po A$

Metamath Proof Explorer