Description: If F is a bijection from the universe to the ordinals, then R well-orders the universe. This is the ZFC version of (2 -> 3) in https://tinyurl.com/hamkins-gblac . (Contributed by BTernaryTau, 6-Dec-2025) (Proof shortened by BTernaryTau, 11-Jun-2026)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | vonf1owev.1 | |- R = { <. x , y >. | ( F ` x ) e. ( F ` y ) } |
|
| Assertion | vonf1owev | |- ( F : _V -1-1-onto-> On -> R We _V ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | vonf1owev.1 | |- R = { <. x , y >. | ( F ` x ) e. ( F ` y ) } |
|
| 2 | f1of1 | |- ( F : _V -1-1-onto-> On -> F : _V -1-1-> On ) |
|
| 3 | 1 | vonf1wev | |- ( F : _V -1-1-> On -> R We _V ) |
| 4 | 2 3 | syl | |- ( F : _V -1-1-onto-> On -> R We _V ) |