Theorem ontr1i

Description: Transitive law for ordinal numbers. Inference form of ontr1 . (Contributed by BTernaryTau, 19-Oct-2026)

	Ref	Expression
Hypotheses	ontr1i.1	⊢ 𝐶 ∈ On
	ontr1i.2	⊢ 𝐴 ∈ 𝐵
	ontr1i.3	⊢ 𝐵 ∈ 𝐶
Assertion	ontr1i	⊢ 𝐴 ∈ 𝐶

Proof

Step	Hyp	Ref	Expression
1		ontr1i.1	⊢ 𝐶 ∈ On
2		ontr1i.2	⊢ 𝐴 ∈ 𝐵
3		ontr1i.3	⊢ 𝐵 ∈ 𝐶
4		ontr1	⊢ ( 𝐶 ∈ On → ( ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ) → 𝐴 ∈ 𝐶 ) )
5	2 3 4	mp2ani	⊢ ( 𝐶 ∈ On → 𝐴 ∈ 𝐶 )
6	1 5	ax-mp	⊢ 𝐴 ∈ 𝐶