Theorem sdomdomtrfi

Description: Transitivity of strict dominance and dominance when A is finite, proved without using the Axiom of Power Sets (unlike sdomdomtr ). (Contributed by BTernaryTau, 25-Nov-2024)

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

Proof

Step	Hyp	Ref	Expression
1		sdomdom	⊢ ( 𝐴 ≺ 𝐵 → 𝐴 ≼ 𝐵 )
2		domtrfil	⊢ ( ( 𝐴 ∈ Fin ∧ 𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐶 ) → 𝐴 ≼ 𝐶 )
3	1 2	syl3an2	⊢ ( ( 𝐴 ∈ Fin ∧ 𝐴 ≺ 𝐵 ∧ 𝐵 ≼ 𝐶 ) → 𝐴 ≼ 𝐶 )
4		simp1	⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ≼ 𝐶 ∧ 𝐴 ≈ 𝐶 ) → 𝐴 ∈ Fin )
5		ensymfib	⊢ ( 𝐴 ∈ Fin → ( 𝐴 ≈ 𝐶 ↔ 𝐶 ≈ 𝐴 ) )
6	5	biimpa	⊢ ( ( 𝐴 ∈ Fin ∧ 𝐴 ≈ 𝐶 ) → 𝐶 ≈ 𝐴 )
7	6	3adant2	⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ≼ 𝐶 ∧ 𝐴 ≈ 𝐶 ) → 𝐶 ≈ 𝐴 )
8		endom	⊢ ( 𝐶 ≈ 𝐴 → 𝐶 ≼ 𝐴 )
9		domtrfir	⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ≼ 𝐶 ∧ 𝐶 ≼ 𝐴 ) → 𝐵 ≼ 𝐴 )
10	8 9	syl3an3	⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ≼ 𝐶 ∧ 𝐶 ≈ 𝐴 ) → 𝐵 ≼ 𝐴 )
11	7 10	syld3an3	⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ≼ 𝐶 ∧ 𝐴 ≈ 𝐶 ) → 𝐵 ≼ 𝐴 )
12		domfi	⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ≼ 𝐴 ) → 𝐵 ∈ Fin )
13		domnsymfi	⊢ ( ( 𝐵 ∈ Fin ∧ 𝐵 ≼ 𝐴 ) → ¬ 𝐴 ≺ 𝐵 )
14	12 13	sylancom	⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ≼ 𝐴 ) → ¬ 𝐴 ≺ 𝐵 )
15	4 11 14	syl2anc	⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ≼ 𝐶 ∧ 𝐴 ≈ 𝐶 ) → ¬ 𝐴 ≺ 𝐵 )
16	15	3expia	⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ≼ 𝐶 ) → ( 𝐴 ≈ 𝐶 → ¬ 𝐴 ≺ 𝐵 ) )
17	16	con2d	⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ≼ 𝐶 ) → ( 𝐴 ≺ 𝐵 → ¬ 𝐴 ≈ 𝐶 ) )
18	17	3impia	⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ≼ 𝐶 ∧ 𝐴 ≺ 𝐵 ) → ¬ 𝐴 ≈ 𝐶 )
19	18	3com23	⊢ ( ( 𝐴 ∈ Fin ∧ 𝐴 ≺ 𝐵 ∧ 𝐵 ≼ 𝐶 ) → ¬ 𝐴 ≈ 𝐶 )
20		brsdom	⊢ ( 𝐴 ≺ 𝐶 ↔ ( 𝐴 ≼ 𝐶 ∧ ¬ 𝐴 ≈ 𝐶 ) )
21	3 19 20	sylanbrc	⊢ ( ( 𝐴 ∈ Fin ∧ 𝐴 ≺ 𝐵 ∧ 𝐵 ≼ 𝐶 ) → 𝐴 ≺ 𝐶 )