Theorem wdomfil

Description: Weak dominance agrees with normal for finite left sets. (Contributed by Stefan O'Rear, 28-Feb-2015) (Revised by Mario Carneiro, 5-May-2015)

	Ref	Expression
Assertion	wdomfil	|- ( X e. Fin -> ( X ~<_* Y <-> X ~<_ Y ) )

Proof

Step	Hyp	Ref	Expression
1		relwdom	|- Rel ~<_*
2	1	brrelex2i	|- ( X ~<_* Y -> Y e. _V )
3		0domg	|- ( Y e. _V -> (/) ~<_ Y )
4	2 3	syl	|- ( X ~<_* Y -> (/) ~<_ Y )
5		breq1	|- ( X = (/) -> ( X ~<_ Y <-> (/) ~<_ Y ) )
6	4 5	imbitrrid	|- ( X = (/) -> ( X ~<_* Y -> X ~<_ Y ) )
7	6	adantl	|- ( ( X e. Fin /\ X = (/) ) -> ( X ~<_* Y -> X ~<_ Y ) )
8		brwdomn0	|- ( X =/= (/) -> ( X ~<_* Y <-> E. x x : Y -onto-> X ) )
9	8	adantl	|- ( ( X e. Fin /\ X =/= (/) ) -> ( X ~<_* Y <-> E. x x : Y -onto-> X ) )
10		vex	|- x e. _V
11		fof	|- ( x : Y -onto-> X -> x : Y --> X )
12		dmfex	|- ( ( x e. _V /\ x : Y --> X ) -> Y e. _V )
13	10 11 12	sylancr	|- ( x : Y -onto-> X -> Y e. _V )
14	13	adantl	|- ( ( X e. Fin /\ x : Y -onto-> X ) -> Y e. _V )
15		simpl	|- ( ( X e. Fin /\ x : Y -onto-> X ) -> X e. Fin )
16		simpr	|- ( ( X e. Fin /\ x : Y -onto-> X ) -> x : Y -onto-> X )
17		fodomfi2	|- ( ( Y e. _V /\ X e. Fin /\ x : Y -onto-> X ) -> X ~<_ Y )
18	14 15 16 17	syl3anc	|- ( ( X e. Fin /\ x : Y -onto-> X ) -> X ~<_ Y )
19	18	ex	|- ( X e. Fin -> ( x : Y -onto-> X -> X ~<_ Y ) )
20	19	adantr	|- ( ( X e. Fin /\ X =/= (/) ) -> ( x : Y -onto-> X -> X ~<_ Y ) )
21	20	exlimdv	|- ( ( X e. Fin /\ X =/= (/) ) -> ( E. x x : Y -onto-> X -> X ~<_ Y ) )
22	9 21	sylbid	|- ( ( X e. Fin /\ X =/= (/) ) -> ( X ~<_* Y -> X ~<_ Y ) )
23	7 22	pm2.61dane	|- ( X e. Fin -> ( X ~<_* Y -> X ~<_ Y ) )
24		domwdom	|- ( X ~<_ Y -> X ~<_* Y )
25	23 24	impbid1	|- ( X e. Fin -> ( X ~<_* Y <-> X ~<_ Y ) )