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 f f : B 1-1 C
11 f1ssres f : B 1-1 C A B f A : A 1-1 C
12 vex f V
13 12 resex f A V
14 f1dom4g f A V A V C V f A : A 1-1 C A C
15 13 14 mp3anl1 A V C V f A : A 1-1 C A C
16 15 ancoms f A : A 1-1 C A V C V A C
17 11 16 sylan f : B 1-1 C A B A V C V A C
18 17 expl f : B 1-1 C A B A V C V A C
19 18 exlimiv f f : B 1-1 C 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