Metamath Proof Explorer

Theorem domssr

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

Ref Expression
Assertion domssr ⊢C∈V∧B⊆C∧A≼B→A≼C

Proof

Step Hyp Ref Expression
1 brdomi ⊢A≼B→∃ff:A⟶1-1B
2 1 3ad2ant3 ⊢C∈V∧B⊆C∧A≼B→∃ff:A⟶1-1B
3 simp2 ⊢C∈V∧B⊆C∧A≼B→B⊆C
4 reldom ⊢Rel⁡≼
5 4 brrelex1i ⊢A≼B→A∈V
6 5 3ad2ant3 ⊢C∈V∧B⊆C∧A≼B→A∈V
7 simp1 ⊢C∈V∧B⊆C∧A≼B→C∈V
8 3 6 7 jca32 ⊢C∈V∧B⊆C∧A≼B→B⊆C∧A∈V∧C∈V
9 f1ss ⊢f:A⟶1-1B∧B⊆C→f:A⟶1-1C
10 vex ⊢f∈V
11 f1dom4g ⊢f∈V∧A∈V∧C∈V∧f:A⟶1-1C→A≼C
12 10 11 mp3anl1 ⊢A∈V∧C∈V∧f:A⟶1-1C→A≼C
13 12 ancoms ⊢f:A⟶1-1C∧A∈V∧C∈V→A≼C
14 9 13 sylan ⊢f:A⟶1-1B∧B⊆C∧A∈V∧C∈V→A≼C
15 14 expl ⊢f:A⟶1-1B→B⊆C∧A∈V∧C∈V→A≼C
16 15 exlimiv ⊢∃ff:A⟶1-1B→B⊆C∧A∈V∧C∈V→A≼C
17 2 8 16 sylc ⊢C∈V∧B⊆C∧A≼B→A≼C