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	$⊢ φ \to F : V \underset{1-1}{⟶} On$
	vonf1onprcf1ac.2	$⊢ φ \to \neg A \in V$
	vonf1onprcf1ac.3	$⊢ I = {({F ↾}_{A})}^{-1} \circ H$
	vonf1onprcf1ac.4	$⊢ H = OrdIso (E, F [A])$
Assertion	vonf1onprcf1ac	$⊢ φ \to (I : On \underset{1-1}{⟶} A \land CHOICE)$

Proof

Step	Hyp	Ref	Expression
1		vonf1onprcf1ac.1	$⊢ φ \to F : V \underset{1-1}{⟶} On$
2		vonf1onprcf1ac.2	$⊢ φ \to \neg A \in V$
3		vonf1onprcf1ac.3	$⊢ I = {({F ↾}_{A})}^{-1} \circ H$
4		vonf1onprcf1ac.4	$⊢ H = OrdIso (E, F [A])$
5		ssv	$⊢ A \subseteq V$
6		f1ores	$⊢ (F : V \underset{1-1}{⟶} On \land A \subseteq V) \to ({F ↾}_{A}) : A \underset{1-1 onto}{⟶} F [A]$
7	1 5 6	sylancl	$⊢ φ \to ({F ↾}_{A}) : A \underset{1-1 onto}{⟶} F [A]$
8		f1ocnv	$⊢ ({F ↾}_{A}) : A \underset{1-1 onto}{⟶} F [A] \to {({F ↾}_{A})}^{-1} : F [A] \underset{1-1 onto}{⟶} A$
9	7 8	syl	$⊢ φ \to {({F ↾}_{A})}^{-1} : F [A] \underset{1-1 onto}{⟶} A$
10		f1f	$⊢ F : V \underset{1-1}{⟶} On \to F : V ⟶ On$
11	1 10	syl	$⊢ φ \to F : V ⟶ On$
12	11	fimassd	$⊢ φ \to F [A] \subseteq On$
13		f1preimaex	$⊢ (F : V \underset{1-1}{⟶} On \land A \subseteq V \land F [A] \in V) \to A \in V$
14	5 13	mp3an2	$⊢ (F : V \underset{1-1}{⟶} On \land F [A] \in V) \to A \in V$
15	14	ex	$⊢ F : V \underset{1-1}{⟶} On \to (F [A] \in V \to A \in V)$
16	1 15	syl	$⊢ φ \to (F [A] \in V \to A \in V)$
17	2 16	mtod	$⊢ φ \to \neg F [A] \in V$
18		epweon	$⊢ E We On$
19		wess	$⊢ F [A] \subseteq On \to (E We On \to E We F [A])$
20	18 19	mpi	$⊢ F [A] \subseteq On \to E We F [A]$
21		epse	$⊢ E Se F [A]$
22	4	ordtypeon	$⊢ (E We F [A] \land E Se F [A] \land \neg F [A] \in V) \to H {Isom}_{E, E} (On, F [A])$
23	21 22	mp3an2	$⊢ (E We F [A] \land \neg F [A] \in V) \to H {Isom}_{E, E} (On, F [A])$
24	20 23	sylan	$⊢ (F [A] \subseteq On \land \neg F [A] \in V) \to H {Isom}_{E, E} (On, F [A])$
25	12 17 24	syl2anc	$⊢ φ \to H {Isom}_{E, E} (On, F [A])$
26		isof1o	$⊢ H {Isom}_{E, E} (On, F [A]) \to H : On \underset{1-1 onto}{⟶} F [A]$
27	25 26	syl	$⊢ φ \to H : On \underset{1-1 onto}{⟶} F [A]$
28		f1oco	$⊢ ({({F ↾}_{A})}^{-1} : F [A] \underset{1-1 onto}{⟶} A \land H : On \underset{1-1 onto}{⟶} F [A]) \to ({({F ↾}_{A})}^{-1} \circ H) : On \underset{1-1 onto}{⟶} A$
29	9 27 28	syl2anc	$⊢ φ \to ({({F ↾}_{A})}^{-1} \circ H) : On \underset{1-1 onto}{⟶} A$
30	3	a1i	$⊢ φ \to I = {({F ↾}_{A})}^{-1} \circ H$
31	30	f1oeq1d	$⊢ φ \to (I : On \underset{1-1 onto}{⟶} A \leftrightarrow ({({F ↾}_{A})}^{-1} \circ H) : On \underset{1-1 onto}{⟶} A)$
32	29 31	mpbird	$⊢ φ \to I : On \underset{1-1 onto}{⟶} A$
33		f1of1	$⊢ I : On \underset{1-1 onto}{⟶} A \to I : On \underset{1-1}{⟶} A$
34	32 33	syl	$⊢ φ \to I : On \underset{1-1}{⟶} A$
35		eqid	$⊢ \{⟨x, y⟩ \| F (x) \in F (y)\} = \{⟨x, y⟩ \| F (x) \in F (y)\}$
36	35	vonf1wev	$⊢ F : V \underset{1-1}{⟶} On \to \{⟨x, y⟩ \| F (x) \in F (y)\} We V$
37		ssv	$⊢ z \subseteq V$
38		wess	$⊢ z \subseteq V \to (\{⟨x, y⟩ \| F (x) \in F (y)\} We V \to \{⟨x, y⟩ \| F (x) \in F (y)\} We z)$
39	37 38	ax-mp	$⊢ \{⟨x, y⟩ \| F (x) \in F (y)\} We V \to \{⟨x, y⟩ \| F (x) \in F (y)\} We z$
40	1 36 39	3syl	$⊢ φ \to \{⟨x, y⟩ \| F (x) \in F (y)\} We z$
41		weinxp	$⊢ \{⟨x, y⟩ \| F (x) \in F (y)\} We z \leftrightarrow (\{⟨x, y⟩ \| F (x) \in F (y)\} \cap (z \times z)) We z$
42		vex	$⊢ z \in V$
43	42 42	xpex	$⊢ z \times z \in V$
44	43	inex2	$⊢ \{⟨x, y⟩ \| F (x) \in F (y)\} \cap (z \times z) \in V$
45		weeq1	$⊢ w = \{⟨x, y⟩ \| F (x) \in F (y)\} \cap (z \times z) \to (w We z \leftrightarrow (\{⟨x, y⟩ \| F (x) \in F (y)\} \cap (z \times z)) We z)$
46	44 45	spcev	$⊢ (\{⟨x, y⟩ \| F (x) \in F (y)\} \cap (z \times z)) We z \to \exists w w We z$
47	41 46	sylbi	$⊢ \{⟨x, y⟩ \| F (x) \in F (y)\} We z \to \exists w w We z$
48	40 47	syl	$⊢ φ \to \exists w w We z$
49	48	alrimiv	$⊢ φ \to \forall z \exists w w We z$
50		dfac8	$⊢ CHOICE \leftrightarrow \forall z \exists w w We z$
51	49 50	sylibr	$⊢ φ \to CHOICE$
52	34 51	jca	$⊢ φ \to (I : On \underset{1-1}{⟶} A \land CHOICE)$

Metamath Proof Explorer

Theorem vonf1onprcf1ac

Proof