Theorem oneptr

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

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

Proof

Step	Hyp	Ref	Expression
1		epweon	⊢ E We On
2		weso	⊢ ( E We On → E Or On )
3		sopo	⊢ ( E Or On → E Po On )
4		potr	⊢ ( ( E Po On ∧ ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ) → ( ( 𝐴 E 𝐵 ∧ 𝐵 E 𝐶 ) → 𝐴 E 𝐶 ) )
5	4	ex	⊢ ( E Po On → ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( ( 𝐴 E 𝐵 ∧ 𝐵 E 𝐶 ) → 𝐴 E 𝐶 ) ) )
6	3 5	syl	⊢ ( E Or On → ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( ( 𝐴 E 𝐵 ∧ 𝐵 E 𝐶 ) → 𝐴 E 𝐶 ) ) )
7	1 2 6	mp2b	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( ( 𝐴 E 𝐵 ∧ 𝐵 E 𝐶 ) → 𝐴 E 𝐶 ) )