Metamath Proof Explorer

Theorem dfac15

Description: Axiom of Choice equivalent: every set can be mapped one-to-one into the ordinals. (Contributed by BTernaryTau, 16-Sep-2026)

Ref Expression
Assertion dfac15 
|- ( CHOICE <-> A. x E. f f : x -1-1-> On )

Proof

Step Hyp Ref Expression
1 dfac10c 
 |-  ( CHOICE <-> A. x E. v e. On v ~~ x )
2 onss 
 |-  ( v e. On -> v C_ On )
3 ensymb 
 |-  ( v ~~ x <-> x ~~ v )
4 bren 
 |-  ( x ~~ v <-> E. f f : x -1-1-onto-> v )
5 3 4 bitri 
 |-  ( v ~~ x <-> E. f f : x -1-1-onto-> v )
6 f1of1 
 |-  ( f : x -1-1-onto-> v -> f : x -1-1-> v )
7 f1ss 
 |-  ( ( f : x -1-1-> v /\ v C_ On ) -> f : x -1-1-> On )
8 6 7 sylan 
 |-  ( ( f : x -1-1-onto-> v /\ v C_ On ) -> f : x -1-1-> On )
9 8 expcom 
 |-  ( v C_ On -> ( f : x -1-1-onto-> v -> f : x -1-1-> On ) )
10 9 eximdv 
 |-  ( v C_ On -> ( E. f f : x -1-1-onto-> v -> E. f f : x -1-1-> On ) )
11 5 10 biimtrid 
 |-  ( v C_ On -> ( v ~~ x -> E. f f : x -1-1-> On ) )
12 2 11 syl 
 |-  ( v e. On -> ( v ~~ x -> E. f f : x -1-1-> On ) )
13 12 rexlimiv 
 |-  ( E. v e. On v ~~ x -> E. f f : x -1-1-> On )
14 13 alimi 
 |-  ( A. x E. v e. On v ~~ x -> A. x E. f f : x -1-1-> On )
15 1 14 sylbi 
 |-  ( CHOICE -> A. x E. f f : x -1-1-> On )
16 eqid 
 |-  { <. y , z >. | ( f ` y ) e. ( f ` z ) } = { <. y , z >. | ( f ` y ) e. ( f ` z ) }
17 16 onf1we 
 |-  ( f : x -1-1-> On -> { <. y , z >. | ( f ` y ) e. ( f ` z ) } We x )
18 weinxp 
 |-  ( { <. y , z >. | ( f ` y ) e. ( f ` z ) } We x <-> ( { <. y , z >. | ( f ` y ) e. ( f ` z ) } i^i ( x X. x ) ) We x )
19 vex 
 |-  x e. _V
20 19 19 xpex 
 |-  ( x X. x ) e. _V
21 20 inex2 
 |-  ( { <. y , z >. | ( f ` y ) e. ( f ` z ) } i^i ( x X. x ) ) e. _V
22 weeq1 
 |-  ( w = ( { <. y , z >. | ( f ` y ) e. ( f ` z ) } i^i ( x X. x ) ) -> ( w We x <-> ( { <. y , z >. | ( f ` y ) e. ( f ` z ) } i^i ( x X. x ) ) We x ) )
23 21 22 spcev 
 |-  ( ( { <. y , z >. | ( f ` y ) e. ( f ` z ) } i^i ( x X. x ) ) We x -> E. w w We x )
24 18 23 sylbi 
 |-  ( { <. y , z >. | ( f ` y ) e. ( f ` z ) } We x -> E. w w We x )
25 17 24 syl 
 |-  ( f : x -1-1-> On -> E. w w We x )
26 25 exlimiv 
 |-  ( E. f f : x -1-1-> On -> E. w w We x )
27 26 alimi 
 |-  ( A. x E. f f : x -1-1-> On -> A. x E. w w We x )
28 dfac8 
 |-  ( CHOICE <-> A. x E. w w We x )
29 27 28 sylibr 
 |-  ( A. x E. f f : x -1-1-> On -> CHOICE )
30 15 29 impbii 
 |-  ( CHOICE <-> A. x E. f f : x -1-1-> On )