Metamath Proof Explorer

Theorem vonf1onprcf1ac

Description: If F maps the universe one-to-one into the ordinals and A is a proper class, then I maps the ordinals one-to-one into A and the Axiom of Choice holds. This is the ZFC version of (6 -> 7) in https://tinyurl.com/hamkins-gblac . Note that in NBG set theory the first hypothesis would be something like ph -> A. X E. F F : X -1-1-> On , but since we cannot quantify over classes, we instead consider only the case X = _V which is sufficient for this proof. (Contributed by BTernaryTau, 22-Jun-2026)

Ref Expression
Hypotheses vonf1onprcf1ac.1 ⊢ ( 𝜑 → 𝐹 : V –1-1→ On )
vonf1onprcf1ac.2 ⊢ ( 𝜑 → ¬ 𝐴 ∈ V )
vonf1onprcf1ac.3 ⊢ 𝐼 = ( ◡ ( 𝐹 ↾ 𝐴 ) ∘ 𝐻 )
vonf1onprcf1ac.4 ⊢ 𝐻 = OrdIso ( E , ( 𝐹 “ 𝐴 ) )
Assertion vonf1onprcf1ac ( 𝜑 → ( 𝐼 : On –1-1→ 𝐴 ∧ CHOICE ) )

Proof

Step Hyp Ref Expression
1 vonf1onprcf1ac.1 ⊢ ( 𝜑 → 𝐹 : V –1-1→ On )
2 vonf1onprcf1ac.2 ⊢ ( 𝜑 → ¬ 𝐴 ∈ V )
3 vonf1onprcf1ac.3 ⊢ 𝐼 = ( ◡ ( 𝐹 ↾ 𝐴 ) ∘ 𝐻 )
4 vonf1onprcf1ac.4 ⊢ 𝐻 = OrdIso ( E , ( 𝐹 “ 𝐴 ) )
5 ssv ⊢ 𝐴 ⊆ V
6 f1ores ⊢ ( ( 𝐹 : V –1-1→ On ∧ 𝐴 ⊆ V ) → ( 𝐹 ↾ 𝐴 ) : 𝐴 –1-1-onto→ ( 𝐹 “ 𝐴 ) )
7 1 5 6 sylancl ⊢ ( 𝜑 → ( 𝐹 ↾ 𝐴 ) : 𝐴 –1-1-onto→ ( 𝐹 “ 𝐴 ) )
8 f1ocnv ⊢ ( ( 𝐹 ↾ 𝐴 ) : 𝐴 –1-1-onto→ ( 𝐹 “ 𝐴 ) → ◡ ( 𝐹 ↾ 𝐴 ) : ( 𝐹 “ 𝐴 ) –1-1-onto→ 𝐴 )
9 7 8 syl ⊢ ( 𝜑 → ◡ ( 𝐹 ↾ 𝐴 ) : ( 𝐹 “ 𝐴 ) –1-1-onto→ 𝐴 )
10 f1f ⊢ ( 𝐹 : V –1-1→ On → 𝐹 : V ⟶ On )
11 1 10 syl ⊢ ( 𝜑 → 𝐹 : V ⟶ On )
12 11 fimassd ⊢ ( 𝜑 → ( 𝐹 “ 𝐴 ) ⊆ On )
13 f1preimaex ⊢ ( ( 𝐹 : V –1-1→ On ∧ 𝐴 ⊆ V ∧ ( 𝐹 “ 𝐴 ) ∈ V ) → 𝐴 ∈ V )
14 5 13 mp3an2 ⊢ ( ( 𝐹 : V –1-1→ On ∧ ( 𝐹 “ 𝐴 ) ∈ V ) → 𝐴 ∈ V )
15 14 ex ⊢ ( 𝐹 : V –1-1→ On → ( ( 𝐹 “ 𝐴 ) ∈ V → 𝐴 ∈ V ) )
16 1 15 syl ⊢ ( 𝜑 → ( ( 𝐹 “ 𝐴 ) ∈ V → 𝐴 ∈ V ) )
17 2 16 mtod ⊢ ( 𝜑 → ¬ ( 𝐹 “ 𝐴 ) ∈ V )
18 epweon ⊢ E We On
19 wess ⊢ ( ( 𝐹 “ 𝐴 ) ⊆ On → ( E We On → E We ( 𝐹 “ 𝐴 ) ) )
20 18 19 mpi ⊢ ( ( 𝐹 “ 𝐴 ) ⊆ On → E We ( 𝐹 “ 𝐴 ) )
21 epse ⊢ E Se ( 𝐹 “ 𝐴 )
22 4 ordtypeon ⊢ ( ( E We ( 𝐹 “ 𝐴 ) ∧ E Se ( 𝐹 “ 𝐴 ) ∧ ¬ ( 𝐹 “ 𝐴 ) ∈ V ) → 𝐻 Isom E , E ( On , ( 𝐹 “ 𝐴 ) ) )
23 21 22 mp3an2 ⊢ ( ( E We ( 𝐹 “ 𝐴 ) ∧ ¬ ( 𝐹 “ 𝐴 ) ∈ V ) → 𝐻 Isom E , E ( On , ( 𝐹 “ 𝐴 ) ) )
24 20 23 sylan ⊢ ( ( ( 𝐹 “ 𝐴 ) ⊆ On ∧ ¬ ( 𝐹 “ 𝐴 ) ∈ V ) → 𝐻 Isom E , E ( On , ( 𝐹 “ 𝐴 ) ) )
25 12 17 24 syl2anc ⊢ ( 𝜑 → 𝐻 Isom E , E ( On , ( 𝐹 “ 𝐴 ) ) )
26 isof1o ⊢ ( 𝐻 Isom E , E ( On , ( 𝐹 “ 𝐴 ) ) → 𝐻 : On –1-1-onto→ ( 𝐹 “ 𝐴 ) )
27 25 26 syl ⊢ ( 𝜑 → 𝐻 : On –1-1-onto→ ( 𝐹 “ 𝐴 ) )
28 f1oco ⊢ ( ( ◡ ( 𝐹 ↾ 𝐴 ) : ( 𝐹 “ 𝐴 ) –1-1-onto→ 𝐴 ∧ 𝐻 : On –1-1-onto→ ( 𝐹 “ 𝐴 ) ) → ( ◡ ( 𝐹 ↾ 𝐴 ) ∘ 𝐻 ) : On –1-1-onto→ 𝐴 )
29 9 27 28 syl2anc ⊢ ( 𝜑 → ( ◡ ( 𝐹 ↾ 𝐴 ) ∘ 𝐻 ) : On –1-1-onto→ 𝐴 )
30 3 a1i ⊢ ( 𝜑 → 𝐼 = ( ◡ ( 𝐹 ↾ 𝐴 ) ∘ 𝐻 ) )
31 30 f1oeq1d ⊢ ( 𝜑 → ( 𝐼 : On –1-1-onto→ 𝐴 ↔ ( ◡ ( 𝐹 ↾ 𝐴 ) ∘ 𝐻 ) : On –1-1-onto→ 𝐴 ) )
32 29 31 mpbird ⊢ ( 𝜑 → 𝐼 : On –1-1-onto→ 𝐴 )
33 f1of1 ⊢ ( 𝐼 : On –1-1-onto→ 𝐴 → 𝐼 : On –1-1→ 𝐴 )
34 32 33 syl ⊢ ( 𝜑 → 𝐼 : On –1-1→ 𝐴 )
35 eqid ⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐹 ‘ 𝑦 ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐹 ‘ 𝑦 ) }
36 35 vonf1wev ⊢ ( 𝐹 : V –1-1→ On → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐹 ‘ 𝑦 ) } We V )
37 ssv ⊢ 𝑧 ⊆ V
38 wess ⊢ ( 𝑧 ⊆ V → ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐹 ‘ 𝑦 ) } We V → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐹 ‘ 𝑦 ) } We 𝑧 ) )
39 37 38 ax-mp ⊢ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐹 ‘ 𝑦 ) } We V → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐹 ‘ 𝑦 ) } We 𝑧 )
40 1 36 39 3syl ⊢ ( 𝜑 → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐹 ‘ 𝑦 ) } We 𝑧 )
41 weinxp ⊢ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐹 ‘ 𝑦 ) } We 𝑧 ↔ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐹 ‘ 𝑦 ) } ∩ ( 𝑧 × 𝑧 ) ) We 𝑧 )
42 vex ⊢ 𝑧 ∈ V
43 42 42 xpex ⊢ ( 𝑧 × 𝑧 ) ∈ V
44 43 inex2 ⊢ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐹 ‘ 𝑦 ) } ∩ ( 𝑧 × 𝑧 ) ) ∈ V
45 weeq1 ⊢ ( 𝑤 = ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐹 ‘ 𝑦 ) } ∩ ( 𝑧 × 𝑧 ) ) → ( 𝑤 We 𝑧 ↔ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐹 ‘ 𝑦 ) } ∩ ( 𝑧 × 𝑧 ) ) We 𝑧 ) )
46 44 45 spcev ⊢ ( ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐹 ‘ 𝑦 ) } ∩ ( 𝑧 × 𝑧 ) ) We 𝑧 → ∃ 𝑤 𝑤 We 𝑧 )
47 41 46 sylbi ⊢ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐹 ‘ 𝑦 ) } We 𝑧 → ∃ 𝑤 𝑤 We 𝑧 )
48 40 47 syl ⊢ ( 𝜑 → ∃ 𝑤 𝑤 We 𝑧 )
49 48 alrimiv ⊢ ( 𝜑 → ∀ 𝑧 ∃ 𝑤 𝑤 We 𝑧 )
50 dfac8 ⊢ ( CHOICE ↔ ∀ 𝑧 ∃ 𝑤 𝑤 We 𝑧 )
51 49 50 sylibr ⊢ ( 𝜑 → CHOICE )
52 34 51 jca ⊢ ( 𝜑 → ( 𝐼 : On –1-1→ 𝐴 ∧ CHOICE ) )