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 
|- A. x e. On A. y e. On ( ( x e. y <-> -. ( y = x \/ y e. x ) ) /\ ( y = x <-> -. ( x e. y \/ y e. x ) ) /\ ( y e. x <-> -. ( x e. y \/ y = x ) ) )

Proof

Step Hyp Ref Expression
1 orcom 
 |-  ( ( y = x \/ y e. x ) <-> ( y e. x \/ y = x ) )
2 1 a1i 
 |-  ( ( y e. On /\ x e. On ) -> ( ( y = x \/ y e. x ) <-> ( y e. x \/ y = x ) ) )
3 onsseleq 
 |-  ( ( y e. On /\ x e. On ) -> ( y C_ x <-> ( y e. x \/ y = x ) ) )
4 ontri1 
 |-  ( ( y e. On /\ x e. On ) -> ( y C_ x <-> -. x e. y ) )
5 2 3 4 3bitr2d 
 |-  ( ( y e. On /\ x e. On ) -> ( ( y = x \/ y e. x ) <-> -. x e. y ) )
6 5 con2bid 
 |-  ( ( y e. On /\ x e. On ) -> ( x e. y <-> -. ( y = x \/ y e. x ) ) )
7 6 ancoms 
 |-  ( ( x e. On /\ y e. On ) -> ( x e. y <-> -. ( y = x \/ y e. x ) ) )
8 4 ancoms 
 |-  ( ( x e. On /\ y e. On ) -> ( y C_ x <-> -. x e. y ) )
9 ontri1 
 |-  ( ( x e. On /\ y e. On ) -> ( x C_ y <-> -. y e. x ) )
10 8 9 anbi12d 
 |-  ( ( x e. On /\ y e. On ) -> ( ( y C_ x /\ x C_ y ) <-> ( -. x e. y /\ -. y e. x ) ) )
11 eqss 
 |-  ( y = x <-> ( y C_ x /\ x C_ y ) )
12 ioran 
 |-  ( -. ( x e. y \/ y e. x ) <-> ( -. x e. y /\ -. y e. x ) )
13 10 11 12 3bitr4g 
 |-  ( ( x e. On /\ y e. On ) -> ( y = x <-> -. ( x e. y \/ y e. x ) ) )
14 equcom 
 |-  ( y = x <-> x = y )
15 14 orbi2i 
 |-  ( ( x e. y \/ y = x ) <-> ( x e. y \/ x = y ) )
16 15 a1i 
 |-  ( ( x e. On /\ y e. On ) -> ( ( x e. y \/ y = x ) <-> ( x e. y \/ x = y ) ) )
17 onsseleq 
 |-  ( ( x e. On /\ y e. On ) -> ( x C_ y <-> ( x e. y \/ x = y ) ) )
18 16 17 9 3bitr2d 
 |-  ( ( x e. On /\ y e. On ) -> ( ( x e. y \/ y = x ) <-> -. y e. x ) )
19 18 con2bid 
 |-  ( ( x e. On /\ y e. On ) -> ( y e. x <-> -. ( x e. y \/ y = x ) ) )
20 7 13 19 3jca 
 |-  ( ( x e. On /\ y e. On ) -> ( ( x e. y <-> -. ( y = x \/ y e. x ) ) /\ ( y = x <-> -. ( x e. y \/ y e. x ) ) /\ ( y e. x <-> -. ( x e. y \/ y = x ) ) ) )
21 20 rgen2 
 |-  A. x e. On A. y e. On ( ( x e. y <-> -. ( y = x \/ y e. x ) ) /\ ( y = x <-> -. ( x e. y \/ y e. x ) ) /\ ( y e. x <-> -. ( x e. y \/ y = x ) ) )