Metamath Proof Explorer


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