Metamath Proof Explorer

Theorem onprcf1of1ord

Description: If F is a bijection from the ordinals to the universe, H is a bijection from the ordinals to A if A is a proper class, and I is a bijection from the ordinals to B if B is a proper class, then J either maps A one-to-one into B or maps B one-to-one into A . This is the ZFC version of (5 -> 10) in https://tinyurl.com/hamkins-gblac . Note that in NBG set theory the first three 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, the case where X is an arbitrary proper class A , 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 onprcf1of1ord.1 
|- ( ph -> F : On -1-1-onto-> _V )
onprcf1of1ord.2 
|- ( ph -> ( -. A e. _V -> H : On -1-1-onto-> A ) )
onprcf1of1ord.3 
|- ( ph -> ( -. B e. _V -> I : On -1-1-onto-> B ) )
onprcf1of1ord.4 
|- J = if ( A e. _V , if ( B e. _V , K , ( I o. ( `' F |` A ) ) ) , ( H o. ( `' F |` B ) ) )
onprcf1of1ord.5 
|- K = ( F ` |^| { x e. On | ( ( F ` x ) : A -1-1-> B \/ ( F ` x ) : B -1-1-> A ) } )
Assertion onprcf1of1ord 
|- ( ph -> ( J : A -1-1-> B \/ J : B -1-1-> A ) )

Proof

Step Hyp Ref Expression
1 onprcf1of1ord.1 
 |-  ( ph -> F : On -1-1-onto-> _V )
2 onprcf1of1ord.2 
 |-  ( ph -> ( -. A e. _V -> H : On -1-1-onto-> A ) )
3 onprcf1of1ord.3 
 |-  ( ph -> ( -. B e. _V -> I : On -1-1-onto-> B ) )
4 onprcf1of1ord.4 
 |-  J = if ( A e. _V , if ( B e. _V , K , ( I o. ( `' F |` A ) ) ) , ( H o. ( `' F |` B ) ) )
5 onprcf1of1ord.5 
 |-  K = ( F ` |^| { x e. On | ( ( F ` x ) : A -1-1-> B \/ ( F ` x ) : B -1-1-> A ) } )
6 1 ad2antrr 
 |-  ( ( ( ph /\ A e. _V ) /\ B e. _V ) -> F : On -1-1-onto-> _V )
7 simplr 
 |-  ( ( ( ph /\ A e. _V ) /\ B e. _V ) -> A e. _V )
8 simpr 
 |-  ( ( ( ph /\ A e. _V ) /\ B e. _V ) -> B e. _V )
9 6 7 8 onprcf1of1orbd 
 |-  ( ( ( ph /\ A e. _V ) /\ B e. _V ) -> ( E. f f : A -1-1-> B \/ E. f f : B -1-1-> A ) )
10 19.43 
 |-  ( E. f ( f : A -1-1-> B \/ f : B -1-1-> A ) <-> ( E. f f : A -1-1-> B \/ E. f f : B -1-1-> A ) )
11 9 10 sylibr 
 |-  ( ( ( ph /\ A e. _V ) /\ B e. _V ) -> E. f ( f : A -1-1-> B \/ f : B -1-1-> A ) )
12 dff1o5 
 |-  ( F : On -1-1-onto-> _V <-> ( F : On -1-1-> _V /\ ran F = _V ) )
13 12 simprbi 
 |-  ( F : On -1-1-onto-> _V -> ran F = _V )
14 1 13 syl 
 |-  ( ph -> ran F = _V )
15 14 rexeqdv 
 |-  ( ph -> ( E. f e. ran F ( f : A -1-1-> B \/ f : B -1-1-> A ) <-> E. f e. _V ( f : A -1-1-> B \/ f : B -1-1-> A ) ) )
16 rexv 
 |-  ( E. f e. _V ( f : A -1-1-> B \/ f : B -1-1-> A ) <-> E. f ( f : A -1-1-> B \/ f : B -1-1-> A ) )
17 15 16 bitrdi 
 |-  ( ph -> ( E. f e. ran F ( f : A -1-1-> B \/ f : B -1-1-> A ) <-> E. f ( f : A -1-1-> B \/ f : B -1-1-> A ) ) )
18 f1ofn 
 |-  ( F : On -1-1-onto-> _V -> F Fn On )
19 f1eq1 
 |-  ( f = ( F ` x ) -> ( f : A -1-1-> B <-> ( F ` x ) : A -1-1-> B ) )
20 f1eq1 
 |-  ( f = ( F ` x ) -> ( f : B -1-1-> A <-> ( F ` x ) : B -1-1-> A ) )
21 19 20 orbi12d 
 |-  ( f = ( F ` x ) -> ( ( f : A -1-1-> B \/ f : B -1-1-> A ) <-> ( ( F ` x ) : A -1-1-> B \/ ( F ` x ) : B -1-1-> A ) ) )
22 21 rexrn 
 |-  ( F Fn On -> ( E. f e. ran F ( f : A -1-1-> B \/ f : B -1-1-> A ) <-> E. x e. On ( ( F ` x ) : A -1-1-> B \/ ( F ` x ) : B -1-1-> A ) ) )
23 1 18 22 3syl 
 |-  ( ph -> ( E. f e. ran F ( f : A -1-1-> B \/ f : B -1-1-> A ) <-> E. x e. On ( ( F ` x ) : A -1-1-> B \/ ( F ` x ) : B -1-1-> A ) ) )
24 17 23 bitr3d 
 |-  ( ph -> ( E. f ( f : A -1-1-> B \/ f : B -1-1-> A ) <-> E. x e. On ( ( F ` x ) : A -1-1-> B \/ ( F ` x ) : B -1-1-> A ) ) )
25 24 ad2antrr 
 |-  ( ( ( ph /\ A e. _V ) /\ B e. _V ) -> ( E. f ( f : A -1-1-> B \/ f : B -1-1-> A ) <-> E. x e. On ( ( F ` x ) : A -1-1-> B \/ ( F ` x ) : B -1-1-> A ) ) )
26 11 25 mpbid 
 |-  ( ( ( ph /\ A e. _V ) /\ B e. _V ) -> E. x e. On ( ( F ` x ) : A -1-1-> B \/ ( F ` x ) : B -1-1-> A ) )
27 nfcv 
 |-  F/_ x F
28 nfrab1 
 |-  F/_ x { x e. On | ( ( F ` x ) : A -1-1-> B \/ ( F ` x ) : B -1-1-> A ) }
29 28 nfint 
 |-  F/_ x |^| { x e. On | ( ( F ` x ) : A -1-1-> B \/ ( F ` x ) : B -1-1-> A ) }
30 27 29 nffv 
 |-  F/_ x ( F ` |^| { x e. On | ( ( F ` x ) : A -1-1-> B \/ ( F ` x ) : B -1-1-> A ) } )
31 nfcv 
 |-  F/_ x A
32 nfcv 
 |-  F/_ x B
33 30 31 32 nff1 
 |-  F/ x ( F ` |^| { x e. On | ( ( F ` x ) : A -1-1-> B \/ ( F ` x ) : B -1-1-> A ) } ) : A -1-1-> B
34 30 32 31 nff1 
 |-  F/ x ( F ` |^| { x e. On | ( ( F ` x ) : A -1-1-> B \/ ( F ` x ) : B -1-1-> A ) } ) : B -1-1-> A
35 33 34 nfor 
 |-  F/ x ( ( F ` |^| { x e. On | ( ( F ` x ) : A -1-1-> B \/ ( F ` x ) : B -1-1-> A ) } ) : A -1-1-> B \/ ( F ` |^| { x e. On | ( ( F ` x ) : A -1-1-> B \/ ( F ` x ) : B -1-1-> A ) } ) : B -1-1-> A )
36 fveq2 
 |-  ( x = |^| { x e. On | ( ( F ` x ) : A -1-1-> B \/ ( F ` x ) : B -1-1-> A ) } -> ( F ` x ) = ( F ` |^| { x e. On | ( ( F ` x ) : A -1-1-> B \/ ( F ` x ) : B -1-1-> A ) } ) )
37 f1eq1 
 |-  ( ( F ` x ) = ( F ` |^| { x e. On | ( ( F ` x ) : A -1-1-> B \/ ( F ` x ) : B -1-1-> A ) } ) -> ( ( F ` x ) : A -1-1-> B <-> ( F ` |^| { x e. On | ( ( F ` x ) : A -1-1-> B \/ ( F ` x ) : B -1-1-> A ) } ) : A -1-1-> B ) )
38 36 37 syl 
 |-  ( x = |^| { x e. On | ( ( F ` x ) : A -1-1-> B \/ ( F ` x ) : B -1-1-> A ) } -> ( ( F ` x ) : A -1-1-> B <-> ( F ` |^| { x e. On | ( ( F ` x ) : A -1-1-> B \/ ( F ` x ) : B -1-1-> A ) } ) : A -1-1-> B ) )
39 f1eq1 
 |-  ( ( F ` x ) = ( F ` |^| { x e. On | ( ( F ` x ) : A -1-1-> B \/ ( F ` x ) : B -1-1-> A ) } ) -> ( ( F ` x ) : B -1-1-> A <-> ( F ` |^| { x e. On | ( ( F ` x ) : A -1-1-> B \/ ( F ` x ) : B -1-1-> A ) } ) : B -1-1-> A ) )
40 36 39 syl 
 |-  ( x = |^| { x e. On | ( ( F ` x ) : A -1-1-> B \/ ( F ` x ) : B -1-1-> A ) } -> ( ( F ` x ) : B -1-1-> A <-> ( F ` |^| { x e. On | ( ( F ` x ) : A -1-1-> B \/ ( F ` x ) : B -1-1-> A ) } ) : B -1-1-> A ) )
41 38 40 orbi12d 
 |-  ( x = |^| { x e. On | ( ( F ` x ) : A -1-1-> B \/ ( F ` x ) : B -1-1-> A ) } -> ( ( ( F ` x ) : A -1-1-> B \/ ( F ` x ) : B -1-1-> A ) <-> ( ( F ` |^| { x e. On | ( ( F ` x ) : A -1-1-> B \/ ( F ` x ) : B -1-1-> A ) } ) : A -1-1-> B \/ ( F ` |^| { x e. On | ( ( F ` x ) : A -1-1-> B \/ ( F ` x ) : B -1-1-> A ) } ) : B -1-1-> A ) ) )
42 35 41 onminsb 
 |-  ( E. x e. On ( ( F ` x ) : A -1-1-> B \/ ( F ` x ) : B -1-1-> A ) -> ( ( F ` |^| { x e. On | ( ( F ` x ) : A -1-1-> B \/ ( F ` x ) : B -1-1-> A ) } ) : A -1-1-> B \/ ( F ` |^| { x e. On | ( ( F ` x ) : A -1-1-> B \/ ( F ` x ) : B -1-1-> A ) } ) : B -1-1-> A ) )
43 26 42 syl 
 |-  ( ( ( ph /\ A e. _V ) /\ B e. _V ) -> ( ( F ` |^| { x e. On | ( ( F ` x ) : A -1-1-> B \/ ( F ` x ) : B -1-1-> A ) } ) : A -1-1-> B \/ ( F ` |^| { x e. On | ( ( F ` x ) : A -1-1-> B \/ ( F ` x ) : B -1-1-> A ) } ) : B -1-1-> A ) )
44 iftrue 
 |-  ( A e. _V -> if ( A e. _V , if ( B e. _V , K , ( I o. ( `' F |` A ) ) ) , ( H o. ( `' F |` B ) ) ) = if ( B e. _V , K , ( I o. ( `' F |` A ) ) ) )
45 4 44 eqtrid 
 |-  ( A e. _V -> J = if ( B e. _V , K , ( I o. ( `' F |` A ) ) ) )
46 45 ad2antlr 
 |-  ( ( ( ph /\ A e. _V ) /\ B e. _V ) -> J = if ( B e. _V , K , ( I o. ( `' F |` A ) ) ) )
47 iftrue 
 |-  ( B e. _V -> if ( B e. _V , K , ( I o. ( `' F |` A ) ) ) = K )
48 47 adantl 
 |-  ( ( ( ph /\ A e. _V ) /\ B e. _V ) -> if ( B e. _V , K , ( I o. ( `' F |` A ) ) ) = K )
49 46 48 eqtrd 
 |-  ( ( ( ph /\ A e. _V ) /\ B e. _V ) -> J = K )
50 49 5 eqtrdi 
 |-  ( ( ( ph /\ A e. _V ) /\ B e. _V ) -> J = ( F ` |^| { x e. On | ( ( F ` x ) : A -1-1-> B \/ ( F ` x ) : B -1-1-> A ) } ) )
51 f1eq1 
 |-  ( J = ( F ` |^| { x e. On | ( ( F ` x ) : A -1-1-> B \/ ( F ` x ) : B -1-1-> A ) } ) -> ( J : A -1-1-> B <-> ( F ` |^| { x e. On | ( ( F ` x ) : A -1-1-> B \/ ( F ` x ) : B -1-1-> A ) } ) : A -1-1-> B ) )
52 50 51 syl 
 |-  ( ( ( ph /\ A e. _V ) /\ B e. _V ) -> ( J : A -1-1-> B <-> ( F ` |^| { x e. On | ( ( F ` x ) : A -1-1-> B \/ ( F ` x ) : B -1-1-> A ) } ) : A -1-1-> B ) )
53 f1eq1 
 |-  ( J = ( F ` |^| { x e. On | ( ( F ` x ) : A -1-1-> B \/ ( F ` x ) : B -1-1-> A ) } ) -> ( J : B -1-1-> A <-> ( F ` |^| { x e. On | ( ( F ` x ) : A -1-1-> B \/ ( F ` x ) : B -1-1-> A ) } ) : B -1-1-> A ) )
54 50 53 syl 
 |-  ( ( ( ph /\ A e. _V ) /\ B e. _V ) -> ( J : B -1-1-> A <-> ( F ` |^| { x e. On | ( ( F ` x ) : A -1-1-> B \/ ( F ` x ) : B -1-1-> A ) } ) : B -1-1-> A ) )
55 52 54 orbi12d 
 |-  ( ( ( ph /\ A e. _V ) /\ B e. _V ) -> ( ( J : A -1-1-> B \/ J : B -1-1-> A ) <-> ( ( F ` |^| { x e. On | ( ( F ` x ) : A -1-1-> B \/ ( F ` x ) : B -1-1-> A ) } ) : A -1-1-> B \/ ( F ` |^| { x e. On | ( ( F ` x ) : A -1-1-> B \/ ( F ` x ) : B -1-1-> A ) } ) : B -1-1-> A ) ) )
56 43 55 mpbird 
 |-  ( ( ( ph /\ A e. _V ) /\ B e. _V ) -> ( J : A -1-1-> B \/ J : B -1-1-> A ) )
57 1 ad2antrr 
 |-  ( ( ( ph /\ A e. _V ) /\ -. B e. _V ) -> F : On -1-1-onto-> _V )
58 3 ad2antrr 
 |-  ( ( ( ph /\ A e. _V ) /\ -. B e. _V ) -> ( -. B e. _V -> I : On -1-1-onto-> B ) )
59 simpr 
 |-  ( ( ( ph /\ A e. _V ) /\ -. B e. _V ) -> -. B e. _V )
60 eqid 
 |-  ( I o. ( `' F |` A ) ) = ( I o. ( `' F |` A ) )
61 57 58 59 60 onprcf1of1orad 
 |-  ( ( ( ph /\ A e. _V ) /\ -. B e. _V ) -> ( I o. ( `' F |` A ) ) : A -1-1-> B )
62 45 ad2antlr 
 |-  ( ( ( ph /\ A e. _V ) /\ -. B e. _V ) -> J = if ( B e. _V , K , ( I o. ( `' F |` A ) ) ) )
63 iffalse 
 |-  ( -. B e. _V -> if ( B e. _V , K , ( I o. ( `' F |` A ) ) ) = ( I o. ( `' F |` A ) ) )
64 63 adantl 
 |-  ( ( ( ph /\ A e. _V ) /\ -. B e. _V ) -> if ( B e. _V , K , ( I o. ( `' F |` A ) ) ) = ( I o. ( `' F |` A ) ) )
65 62 64 eqtrd 
 |-  ( ( ( ph /\ A e. _V ) /\ -. B e. _V ) -> J = ( I o. ( `' F |` A ) ) )
66 f1eq1 
 |-  ( J = ( I o. ( `' F |` A ) ) -> ( J : A -1-1-> B <-> ( I o. ( `' F |` A ) ) : A -1-1-> B ) )
67 65 66 syl 
 |-  ( ( ( ph /\ A e. _V ) /\ -. B e. _V ) -> ( J : A -1-1-> B <-> ( I o. ( `' F |` A ) ) : A -1-1-> B ) )
68 61 67 mpbird 
 |-  ( ( ( ph /\ A e. _V ) /\ -. B e. _V ) -> J : A -1-1-> B )
69 68 orcd 
 |-  ( ( ( ph /\ A e. _V ) /\ -. B e. _V ) -> ( J : A -1-1-> B \/ J : B -1-1-> A ) )
70 56 69 pm2.61dan 
 |-  ( ( ph /\ A e. _V ) -> ( J : A -1-1-> B \/ J : B -1-1-> A ) )
71 1 adantr 
 |-  ( ( ph /\ -. A e. _V ) -> F : On -1-1-onto-> _V )
72 2 adantr 
 |-  ( ( ph /\ -. A e. _V ) -> ( -. A e. _V -> H : On -1-1-onto-> A ) )
73 simpr 
 |-  ( ( ph /\ -. A e. _V ) -> -. A e. _V )
74 eqid 
 |-  ( H o. ( `' F |` B ) ) = ( H o. ( `' F |` B ) )
75 71 72 73 74 onprcf1of1orad 
 |-  ( ( ph /\ -. A e. _V ) -> ( H o. ( `' F |` B ) ) : B -1-1-> A )
76 iffalse 
 |-  ( -. A e. _V -> if ( A e. _V , if ( B e. _V , K , ( I o. ( `' F |` A ) ) ) , ( H o. ( `' F |` B ) ) ) = ( H o. ( `' F |` B ) ) )
77 4 76 eqtrid 
 |-  ( -. A e. _V -> J = ( H o. ( `' F |` B ) ) )
78 f1eq1 
 |-  ( J = ( H o. ( `' F |` B ) ) -> ( J : B -1-1-> A <-> ( H o. ( `' F |` B ) ) : B -1-1-> A ) )
79 77 78 syl 
 |-  ( -. A e. _V -> ( J : B -1-1-> A <-> ( H o. ( `' F |` B ) ) : B -1-1-> A ) )
80 79 adantl 
 |-  ( ( ph /\ -. A e. _V ) -> ( J : B -1-1-> A <-> ( H o. ( `' F |` B ) ) : B -1-1-> A ) )
81 75 80 mpbird 
 |-  ( ( ph /\ -. A e. _V ) -> J : B -1-1-> A )
82 81 olcd 
 |-  ( ( ph /\ -. A e. _V ) -> ( J : A -1-1-> B \/ J : B -1-1-> A ) )
83 70 82 pm2.61dan 
 |-  ( ph -> ( J : A -1-1-> B \/ J : B -1-1-> A ) )