Theorem ordtri2

Description: A trichotomy law for ordinals. (Contributed by NM, 25-Nov-1995)

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

Proof

Step	Hyp	Ref	Expression
1		ordsseleq	⊢ ( ( Ord 𝐵 ∧ Ord 𝐴 ) → ( 𝐵 ⊆ 𝐴 ↔ ( 𝐵 ∈ 𝐴 ∨ 𝐵 = 𝐴 ) ) )
2		eqcom	⊢ ( 𝐵 = 𝐴 ↔ 𝐴 = 𝐵 )
3	2	orbi2i	⊢ ( ( 𝐵 ∈ 𝐴 ∨ 𝐵 = 𝐴 ) ↔ ( 𝐵 ∈ 𝐴 ∨ 𝐴 = 𝐵 ) )
4		orcom	⊢ ( ( 𝐵 ∈ 𝐴 ∨ 𝐴 = 𝐵 ) ↔ ( 𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴 ) )
5	3 4	bitri	⊢ ( ( 𝐵 ∈ 𝐴 ∨ 𝐵 = 𝐴 ) ↔ ( 𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴 ) )
6	1 5	bitrdi	⊢ ( ( Ord 𝐵 ∧ Ord 𝐴 ) → ( 𝐵 ⊆ 𝐴 ↔ ( 𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴 ) ) )
7		ordtri1	⊢ ( ( Ord 𝐵 ∧ Ord 𝐴 ) → ( 𝐵 ⊆ 𝐴 ↔ ¬ 𝐴 ∈ 𝐵 ) )
8	6 7	bitr3d	⊢ ( ( Ord 𝐵 ∧ Ord 𝐴 ) → ( ( 𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴 ) ↔ ¬ 𝐴 ∈ 𝐵 ) )
9	8	ancoms	⊢ ( ( Ord 𝐴 ∧ Ord 𝐵 ) → ( ( 𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴 ) ↔ ¬ 𝐴 ∈ 𝐵 ) )
10	9	con2bid	⊢ ( ( Ord 𝐴 ∧ Ord 𝐵 ) → ( 𝐴 ∈ 𝐵 ↔ ¬ ( 𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴 ) ) )