This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )