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 ⊢ φ → F : On ⟶ 1-1 onto V
onprcf1of1ord.2 ⊢ φ → ¬ A ∈ V → H : On ⟶ 1-1 onto A
onprcf1of1ord.3 ⊢ φ → ¬ B ∈ V → I : On ⟶ 1-1 onto B
onprcf1of1ord.4 ⊢ J = if A ∈ V if B ∈ V K I ∘ F -1 ↾ A H ∘ F -1 ↾ B
onprcf1of1ord.5 ⊢ K = F ⁡ ⋂ x ∈ On | F ⁡ x : A ⟶ 1-1 B ∨ F ⁡ x : B ⟶ 1-1 A
Assertion onprcf1of1ord ⊢ φ → J : A ⟶ 1-1 B ∨ J : B ⟶ 1-1 A

Proof

Step Hyp Ref Expression
1 onprcf1of1ord.1 ⊢ φ → F : On ⟶ 1-1 onto V
2 onprcf1of1ord.2 ⊢ φ → ¬ A ∈ V → H : On ⟶ 1-1 onto A
3 onprcf1of1ord.3 ⊢ φ → ¬ B ∈ V → I : On ⟶ 1-1 onto B
4 onprcf1of1ord.4 ⊢ J = if A ∈ V if B ∈ V K I ∘ F -1 ↾ A H ∘ F -1 ↾ B
5 onprcf1of1ord.5 ⊢ K = F ⁡ ⋂ x ∈ On | F ⁡ x : A ⟶ 1-1 B ∨ F ⁡ x : B ⟶ 1-1 A
6 1 ad2antrr ⊢ φ ∧ A ∈ V ∧ B ∈ V → F : On ⟶ 1-1 onto V
7 simplr ⊢ φ ∧ A ∈ V ∧ B ∈ V → A ∈ V
8 simpr ⊢ φ ∧ A ∈ V ∧ B ∈ V → B ∈ V
9 6 7 8 onprcf1of1orbd ⊢ φ ∧ A ∈ V ∧ B ∈ V → ∃ f f : A ⟶ 1-1 B ∨ ∃ f f : B ⟶ 1-1 A
10 19.43 ⊢ ∃ f f : A ⟶ 1-1 B ∨ f : B ⟶ 1-1 A ↔ ∃ f f : A ⟶ 1-1 B ∨ ∃ f f : B ⟶ 1-1 A
11 9 10 sylibr ⊢ φ ∧ A ∈ V ∧ B ∈ V → ∃ 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 ⊢ φ → ran ⁡ F = V
15 14 rexeqdv ⊢ φ → ∃ f ∈ ran ⁡ F f : A ⟶ 1-1 B ∨ f : B ⟶ 1-1 A ↔ ∃ f ∈ V f : A ⟶ 1-1 B ∨ f : B ⟶ 1-1 A
16 rexv ⊢ ∃ f ∈ V f : A ⟶ 1-1 B ∨ f : B ⟶ 1-1 A ↔ ∃ f f : A ⟶ 1-1 B ∨ f : B ⟶ 1-1 A
17 15 16 bitrdi ⊢ φ → ∃ f ∈ ran ⁡ F f : A ⟶ 1-1 B ∨ f : B ⟶ 1-1 A ↔ ∃ 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 → ∃ f ∈ ran ⁡ F f : A ⟶ 1-1 B ∨ f : B ⟶ 1-1 A ↔ ∃ x ∈ On F ⁡ x : A ⟶ 1-1 B ∨ F ⁡ x : B ⟶ 1-1 A
23 1 18 22 3syl ⊢ φ → ∃ f ∈ ran ⁡ F f : A ⟶ 1-1 B ∨ f : B ⟶ 1-1 A ↔ ∃ x ∈ On F ⁡ x : A ⟶ 1-1 B ∨ F ⁡ x : B ⟶ 1-1 A
24 17 23 bitr3d ⊢ φ → ∃ f f : A ⟶ 1-1 B ∨ f : B ⟶ 1-1 A ↔ ∃ x ∈ On F ⁡ x : A ⟶ 1-1 B ∨ F ⁡ x : B ⟶ 1-1 A
25 24 ad2antrr ⊢ φ ∧ A ∈ V ∧ B ∈ V → ∃ f f : A ⟶ 1-1 B ∨ f : B ⟶ 1-1 A ↔ ∃ x ∈ On F ⁡ x : A ⟶ 1-1 B ∨ F ⁡ x : B ⟶ 1-1 A
26 11 25 mpbid ⊢ φ ∧ A ∈ V ∧ B ∈ V → ∃ x ∈ On F ⁡ x : A ⟶ 1-1 B ∨ F ⁡ x : B ⟶ 1-1 A
27 nfcv ⊢ Ⅎ _ x F
28 nfrab1 ⊢ Ⅎ _ x x ∈ On | F ⁡ x : A ⟶ 1-1 B ∨ F ⁡ x : B ⟶ 1-1 A
29 28 nfint ⊢ Ⅎ _ x ⋂ x ∈ On | F ⁡ x : A ⟶ 1-1 B ∨ F ⁡ x : B ⟶ 1-1 A
30 27 29 nffv ⊢ Ⅎ _ x F ⁡ ⋂ x ∈ On | F ⁡ x : A ⟶ 1-1 B ∨ F ⁡ x : B ⟶ 1-1 A
31 nfcv ⊢ Ⅎ _ x A
32 nfcv ⊢ Ⅎ _ x B
33 30 31 32 nff1 ⊢ Ⅎ x F ⁡ ⋂ x ∈ On | F ⁡ x : A ⟶ 1-1 B ∨ F ⁡ x : B ⟶ 1-1 A : A ⟶ 1-1 B
34 30 32 31 nff1 ⊢ Ⅎ x F ⁡ ⋂ x ∈ On | F ⁡ x : A ⟶ 1-1 B ∨ F ⁡ x : B ⟶ 1-1 A : B ⟶ 1-1 A
35 33 34 nfor ⊢ Ⅎ x F ⁡ ⋂ x ∈ On | F ⁡ x : A ⟶ 1-1 B ∨ F ⁡ x : B ⟶ 1-1 A : A ⟶ 1-1 B ∨ F ⁡ ⋂ x ∈ On | F ⁡ x : A ⟶ 1-1 B ∨ F ⁡ x : B ⟶ 1-1 A : B ⟶ 1-1 A
36 fveq2 ⊢ x = ⋂ x ∈ On | F ⁡ x : A ⟶ 1-1 B ∨ F ⁡ x : B ⟶ 1-1 A → F ⁡ x = F ⁡ ⋂ x ∈ On | F ⁡ x : A ⟶ 1-1 B ∨ F ⁡ x : B ⟶ 1-1 A
37 f1eq1 ⊢ F ⁡ x = F ⁡ ⋂ x ∈ On | F ⁡ x : A ⟶ 1-1 B ∨ F ⁡ x : B ⟶ 1-1 A → F ⁡ x : A ⟶ 1-1 B ↔ F ⁡ ⋂ x ∈ On | F ⁡ x : A ⟶ 1-1 B ∨ F ⁡ x : B ⟶ 1-1 A : A ⟶ 1-1 B
38 36 37 syl ⊢ x = ⋂ x ∈ On | F ⁡ x : A ⟶ 1-1 B ∨ F ⁡ x : B ⟶ 1-1 A → F ⁡ x : A ⟶ 1-1 B ↔ F ⁡ ⋂ x ∈ On | F ⁡ x : A ⟶ 1-1 B ∨ F ⁡ x : B ⟶ 1-1 A : A ⟶ 1-1 B
39 f1eq1 ⊢ F ⁡ x = F ⁡ ⋂ x ∈ On | F ⁡ x : A ⟶ 1-1 B ∨ F ⁡ x : B ⟶ 1-1 A → F ⁡ x : B ⟶ 1-1 A ↔ F ⁡ ⋂ x ∈ On | F ⁡ x : A ⟶ 1-1 B ∨ F ⁡ x : B ⟶ 1-1 A : B ⟶ 1-1 A
40 36 39 syl ⊢ x = ⋂ x ∈ On | F ⁡ x : A ⟶ 1-1 B ∨ F ⁡ x : B ⟶ 1-1 A → F ⁡ x : B ⟶ 1-1 A ↔ F ⁡ ⋂ x ∈ On | F ⁡ x : A ⟶ 1-1 B ∨ F ⁡ x : B ⟶ 1-1 A : B ⟶ 1-1 A
41 38 40 orbi12d ⊢ x = ⋂ x ∈ 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 ∈ On | F ⁡ x : A ⟶ 1-1 B ∨ F ⁡ x : B ⟶ 1-1 A : A ⟶ 1-1 B ∨ F ⁡ ⋂ x ∈ On | F ⁡ x : A ⟶ 1-1 B ∨ F ⁡ x : B ⟶ 1-1 A : B ⟶ 1-1 A
42 35 41 onminsb ⊢ ∃ x ∈ On F ⁡ x : A ⟶ 1-1 B ∨ F ⁡ x : B ⟶ 1-1 A → F ⁡ ⋂ x ∈ On | F ⁡ x : A ⟶ 1-1 B ∨ F ⁡ x : B ⟶ 1-1 A : A ⟶ 1-1 B ∨ F ⁡ ⋂ x ∈ On | F ⁡ x : A ⟶ 1-1 B ∨ F ⁡ x : B ⟶ 1-1 A : B ⟶ 1-1 A
43 26 42 syl ⊢ φ ∧ A ∈ V ∧ B ∈ V → F ⁡ ⋂ x ∈ On | F ⁡ x : A ⟶ 1-1 B ∨ F ⁡ x : B ⟶ 1-1 A : A ⟶ 1-1 B ∨ F ⁡ ⋂ x ∈ On | F ⁡ x : A ⟶ 1-1 B ∨ F ⁡ x : B ⟶ 1-1 A : B ⟶ 1-1 A
44 iftrue ⊢ A ∈ V → if A ∈ V if B ∈ V K I ∘ F -1 ↾ A H ∘ F -1 ↾ B = if B ∈ V K I ∘ F -1 ↾ A
45 4 44 eqtrid ⊢ A ∈ V → J = if B ∈ V K I ∘ F -1 ↾ A
46 45 ad2antlr ⊢ φ ∧ A ∈ V ∧ B ∈ V → J = if B ∈ V K I ∘ F -1 ↾ A
47 iftrue ⊢ B ∈ V → if B ∈ V K I ∘ F -1 ↾ A = K
48 47 adantl ⊢ φ ∧ A ∈ V ∧ B ∈ V → if B ∈ V K I ∘ F -1 ↾ A = K
49 46 48 eqtrd ⊢ φ ∧ A ∈ V ∧ B ∈ V → J = K
50 49 5 eqtrdi ⊢ φ ∧ A ∈ V ∧ B ∈ V → J = F ⁡ ⋂ x ∈ On | F ⁡ x : A ⟶ 1-1 B ∨ F ⁡ x : B ⟶ 1-1 A
51 f1eq1 ⊢ J = F ⁡ ⋂ x ∈ On | F ⁡ x : A ⟶ 1-1 B ∨ F ⁡ x : B ⟶ 1-1 A → J : A ⟶ 1-1 B ↔ F ⁡ ⋂ x ∈ On | F ⁡ x : A ⟶ 1-1 B ∨ F ⁡ x : B ⟶ 1-1 A : A ⟶ 1-1 B
52 50 51 syl ⊢ φ ∧ A ∈ V ∧ B ∈ V → J : A ⟶ 1-1 B ↔ F ⁡ ⋂ x ∈ On | F ⁡ x : A ⟶ 1-1 B ∨ F ⁡ x : B ⟶ 1-1 A : A ⟶ 1-1 B
53 f1eq1 ⊢ J = F ⁡ ⋂ x ∈ On | F ⁡ x : A ⟶ 1-1 B ∨ F ⁡ x : B ⟶ 1-1 A → J : B ⟶ 1-1 A ↔ F ⁡ ⋂ x ∈ On | F ⁡ x : A ⟶ 1-1 B ∨ F ⁡ x : B ⟶ 1-1 A : B ⟶ 1-1 A
54 50 53 syl ⊢ φ ∧ A ∈ V ∧ B ∈ V → J : B ⟶ 1-1 A ↔ F ⁡ ⋂ x ∈ On | F ⁡ x : A ⟶ 1-1 B ∨ F ⁡ x : B ⟶ 1-1 A : B ⟶ 1-1 A
55 52 54 orbi12d ⊢ φ ∧ A ∈ V ∧ B ∈ V → J : A ⟶ 1-1 B ∨ J : B ⟶ 1-1 A ↔ F ⁡ ⋂ x ∈ On | F ⁡ x : A ⟶ 1-1 B ∨ F ⁡ x : B ⟶ 1-1 A : A ⟶ 1-1 B ∨ F ⁡ ⋂ x ∈ On | F ⁡ x : A ⟶ 1-1 B ∨ F ⁡ x : B ⟶ 1-1 A : B ⟶ 1-1 A
56 43 55 mpbird ⊢ φ ∧ A ∈ V ∧ B ∈ V → J : A ⟶ 1-1 B ∨ J : B ⟶ 1-1 A
57 1 ad2antrr ⊢ φ ∧ A ∈ V ∧ ¬ B ∈ V → F : On ⟶ 1-1 onto V
58 3 ad2antrr ⊢ φ ∧ A ∈ V ∧ ¬ B ∈ V → ¬ B ∈ V → I : On ⟶ 1-1 onto B
59 simpr ⊢ φ ∧ A ∈ V ∧ ¬ B ∈ V → ¬ B ∈ V
60 eqid ⊢ I ∘ F -1 ↾ A = I ∘ F -1 ↾ A
61 57 58 59 60 onprcf1of1orad ⊢ φ ∧ A ∈ V ∧ ¬ B ∈ V → I ∘ F -1 ↾ A : A ⟶ 1-1 B
62 45 ad2antlr ⊢ φ ∧ A ∈ V ∧ ¬ B ∈ V → J = if B ∈ V K I ∘ F -1 ↾ A
63 iffalse ⊢ ¬ B ∈ V → if B ∈ V K I ∘ F -1 ↾ A = I ∘ F -1 ↾ A
64 63 adantl ⊢ φ ∧ A ∈ V ∧ ¬ B ∈ V → if B ∈ V K I ∘ F -1 ↾ A = I ∘ F -1 ↾ A
65 62 64 eqtrd ⊢ φ ∧ A ∈ V ∧ ¬ B ∈ V → J = I ∘ F -1 ↾ A
66 f1eq1 ⊢ J = I ∘ F -1 ↾ A → J : A ⟶ 1-1 B ↔ I ∘ F -1 ↾ A : A ⟶ 1-1 B
67 65 66 syl ⊢ φ ∧ A ∈ V ∧ ¬ B ∈ V → J : A ⟶ 1-1 B ↔ I ∘ F -1 ↾ A : A ⟶ 1-1 B
68 61 67 mpbird ⊢ φ ∧ A ∈ V ∧ ¬ B ∈ V → J : A ⟶ 1-1 B
69 68 orcd ⊢ φ ∧ A ∈ V ∧ ¬ B ∈ V → J : A ⟶ 1-1 B ∨ J : B ⟶ 1-1 A
70 56 69 pm2.61dan ⊢ φ ∧ A ∈ V → J : A ⟶ 1-1 B ∨ J : B ⟶ 1-1 A
71 1 adantr ⊢ φ ∧ ¬ A ∈ V → F : On ⟶ 1-1 onto V
72 2 adantr ⊢ φ ∧ ¬ A ∈ V → ¬ A ∈ V → H : On ⟶ 1-1 onto A
73 simpr ⊢ φ ∧ ¬ A ∈ V → ¬ A ∈ V
74 eqid ⊢ H ∘ F -1 ↾ B = H ∘ F -1 ↾ B
75 71 72 73 74 onprcf1of1orad ⊢ φ ∧ ¬ A ∈ V → H ∘ F -1 ↾ B : B ⟶ 1-1 A
76 iffalse ⊢ ¬ A ∈ V → if A ∈ V if B ∈ V K I ∘ F -1 ↾ A H ∘ F -1 ↾ B = H ∘ F -1 ↾ B
77 4 76 eqtrid ⊢ ¬ A ∈ V → J = H ∘ F -1 ↾ B
78 f1eq1 ⊢ J = H ∘ F -1 ↾ B → J : B ⟶ 1-1 A ↔ H ∘ F -1 ↾ B : B ⟶ 1-1 A
79 77 78 syl ⊢ ¬ A ∈ V → J : B ⟶ 1-1 A ↔ H ∘ F -1 ↾ B : B ⟶ 1-1 A
80 79 adantl ⊢ φ ∧ ¬ A ∈ V → J : B ⟶ 1-1 A ↔ H ∘ F -1 ↾ B : B ⟶ 1-1 A
81 75 80 mpbird ⊢ φ ∧ ¬ A ∈ V → J : B ⟶ 1-1 A
82 81 olcd ⊢ φ ∧ ¬ A ∈ V → J : A ⟶ 1-1 B ∨ J : B ⟶ 1-1 A
83 70 82 pm2.61dan ⊢ φ → J : A ⟶ 1-1 B ∨ J : B ⟶ 1-1 A