onvf1od

Description: If G is a global choice function, then F is a bijection from the ordinals to the universe. This is the ZFC version of (1 -> 2) in https://tinyurl.com/hamkins-gblac . (Contributed by BTernaryTau, 5-Dec-2025)

	Ref	Expression
Hypotheses	onvf1od.1	$⊢ φ \to \forall z (z \neq \emptyset \to G (z) \in z)$
	onvf1od.2	$⊢ M = ⋂ \{x \in On \| \exists y \in R_{1} (x) \neg y \in ran w\}$
	onvf1od.3	$⊢ N = G (R_{1} (M) ∖ ran w)$
	onvf1od.4	$⊢ F = recs ((w \in V ⟼ N))$
Assertion	onvf1od	$⊢ φ \to F : On \underset{1-1 onto}{⟶} V$

Proof

Step	Hyp	Ref	Expression
1		onvf1od.1	$⊢ φ \to \forall z (z \neq \emptyset \to G (z) \in z)$
2		onvf1od.2	$⊢ M = ⋂ \{x \in On \| \exists y \in R_{1} (x) \neg y \in ran w\}$
3		onvf1od.3	$⊢ N = G (R_{1} (M) ∖ ran w)$
4		onvf1od.4	$⊢ F = recs ((w \in V ⟼ N))$
5	4	tfr1	$⊢ F Fn On$
6		dffn2	$⊢ F Fn On \leftrightarrow F : On ⟶ V$
7	5 6	mpbi	$⊢ F : On ⟶ V$
8		eqid	$⊢ ⋂ \{u \in On \| \exists v \in R_{1} (u) \neg v \in F [t]\} = ⋂ \{u \in On \| \exists v \in R_{1} (u) \neg v \in F [t]\}$
9		eqid	$⊢ G (R_{1} (⋂ \{u \in On \| \exists v \in R_{1} (u) \neg v \in F [t]\}) ∖ F [t]) = G (R_{1} (⋂ \{u \in On \| \exists v \in R_{1} (u) \neg v \in F [t]\}) ∖ F [t])$
10	2 3 4 8 9	onvf1odlem3	$⊢ t \in On \to F (t) = G (R_{1} (⋂ \{u \in On \| \exists v \in R_{1} (u) \neg v \in F [t]\}) ∖ F [t])$
11	10	adantl	$⊢ (φ \land t \in On) \to F (t) = G (R_{1} (⋂ \{u \in On \| \exists v \in R_{1} (u) \neg v \in F [t]\}) ∖ F [t])$
12		fnfun	$⊢ F Fn On \to Fun F$
13		vex	$⊢ t \in V$
14	13	funimaex	$⊢ Fun F \to F [t] \in V$
15	5 12 14	mp2b	$⊢ F [t] \in V$
16	1 8 9	onvf1odlem2	$⊢ φ \to (F [t] \in V \to G (R_{1} (⋂ \{u \in On \| \exists v \in R_{1} (u) \neg v \in F [t]\}) ∖ F [t]) \in (R_{1} (⋂ \{u \in On \| \exists v \in R_{1} (u) \neg v \in F [t]\}) ∖ F [t]))$
17	15 16	mpi	$⊢ φ \to G (R_{1} (⋂ \{u \in On \| \exists v \in R_{1} (u) \neg v \in F [t]\}) ∖ F [t]) \in (R_{1} (⋂ \{u \in On \| \exists v \in R_{1} (u) \neg v \in F [t]\}) ∖ F [t])$
18	17	eldifbd	$⊢ φ \to \neg G (R_{1} (⋂ \{u \in On \| \exists v \in R_{1} (u) \neg v \in F [t]\}) ∖ F [t]) \in F [t]$
19	18	adantr	$⊢ (φ \land t \in On) \to \neg G (R_{1} (⋂ \{u \in On \| \exists v \in R_{1} (u) \neg v \in F [t]\}) ∖ F [t]) \in F [t]$
20	11 19	eqneltrd	$⊢ (φ \land t \in On) \to \neg F (t) \in F [t]$
21	20	ralrimiva	$⊢ φ \to \forall t \in On \neg F (t) \in F [t]$
22		fvex	$⊢ F (t) \in V$
23		eldif	$⊢ F (t) \in (V ∖ F [t]) \leftrightarrow (F (t) \in V \land \neg F (t) \in F [t])$
24	22 23	mpbiran	$⊢ F (t) \in (V ∖ F [t]) \leftrightarrow \neg F (t) \in F [t]$
25	24	ralbii	$⊢ \forall t \in On F (t) \in (V ∖ F [t]) \leftrightarrow \forall t \in On \neg F (t) \in F [t]$
26	5	tz7.48-2	$⊢ \forall t \in On F (t) \in (V ∖ F [t]) \to Fun F^{-1}$
27	25 26	sylbir	$⊢ \forall t \in On \neg F (t) \in F [t] \to Fun F^{-1}$
28	21 27	syl	$⊢ φ \to Fun F^{-1}$
29		df-f1	$⊢ F : On \underset{1-1}{⟶} V \leftrightarrow (F : On ⟶ V \land Fun F^{-1})$
30	29	biimpri	$⊢ (F : On ⟶ V \land Fun F^{-1}) \to F : On \underset{1-1}{⟶} V$
31	7 28 30	sylancr	$⊢ φ \to F : On \underset{1-1}{⟶} V$
32		onprc	$⊢ \neg On \in V$
33		f1f1orn	$⊢ F : On \underset{1-1}{⟶} V \to F : On \underset{1-1 onto}{⟶} ran F$
34		f1of1	$⊢ F : On \underset{1-1 onto}{⟶} ran F \to F : On \underset{1-1}{⟶} ran F$
35	31 33 34	3syl	$⊢ φ \to F : On \underset{1-1}{⟶} ran F$
36		f1dmex	$⊢ (F : On \underset{1-1}{⟶} ran F \land ran F \in V) \to On \in V$
37	35 36	sylan	$⊢ (φ \land ran F \in V) \to On \in V$
38	37	stoic1a	$⊢ (φ \land \neg On \in V) \to \neg ran F \in V$
39	32 38	mpan2	$⊢ φ \to \neg ran F \in V$
40	1 2 3 4 8 9	onvf1odlem4	$⊢ φ \to (\neg ran F \in V \to ran F = V)$
41	39 40	mpd	$⊢ φ \to ran F = V$
42		dff1o5	$⊢ F : On \underset{1-1 onto}{⟶} V \leftrightarrow (F : On \underset{1-1}{⟶} V \land ran F = V)$
43	31 41 42	sylanbrc	$⊢ φ \to F : On \underset{1-1 onto}{⟶} V$

Metamath Proof Explorer

Theorem onvf1od

Proof