Theorem domtrfil

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

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

Proof

Step	Hyp	Ref	Expression
1		reldom	⊢ Rel ≼
2	1	brrelex2i	⊢ ( 𝐵 ≼ 𝐶 → 𝐶 ∈ V )
3	2	anim2i	⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ≼ 𝐶 ) → ( 𝐴 ∈ Fin ∧ 𝐶 ∈ V ) )
4	3	3adant2	⊢ ( ( 𝐴 ∈ Fin ∧ 𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐶 ) → ( 𝐴 ∈ Fin ∧ 𝐶 ∈ V ) )
5		brdomi	⊢ ( 𝐴 ≼ 𝐵 → ∃ 𝑔 𝑔 : 𝐴 –1-1→ 𝐵 )
6		brdomi	⊢ ( 𝐵 ≼ 𝐶 → ∃ 𝑓 𝑓 : 𝐵 –1-1→ 𝐶 )
7		exdistrv	⊢ ( ∃ 𝑔 ∃ 𝑓 ( 𝑔 : 𝐴 –1-1→ 𝐵 ∧ 𝑓 : 𝐵 –1-1→ 𝐶 ) ↔ ( ∃ 𝑔 𝑔 : 𝐴 –1-1→ 𝐵 ∧ ∃ 𝑓 𝑓 : 𝐵 –1-1→ 𝐶 ) )
8		19.42vv	⊢ ( ∃ 𝑔 ∃ 𝑓 ( ( 𝐴 ∈ Fin ∧ 𝐶 ∈ V ) ∧ ( 𝑔 : 𝐴 –1-1→ 𝐵 ∧ 𝑓 : 𝐵 –1-1→ 𝐶 ) ) ↔ ( ( 𝐴 ∈ Fin ∧ 𝐶 ∈ V ) ∧ ∃ 𝑔 ∃ 𝑓 ( 𝑔 : 𝐴 –1-1→ 𝐵 ∧ 𝑓 : 𝐵 –1-1→ 𝐶 ) ) )
9		f1co	⊢ ( ( 𝑓 : 𝐵 –1-1→ 𝐶 ∧ 𝑔 : 𝐴 –1-1→ 𝐵 ) → ( 𝑓 ∘ 𝑔 ) : 𝐴 –1-1→ 𝐶 )
10	9	ancoms	⊢ ( ( 𝑔 : 𝐴 –1-1→ 𝐵 ∧ 𝑓 : 𝐵 –1-1→ 𝐶 ) → ( 𝑓 ∘ 𝑔 ) : 𝐴 –1-1→ 𝐶 )
11		f1domfi2	⊢ ( ( 𝐴 ∈ Fin ∧ 𝐶 ∈ V ∧ ( 𝑓 ∘ 𝑔 ) : 𝐴 –1-1→ 𝐶 ) → 𝐴 ≼ 𝐶 )
12	11	3expa	⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐶 ∈ V ) ∧ ( 𝑓 ∘ 𝑔 ) : 𝐴 –1-1→ 𝐶 ) → 𝐴 ≼ 𝐶 )
13	10 12	sylan2	⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐶 ∈ V ) ∧ ( 𝑔 : 𝐴 –1-1→ 𝐵 ∧ 𝑓 : 𝐵 –1-1→ 𝐶 ) ) → 𝐴 ≼ 𝐶 )
14	13	exlimivv	⊢ ( ∃ 𝑔 ∃ 𝑓 ( ( 𝐴 ∈ Fin ∧ 𝐶 ∈ V ) ∧ ( 𝑔 : 𝐴 –1-1→ 𝐵 ∧ 𝑓 : 𝐵 –1-1→ 𝐶 ) ) → 𝐴 ≼ 𝐶 )
15	8 14	sylbir	⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐶 ∈ V ) ∧ ∃ 𝑔 ∃ 𝑓 ( 𝑔 : 𝐴 –1-1→ 𝐵 ∧ 𝑓 : 𝐵 –1-1→ 𝐶 ) ) → 𝐴 ≼ 𝐶 )
16	7 15	sylan2br	⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐶 ∈ V ) ∧ ( ∃ 𝑔 𝑔 : 𝐴 –1-1→ 𝐵 ∧ ∃ 𝑓 𝑓 : 𝐵 –1-1→ 𝐶 ) ) → 𝐴 ≼ 𝐶 )
17	16	3impb	⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐶 ∈ V ) ∧ ∃ 𝑔 𝑔 : 𝐴 –1-1→ 𝐵 ∧ ∃ 𝑓 𝑓 : 𝐵 –1-1→ 𝐶 ) → 𝐴 ≼ 𝐶 )
18	6 17	syl3an3	⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐶 ∈ V ) ∧ ∃ 𝑔 𝑔 : 𝐴 –1-1→ 𝐵 ∧ 𝐵 ≼ 𝐶 ) → 𝐴 ≼ 𝐶 )
19	5 18	syl3an2	⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐶 ∈ V ) ∧ 𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐶 ) → 𝐴 ≼ 𝐶 )
20	4 19	syld3an1	⊢ ( ( 𝐴 ∈ Fin ∧ 𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐶 ) → 𝐴 ≼ 𝐶 )