Theorem domtrfir

Description: Transitivity of dominance relation for finite sets, proved without using the Axiom of Power Sets (unlike domtr ). (Contributed by BTernaryTau, 24-Nov-2024)

	Ref	Expression
Assertion	domtrfir	⊢ ( ( 𝐶 ∈ Fin ∧ 𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐶 ) → 𝐴 ≼ 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		domfi	⊢ ( ( 𝐶 ∈ Fin ∧ 𝐵 ≼ 𝐶 ) → 𝐵 ∈ Fin )
2	1	3adant2	⊢ ( ( 𝐶 ∈ Fin ∧ 𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐶 ) → 𝐵 ∈ Fin )
3		domtrfi	⊢ ( ( 𝐵 ∈ Fin ∧ 𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐶 ) → 𝐴 ≼ 𝐶 )
4	2 3	syld3an1	⊢ ( ( 𝐶 ∈ Fin ∧ 𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐶 ) → 𝐴 ≼ 𝐶 )