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 ) )