Metamath Proof Explorer

Theorem onsdominel

Description: An ordinal with more elements of some type is larger. (Contributed by Stefan O'Rear, 2-Nov-2014)

Ref Expression
Assertion onsdominel 
|- ( ( A e. On /\ B e. On /\ ( A i^i C ) ~< ( B i^i C ) ) -> A e. B )

Proof

Step Hyp Ref Expression
1 ontri1 
 |-  ( ( B e. On /\ A e. On ) -> ( B C_ A <-> -. A e. B ) )
2 1 ancoms 
 |-  ( ( A e. On /\ B e. On ) -> ( B C_ A <-> -. A e. B ) )
3 inex1g 
 |-  ( A e. On -> ( A i^i C ) e. _V )
4 ssrin 
 |-  ( B C_ A -> ( B i^i C ) C_ ( A i^i C ) )
5 ssdomg 
 |-  ( ( A i^i C ) e. _V -> ( ( B i^i C ) C_ ( A i^i C ) -> ( B i^i C ) ~<_ ( A i^i C ) ) )
6 3 4 5 syl2im 
 |-  ( A e. On -> ( B C_ A -> ( B i^i C ) ~<_ ( A i^i C ) ) )
7 domnsym 
 |-  ( ( B i^i C ) ~<_ ( A i^i C ) -> -. ( A i^i C ) ~< ( B i^i C ) )
8 6 7 syl6 
 |-  ( A e. On -> ( B C_ A -> -. ( A i^i C ) ~< ( B i^i C ) ) )
9 8 adantr 
 |-  ( ( A e. On /\ B e. On ) -> ( B C_ A -> -. ( A i^i C ) ~< ( B i^i C ) ) )
10 2 9 sylbird 
 |-  ( ( A e. On /\ B e. On ) -> ( -. A e. B -> -. ( A i^i C ) ~< ( B i^i C ) ) )
11 10 con4d 
 |-  ( ( A e. On /\ B e. On ) -> ( ( A i^i C ) ~< ( B i^i C ) -> A e. B ) )
12 11 3impia 
 |-  ( ( A e. On /\ B e. On /\ ( A i^i C ) ~< ( B i^i C ) ) -> A e. B )