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

Metamath Proof Explorer

Theorem domssl

Description: If A is a subset of B and C dominates B , then C also dominates A . (Contributed by BTernaryTau, 7-Dec-2024)

Ref Expression
Assertion domssl ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ≼ 𝐶 ) → 𝐴 ≼ 𝐶 )

Proof

Step Hyp Ref Expression
1 simpr ⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ≼ 𝐶 ) → 𝐵 ≼ 𝐶 )
2 reldom ⊢ Rel ≼
3 2 brrelex12i ⊢ ( 𝐵 ≼ 𝐶 → ( 𝐵 ∈ V ∧ 𝐶 ∈ V ) )
4 simpl ⊢ ( ( 𝐴 ⊆ 𝐵 ∧ ( 𝐵 ∈ V ∧ 𝐶 ∈ V ) ) → 𝐴 ⊆ 𝐵 )
5 ssexg ⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ V ) → 𝐴 ∈ V )
6 5 adantrr ⊢ ( ( 𝐴 ⊆ 𝐵 ∧ ( 𝐵 ∈ V ∧ 𝐶 ∈ V ) ) → 𝐴 ∈ V )
7 simprr ⊢ ( ( 𝐴 ⊆ 𝐵 ∧ ( 𝐵 ∈ V ∧ 𝐶 ∈ V ) ) → 𝐶 ∈ V )
8 4 6 7 jca32 ⊢ ( ( 𝐴 ⊆ 𝐵 ∧ ( 𝐵 ∈ V ∧ 𝐶 ∈ V ) ) → ( 𝐴 ⊆ 𝐵 ∧ ( 𝐴 ∈ V ∧ 𝐶 ∈ V ) ) )
9 3 8 sylan2 ⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ≼ 𝐶 ) → ( 𝐴 ⊆ 𝐵 ∧ ( 𝐴 ∈ V ∧ 𝐶 ∈ V ) ) )
10 brdomi ⊢ ( 𝐵 ≼ 𝐶 → ∃ 𝑓 𝑓 : 𝐵 –1-1→ 𝐶 )
11 f1ssres ⊢ ( ( 𝑓 : 𝐵 –1-1→ 𝐶 ∧ 𝐴 ⊆ 𝐵 ) → ( 𝑓 ↾ 𝐴 ) : 𝐴 –1-1→ 𝐶 )
12 vex ⊢ 𝑓 ∈ V
13 12 resex ⊢ ( 𝑓 ↾ 𝐴 ) ∈ V
14 f1dom4g ⊢ ( ( ( ( 𝑓 ↾ 𝐴 ) ∈ V ∧ 𝐴 ∈ V ∧ 𝐶 ∈ V ) ∧ ( 𝑓 ↾ 𝐴 ) : 𝐴 –1-1→ 𝐶 ) → 𝐴 ≼ 𝐶 )
15 13 14 mp3anl1 ⊢ ( ( ( 𝐴 ∈ V ∧ 𝐶 ∈ V ) ∧ ( 𝑓 ↾ 𝐴 ) : 𝐴 –1-1→ 𝐶 ) → 𝐴 ≼ 𝐶 )
16 15 ancoms ⊢ ( ( ( 𝑓 ↾ 𝐴 ) : 𝐴 –1-1→ 𝐶 ∧ ( 𝐴 ∈ V ∧ 𝐶 ∈ V ) ) → 𝐴 ≼ 𝐶 )
17 11 16 sylan ⊢ ( ( ( 𝑓 : 𝐵 –1-1→ 𝐶 ∧ 𝐴 ⊆ 𝐵 ) ∧ ( 𝐴 ∈ V ∧ 𝐶 ∈ V ) ) → 𝐴 ≼ 𝐶 )
18 17 expl ⊢ ( 𝑓 : 𝐵 –1-1→ 𝐶 → ( ( 𝐴 ⊆ 𝐵 ∧ ( 𝐴 ∈ V ∧ 𝐶 ∈ V ) ) → 𝐴 ≼ 𝐶 ) )
19 18 exlimiv ⊢ ( ∃ 𝑓 𝑓 : 𝐵 –1-1→ 𝐶 → ( ( 𝐴 ⊆ 𝐵 ∧ ( 𝐴 ∈ V ∧ 𝐶 ∈ V ) ) → 𝐴 ≼ 𝐶 ) )
20 10 19 syl ⊢ ( 𝐵 ≼ 𝐶 → ( ( 𝐴 ⊆ 𝐵 ∧ ( 𝐴 ∈ V ∧ 𝐶 ∈ V ) ) → 𝐴 ≼ 𝐶 ) )
21 1 9 20 sylc ⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ≼ 𝐶 ) → 𝐴 ≼ 𝐶 )