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

Proof

Step Hyp Ref Expression
1 brdomi
 |-  ( A ~<_ B -> E. f f : A -1-1-> B )
2 1 3ad2ant3
 |-  ( ( C e. V /\ B C_ C /\ A ~<_ B ) -> E. f f : A -1-1-> B )
3 simp2
 |-  ( ( C e. V /\ B C_ C /\ A ~<_ B ) -> B C_ C )
4 reldom
 |-  Rel ~<_
5 4 brrelex1i
 |-  ( A ~<_ B -> A e. _V )
6 5 3ad2ant3
 |-  ( ( C e. V /\ B C_ C /\ A ~<_ B ) -> A e. _V )
7 simp1
 |-  ( ( C e. V /\ B C_ C /\ A ~<_ B ) -> C e. V )
8 3 6 7 jca32
 |-  ( ( C e. V /\ B C_ C /\ A ~<_ B ) -> ( B C_ C /\ ( A e. _V /\ C e. V ) ) )
9 f1ss
 |-  ( ( f : A -1-1-> B /\ B C_ C ) -> f : A -1-1-> C )
10 vex
 |-  f e. _V
11 f1dom4g
 |-  ( ( ( f e. _V /\ A e. _V /\ C e. V ) /\ f : A -1-1-> C ) -> A ~<_ C )
12 10 11 mp3anl1
 |-  ( ( ( A e. _V /\ C e. V ) /\ f : A -1-1-> C ) -> A ~<_ C )
13 12 ancoms
 |-  ( ( f : A -1-1-> C /\ ( A e. _V /\ C e. V ) ) -> A ~<_ C )
14 9 13 sylan
 |-  ( ( ( f : A -1-1-> B /\ B C_ C ) /\ ( A e. _V /\ C e. V ) ) -> A ~<_ C )
15 14 expl
 |-  ( f : A -1-1-> B -> ( ( B C_ C /\ ( A e. _V /\ C e. V ) ) -> A ~<_ C ) )
16 15 exlimiv
 |-  ( E. f f : A -1-1-> B -> ( ( B C_ C /\ ( A e. _V /\ C e. V ) ) -> A ~<_ C ) )
17 2 8 16 sylc
 |-  ( ( C e. V /\ B C_ C /\ A ~<_ B ) -> A ~<_ C )