Description: If F is a bijection from the ordinals to the universe and H is a bijection from the ordinals to the proper class B , then I maps A one-to-one into B . This is the ZFC version of (5 -> 10) in https://tinyurl.com/hamkins-gblac in the case where one of the classes is a proper class. See onprcf1of1orbd for the case where neither class is a proper class, and see onprcf1of1ord for a theorem that covers both cases. Note that in NBG set theory the first two hypotheses would be replaced by something like ( ph -> A. X ( -. X e. _V -> E. F F : On -1-1-onto-> X ) ) . However, we cannot quantify over classes, so we split this into the case where X is the universe and the case where X is an arbitrary proper class B which together are sufficient for this proof. (Contributed by BTernaryTau, 17-Sep-2026)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | onprcf1of1orad.1 | |- ( ph -> F : On -1-1-onto-> _V ) |
|
| onprcf1of1orad.2 | |- ( ph -> ( -. B e. _V -> H : On -1-1-onto-> B ) ) |
||
| onprcf1of1orad.3 | |- ( ph -> -. B e. _V ) |
||
| onprcf1of1orad.4 | |- I = ( H o. ( `' F |` A ) ) |
||
| Assertion | onprcf1of1orad | |- ( ph -> I : A -1-1-> B ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | onprcf1of1orad.1 | |- ( ph -> F : On -1-1-onto-> _V ) |
|
| 2 | onprcf1of1orad.2 | |- ( ph -> ( -. B e. _V -> H : On -1-1-onto-> B ) ) |
|
| 3 | onprcf1of1orad.3 | |- ( ph -> -. B e. _V ) |
|
| 4 | onprcf1of1orad.4 | |- I = ( H o. ( `' F |` A ) ) |
|
| 5 | 3 2 | mpd | |- ( ph -> H : On -1-1-onto-> B ) |
| 6 | f1of1 | |- ( H : On -1-1-onto-> B -> H : On -1-1-> B ) |
|
| 7 | 5 6 | syl | |- ( ph -> H : On -1-1-> B ) |
| 8 | f1ocnv | |- ( F : On -1-1-onto-> _V -> `' F : _V -1-1-onto-> On ) |
|
| 9 | f1of1 | |- ( `' F : _V -1-1-onto-> On -> `' F : _V -1-1-> On ) |
|
| 10 | ssv | |- A C_ _V |
|
| 11 | f1ssres | |- ( ( `' F : _V -1-1-> On /\ A C_ _V ) -> ( `' F |` A ) : A -1-1-> On ) |
|
| 12 | 9 10 11 | sylancl | |- ( `' F : _V -1-1-onto-> On -> ( `' F |` A ) : A -1-1-> On ) |
| 13 | 1 8 12 | 3syl | |- ( ph -> ( `' F |` A ) : A -1-1-> On ) |
| 14 | f1co | |- ( ( H : On -1-1-> B /\ ( `' F |` A ) : A -1-1-> On ) -> ( H o. ( `' F |` A ) ) : A -1-1-> B ) |
|
| 15 | 7 13 14 | syl2anc | |- ( ph -> ( H o. ( `' F |` A ) ) : A -1-1-> B ) |
| 16 | f1eq1 | |- ( I = ( H o. ( `' F |` A ) ) -> ( I : A -1-1-> B <-> ( H o. ( `' F |` A ) ) : A -1-1-> B ) ) |
|
| 17 | 4 16 | ax-mp | |- ( I : A -1-1-> B <-> ( H o. ( `' F |` A ) ) : A -1-1-> B ) |
| 18 | 15 17 | sylibr | |- ( ph -> I : A -1-1-> B ) |