Theorem ordtr3

Description: Transitive law for ordinal classes. (Contributed by Mario Carneiro, 30-Dec-2014) (Proof shortened by JJ, 24-Sep-2021)

	Ref	Expression
Assertion	ordtr3	⊢ ( ( Ord 𝐵 ∧ Ord 𝐶 ) → ( 𝐴 ∈ 𝐵 → ( 𝐴 ∈ 𝐶 ∨ 𝐶 ∈ 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		nelss	⊢ ( ( 𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶 ) → ¬ 𝐵 ⊆ 𝐶 )
2	1	adantl	⊢ ( ( ( Ord 𝐵 ∧ Ord 𝐶 ) ∧ ( 𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶 ) ) → ¬ 𝐵 ⊆ 𝐶 )
3		ordtri1	⊢ ( ( Ord 𝐵 ∧ Ord 𝐶 ) → ( 𝐵 ⊆ 𝐶 ↔ ¬ 𝐶 ∈ 𝐵 ) )
4	3	con2bid	⊢ ( ( Ord 𝐵 ∧ Ord 𝐶 ) → ( 𝐶 ∈ 𝐵 ↔ ¬ 𝐵 ⊆ 𝐶 ) )
5	4	adantr	⊢ ( ( ( Ord 𝐵 ∧ Ord 𝐶 ) ∧ ( 𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶 ) ) → ( 𝐶 ∈ 𝐵 ↔ ¬ 𝐵 ⊆ 𝐶 ) )
6	2 5	mpbird	⊢ ( ( ( Ord 𝐵 ∧ Ord 𝐶 ) ∧ ( 𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶 ) ) → 𝐶 ∈ 𝐵 )
7	6	expr	⊢ ( ( ( Ord 𝐵 ∧ Ord 𝐶 ) ∧ 𝐴 ∈ 𝐵 ) → ( ¬ 𝐴 ∈ 𝐶 → 𝐶 ∈ 𝐵 ) )
8	7	orrd	⊢ ( ( ( Ord 𝐵 ∧ Ord 𝐶 ) ∧ 𝐴 ∈ 𝐵 ) → ( 𝐴 ∈ 𝐶 ∨ 𝐶 ∈ 𝐵 ) )
9	8	ex	⊢ ( ( Ord 𝐵 ∧ Ord 𝐶 ) → ( 𝐴 ∈ 𝐵 → ( 𝐴 ∈ 𝐶 ∨ 𝐶 ∈ 𝐵 ) ) )