Metamath Proof Explorer

Theorem brwdom2

Description: Alternate characterization of the weak dominance predicate which does not require special treatment of the empty set. (Contributed by Stefan O'Rear, 11-Feb-2015)

Ref Expression
Assertion brwdom2 
|- ( Y e. V -> ( X ~<_* Y <-> E. y e. ~P Y E. z z : y -onto-> X ) )

Proof

Step Hyp Ref Expression
1 elex 
 |-  ( Y e. V -> Y e. _V )
2 0wdom 
 |-  ( Y e. _V -> (/) ~<_* Y )
3 breq1 
 |-  ( X = (/) -> ( X ~<_* Y <-> (/) ~<_* Y ) )
4 2 3 syl5ibrcom 
 |-  ( Y e. _V -> ( X = (/) -> X ~<_* Y ) )
5 4 imp 
 |-  ( ( Y e. _V /\ X = (/) ) -> X ~<_* Y )
6 0elpw 
 |-  (/) e. ~P Y
7 f1o0 
 |-  (/) : (/) -1-1-onto-> (/)
8 f1ofo 
 |-  ( (/) : (/) -1-1-onto-> (/) -> (/) : (/) -onto-> (/) )
9 0ex 
 |-  (/) e. _V
10 foeq1 
 |-  ( z = (/) -> ( z : (/) -onto-> (/) <-> (/) : (/) -onto-> (/) ) )
11 9 10 spcev 
 |-  ( (/) : (/) -onto-> (/) -> E. z z : (/) -onto-> (/) )
12 7 8 11 mp2b 
 |-  E. z z : (/) -onto-> (/)
13 foeq2 
 |-  ( y = (/) -> ( z : y -onto-> (/) <-> z : (/) -onto-> (/) ) )
14 13 exbidv 
 |-  ( y = (/) -> ( E. z z : y -onto-> (/) <-> E. z z : (/) -onto-> (/) ) )
15 14 rspcev 
 |-  ( ( (/) e. ~P Y /\ E. z z : (/) -onto-> (/) ) -> E. y e. ~P Y E. z z : y -onto-> (/) )
16 6 12 15 mp2an 
 |-  E. y e. ~P Y E. z z : y -onto-> (/)
17 foeq3 
 |-  ( X = (/) -> ( z : y -onto-> X <-> z : y -onto-> (/) ) )
18 17 exbidv 
 |-  ( X = (/) -> ( E. z z : y -onto-> X <-> E. z z : y -onto-> (/) ) )
19 18 rexbidv 
 |-  ( X = (/) -> ( E. y e. ~P Y E. z z : y -onto-> X <-> E. y e. ~P Y E. z z : y -onto-> (/) ) )
20 16 19 mpbiri 
 |-  ( X = (/) -> E. y e. ~P Y E. z z : y -onto-> X )
21 20 adantl 
 |-  ( ( Y e. _V /\ X = (/) ) -> E. y e. ~P Y E. z z : y -onto-> X )
22 5 21 2thd 
 |-  ( ( Y e. _V /\ X = (/) ) -> ( X ~<_* Y <-> E. y e. ~P Y E. z z : y -onto-> X ) )
23 brwdomn0 
 |-  ( X =/= (/) -> ( X ~<_* Y <-> E. x x : Y -onto-> X ) )
24 23 adantl 
 |-  ( ( Y e. _V /\ X =/= (/) ) -> ( X ~<_* Y <-> E. x x : Y -onto-> X ) )
25 foeq1 
 |-  ( x = z -> ( x : Y -onto-> X <-> z : Y -onto-> X ) )
26 25 cbvexvw 
 |-  ( E. x x : Y -onto-> X <-> E. z z : Y -onto-> X )
27 pwidg 
 |-  ( Y e. _V -> Y e. ~P Y )
28 27 ad2antrr 
 |-  ( ( ( Y e. _V /\ X =/= (/) ) /\ E. z z : Y -onto-> X ) -> Y e. ~P Y )
29 foeq2 
 |-  ( y = Y -> ( z : y -onto-> X <-> z : Y -onto-> X ) )
30 29 exbidv 
 |-  ( y = Y -> ( E. z z : y -onto-> X <-> E. z z : Y -onto-> X ) )
31 30 rspcev 
 |-  ( ( Y e. ~P Y /\ E. z z : Y -onto-> X ) -> E. y e. ~P Y E. z z : y -onto-> X )
32 28 31 sylancom 
 |-  ( ( ( Y e. _V /\ X =/= (/) ) /\ E. z z : Y -onto-> X ) -> E. y e. ~P Y E. z z : y -onto-> X )
33 32 ex 
 |-  ( ( Y e. _V /\ X =/= (/) ) -> ( E. z z : Y -onto-> X -> E. y e. ~P Y E. z z : y -onto-> X ) )
34 26 33 syl5bi 
 |-  ( ( Y e. _V /\ X =/= (/) ) -> ( E. x x : Y -onto-> X -> E. y e. ~P Y E. z z : y -onto-> X ) )
35 n0 
 |-  ( X =/= (/) <-> E. w w e. X )
36 35 biimpi 
 |-  ( X =/= (/) -> E. w w e. X )
37 36 ad2antlr 
 |-  ( ( ( Y e. _V /\ X =/= (/) ) /\ ( y e. ~P Y /\ z : y -onto-> X ) ) -> E. w w e. X )
38 vex 
 |-  z e. _V
39 difexg 
 |-  ( Y e. _V -> ( Y \ y ) e. _V )
40 snex 
 |-  { w } e. _V
41 xpexg 
 |-  ( ( ( Y \ y ) e. _V /\ { w } e. _V ) -> ( ( Y \ y ) X. { w } ) e. _V )
42 39 40 41 sylancl 
 |-  ( Y e. _V -> ( ( Y \ y ) X. { w } ) e. _V )
43 unexg 
 |-  ( ( z e. _V /\ ( ( Y \ y ) X. { w } ) e. _V ) -> ( z u. ( ( Y \ y ) X. { w } ) ) e. _V )
44 38 42 43 sylancr 
 |-  ( Y e. _V -> ( z u. ( ( Y \ y ) X. { w } ) ) e. _V )
45 44 adantr 
 |-  ( ( Y e. _V /\ X =/= (/) ) -> ( z u. ( ( Y \ y ) X. { w } ) ) e. _V )
46 45 ad2antrr 
 |-  ( ( ( ( Y e. _V /\ X =/= (/) ) /\ ( y e. ~P Y /\ z : y -onto-> X ) ) /\ w e. X ) -> ( z u. ( ( Y \ y ) X. { w } ) ) e. _V )
47 fofn 
 |-  ( z : y -onto-> X -> z Fn y )
48 47 adantl 
 |-  ( ( y e. ~P Y /\ z : y -onto-> X ) -> z Fn y )
49 48 ad2antlr 
 |-  ( ( ( ( Y e. _V /\ X =/= (/) ) /\ ( y e. ~P Y /\ z : y -onto-> X ) ) /\ w e. X ) -> z Fn y )
50 vex 
 |-  w e. _V
51 fnconstg 
 |-  ( w e. _V -> ( ( Y \ y ) X. { w } ) Fn ( Y \ y ) )
52 50 51 mp1i 
 |-  ( ( ( ( Y e. _V /\ X =/= (/) ) /\ ( y e. ~P Y /\ z : y -onto-> X ) ) /\ w e. X ) -> ( ( Y \ y ) X. { w } ) Fn ( Y \ y ) )
53 disjdif 
 |-  ( y i^i ( Y \ y ) ) = (/)
54 53 a1i 
 |-  ( ( ( ( Y e. _V /\ X =/= (/) ) /\ ( y e. ~P Y /\ z : y -onto-> X ) ) /\ w e. X ) -> ( y i^i ( Y \ y ) ) = (/) )
55 49 52 54 fnund 
 |-  ( ( ( ( Y e. _V /\ X =/= (/) ) /\ ( y e. ~P Y /\ z : y -onto-> X ) ) /\ w e. X ) -> ( z u. ( ( Y \ y ) X. { w } ) ) Fn ( y u. ( Y \ y ) ) )
56 elpwi 
 |-  ( y e. ~P Y -> y C_ Y )
57 undif 
 |-  ( y C_ Y <-> ( y u. ( Y \ y ) ) = Y )
58 56 57 sylib 
 |-  ( y e. ~P Y -> ( y u. ( Y \ y ) ) = Y )
59 58 ad2antrl 
 |-  ( ( ( Y e. _V /\ X =/= (/) ) /\ ( y e. ~P Y /\ z : y -onto-> X ) ) -> ( y u. ( Y \ y ) ) = Y )
60 59 adantr 
 |-  ( ( ( ( Y e. _V /\ X =/= (/) ) /\ ( y e. ~P Y /\ z : y -onto-> X ) ) /\ w e. X ) -> ( y u. ( Y \ y ) ) = Y )
61 60 fneq2d 
 |-  ( ( ( ( Y e. _V /\ X =/= (/) ) /\ ( y e. ~P Y /\ z : y -onto-> X ) ) /\ w e. X ) -> ( ( z u. ( ( Y \ y ) X. { w } ) ) Fn ( y u. ( Y \ y ) ) <-> ( z u. ( ( Y \ y ) X. { w } ) ) Fn Y ) )
62 55 61 mpbid 
 |-  ( ( ( ( Y e. _V /\ X =/= (/) ) /\ ( y e. ~P Y /\ z : y -onto-> X ) ) /\ w e. X ) -> ( z u. ( ( Y \ y ) X. { w } ) ) Fn Y )
63 rnun 
 |-  ran ( z u. ( ( Y \ y ) X. { w } ) ) = ( ran z u. ran ( ( Y \ y ) X. { w } ) )
64 forn 
 |-  ( z : y -onto-> X -> ran z = X )
65 64 ad2antll 
 |-  ( ( ( Y e. _V /\ X =/= (/) ) /\ ( y e. ~P Y /\ z : y -onto-> X ) ) -> ran z = X )
66 65 adantr 
 |-  ( ( ( ( Y e. _V /\ X =/= (/) ) /\ ( y e. ~P Y /\ z : y -onto-> X ) ) /\ w e. X ) -> ran z = X )
67 66 uneq1d 
 |-  ( ( ( ( Y e. _V /\ X =/= (/) ) /\ ( y e. ~P Y /\ z : y -onto-> X ) ) /\ w e. X ) -> ( ran z u. ran ( ( Y \ y ) X. { w } ) ) = ( X u. ran ( ( Y \ y ) X. { w } ) ) )
68 fconst6g 
 |-  ( w e. X -> ( ( Y \ y ) X. { w } ) : ( Y \ y ) --> X )
69 68 frnd 
 |-  ( w e. X -> ran ( ( Y \ y ) X. { w } ) C_ X )
70 69 adantl 
 |-  ( ( ( ( Y e. _V /\ X =/= (/) ) /\ ( y e. ~P Y /\ z : y -onto-> X ) ) /\ w e. X ) -> ran ( ( Y \ y ) X. { w } ) C_ X )
71 ssequn2 
 |-  ( ran ( ( Y \ y ) X. { w } ) C_ X <-> ( X u. ran ( ( Y \ y ) X. { w } ) ) = X )
72 70 71 sylib 
 |-  ( ( ( ( Y e. _V /\ X =/= (/) ) /\ ( y e. ~P Y /\ z : y -onto-> X ) ) /\ w e. X ) -> ( X u. ran ( ( Y \ y ) X. { w } ) ) = X )
73 67 72 eqtrd 
 |-  ( ( ( ( Y e. _V /\ X =/= (/) ) /\ ( y e. ~P Y /\ z : y -onto-> X ) ) /\ w e. X ) -> ( ran z u. ran ( ( Y \ y ) X. { w } ) ) = X )
74 63 73 eqtrid 
 |-  ( ( ( ( Y e. _V /\ X =/= (/) ) /\ ( y e. ~P Y /\ z : y -onto-> X ) ) /\ w e. X ) -> ran ( z u. ( ( Y \ y ) X. { w } ) ) = X )
75 df-fo 
 |-  ( ( z u. ( ( Y \ y ) X. { w } ) ) : Y -onto-> X <-> ( ( z u. ( ( Y \ y ) X. { w } ) ) Fn Y /\ ran ( z u. ( ( Y \ y ) X. { w } ) ) = X ) )
76 62 74 75 sylanbrc 
 |-  ( ( ( ( Y e. _V /\ X =/= (/) ) /\ ( y e. ~P Y /\ z : y -onto-> X ) ) /\ w e. X ) -> ( z u. ( ( Y \ y ) X. { w } ) ) : Y -onto-> X )
77 foeq1 
 |-  ( x = ( z u. ( ( Y \ y ) X. { w } ) ) -> ( x : Y -onto-> X <-> ( z u. ( ( Y \ y ) X. { w } ) ) : Y -onto-> X ) )
78 46 76 77 spcedv 
 |-  ( ( ( ( Y e. _V /\ X =/= (/) ) /\ ( y e. ~P Y /\ z : y -onto-> X ) ) /\ w e. X ) -> E. x x : Y -onto-> X )
79 37 78 exlimddv 
 |-  ( ( ( Y e. _V /\ X =/= (/) ) /\ ( y e. ~P Y /\ z : y -onto-> X ) ) -> E. x x : Y -onto-> X )
80 79 expr 
 |-  ( ( ( Y e. _V /\ X =/= (/) ) /\ y e. ~P Y ) -> ( z : y -onto-> X -> E. x x : Y -onto-> X ) )
81 80 exlimdv 
 |-  ( ( ( Y e. _V /\ X =/= (/) ) /\ y e. ~P Y ) -> ( E. z z : y -onto-> X -> E. x x : Y -onto-> X ) )
82 81 rexlimdva 
 |-  ( ( Y e. _V /\ X =/= (/) ) -> ( E. y e. ~P Y E. z z : y -onto-> X -> E. x x : Y -onto-> X ) )
83 34 82 impbid 
 |-  ( ( Y e. _V /\ X =/= (/) ) -> ( E. x x : Y -onto-> X <-> E. y e. ~P Y E. z z : y -onto-> X ) )
84 24 83 bitrd 
 |-  ( ( Y e. _V /\ X =/= (/) ) -> ( X ~<_* Y <-> E. y e. ~P Y E. z z : y -onto-> X ) )
85 22 84 pm2.61dane 
 |-  ( Y e. _V -> ( X ~<_* Y <-> E. y e. ~P Y E. z z : y -onto-> X ) )
86 1 85 syl 
 |-  ( Y e. V -> ( X ~<_* Y <-> E. y e. ~P Y E. z z : y -onto-> X ) )