Metamath Proof Explorer

Theorem dfso3

Description: Expansion of the definition of a strict order. (Contributed by Scott Fenton, 6-Jun-2016)

		Ref	Expression
	Assertion	dfso3	$⊢ R Or A \leftrightarrow \forall x \in A \forall y \in A \forall z \in A (\neg x R x \land ((x R y \land y R z) \to x R z) \land (x R y \lor x = y \lor y R x))$

Proof

Step	Hyp	Ref	Expression
1		ne0i	$⊢ y \in A \to A \neq \emptyset$
2		r19.27zv	$⊢ A \neq \emptyset \to (\forall z \in A ((\neg x R x \land ((x R y \land y R z) \to x R z)) \land (x R y \lor x = y \lor y R x)) \leftrightarrow (\forall z \in A (\neg x R x \land ((x R y \land y R z) \to x R z)) \land (x R y \lor x = y \lor y R x)))$
3	1 2	syl	$⊢ y \in A \to (\forall z \in A ((\neg x R x \land ((x R y \land y R z) \to x R z)) \land (x R y \lor x = y \lor y R x)) \leftrightarrow (\forall z \in A (\neg x R x \land ((x R y \land y R z) \to x R z)) \land (x R y \lor x = y \lor y R x)))$
4	3	ralbiia	$⊢ \forall y \in A \forall z \in A ((\neg x R x \land ((x R y \land y R z) \to x R z)) \land (x R y \lor x = y \lor y R x)) \leftrightarrow \forall y \in A (\forall z \in A (\neg x R x \land ((x R y \land y R z) \to x R z)) \land (x R y \lor x = y \lor y R x))$
5	4	ralbii	$⊢ \forall x \in A \forall y \in A \forall z \in A ((\neg x R x \land ((x R y \land y R z) \to x R z)) \land (x R y \lor x = y \lor y R x)) \leftrightarrow \forall x \in A \forall y \in A (\forall z \in A (\neg x R x \land ((x R y \land y R z) \to x R z)) \land (x R y \lor x = y \lor y R x))$
6		df-3an	$⊢ (\neg x R x \land ((x R y \land y R z) \to x R z) \land (x R y \lor x = y \lor y R x)) \leftrightarrow ((\neg x R x \land ((x R y \land y R z) \to x R z)) \land (x R y \lor x = y \lor y R x))$
7	6	ralbii	$⊢ \forall z \in A (\neg x R x \land ((x R y \land y R z) \to x R z) \land (x R y \lor x = y \lor y R x)) \leftrightarrow \forall z \in A ((\neg x R x \land ((x R y \land y R z) \to x R z)) \land (x R y \lor x = y \lor y R x))$
8	7	2ralbii	$⊢ \forall x \in A \forall y \in A \forall z \in A (\neg x R x \land ((x R y \land y R z) \to x R z) \land (x R y \lor x = y \lor y R x)) \leftrightarrow \forall x \in A \forall y \in A \forall z \in A ((\neg x R x \land ((x R y \land y R z) \to x R z)) \land (x R y \lor x = y \lor y R x))$
9		df-po	$⊢ R Po A \leftrightarrow \forall x \in A \forall y \in A \forall z \in A (\neg x R x \land ((x R y \land y R z) \to x R z))$
10	9	anbi1i	$⊢ (R Po A \land \forall x \in A \forall y \in A (x R y \lor x = y \lor y R x)) \leftrightarrow (\forall x \in A \forall y \in A \forall z \in A (\neg x R x \land ((x R y \land y R z) \to x R z)) \land \forall x \in A \forall y \in A (x R y \lor x = y \lor y R x))$
11		df-so	$⊢ R Or A \leftrightarrow (R Po A \land \forall x \in A \forall y \in A (x R y \lor x = y \lor y R x))$
12		r19.26-2	$⊢ \forall x \in A \forall y \in A (\forall z \in A (\neg x R x \land ((x R y \land y R z) \to x R z)) \land (x R y \lor x = y \lor y R x)) \leftrightarrow (\forall x \in A \forall y \in A \forall z \in A (\neg x R x \land ((x R y \land y R z) \to x R z)) \land \forall x \in A \forall y \in A (x R y \lor x = y \lor y R x))$
13	10 11 12	3bitr4i	$⊢ R Or A \leftrightarrow \forall x \in A \forall y \in A (\forall z \in A (\neg x R x \land ((x R y \land y R z) \to x R z)) \land (x R y \lor x = y \lor y R x))$
14	5 8 13	3bitr4ri	$⊢ R Or A \leftrightarrow \forall x \in A \forall y \in A \forall z \in A (\neg x R x \land ((x R y \land y R z) \to x R z) \land (x R y \lor x = y \lor y R x))$