Metamath Proof Explorer

Theorem brwdom3

Description: Condition for weak dominance with a condition reminiscent of wdomd . (Contributed by Stefan O'Rear, 13-Feb-2015) (Revised by Mario Carneiro, 25-Jun-2015)

Ref Expression
Assertion brwdom3 
|- ( ( X e. V /\ Y e. W ) -> ( X ~<_* Y <-> E. f A. x e. X E. y e. Y x = ( f ` y ) ) )

Proof

Step Hyp Ref Expression
1 elex 
 |-  ( X e. V -> X e. _V )
2 elex 
 |-  ( Y e. W -> Y e. _V )
3 brwdom2 
 |-  ( Y e. _V -> ( X ~<_* Y <-> E. z e. ~P Y E. f f : z -onto-> X ) )
4 3 adantl 
 |-  ( ( X e. _V /\ Y e. _V ) -> ( X ~<_* Y <-> E. z e. ~P Y E. f f : z -onto-> X ) )
5 dffo3 
 |-  ( f : z -onto-> X <-> ( f : z --> X /\ A. x e. X E. y e. z x = ( f ` y ) ) )
6 5 simprbi 
 |-  ( f : z -onto-> X -> A. x e. X E. y e. z x = ( f ` y ) )
7 elpwi 
 |-  ( z e. ~P Y -> z C_ Y )
8 ssrexv 
 |-  ( z C_ Y -> ( E. y e. z x = ( f ` y ) -> E. y e. Y x = ( f ` y ) ) )
9 7 8 syl 
 |-  ( z e. ~P Y -> ( E. y e. z x = ( f ` y ) -> E. y e. Y x = ( f ` y ) ) )
10 9 adantl 
 |-  ( ( ( X e. _V /\ Y e. _V ) /\ z e. ~P Y ) -> ( E. y e. z x = ( f ` y ) -> E. y e. Y x = ( f ` y ) ) )
11 10 ralimdv 
 |-  ( ( ( X e. _V /\ Y e. _V ) /\ z e. ~P Y ) -> ( A. x e. X E. y e. z x = ( f ` y ) -> A. x e. X E. y e. Y x = ( f ` y ) ) )
12 6 11 syl5 
 |-  ( ( ( X e. _V /\ Y e. _V ) /\ z e. ~P Y ) -> ( f : z -onto-> X -> A. x e. X E. y e. Y x = ( f ` y ) ) )
13 12 eximdv 
 |-  ( ( ( X e. _V /\ Y e. _V ) /\ z e. ~P Y ) -> ( E. f f : z -onto-> X -> E. f A. x e. X E. y e. Y x = ( f ` y ) ) )
14 13 rexlimdva 
 |-  ( ( X e. _V /\ Y e. _V ) -> ( E. z e. ~P Y E. f f : z -onto-> X -> E. f A. x e. X E. y e. Y x = ( f ` y ) ) )
15 4 14 sylbid 
 |-  ( ( X e. _V /\ Y e. _V ) -> ( X ~<_* Y -> E. f A. x e. X E. y e. Y x = ( f ` y ) ) )
16 simpll 
 |-  ( ( ( X e. _V /\ Y e. _V ) /\ A. x e. X E. y e. Y x = ( f ` y ) ) -> X e. _V )
17 simplr 
 |-  ( ( ( X e. _V /\ Y e. _V ) /\ A. x e. X E. y e. Y x = ( f ` y ) ) -> Y e. _V )
18 eqeq1 
 |-  ( x = z -> ( x = ( f ` y ) <-> z = ( f ` y ) ) )
19 18 rexbidv 
 |-  ( x = z -> ( E. y e. Y x = ( f ` y ) <-> E. y e. Y z = ( f ` y ) ) )
20 fveq2 
 |-  ( y = w -> ( f ` y ) = ( f ` w ) )
21 20 eqeq2d 
 |-  ( y = w -> ( z = ( f ` y ) <-> z = ( f ` w ) ) )
22 21 cbvrexvw 
 |-  ( E. y e. Y z = ( f ` y ) <-> E. w e. Y z = ( f ` w ) )
23 19 22 bitrdi 
 |-  ( x = z -> ( E. y e. Y x = ( f ` y ) <-> E. w e. Y z = ( f ` w ) ) )
24 23 cbvralvw 
 |-  ( A. x e. X E. y e. Y x = ( f ` y ) <-> A. z e. X E. w e. Y z = ( f ` w ) )
25 24 biimpi 
 |-  ( A. x e. X E. y e. Y x = ( f ` y ) -> A. z e. X E. w e. Y z = ( f ` w ) )
26 25 adantl 
 |-  ( ( ( X e. _V /\ Y e. _V ) /\ A. x e. X E. y e. Y x = ( f ` y ) ) -> A. z e. X E. w e. Y z = ( f ` w ) )
27 26 r19.21bi 
 |-  ( ( ( ( X e. _V /\ Y e. _V ) /\ A. x e. X E. y e. Y x = ( f ` y ) ) /\ z e. X ) -> E. w e. Y z = ( f ` w ) )
28 16 17 27 wdom2d 
 |-  ( ( ( X e. _V /\ Y e. _V ) /\ A. x e. X E. y e. Y x = ( f ` y ) ) -> X ~<_* Y )
29 28 ex 
 |-  ( ( X e. _V /\ Y e. _V ) -> ( A. x e. X E. y e. Y x = ( f ` y ) -> X ~<_* Y ) )
30 29 exlimdv 
 |-  ( ( X e. _V /\ Y e. _V ) -> ( E. f A. x e. X E. y e. Y x = ( f ` y ) -> X ~<_* Y ) )
31 15 30 impbid 
 |-  ( ( X e. _V /\ Y e. _V ) -> ( X ~<_* Y <-> E. f A. x e. X E. y e. Y x = ( f ` y ) ) )
32 1 2 31 syl2an 
 |-  ( ( X e. V /\ Y e. W ) -> ( X ~<_* Y <-> E. f A. x e. X E. y e. Y x = ( f ` y ) ) )