Theorem onprcf1of1orbd

Description: If F is a bijection from the ordinals to the universe and both A and B are sets, then either A can be mapped one-to-one into B or B can be mapped one-to-one into A . This is the ZFC version of (5 -> 10) in https://tinyurl.com/hamkins-gblac in the case where neither class is a proper class. See onprcf1of1orad for the case where one of the classes is a proper class, and see onprcf1of1ord for a theorem that covers both cases. Note that in NBG set theory the first hypothesis would be replaced by something like ( ph -> A. X ( -. X e.V -> E. F F : On -1-1-onto-> X ) ) , but since we cannot quantify over classes, we instead consider only the case X = V which is sufficient for this proof. (Contributed by BTernaryTau, 17-Sep-2026)

	Ref	Expression
Hypotheses	onprcf1of1orbd.1	⊢ ( 𝜑 → 𝐹 : On –1-1-onto→ V )
	onprcf1of1orbd.2	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	onprcf1of1orbd.3	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
Assertion	onprcf1of1orbd	⊢ ( 𝜑 → ( ∃ 𝑓 𝑓 : 𝐴 –1-1→ 𝐵 ∨ ∃ ℎ ℎ : 𝐵 –1-1→ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		onprcf1of1orbd.1	⊢ ( 𝜑 → 𝐹 : On –1-1-onto→ V )
2		onprcf1of1orbd.2	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
3		onprcf1of1orbd.3	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
4		f1ocnv	⊢ ( 𝐹 : On –1-1-onto→ V → ◡ 𝐹 : V –1-1-onto→ On )
5		f1ofun	⊢ ( ◡ 𝐹 : V –1-1-onto→ On → Fun ◡ 𝐹 )
6		resfunexg	⊢ ( ( Fun ◡ 𝐹 ∧ 𝑧 ∈ V ) → ( ◡ 𝐹 ↾ 𝑧 ) ∈ V )
7	6	elvd	⊢ ( Fun ◡ 𝐹 → ( ◡ 𝐹 ↾ 𝑧 ) ∈ V )
8	4 5 7	3syl	⊢ ( 𝐹 : On –1-1-onto→ V → ( ◡ 𝐹 ↾ 𝑧 ) ∈ V )
9	1 8	syl	⊢ ( 𝜑 → ( ◡ 𝐹 ↾ 𝑧 ) ∈ V )
10		f1of1	⊢ ( ◡ 𝐹 : V –1-1-onto→ On → ◡ 𝐹 : V –1-1→ On )
11		ssv	⊢ 𝑧 ⊆ V
12		f1ssres	⊢ ( ( ◡ 𝐹 : V –1-1→ On ∧ 𝑧 ⊆ V ) → ( ◡ 𝐹 ↾ 𝑧 ) : 𝑧 –1-1→ On )
13	10 11 12	sylancl	⊢ ( ◡ 𝐹 : V –1-1-onto→ On → ( ◡ 𝐹 ↾ 𝑧 ) : 𝑧 –1-1→ On )
14	1 4 13	3syl	⊢ ( 𝜑 → ( ◡ 𝐹 ↾ 𝑧 ) : 𝑧 –1-1→ On )
15		f1eq1	⊢ ( 𝑖 = ( ◡ 𝐹 ↾ 𝑧 ) → ( 𝑖 : 𝑧 –1-1→ On ↔ ( ◡ 𝐹 ↾ 𝑧 ) : 𝑧 –1-1→ On ) )
16	9 14 15	spcedv	⊢ ( 𝜑 → ∃ 𝑖 𝑖 : 𝑧 –1-1→ On )
17	16	alrimiv	⊢ ( 𝜑 → ∀ 𝑧 ∃ 𝑖 𝑖 : 𝑧 –1-1→ On )
18		dfac15	⊢ ( CHOICE ↔ ∀ 𝑧 ∃ 𝑖 𝑖 : 𝑧 –1-1→ On )
19	17 18	sylibr	⊢ ( 𝜑 → CHOICE )
20		dfac16	⊢ ( CHOICE ↔ ∀ 𝑥 ∀ 𝑦 ( 𝑥 ≼ 𝑦 ∨ 𝑦 ≼ 𝑥 ) )
21		breq2	⊢ ( 𝑦 = 𝐵 → ( 𝑥 ≼ 𝑦 ↔ 𝑥 ≼ 𝐵 ) )
22		breq1	⊢ ( 𝑦 = 𝐵 → ( 𝑦 ≼ 𝑥 ↔ 𝐵 ≼ 𝑥 ) )
23	21 22	orbi12d	⊢ ( 𝑦 = 𝐵 → ( ( 𝑥 ≼ 𝑦 ∨ 𝑦 ≼ 𝑥 ) ↔ ( 𝑥 ≼ 𝐵 ∨ 𝐵 ≼ 𝑥 ) ) )
24	23	spcgv	⊢ ( 𝐵 ∈ 𝑊 → ( ∀ 𝑦 ( 𝑥 ≼ 𝑦 ∨ 𝑦 ≼ 𝑥 ) → ( 𝑥 ≼ 𝐵 ∨ 𝐵 ≼ 𝑥 ) ) )
25	3 24	syl	⊢ ( 𝜑 → ( ∀ 𝑦 ( 𝑥 ≼ 𝑦 ∨ 𝑦 ≼ 𝑥 ) → ( 𝑥 ≼ 𝐵 ∨ 𝐵 ≼ 𝑥 ) ) )
26	25	alimdv	⊢ ( 𝜑 → ( ∀ 𝑥 ∀ 𝑦 ( 𝑥 ≼ 𝑦 ∨ 𝑦 ≼ 𝑥 ) → ∀ 𝑥 ( 𝑥 ≼ 𝐵 ∨ 𝐵 ≼ 𝑥 ) ) )
27		breq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 ≼ 𝐵 ↔ 𝐴 ≼ 𝐵 ) )
28		breq2	⊢ ( 𝑥 = 𝐴 → ( 𝐵 ≼ 𝑥 ↔ 𝐵 ≼ 𝐴 ) )
29	27 28	orbi12d	⊢ ( 𝑥 = 𝐴 → ( ( 𝑥 ≼ 𝐵 ∨ 𝐵 ≼ 𝑥 ) ↔ ( 𝐴 ≼ 𝐵 ∨ 𝐵 ≼ 𝐴 ) ) )
30	29	spcgv	⊢ ( 𝐴 ∈ 𝑉 → ( ∀ 𝑥 ( 𝑥 ≼ 𝐵 ∨ 𝐵 ≼ 𝑥 ) → ( 𝐴 ≼ 𝐵 ∨ 𝐵 ≼ 𝐴 ) ) )
31	2 26 30	sylsyld	⊢ ( 𝜑 → ( ∀ 𝑥 ∀ 𝑦 ( 𝑥 ≼ 𝑦 ∨ 𝑦 ≼ 𝑥 ) → ( 𝐴 ≼ 𝐵 ∨ 𝐵 ≼ 𝐴 ) ) )
32	20 31	biimtrid	⊢ ( 𝜑 → ( CHOICE → ( 𝐴 ≼ 𝐵 ∨ 𝐵 ≼ 𝐴 ) ) )
33	19 32	mpd	⊢ ( 𝜑 → ( 𝐴 ≼ 𝐵 ∨ 𝐵 ≼ 𝐴 ) )
34		brdomg	⊢ ( 𝐵 ∈ 𝑊 → ( 𝐴 ≼ 𝐵 ↔ ∃ 𝑓 𝑓 : 𝐴 –1-1→ 𝐵 ) )
35	3 34	syl	⊢ ( 𝜑 → ( 𝐴 ≼ 𝐵 ↔ ∃ 𝑓 𝑓 : 𝐴 –1-1→ 𝐵 ) )
36		brdomg	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐵 ≼ 𝐴 ↔ ∃ ℎ ℎ : 𝐵 –1-1→ 𝐴 ) )
37	2 36	syl	⊢ ( 𝜑 → ( 𝐵 ≼ 𝐴 ↔ ∃ ℎ ℎ : 𝐵 –1-1→ 𝐴 ) )
38	35 37	orbi12d	⊢ ( 𝜑 → ( ( 𝐴 ≼ 𝐵 ∨ 𝐵 ≼ 𝐴 ) ↔ ( ∃ 𝑓 𝑓 : 𝐴 –1-1→ 𝐵 ∨ ∃ ℎ ℎ : 𝐵 –1-1→ 𝐴 ) ) )
39	33 38	mpbid	⊢ ( 𝜑 → ( ∃ 𝑓 𝑓 : 𝐴 –1-1→ 𝐵 ∨ ∃ ℎ ℎ : 𝐵 –1-1→ 𝐴 ) )