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	|- ( ph -> F : On -1-1-onto-> _V )
	onprcf1of1orbd.2	|- ( ph -> A e. V )
	onprcf1of1orbd.3	|- ( ph -> B e. W )
Assertion	onprcf1of1orbd	|- ( ph -> ( E. f f : A -1-1-> B \/ E. h h : B -1-1-> A ) )

Proof

Step	Hyp	Ref	Expression
1		onprcf1of1orbd.1	|- ( ph -> F : On -1-1-onto-> _V )
2		onprcf1of1orbd.2	|- ( ph -> A e. V )
3		onprcf1of1orbd.3	|- ( ph -> B e. W )
4		f1ocnv	|- ( F : On -1-1-onto-> _V -> `' F : _V -1-1-onto-> On )
5		f1ofun	|- ( `' F : _V -1-1-onto-> On -> Fun `' F )
6		resfunexg	|- ( ( Fun `' F /\ z e. _V ) -> ( `' F |` z ) e. _V )
7	6	elvd	|- ( Fun `' F -> ( `' F |` z ) e. _V )
8	4 5 7	3syl	|- ( F : On -1-1-onto-> _V -> ( `' F |` z ) e. _V )
9	1 8	syl	|- ( ph -> ( `' F |` z ) e. _V )
10		f1of1	|- ( `' F : _V -1-1-onto-> On -> `' F : _V -1-1-> On )
11		ssv	|- z C_ _V
12		f1ssres	|- ( ( `' F : _V -1-1-> On /\ z C_ _V ) -> ( `' F |` z ) : z -1-1-> On )
13	10 11 12	sylancl	|- ( `' F : _V -1-1-onto-> On -> ( `' F |` z ) : z -1-1-> On )
14	1 4 13	3syl	|- ( ph -> ( `' F |` z ) : z -1-1-> On )
15		f1eq1	|- ( i = ( `' F |` z ) -> ( i : z -1-1-> On <-> ( `' F |` z ) : z -1-1-> On ) )
16	9 14 15	spcedv	|- ( ph -> E. i i : z -1-1-> On )
17	16	alrimiv	|- ( ph -> A. z E. i i : z -1-1-> On )
18		dfac15	|- ( CHOICE <-> A. z E. i i : z -1-1-> On )
19	17 18	sylibr	|- ( ph -> CHOICE )
20		dfac16	|- ( CHOICE <-> A. x A. y ( x ~<_ y \/ y ~<_ x ) )
21		breq2	|- ( y = B -> ( x ~<_ y <-> x ~<_ B ) )
22		breq1	|- ( y = B -> ( y ~<_ x <-> B ~<_ x ) )
23	21 22	orbi12d	|- ( y = B -> ( ( x ~<_ y \/ y ~<_ x ) <-> ( x ~<_ B \/ B ~<_ x ) ) )
24	23	spcgv	|- ( B e. W -> ( A. y ( x ~<_ y \/ y ~<_ x ) -> ( x ~<_ B \/ B ~<_ x ) ) )
25	3 24	syl	|- ( ph -> ( A. y ( x ~<_ y \/ y ~<_ x ) -> ( x ~<_ B \/ B ~<_ x ) ) )
26	25	alimdv	|- ( ph -> ( A. x A. y ( x ~<_ y \/ y ~<_ x ) -> A. x ( x ~<_ B \/ B ~<_ x ) ) )
27		breq1	|- ( x = A -> ( x ~<_ B <-> A ~<_ B ) )
28		breq2	|- ( x = A -> ( B ~<_ x <-> B ~<_ A ) )
29	27 28	orbi12d	|- ( x = A -> ( ( x ~<_ B \/ B ~<_ x ) <-> ( A ~<_ B \/ B ~<_ A ) ) )
30	29	spcgv	|- ( A e. V -> ( A. x ( x ~<_ B \/ B ~<_ x ) -> ( A ~<_ B \/ B ~<_ A ) ) )
31	2 26 30	sylsyld	|- ( ph -> ( A. x A. y ( x ~<_ y \/ y ~<_ x ) -> ( A ~<_ B \/ B ~<_ A ) ) )
32	20 31	biimtrid	|- ( ph -> ( CHOICE -> ( A ~<_ B \/ B ~<_ A ) ) )
33	19 32	mpd	|- ( ph -> ( A ~<_ B \/ B ~<_ A ) )
34		brdomg	|- ( B e. W -> ( A ~<_ B <-> E. f f : A -1-1-> B ) )
35	3 34	syl	|- ( ph -> ( A ~<_ B <-> E. f f : A -1-1-> B ) )
36		brdomg	|- ( A e. V -> ( B ~<_ A <-> E. h h : B -1-1-> A ) )
37	2 36	syl	|- ( ph -> ( B ~<_ A <-> E. h h : B -1-1-> A ) )
38	35 37	orbi12d	|- ( ph -> ( ( A ~<_ B \/ B ~<_ A ) <-> ( E. f f : A -1-1-> B \/ E. h h : B -1-1-> A ) ) )
39	33 38	mpbid	|- ( ph -> ( E. f f : A -1-1-> B \/ E. h h : B -1-1-> A ) )