Theorem ordtri3

Description: A trichotomy law for ordinals. (Contributed by NM, 18-Oct-1995) (Proof shortened by Andrew Salmon, 25-Jul-2011) (Proof shortened by JJ, 24-Sep-2021)

	Ref	Expression
Assertion	ordtri3	⊢ ( ( Ord 𝐴 ∧ Ord 𝐵 ) → ( 𝐴 = 𝐵 ↔ ¬ ( 𝐴 ∈ 𝐵 ∨ 𝐵 ∈ 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		ordirr	⊢ ( Ord 𝐵 → ¬ 𝐵 ∈ 𝐵 )
2	1	adantl	⊢ ( ( Ord 𝐴 ∧ Ord 𝐵 ) → ¬ 𝐵 ∈ 𝐵 )
3		eleq2	⊢ ( 𝐴 = 𝐵 → ( 𝐵 ∈ 𝐴 ↔ 𝐵 ∈ 𝐵 ) )
4	3	notbid	⊢ ( 𝐴 = 𝐵 → ( ¬ 𝐵 ∈ 𝐴 ↔ ¬ 𝐵 ∈ 𝐵 ) )
5	2 4	syl5ibrcom	⊢ ( ( Ord 𝐴 ∧ Ord 𝐵 ) → ( 𝐴 = 𝐵 → ¬ 𝐵 ∈ 𝐴 ) )
6	5	pm4.71d	⊢ ( ( Ord 𝐴 ∧ Ord 𝐵 ) → ( 𝐴 = 𝐵 ↔ ( 𝐴 = 𝐵 ∧ ¬ 𝐵 ∈ 𝐴 ) ) )
7		pm5.61	⊢ ( ( ( 𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴 ) ∧ ¬ 𝐵 ∈ 𝐴 ) ↔ ( 𝐴 = 𝐵 ∧ ¬ 𝐵 ∈ 𝐴 ) )
8		pm4.52	⊢ ( ( ( 𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴 ) ∧ ¬ 𝐵 ∈ 𝐴 ) ↔ ¬ ( ¬ ( 𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴 ) ∨ 𝐵 ∈ 𝐴 ) )
9	7 8	bitr3i	⊢ ( ( 𝐴 = 𝐵 ∧ ¬ 𝐵 ∈ 𝐴 ) ↔ ¬ ( ¬ ( 𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴 ) ∨ 𝐵 ∈ 𝐴 ) )
10	6 9	bitrdi	⊢ ( ( Ord 𝐴 ∧ Ord 𝐵 ) → ( 𝐴 = 𝐵 ↔ ¬ ( ¬ ( 𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴 ) ∨ 𝐵 ∈ 𝐴 ) ) )
11		ordtri2	⊢ ( ( Ord 𝐴 ∧ Ord 𝐵 ) → ( 𝐴 ∈ 𝐵 ↔ ¬ ( 𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴 ) ) )
12	11	orbi1d	⊢ ( ( Ord 𝐴 ∧ Ord 𝐵 ) → ( ( 𝐴 ∈ 𝐵 ∨ 𝐵 ∈ 𝐴 ) ↔ ( ¬ ( 𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴 ) ∨ 𝐵 ∈ 𝐴 ) ) )
13	12	notbid	⊢ ( ( Ord 𝐴 ∧ Ord 𝐵 ) → ( ¬ ( 𝐴 ∈ 𝐵 ∨ 𝐵 ∈ 𝐴 ) ↔ ¬ ( ¬ ( 𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴 ) ∨ 𝐵 ∈ 𝐴 ) ) )
14	10 13	bitr4d	⊢ ( ( Ord 𝐴 ∧ Ord 𝐵 ) → ( 𝐴 = 𝐵 ↔ ¬ ( 𝐴 ∈ 𝐵 ∨ 𝐵 ∈ 𝐴 ) ) )