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

Metamath Proof Explorer

Theorem harword

Description: Weak ordering property of the Hartogs function. (Contributed by Stefan O'Rear, 14-Feb-2015)

Ref Expression
Assertion harword 
|- ( X ~<_ Y -> ( har ` X ) C_ ( har ` Y ) )

Proof

Step Hyp Ref Expression
1 domtr 
 |-  ( ( y ~<_ X /\ X ~<_ Y ) -> y ~<_ Y )
2 1 expcom 
 |-  ( X ~<_ Y -> ( y ~<_ X -> y ~<_ Y ) )
3 2 adantr 
 |-  ( ( X ~<_ Y /\ y e. On ) -> ( y ~<_ X -> y ~<_ Y ) )
4 3 ss2rabdv 
 |-  ( X ~<_ Y -> { y e. On | y ~<_ X } C_ { y e. On | y ~<_ Y } )
5 reldom 
 |-  Rel ~<_
6 5 brrelex1i 
 |-  ( X ~<_ Y -> X e. _V )
7 harval 
 |-  ( X e. _V -> ( har ` X ) = { y e. On | y ~<_ X } )
8 6 7 syl 
 |-  ( X ~<_ Y -> ( har ` X ) = { y e. On | y ~<_ X } )
9 5 brrelex2i 
 |-  ( X ~<_ Y -> Y e. _V )
10 harval 
 |-  ( Y e. _V -> ( har ` Y ) = { y e. On | y ~<_ Y } )
11 9 10 syl 
 |-  ( X ~<_ Y -> ( har ` Y ) = { y e. On | y ~<_ Y } )
12 4 8 11 3sstr4d 
 |-  ( X ~<_ Y -> ( har ` X ) C_ ( har ` Y ) )