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 f f : A 1-1 B
2 1 3ad2ant3 C V B C A B f f : A 1-1 B
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-1 B B C f : A 1-1 C
10 vex f V
11 f1dom4g f V A V C V f : A 1-1 C A C
12 10 11 mp3anl1 A V C V f : A 1-1 C A C
13 12 ancoms f : A 1-1 C A V C V A C
14 9 13 sylan f : A 1-1 B B C A V C V A C
15 14 expl f : A 1-1 B B C A V C V A C
16 15 exlimiv f f : A 1-1 B B C A V C V A C
17 2 8 16 sylc C V B C A B A C