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 C_ B /\ B ~<_ C ) -> A ~<_ C )

Proof

Step Hyp Ref Expression
1 simpr 
 |-  ( ( A C_ B /\ B ~<_ C ) -> B ~<_ C )
2 reldom 
 |-  Rel ~<_
3 2 brrelex12i 
 |-  ( B ~<_ C -> ( B e. _V /\ C e. _V ) )
4 simpl 
 |-  ( ( A C_ B /\ ( B e. _V /\ C e. _V ) ) -> A C_ B )
5 ssexg 
 |-  ( ( A C_ B /\ B e. _V ) -> A e. _V )
6 5 adantrr 
 |-  ( ( A C_ B /\ ( B e. _V /\ C e. _V ) ) -> A e. _V )
7 simprr 
 |-  ( ( A C_ B /\ ( B e. _V /\ C e. _V ) ) -> C e. _V )
8 4 6 7 jca32 
 |-  ( ( A C_ B /\ ( B e. _V /\ C e. _V ) ) -> ( A C_ B /\ ( A e. _V /\ C e. _V ) ) )
9 3 8 sylan2 
 |-  ( ( A C_ B /\ B ~<_ C ) -> ( A C_ B /\ ( A e. _V /\ C e. _V ) ) )
10 brdomi 
 |-  ( B ~<_ C -> E. f f : B -1-1-> C )
11 f1ssres 
 |-  ( ( f : B -1-1-> C /\ A C_ B ) -> ( f |` A ) : A -1-1-> C )
12 vex 
 |-  f e. _V
13 12 resex 
 |-  ( f |` A ) e. _V
14 f1dom4g 
 |-  ( ( ( ( f |` A ) e. _V /\ A e. _V /\ C e. _V ) /\ ( f |` A ) : A -1-1-> C ) -> A ~<_ C )
15 13 14 mp3anl1 
 |-  ( ( ( A e. _V /\ C e. _V ) /\ ( f |` A ) : A -1-1-> C ) -> A ~<_ C )
16 15 ancoms 
 |-  ( ( ( f |` A ) : A -1-1-> C /\ ( A e. _V /\ C e. _V ) ) -> A ~<_ C )
17 11 16 sylan 
 |-  ( ( ( f : B -1-1-> C /\ A C_ B ) /\ ( A e. _V /\ C e. _V ) ) -> A ~<_ C )
18 17 expl 
 |-  ( f : B -1-1-> C -> ( ( A C_ B /\ ( A e. _V /\ C e. _V ) ) -> A ~<_ C ) )
19 18 exlimiv 
 |-  ( E. f f : B -1-1-> C -> ( ( A C_ B /\ ( A e. _V /\ C e. _V ) ) -> A ~<_ C ) )
20 10 19 syl 
 |-  ( B ~<_ C -> ( ( A C_ B /\ ( A e. _V /\ C e. _V ) ) -> A ~<_ C ) )
21 1 9 20 sylc 
 |-  ( ( A C_ B /\ B ~<_ C ) -> A ~<_ C )