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