Metamath Proof Explorer

Theorem wevgblacfn

Description: If R is a well-ordering of the universe, then F is a global choice function. Here F maps each set z to its minimal element with respect to R (except when z is the empty set, in which case it is mapped to the empty set, though this is only done for convenience). (Contributed by BTernaryTau, 29-Jun-2025)

Ref Expression
Hypothesis wevgblacfn.1 
|- F = ( z e. _V |-> U. { y e. z | A. x e. z -. x R y } )
Assertion wevgblacfn 
|- ( R We _V -> ( F Fn _V /\ A. z ( z =/= (/) -> ( F ` z ) e. z ) ) )

Proof

Step Hyp Ref Expression
1 wevgblacfn.1 
 |-  F = ( z e. _V |-> U. { y e. z | A. x e. z -. x R y } )
2 eleq2 
 |-  ( z = (/) -> ( y e. z <-> y e. (/) ) )
3 raleq 
 |-  ( z = (/) -> ( A. x e. z -. x R y <-> A. x e. (/) -. x R y ) )
4 2 3 anbi12d 
 |-  ( z = (/) -> ( ( y e. z /\ A. x e. z -. x R y ) <-> ( y e. (/) /\ A. x e. (/) -. x R y ) ) )
5 4 rabbidva2 
 |-  ( z = (/) -> { y e. z | A. x e. z -. x R y } = { y e. (/) | A. x e. (/) -. x R y } )
6 5 unieqd 
 |-  ( z = (/) -> U. { y e. z | A. x e. z -. x R y } = U. { y e. (/) | A. x e. (/) -. x R y } )
7 rab0 
 |-  { y e. (/) | A. x e. (/) -. x R y } = (/)
8 7 unieqi 
 |-  U. { y e. (/) | A. x e. (/) -. x R y } = U. (/)
9 uni0 
 |-  U. (/) = (/)
10 8 9 eqtri 
 |-  U. { y e. (/) | A. x e. (/) -. x R y } = (/)
11 6 10 eqtrdi 
 |-  ( z = (/) -> U. { y e. z | A. x e. z -. x R y } = (/) )
12 0ex 
 |-  (/) e. _V
13 11 12 eqeltrdi 
 |-  ( z = (/) -> U. { y e. z | A. x e. z -. x R y } e. _V )
14 13 adantl 
 |-  ( ( R We _V /\ z = (/) ) -> U. { y e. z | A. x e. z -. x R y } e. _V )
15 ssv 
 |-  z C_ _V
16 15 jctl 
 |-  ( z =/= (/) -> ( z C_ _V /\ z =/= (/) ) )
17 vex 
 |-  z e. _V
18 16 17 jctil 
 |-  ( z =/= (/) -> ( z e. _V /\ ( z C_ _V /\ z =/= (/) ) ) )
19 3anass 
 |-  ( ( z e. _V /\ z C_ _V /\ z =/= (/) ) <-> ( z e. _V /\ ( z C_ _V /\ z =/= (/) ) ) )
20 18 19 sylibr 
 |-  ( z =/= (/) -> ( z e. _V /\ z C_ _V /\ z =/= (/) ) )
21 wereu 
 |-  ( ( R We _V /\ ( z e. _V /\ z C_ _V /\ z =/= (/) ) ) -> E! y e. z A. x e. z -. x R y )
22 20 21 sylan2 
 |-  ( ( R We _V /\ z =/= (/) ) -> E! y e. z A. x e. z -. x R y )
23 vsnid 
 |-  w e. { w }
24 eleq2 
 |-  ( { y e. z | A. x e. z -. x R y } = { w } -> ( w e. { y e. z | A. x e. z -. x R y } <-> w e. { w } ) )
25 23 24 mpbiri 
 |-  ( { y e. z | A. x e. z -. x R y } = { w } -> w e. { y e. z | A. x e. z -. x R y } )
26 elrabi 
 |-  ( w e. { y e. z | A. x e. z -. x R y } -> w e. z )
27 25 26 syl 
 |-  ( { y e. z | A. x e. z -. x R y } = { w } -> w e. z )
28 unieq 
 |-  ( { y e. z | A. x e. z -. x R y } = { w } -> U. { y e. z | A. x e. z -. x R y } = U. { w } )
29 unisnv 
 |-  U. { w } = w
30 28 29 eqtrdi 
 |-  ( { y e. z | A. x e. z -. x R y } = { w } -> U. { y e. z | A. x e. z -. x R y } = w )
31 27 30 jca 
 |-  ( { y e. z | A. x e. z -. x R y } = { w } -> ( w e. z /\ U. { y e. z | A. x e. z -. x R y } = w ) )
32 31 eximi 
 |-  ( E. w { y e. z | A. x e. z -. x R y } = { w } -> E. w ( w e. z /\ U. { y e. z | A. x e. z -. x R y } = w ) )
33 reusn 
 |-  ( E! y e. z A. x e. z -. x R y <-> E. w { y e. z | A. x e. z -. x R y } = { w } )
34 df-rex 
 |-  ( E. w e. z U. { y e. z | A. x e. z -. x R y } = w <-> E. w ( w e. z /\ U. { y e. z | A. x e. z -. x R y } = w ) )
35 32 33 34 3imtr4i 
 |-  ( E! y e. z A. x e. z -. x R y -> E. w e. z U. { y e. z | A. x e. z -. x R y } = w )
36 22 35 syl 
 |-  ( ( R We _V /\ z =/= (/) ) -> E. w e. z U. { y e. z | A. x e. z -. x R y } = w )
37 eleq1 
 |-  ( U. { y e. z | A. x e. z -. x R y } = w -> ( U. { y e. z | A. x e. z -. x R y } e. z <-> w e. z ) )
38 37 biimparc 
 |-  ( ( w e. z /\ U. { y e. z | A. x e. z -. x R y } = w ) -> U. { y e. z | A. x e. z -. x R y } e. z )
39 38 rexlimiva 
 |-  ( E. w e. z U. { y e. z | A. x e. z -. x R y } = w -> U. { y e. z | A. x e. z -. x R y } e. z )
40 36 39 syl 
 |-  ( ( R We _V /\ z =/= (/) ) -> U. { y e. z | A. x e. z -. x R y } e. z )
41 40 elexd 
 |-  ( ( R We _V /\ z =/= (/) ) -> U. { y e. z | A. x e. z -. x R y } e. _V )
42 14 41 pm2.61dane 
 |-  ( R We _V -> U. { y e. z | A. x e. z -. x R y } e. _V )
43 42 ralrimivw 
 |-  ( R We _V -> A. z e. _V U. { y e. z | A. x e. z -. x R y } e. _V )
44 1 fnmpt 
 |-  ( A. z e. _V U. { y e. z | A. x e. z -. x R y } e. _V -> F Fn _V )
45 43 44 syl 
 |-  ( R We _V -> F Fn _V )
46 1 fvmpt2 
 |-  ( ( z e. _V /\ U. { y e. z | A. x e. z -. x R y } e. z ) -> ( F ` z ) = U. { y e. z | A. x e. z -. x R y } )
47 17 40 46 sylancr 
 |-  ( ( R We _V /\ z =/= (/) ) -> ( F ` z ) = U. { y e. z | A. x e. z -. x R y } )
48 47 40 eqeltrd 
 |-  ( ( R We _V /\ z =/= (/) ) -> ( F ` z ) e. z )
49 48 ex 
 |-  ( R We _V -> ( z =/= (/) -> ( F ` z ) e. z ) )
50 49 alrimiv 
 |-  ( R We _V -> A. z ( z =/= (/) -> ( F ` z ) e. z ) )
51 45 50 jca 
 |-  ( R We _V -> ( F Fn _V /\ A. z ( z =/= (/) -> ( F ` z ) e. z ) ) )