Metamath Proof Explorer


Theorem 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 xOnyOnxy¬y=xyxy=x¬xyyxyx¬xyy=x

Proof

Step Hyp Ref Expression
1 orcom y=xyxyxy=x
2 1 a1i yOnxOny=xyxyxy=x
3 onsseleq yOnxOnyxyxy=x
4 ontri1 yOnxOnyx¬xy
5 2 3 4 3bitr2d yOnxOny=xyx¬xy
6 5 con2bid yOnxOnxy¬y=xyx
7 6 ancoms xOnyOnxy¬y=xyx
8 4 ancoms xOnyOnyx¬xy
9 ontri1 xOnyOnxy¬yx
10 8 9 anbi12d xOnyOnyxxy¬xy¬yx
11 eqss y=xyxxy
12 ioran ¬xyyx¬xy¬yx
13 10 11 12 3bitr4g xOnyOny=x¬xyyx
14 equcom y=xx=y
15 14 orbi2i xyy=xxyx=y
16 15 a1i xOnyOnxyy=xxyx=y
17 onsseleq xOnyOnxyxyx=y
18 16 17 9 3bitr2d xOnyOnxyy=x¬yx
19 18 con2bid xOnyOnyx¬xyy=x
20 7 13 19 3jca xOnyOnxy¬y=xyxy=x¬xyyxyx¬xyy=x
21 20 rgen2 xOnyOnxy¬y=xyxy=x¬xyyxyx¬xyy=x