Theorem 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	⊢ ( 𝜑 → ∀ 𝑧 ( 𝑧 ≠ ∅ → ( 𝐺 ‘ 𝑧 ) ∈ 𝑧 ) )
	onvf1od.2	⊢ 𝑀 = ∩ { 𝑥 ∈ On ∣ ∃ 𝑦 ∈ ( 𝑅1 ‘ 𝑥 ) ¬ 𝑦 ∈ ran 𝑤 }
	onvf1od.3	⊢ 𝑁 = ( 𝐺 ‘ ( ( 𝑅1 ‘ 𝑀 ) ∖ ran 𝑤 ) )
	onvf1od.4	⊢ 𝐹 = recs ( ( 𝑤 ∈ V ↦ 𝑁 ) )
Assertion	onvf1od	⊢ ( 𝜑 → 𝐹 : On –1-1-onto→ V )

Proof

Step	Hyp	Ref	Expression
1		onvf1od.1	⊢ ( 𝜑 → ∀ 𝑧 ( 𝑧 ≠ ∅ → ( 𝐺 ‘ 𝑧 ) ∈ 𝑧 ) )
2		onvf1od.2	⊢ 𝑀 = ∩ { 𝑥 ∈ On ∣ ∃ 𝑦 ∈ ( 𝑅1 ‘ 𝑥 ) ¬ 𝑦 ∈ ran 𝑤 }
3		onvf1od.3	⊢ 𝑁 = ( 𝐺 ‘ ( ( 𝑅1 ‘ 𝑀 ) ∖ ran 𝑤 ) )
4		onvf1od.4	⊢ 𝐹 = recs ( ( 𝑤 ∈ V ↦ 𝑁 ) )
5	4	tfr1	⊢ 𝐹 Fn On
6		dffn2	⊢ ( 𝐹 Fn On ↔ 𝐹 : On ⟶ V )
7	5 6	mpbi	⊢ 𝐹 : On ⟶ V
8		eqid	⊢ ∩ { 𝑢 ∈ On ∣ ∃ 𝑣 ∈ ( 𝑅1 ‘ 𝑢 ) ¬ 𝑣 ∈ ( 𝐹 “ 𝑡 ) } = ∩ { 𝑢 ∈ On ∣ ∃ 𝑣 ∈ ( 𝑅1 ‘ 𝑢 ) ¬ 𝑣 ∈ ( 𝐹 “ 𝑡 ) }
9		eqid	⊢ ( 𝐺 ‘ ( ( 𝑅1 ‘ ∩ { 𝑢 ∈ On ∣ ∃ 𝑣 ∈ ( 𝑅1 ‘ 𝑢 ) ¬ 𝑣 ∈ ( 𝐹 “ 𝑡 ) } ) ∖ ( 𝐹 “ 𝑡 ) ) ) = ( 𝐺 ‘ ( ( 𝑅1 ‘ ∩ { 𝑢 ∈ On ∣ ∃ 𝑣 ∈ ( 𝑅1 ‘ 𝑢 ) ¬ 𝑣 ∈ ( 𝐹 “ 𝑡 ) } ) ∖ ( 𝐹 “ 𝑡 ) ) )
10	2 3 4 8 9	onvf1odlem3	⊢ ( 𝑡 ∈ On → ( 𝐹 ‘ 𝑡 ) = ( 𝐺 ‘ ( ( 𝑅1 ‘ ∩ { 𝑢 ∈ On ∣ ∃ 𝑣 ∈ ( 𝑅1 ‘ 𝑢 ) ¬ 𝑣 ∈ ( 𝐹 “ 𝑡 ) } ) ∖ ( 𝐹 “ 𝑡 ) ) ) )
11	10	adantl	⊢ ( ( 𝜑 ∧ 𝑡 ∈ On ) → ( 𝐹 ‘ 𝑡 ) = ( 𝐺 ‘ ( ( 𝑅1 ‘ ∩ { 𝑢 ∈ On ∣ ∃ 𝑣 ∈ ( 𝑅1 ‘ 𝑢 ) ¬ 𝑣 ∈ ( 𝐹 “ 𝑡 ) } ) ∖ ( 𝐹 “ 𝑡 ) ) ) )
12		fnfun	⊢ ( 𝐹 Fn On → Fun 𝐹 )
13		vex	⊢ 𝑡 ∈ V
14	13	funimaex	⊢ ( Fun 𝐹 → ( 𝐹 “ 𝑡 ) ∈ V )
15	5 12 14	mp2b	⊢ ( 𝐹 “ 𝑡 ) ∈ V
16	1 8 9	onvf1odlem2	⊢ ( 𝜑 → ( ( 𝐹 “ 𝑡 ) ∈ V → ( 𝐺 ‘ ( ( 𝑅1 ‘ ∩ { 𝑢 ∈ On ∣ ∃ 𝑣 ∈ ( 𝑅1 ‘ 𝑢 ) ¬ 𝑣 ∈ ( 𝐹 “ 𝑡 ) } ) ∖ ( 𝐹 “ 𝑡 ) ) ) ∈ ( ( 𝑅1 ‘ ∩ { 𝑢 ∈ On ∣ ∃ 𝑣 ∈ ( 𝑅1 ‘ 𝑢 ) ¬ 𝑣 ∈ ( 𝐹 “ 𝑡 ) } ) ∖ ( 𝐹 “ 𝑡 ) ) ) )
17	15 16	mpi	⊢ ( 𝜑 → ( 𝐺 ‘ ( ( 𝑅1 ‘ ∩ { 𝑢 ∈ On ∣ ∃ 𝑣 ∈ ( 𝑅1 ‘ 𝑢 ) ¬ 𝑣 ∈ ( 𝐹 “ 𝑡 ) } ) ∖ ( 𝐹 “ 𝑡 ) ) ) ∈ ( ( 𝑅1 ‘ ∩ { 𝑢 ∈ On ∣ ∃ 𝑣 ∈ ( 𝑅1 ‘ 𝑢 ) ¬ 𝑣 ∈ ( 𝐹 “ 𝑡 ) } ) ∖ ( 𝐹 “ 𝑡 ) ) )
18	17	eldifbd	⊢ ( 𝜑 → ¬ ( 𝐺 ‘ ( ( 𝑅1 ‘ ∩ { 𝑢 ∈ On ∣ ∃ 𝑣 ∈ ( 𝑅1 ‘ 𝑢 ) ¬ 𝑣 ∈ ( 𝐹 “ 𝑡 ) } ) ∖ ( 𝐹 “ 𝑡 ) ) ) ∈ ( 𝐹 “ 𝑡 ) )
19	18	adantr	⊢ ( ( 𝜑 ∧ 𝑡 ∈ On ) → ¬ ( 𝐺 ‘ ( ( 𝑅1 ‘ ∩ { 𝑢 ∈ On ∣ ∃ 𝑣 ∈ ( 𝑅1 ‘ 𝑢 ) ¬ 𝑣 ∈ ( 𝐹 “ 𝑡 ) } ) ∖ ( 𝐹 “ 𝑡 ) ) ) ∈ ( 𝐹 “ 𝑡 ) )
20	11 19	eqneltrd	⊢ ( ( 𝜑 ∧ 𝑡 ∈ On ) → ¬ ( 𝐹 ‘ 𝑡 ) ∈ ( 𝐹 “ 𝑡 ) )
21	20	ralrimiva	⊢ ( 𝜑 → ∀ 𝑡 ∈ On ¬ ( 𝐹 ‘ 𝑡 ) ∈ ( 𝐹 “ 𝑡 ) )
22		fvex	⊢ ( 𝐹 ‘ 𝑡 ) ∈ V
23		eldif	⊢ ( ( 𝐹 ‘ 𝑡 ) ∈ ( V ∖ ( 𝐹 “ 𝑡 ) ) ↔ ( ( 𝐹 ‘ 𝑡 ) ∈ V ∧ ¬ ( 𝐹 ‘ 𝑡 ) ∈ ( 𝐹 “ 𝑡 ) ) )
24	22 23	mpbiran	⊢ ( ( 𝐹 ‘ 𝑡 ) ∈ ( V ∖ ( 𝐹 “ 𝑡 ) ) ↔ ¬ ( 𝐹 ‘ 𝑡 ) ∈ ( 𝐹 “ 𝑡 ) )
25	24	ralbii	⊢ ( ∀ 𝑡 ∈ On ( 𝐹 ‘ 𝑡 ) ∈ ( V ∖ ( 𝐹 “ 𝑡 ) ) ↔ ∀ 𝑡 ∈ On ¬ ( 𝐹 ‘ 𝑡 ) ∈ ( 𝐹 “ 𝑡 ) )
26	5	tz7.48-2	⊢ ( ∀ 𝑡 ∈ On ( 𝐹 ‘ 𝑡 ) ∈ ( V ∖ ( 𝐹 “ 𝑡 ) ) → Fun ◡ 𝐹 )
27	25 26	sylbir	⊢ ( ∀ 𝑡 ∈ On ¬ ( 𝐹 ‘ 𝑡 ) ∈ ( 𝐹 “ 𝑡 ) → Fun ◡ 𝐹 )
28	21 27	syl	⊢ ( 𝜑 → Fun ◡ 𝐹 )
29		df-f1	⊢ ( 𝐹 : On –1-1→ V ↔ ( 𝐹 : On ⟶ V ∧ Fun ◡ 𝐹 ) )
30	29	biimpri	⊢ ( ( 𝐹 : On ⟶ V ∧ Fun ◡ 𝐹 ) → 𝐹 : On –1-1→ V )
31	7 28 30	sylancr	⊢ ( 𝜑 → 𝐹 : On –1-1→ V )
32		onprc	⊢ ¬ On ∈ V
33		f1f1orn	⊢ ( 𝐹 : On –1-1→ V → 𝐹 : On –1-1-onto→ ran 𝐹 )
34		f1of1	⊢ ( 𝐹 : On –1-1-onto→ ran 𝐹 → 𝐹 : On –1-1→ ran 𝐹 )
35	31 33 34	3syl	⊢ ( 𝜑 → 𝐹 : On –1-1→ ran 𝐹 )
36		f1dmex	⊢ ( ( 𝐹 : On –1-1→ ran 𝐹 ∧ ran 𝐹 ∈ V ) → On ∈ V )
37	35 36	sylan	⊢ ( ( 𝜑 ∧ ran 𝐹 ∈ V ) → On ∈ V )
38	37	stoic1a	⊢ ( ( 𝜑 ∧ ¬ On ∈ V ) → ¬ ran 𝐹 ∈ V )
39	32 38	mpan2	⊢ ( 𝜑 → ¬ ran 𝐹 ∈ V )
40	1 2 3 4 8 9	onvf1odlem4	⊢ ( 𝜑 → ( ¬ ran 𝐹 ∈ V → ran 𝐹 = V ) )
41	39 40	mpd	⊢ ( 𝜑 → ran 𝐹 = V )
42		dff1o5	⊢ ( 𝐹 : On –1-1-onto→ V ↔ ( 𝐹 : On –1-1→ V ∧ ran 𝐹 = V ) )
43	31 41 42	sylanbrc	⊢ ( 𝜑 → 𝐹 : On –1-1-onto→ V )