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

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