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 ⊢A⊆B∧B≼C→A≼C

Proof

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