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 x On y On x y ¬ y = x y x y = x ¬ x y y x y x ¬ x y y = x

Proof

Step Hyp Ref Expression
1 orcom y = x y x y x y = x
2 1 a1i y On x On y = x y x y x y = x
3 onsseleq y On x On y x y x y = x
4 ontri1 y On x On y x ¬ x y
5 2 3 4 3bitr2d y On x On y = x y x ¬ x y
6 5 con2bid y On x On x y ¬ y = x y x
7 6 ancoms x On y On x y ¬ y = x y x
8 4 ancoms x On y On y x ¬ x y
9 ontri1 x On y On x y ¬ y x
10 8 9 anbi12d x On y On y x x y ¬ x y ¬ y x
11 eqss y = x y x x y
12 ioran ¬ x y y x ¬ x y ¬ y x
13 10 11 12 3bitr4g x On y On y = x ¬ x y y x
14 equcom y = x x = y
15 14 orbi2i x y y = x x y x = y
16 15 a1i x On y On x y y = x x y x = y
17 onsseleq x On y On x y x y x = y
18 16 17 9 3bitr2d x On y On x y y = x ¬ y x
19 18 con2bid x On y On y x ¬ x y y = x
20 7 13 19 3jca x On y On x y ¬ y = x y x y = x ¬ x y y x y x ¬ x y y = x
21 20 rgen2 x On y On x y ¬ y = x y x y = x ¬ x y y x y x ¬ x y y = x