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 𝑥 ∈ On ∀ 𝑦 ∈ On ( ( 𝑥𝑦 ↔ ¬ ( 𝑦 = 𝑥𝑦𝑥 ) ) ∧ ( 𝑦 = 𝑥 ↔ ¬ ( 𝑥𝑦𝑦𝑥 ) ) ∧ ( 𝑦𝑥 ↔ ¬ ( 𝑥𝑦𝑦 = 𝑥 ) ) )

Proof

Step Hyp Ref Expression
1 orcom ( ( 𝑦 = 𝑥𝑦𝑥 ) ↔ ( 𝑦𝑥𝑦 = 𝑥 ) )
2 1 a1i ( ( 𝑦 ∈ On ∧ 𝑥 ∈ On ) → ( ( 𝑦 = 𝑥𝑦𝑥 ) ↔ ( 𝑦𝑥𝑦 = 𝑥 ) ) )
3 onsseleq ( ( 𝑦 ∈ On ∧ 𝑥 ∈ On ) → ( 𝑦𝑥 ↔ ( 𝑦𝑥𝑦 = 𝑥 ) ) )
4 ontri1 ( ( 𝑦 ∈ On ∧ 𝑥 ∈ On ) → ( 𝑦𝑥 ↔ ¬ 𝑥𝑦 ) )
5 2 3 4 3bitr2d ( ( 𝑦 ∈ On ∧ 𝑥 ∈ On ) → ( ( 𝑦 = 𝑥𝑦𝑥 ) ↔ ¬ 𝑥𝑦 ) )
6 5 con2bid ( ( 𝑦 ∈ On ∧ 𝑥 ∈ On ) → ( 𝑥𝑦 ↔ ¬ ( 𝑦 = 𝑥𝑦𝑥 ) ) )
7 6 ancoms ( ( 𝑥 ∈ On ∧ 𝑦 ∈ On ) → ( 𝑥𝑦 ↔ ¬ ( 𝑦 = 𝑥𝑦𝑥 ) ) )
8 4 ancoms ( ( 𝑥 ∈ On ∧ 𝑦 ∈ On ) → ( 𝑦𝑥 ↔ ¬ 𝑥𝑦 ) )
9 ontri1 ( ( 𝑥 ∈ On ∧ 𝑦 ∈ On ) → ( 𝑥𝑦 ↔ ¬ 𝑦𝑥 ) )
10 8 9 anbi12d ( ( 𝑥 ∈ On ∧ 𝑦 ∈ On ) → ( ( 𝑦𝑥𝑥𝑦 ) ↔ ( ¬ 𝑥𝑦 ∧ ¬ 𝑦𝑥 ) ) )
11 eqss ( 𝑦 = 𝑥 ↔ ( 𝑦𝑥𝑥𝑦 ) )
12 ioran ( ¬ ( 𝑥𝑦𝑦𝑥 ) ↔ ( ¬ 𝑥𝑦 ∧ ¬ 𝑦𝑥 ) )
13 10 11 12 3bitr4g ( ( 𝑥 ∈ On ∧ 𝑦 ∈ On ) → ( 𝑦 = 𝑥 ↔ ¬ ( 𝑥𝑦𝑦𝑥 ) ) )
14 equcom ( 𝑦 = 𝑥𝑥 = 𝑦 )
15 14 orbi2i ( ( 𝑥𝑦𝑦 = 𝑥 ) ↔ ( 𝑥𝑦𝑥 = 𝑦 ) )
16 15 a1i ( ( 𝑥 ∈ On ∧ 𝑦 ∈ On ) → ( ( 𝑥𝑦𝑦 = 𝑥 ) ↔ ( 𝑥𝑦𝑥 = 𝑦 ) ) )
17 onsseleq ( ( 𝑥 ∈ On ∧ 𝑦 ∈ On ) → ( 𝑥𝑦 ↔ ( 𝑥𝑦𝑥 = 𝑦 ) ) )
18 16 17 9 3bitr2d ( ( 𝑥 ∈ On ∧ 𝑦 ∈ On ) → ( ( 𝑥𝑦𝑦 = 𝑥 ) ↔ ¬ 𝑦𝑥 ) )
19 18 con2bid ( ( 𝑥 ∈ On ∧ 𝑦 ∈ On ) → ( 𝑦𝑥 ↔ ¬ ( 𝑥𝑦𝑦 = 𝑥 ) ) )
20 7 13 19 3jca ( ( 𝑥 ∈ On ∧ 𝑦 ∈ On ) → ( ( 𝑥𝑦 ↔ ¬ ( 𝑦 = 𝑥𝑦𝑥 ) ) ∧ ( 𝑦 = 𝑥 ↔ ¬ ( 𝑥𝑦𝑦𝑥 ) ) ∧ ( 𝑦𝑥 ↔ ¬ ( 𝑥𝑦𝑦 = 𝑥 ) ) ) )
21 20 rgen2 𝑥 ∈ On ∀ 𝑦 ∈ On ( ( 𝑥𝑦 ↔ ¬ ( 𝑦 = 𝑥𝑦𝑥 ) ) ∧ ( 𝑦 = 𝑥 ↔ ¬ ( 𝑥𝑦𝑦𝑥 ) ) ∧ ( 𝑦𝑥 ↔ ¬ ( 𝑥𝑦𝑦 = 𝑥 ) ) )