Theorem domwdom

Description: Weak dominance is implied by dominance in the usual sense. (Contributed by Stefan O'Rear, 11-Feb-2015)

	Ref	Expression
Assertion	domwdom	|- ( X ~<_ Y -> X ~<_* Y )

Proof

Step	Hyp	Ref	Expression
1		neqne	|- ( -. X = (/) -> X =/= (/) )
2	1	adantl	|- ( ( X ~<_ Y /\ -. X = (/) ) -> X =/= (/) )
3		reldom	|- Rel ~<_
4	3	brrelex1i	|- ( X ~<_ Y -> X e. _V )
5		0sdomg	|- ( X e. _V -> ( (/) ~< X <-> X =/= (/) ) )
6	4 5	syl	|- ( X ~<_ Y -> ( (/) ~< X <-> X =/= (/) ) )
7	6	adantr	|- ( ( X ~<_ Y /\ -. X = (/) ) -> ( (/) ~< X <-> X =/= (/) ) )
8	2 7	mpbird	|- ( ( X ~<_ Y /\ -. X = (/) ) -> (/) ~< X )
9		simpl	|- ( ( X ~<_ Y /\ -. X = (/) ) -> X ~<_ Y )
10		fodomr	|- ( ( (/) ~< X /\ X ~<_ Y ) -> E. y y : Y -onto-> X )
11	8 9 10	syl2anc	|- ( ( X ~<_ Y /\ -. X = (/) ) -> E. y y : Y -onto-> X )
12	11	ex	|- ( X ~<_ Y -> ( -. X = (/) -> E. y y : Y -onto-> X ) )
13	12	orrd	|- ( X ~<_ Y -> ( X = (/) \/ E. y y : Y -onto-> X ) )
14	3	brrelex2i	|- ( X ~<_ Y -> Y e. _V )
15		brwdom	|- ( Y e. _V -> ( X ~<_* Y <-> ( X = (/) \/ E. y y : Y -onto-> X ) ) )
16	14 15	syl	|- ( X ~<_ Y -> ( X ~<_* Y <-> ( X = (/) \/ E. y y : Y -onto-> X ) ) )
17	13 16	mpbird	|- ( X ~<_ Y -> X ~<_* Y )