Theorem ordtri4

Description: A trichotomy law for ordinals. (Contributed by NM, 1-Nov-2003) (Proof shortened by Andrew Salmon, 25-Jul-2011)

	Ref	Expression
Assertion	ordtri4	⊢ ( ( Ord 𝐴 ∧ Ord 𝐵 ) → ( 𝐴 = 𝐵 ↔ ( 𝐴 ⊆ 𝐵 ∧ ¬ 𝐴 ∈ 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		eqss	⊢ ( 𝐴 = 𝐵 ↔ ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴 ) )
2		ordtri1	⊢ ( ( Ord 𝐵 ∧ Ord 𝐴 ) → ( 𝐵 ⊆ 𝐴 ↔ ¬ 𝐴 ∈ 𝐵 ) )
3	2	ancoms	⊢ ( ( Ord 𝐴 ∧ Ord 𝐵 ) → ( 𝐵 ⊆ 𝐴 ↔ ¬ 𝐴 ∈ 𝐵 ) )
4	3	anbi2d	⊢ ( ( Ord 𝐴 ∧ Ord 𝐵 ) → ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴 ) ↔ ( 𝐴 ⊆ 𝐵 ∧ ¬ 𝐴 ∈ 𝐵 ) ) )
5	1 4	bitrid	⊢ ( ( Ord 𝐴 ∧ Ord 𝐵 ) → ( 𝐴 = 𝐵 ↔ ( 𝐴 ⊆ 𝐵 ∧ ¬ 𝐴 ∈ 𝐵 ) ) )