Theorem domtrfi

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

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

Proof

Step	Hyp	Ref	Expression
1		domfi	⊢ ( ( 𝐶 ∈ Fin ∧ 𝐵 ≼ 𝐶 ) → 𝐵 ∈ Fin )
2		brdomg	⊢ ( 𝐵 ∈ Fin → ( 𝐴 ≼ 𝐵 ↔ ∃ 𝑔 𝑔 : 𝐴 –1-1→ 𝐵 ) )
3	2	biimpa	⊢ ( ( 𝐵 ∈ Fin ∧ 𝐴 ≼ 𝐵 ) → ∃ 𝑔 𝑔 : 𝐴 –1-1→ 𝐵 )
4	1 3	stoic3	⊢ ( ( 𝐶 ∈ Fin ∧ 𝐵 ≼ 𝐶 ∧ 𝐴 ≼ 𝐵 ) → ∃ 𝑔 𝑔 : 𝐴 –1-1→ 𝐵 )
5	4	3com23	⊢ ( ( 𝐶 ∈ Fin ∧ 𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐶 ) → ∃ 𝑔 𝑔 : 𝐴 –1-1→ 𝐵 )
6		brdomg	⊢ ( 𝐶 ∈ Fin → ( 𝐵 ≼ 𝐶 ↔ ∃ 𝑓 𝑓 : 𝐵 –1-1→ 𝐶 ) )
7	6	biimpa	⊢ ( ( 𝐶 ∈ Fin ∧ 𝐵 ≼ 𝐶 ) → ∃ 𝑓 𝑓 : 𝐵 –1-1→ 𝐶 )
8	7	3adant2	⊢ ( ( 𝐶 ∈ Fin ∧ ∃ 𝑔 𝑔 : 𝐴 –1-1→ 𝐵 ∧ 𝐵 ≼ 𝐶 ) → ∃ 𝑓 𝑓 : 𝐵 –1-1→ 𝐶 )
9		exdistrv	⊢ ( ∃ 𝑔 ∃ 𝑓 ( 𝑔 : 𝐴 –1-1→ 𝐵 ∧ 𝑓 : 𝐵 –1-1→ 𝐶 ) ↔ ( ∃ 𝑔 𝑔 : 𝐴 –1-1→ 𝐵 ∧ ∃ 𝑓 𝑓 : 𝐵 –1-1→ 𝐶 ) )
10		19.42vv	⊢ ( ∃ 𝑔 ∃ 𝑓 ( 𝐶 ∈ Fin ∧ ( 𝑔 : 𝐴 –1-1→ 𝐵 ∧ 𝑓 : 𝐵 –1-1→ 𝐶 ) ) ↔ ( 𝐶 ∈ Fin ∧ ∃ 𝑔 ∃ 𝑓 ( 𝑔 : 𝐴 –1-1→ 𝐵 ∧ 𝑓 : 𝐵 –1-1→ 𝐶 ) ) )
11		f1co	⊢ ( ( 𝑓 : 𝐵 –1-1→ 𝐶 ∧ 𝑔 : 𝐴 –1-1→ 𝐵 ) → ( 𝑓 ∘ 𝑔 ) : 𝐴 –1-1→ 𝐶 )
12	11	ancoms	⊢ ( ( 𝑔 : 𝐴 –1-1→ 𝐵 ∧ 𝑓 : 𝐵 –1-1→ 𝐶 ) → ( 𝑓 ∘ 𝑔 ) : 𝐴 –1-1→ 𝐶 )
13		f1domfi	⊢ ( ( 𝐶 ∈ Fin ∧ ( 𝑓 ∘ 𝑔 ) : 𝐴 –1-1→ 𝐶 ) → 𝐴 ≼ 𝐶 )
14	12 13	sylan2	⊢ ( ( 𝐶 ∈ Fin ∧ ( 𝑔 : 𝐴 –1-1→ 𝐵 ∧ 𝑓 : 𝐵 –1-1→ 𝐶 ) ) → 𝐴 ≼ 𝐶 )
15	14	exlimivv	⊢ ( ∃ 𝑔 ∃ 𝑓 ( 𝐶 ∈ Fin ∧ ( 𝑔 : 𝐴 –1-1→ 𝐵 ∧ 𝑓 : 𝐵 –1-1→ 𝐶 ) ) → 𝐴 ≼ 𝐶 )
16	10 15	sylbir	⊢ ( ( 𝐶 ∈ Fin ∧ ∃ 𝑔 ∃ 𝑓 ( 𝑔 : 𝐴 –1-1→ 𝐵 ∧ 𝑓 : 𝐵 –1-1→ 𝐶 ) ) → 𝐴 ≼ 𝐶 )
17	9 16	sylan2br	⊢ ( ( 𝐶 ∈ Fin ∧ ( ∃ 𝑔 𝑔 : 𝐴 –1-1→ 𝐵 ∧ ∃ 𝑓 𝑓 : 𝐵 –1-1→ 𝐶 ) ) → 𝐴 ≼ 𝐶 )
18	17	3impb	⊢ ( ( 𝐶 ∈ Fin ∧ ∃ 𝑔 𝑔 : 𝐴 –1-1→ 𝐵 ∧ ∃ 𝑓 𝑓 : 𝐵 –1-1→ 𝐶 ) → 𝐴 ≼ 𝐶 )
19	8 18	syld3an3	⊢ ( ( 𝐶 ∈ Fin ∧ ∃ 𝑔 𝑔 : 𝐴 –1-1→ 𝐵 ∧ 𝐵 ≼ 𝐶 ) → 𝐴 ≼ 𝐶 )
20	5 19	syld3an2	⊢ ( ( 𝐶 ∈ Fin ∧ 𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐶 ) → 𝐴 ≼ 𝐶 )