Theorem oneltr

Description: The elementhood relation on the ordinals is transitive. Theorem 1.9(ii) of Schloeder p. 1. See ontr1 . (Contributed by RP, 15-Jan-2025)

	Ref	Expression
Assertion	oneltr	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ) → 𝐴 ∈ 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		ontr1	⊢ ( 𝐶 ∈ On → ( ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ) → 𝐴 ∈ 𝐶 ) )
2	1	3ad2ant3	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ) → 𝐴 ∈ 𝐶 ) )