This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ∧ 𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐶 ) → 𝐴 ≼ 𝐶 )