ontric3g

Description: For all x , y e. On , one and only one of the following hold: x e. y , y = x , or y e. x . This is a transparent strict trichotomy. (Contributed by RP, 27-Sep-2023)

		Ref	Expression
	Assertion	ontric3g	$⊢ \forall x \in On \forall y \in On ((x \in y \leftrightarrow \neg (y = x \lor y \in x)) \land (y = x \leftrightarrow \neg (x \in y \lor y \in x)) \land (y \in x \leftrightarrow \neg (x \in y \lor y = x)))$

Proof

Step	Hyp	Ref	Expression
1		orcom	$⊢ (y = x \lor y \in x) \leftrightarrow (y \in x \lor y = x)$
2	1	a1i	$⊢ (y \in On \land x \in On) \to ((y = x \lor y \in x) \leftrightarrow (y \in x \lor y = x))$
3		onsseleq	$⊢ (y \in On \land x \in On) \to (y \subseteq x \leftrightarrow (y \in x \lor y = x))$
4		ontri1	$⊢ (y \in On \land x \in On) \to (y \subseteq x \leftrightarrow \neg x \in y)$
5	2 3 4	3bitr2d	$⊢ (y \in On \land x \in On) \to ((y = x \lor y \in x) \leftrightarrow \neg x \in y)$
6	5	con2bid	$⊢ (y \in On \land x \in On) \to (x \in y \leftrightarrow \neg (y = x \lor y \in x))$
7	6	ancoms	$⊢ (x \in On \land y \in On) \to (x \in y \leftrightarrow \neg (y = x \lor y \in x))$
8	4	ancoms	$⊢ (x \in On \land y \in On) \to (y \subseteq x \leftrightarrow \neg x \in y)$
9		ontri1	$⊢ (x \in On \land y \in On) \to (x \subseteq y \leftrightarrow \neg y \in x)$
10	8 9	anbi12d	$⊢ (x \in On \land y \in On) \to ((y \subseteq x \land x \subseteq y) \leftrightarrow (\neg x \in y \land \neg y \in x))$
11		eqss	$⊢ y = x \leftrightarrow (y \subseteq x \land x \subseteq y)$
12		ioran	$⊢ \neg (x \in y \lor y \in x) \leftrightarrow (\neg x \in y \land \neg y \in x)$
13	10 11 12	3bitr4g	$⊢ (x \in On \land y \in On) \to (y = x \leftrightarrow \neg (x \in y \lor y \in x))$
14		equcom	$⊢ y = x \leftrightarrow x = y$
15	14	orbi2i	$⊢ (x \in y \lor y = x) \leftrightarrow (x \in y \lor x = y)$
16	15	a1i	$⊢ (x \in On \land y \in On) \to ((x \in y \lor y = x) \leftrightarrow (x \in y \lor x = y))$
17		onsseleq	$⊢ (x \in On \land y \in On) \to (x \subseteq y \leftrightarrow (x \in y \lor x = y))$
18	16 17 9	3bitr2d	$⊢ (x \in On \land y \in On) \to ((x \in y \lor y = x) \leftrightarrow \neg y \in x)$
19	18	con2bid	$⊢ (x \in On \land y \in On) \to (y \in x \leftrightarrow \neg (x \in y \lor y = x))$
20	7 13 19	3jca	$⊢ (x \in On \land y \in On) \to ((x \in y \leftrightarrow \neg (y = x \lor y \in x)) \land (y = x \leftrightarrow \neg (x \in y \lor y \in x)) \land (y \in x \leftrightarrow \neg (x \in y \lor y = x)))$
21	20	rgen2	$⊢ \forall x \in On \forall y \in On ((x \in y \leftrightarrow \neg (y = x \lor y \in x)) \land (y = x \leftrightarrow \neg (x \in y \lor y \in x)) \land (y \in x \leftrightarrow \neg (x \in y \lor y = x)))$

Metamath Proof Explorer

Theorem ontric3g

Proof