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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | orcom | |
|
2 | 1 | a1i | |
3 | onsseleq | |
|
4 | ontri1 | |
|
5 | 2 3 4 | 3bitr2d | |
6 | 5 | con2bid | |
7 | 6 | ancoms | |
8 | 4 | ancoms | |
9 | ontri1 | |
|
10 | 8 9 | anbi12d | |
11 | eqss | |
|
12 | ioran | |
|
13 | 10 11 12 | 3bitr4g | |
14 | equcom | |
|
15 | 14 | orbi2i | |
16 | 15 | a1i | |
17 | onsseleq | |
|
18 | 16 17 9 | 3bitr2d | |
19 | 18 | con2bid | |
20 | 7 13 19 | 3jca | |
21 | 20 | rgen2 | |