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 | ⊢ ( 𝜑 → 𝐹 : On –1-1-onto→ V ) | |
| onprcf1of1orad.2 | ⊢ ( 𝜑 → ( ¬ 𝐵 ∈ V → 𝐻 : On –1-1-onto→ 𝐵 ) ) | ||
| onprcf1of1orad.3 | ⊢ ( 𝜑 → ¬ 𝐵 ∈ V ) | ||
| onprcf1of1orad.4 | ⊢ 𝐼 = ( 𝐻 ∘ ( ◡ 𝐹 ↾ 𝐴 ) ) | ||
| Assertion | onprcf1of1orad | ⊢ ( 𝜑 → 𝐼 : 𝐴 –1-1→ 𝐵 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | onprcf1of1orad.1 | ⊢ ( 𝜑 → 𝐹 : On –1-1-onto→ V ) | |
| 2 | onprcf1of1orad.2 | ⊢ ( 𝜑 → ( ¬ 𝐵 ∈ V → 𝐻 : On –1-1-onto→ 𝐵 ) ) | |
| 3 | onprcf1of1orad.3 | ⊢ ( 𝜑 → ¬ 𝐵 ∈ V ) | |
| 4 | onprcf1of1orad.4 | ⊢ 𝐼 = ( 𝐻 ∘ ( ◡ 𝐹 ↾ 𝐴 ) ) | |
| 5 | 3 2 | mpd | ⊢ ( 𝜑 → 𝐻 : On –1-1-onto→ 𝐵 ) |
| 6 | f1of1 | ⊢ ( 𝐻 : On –1-1-onto→ 𝐵 → 𝐻 : On –1-1→ 𝐵 ) | |
| 7 | 5 6 | syl | ⊢ ( 𝜑 → 𝐻 : On –1-1→ 𝐵 ) |
| 8 | f1ocnv | ⊢ ( 𝐹 : On –1-1-onto→ V → ◡ 𝐹 : V –1-1-onto→ On ) | |
| 9 | f1of1 | ⊢ ( ◡ 𝐹 : V –1-1-onto→ On → ◡ 𝐹 : V –1-1→ On ) | |
| 10 | ssv | ⊢ 𝐴 ⊆ V | |
| 11 | f1ssres | ⊢ ( ( ◡ 𝐹 : V –1-1→ On ∧ 𝐴 ⊆ V ) → ( ◡ 𝐹 ↾ 𝐴 ) : 𝐴 –1-1→ On ) | |
| 12 | 9 10 11 | sylancl | ⊢ ( ◡ 𝐹 : V –1-1-onto→ On → ( ◡ 𝐹 ↾ 𝐴 ) : 𝐴 –1-1→ On ) |
| 13 | 1 8 12 | 3syl | ⊢ ( 𝜑 → ( ◡ 𝐹 ↾ 𝐴 ) : 𝐴 –1-1→ On ) |
| 14 | f1co | ⊢ ( ( 𝐻 : On –1-1→ 𝐵 ∧ ( ◡ 𝐹 ↾ 𝐴 ) : 𝐴 –1-1→ On ) → ( 𝐻 ∘ ( ◡ 𝐹 ↾ 𝐴 ) ) : 𝐴 –1-1→ 𝐵 ) | |
| 15 | 7 13 14 | syl2anc | ⊢ ( 𝜑 → ( 𝐻 ∘ ( ◡ 𝐹 ↾ 𝐴 ) ) : 𝐴 –1-1→ 𝐵 ) |
| 16 | f1eq1 | ⊢ ( 𝐼 = ( 𝐻 ∘ ( ◡ 𝐹 ↾ 𝐴 ) ) → ( 𝐼 : 𝐴 –1-1→ 𝐵 ↔ ( 𝐻 ∘ ( ◡ 𝐹 ↾ 𝐴 ) ) : 𝐴 –1-1→ 𝐵 ) ) | |
| 17 | 4 16 | ax-mp | ⊢ ( 𝐼 : 𝐴 –1-1→ 𝐵 ↔ ( 𝐻 ∘ ( ◡ 𝐹 ↾ 𝐴 ) ) : 𝐴 –1-1→ 𝐵 ) |
| 18 | 15 17 | sylibr | ⊢ ( 𝜑 → 𝐼 : 𝐴 –1-1→ 𝐵 ) |