Metamath Proof Explorer

Theorem vonf1onprcf1ac

Description: If F maps the universe one-to-one into the ordinals and A is a proper class, then I maps the ordinals one-to-one into A and the Axiom of Choice holds. This is the ZFC version of (6 -> 7) in https://tinyurl.com/hamkins-gblac . Note that in NBG set theory the first hypothesis would be something like ph -> A. X E. F F : X -1-1-> On , but since we cannot quantify over classes, we instead consider only the case X = _V which is sufficient for this proof. (Contributed by BTernaryTau, 22-Jun-2026)

Ref Expression
Hypotheses vonf1onprcf1ac.1 
|- ( ph -> F : _V -1-1-> On )
vonf1onprcf1ac.2 
|- ( ph -> -. A e. _V )
vonf1onprcf1ac.3 
|- I = ( `' ( F |` A ) o. H )
vonf1onprcf1ac.4 
|- H = OrdIso ( _E , ( F " A ) )
Assertion vonf1onprcf1ac 
|- ( ph -> ( I : On -1-1-> A /\ CHOICE ) )

Proof

Step Hyp Ref Expression
1 vonf1onprcf1ac.1 
 |-  ( ph -> F : _V -1-1-> On )
2 vonf1onprcf1ac.2 
 |-  ( ph -> -. A e. _V )
3 vonf1onprcf1ac.3 
 |-  I = ( `' ( F |` A ) o. H )
4 vonf1onprcf1ac.4 
 |-  H = OrdIso ( _E , ( F " A ) )
5 ssv 
 |-  A C_ _V
6 f1ores 
 |-  ( ( F : _V -1-1-> On /\ A C_ _V ) -> ( F |` A ) : A -1-1-onto-> ( F " A ) )
7 1 5 6 sylancl 
 |-  ( ph -> ( F |` A ) : A -1-1-onto-> ( F " A ) )
8 f1ocnv 
 |-  ( ( F |` A ) : A -1-1-onto-> ( F " A ) -> `' ( F |` A ) : ( F " A ) -1-1-onto-> A )
9 7 8 syl 
 |-  ( ph -> `' ( F |` A ) : ( F " A ) -1-1-onto-> A )
10 f1f 
 |-  ( F : _V -1-1-> On -> F : _V --> On )
11 1 10 syl 
 |-  ( ph -> F : _V --> On )
12 11 fimassd 
 |-  ( ph -> ( F " A ) C_ On )
13 f1preimaex 
 |-  ( ( F : _V -1-1-> On /\ A C_ _V /\ ( F " A ) e. _V ) -> A e. _V )
14 5 13 mp3an2 
 |-  ( ( F : _V -1-1-> On /\ ( F " A ) e. _V ) -> A e. _V )
15 14 ex 
 |-  ( F : _V -1-1-> On -> ( ( F " A ) e. _V -> A e. _V ) )
16 1 15 syl 
 |-  ( ph -> ( ( F " A ) e. _V -> A e. _V ) )
17 2 16 mtod 
 |-  ( ph -> -. ( F " A ) e. _V )
18 epweon 
 |-  _E We On
19 wess 
 |-  ( ( F " A ) C_ On -> ( _E We On -> _E We ( F " A ) ) )
20 18 19 mpi 
 |-  ( ( F " A ) C_ On -> _E We ( F " A ) )
21 epse 
 |-  _E Se ( F " A )
22 4 ordtypeon 
 |-  ( ( _E We ( F " A ) /\ _E Se ( F " A ) /\ -. ( F " A ) e. _V ) -> H Isom _E , _E ( On , ( F " A ) ) )
23 21 22 mp3an2 
 |-  ( ( _E We ( F " A ) /\ -. ( F " A ) e. _V ) -> H Isom _E , _E ( On , ( F " A ) ) )
24 20 23 sylan 
 |-  ( ( ( F " A ) C_ On /\ -. ( F " A ) e. _V ) -> H Isom _E , _E ( On , ( F " A ) ) )
25 12 17 24 syl2anc 
 |-  ( ph -> H Isom _E , _E ( On , ( F " A ) ) )
26 isof1o 
 |-  ( H Isom _E , _E ( On , ( F " A ) ) -> H : On -1-1-onto-> ( F " A ) )
27 25 26 syl 
 |-  ( ph -> H : On -1-1-onto-> ( F " A ) )
28 f1oco 
 |-  ( ( `' ( F |` A ) : ( F " A ) -1-1-onto-> A /\ H : On -1-1-onto-> ( F " A ) ) -> ( `' ( F |` A ) o. H ) : On -1-1-onto-> A )
29 9 27 28 syl2anc 
 |-  ( ph -> ( `' ( F |` A ) o. H ) : On -1-1-onto-> A )
30 3 a1i 
 |-  ( ph -> I = ( `' ( F |` A ) o. H ) )
31 30 f1oeq1d 
 |-  ( ph -> ( I : On -1-1-onto-> A <-> ( `' ( F |` A ) o. H ) : On -1-1-onto-> A ) )
32 29 31 mpbird 
 |-  ( ph -> I : On -1-1-onto-> A )
33 f1of1 
 |-  ( I : On -1-1-onto-> A -> I : On -1-1-> A )
34 32 33 syl 
 |-  ( ph -> I : On -1-1-> A )
35 eqid 
 |-  { <. x , y >. | ( F ` x ) e. ( F ` y ) } = { <. x , y >. | ( F ` x ) e. ( F ` y ) }
36 35 vonf1wev 
 |-  ( F : _V -1-1-> On -> { <. x , y >. | ( F ` x ) e. ( F ` y ) } We _V )
37 ssv 
 |-  z C_ _V
38 wess 
 |-  ( z C_ _V -> ( { <. x , y >. | ( F ` x ) e. ( F ` y ) } We _V -> { <. x , y >. | ( F ` x ) e. ( F ` y ) } We z ) )
39 37 38 ax-mp 
 |-  ( { <. x , y >. | ( F ` x ) e. ( F ` y ) } We _V -> { <. x , y >. | ( F ` x ) e. ( F ` y ) } We z )
40 1 36 39 3syl 
 |-  ( ph -> { <. x , y >. | ( F ` x ) e. ( F ` y ) } We z )
41 weinxp 
 |-  ( { <. x , y >. | ( F ` x ) e. ( F ` y ) } We z <-> ( { <. x , y >. | ( F ` x ) e. ( F ` y ) } i^i ( z X. z ) ) We z )
42 vex 
 |-  z e. _V
43 42 42 xpex 
 |-  ( z X. z ) e. _V
44 43 inex2 
 |-  ( { <. x , y >. | ( F ` x ) e. ( F ` y ) } i^i ( z X. z ) ) e. _V
45 weeq1 
 |-  ( w = ( { <. x , y >. | ( F ` x ) e. ( F ` y ) } i^i ( z X. z ) ) -> ( w We z <-> ( { <. x , y >. | ( F ` x ) e. ( F ` y ) } i^i ( z X. z ) ) We z ) )
46 44 45 spcev 
 |-  ( ( { <. x , y >. | ( F ` x ) e. ( F ` y ) } i^i ( z X. z ) ) We z -> E. w w We z )
47 41 46 sylbi 
 |-  ( { <. x , y >. | ( F ` x ) e. ( F ` y ) } We z -> E. w w We z )
48 40 47 syl 
 |-  ( ph -> E. w w We z )
49 48 alrimiv 
 |-  ( ph -> A. z E. w w We z )
50 dfac8 
 |-  ( CHOICE <-> A. z E. w w We z )
51 49 50 sylibr 
 |-  ( ph -> CHOICE )
52 34 51 jca 
 |-  ( ph -> ( I : On -1-1-> A /\ CHOICE ) )