Theorem onvf1odlem4

Description: Lemma for onvf1od . If the range of F does not exist, then it must equal the universe. (Contributed by BTernaryTau, 4-Dec-2025)

	Ref	Expression
Hypotheses	onvf1odlem4.1	⊢ ( 𝜑 → ∀ 𝑧 ( 𝑧 ≠ ∅ → ( 𝐺 ‘ 𝑧 ) ∈ 𝑧 ) )
	onvf1odlem4.2	⊢ 𝑀 = ∩ { 𝑥 ∈ On ∣ ∃ 𝑦 ∈ ( 𝑅1 ‘ 𝑥 ) ¬ 𝑦 ∈ ran 𝑤 }
	onvf1odlem4.3	⊢ 𝑁 = ( 𝐺 ‘ ( ( 𝑅1 ‘ 𝑀 ) ∖ ran 𝑤 ) )
	onvf1odlem4.4	⊢ 𝐹 = recs ( ( 𝑤 ∈ V ↦ 𝑁 ) )
	onvf1odlem4.5	⊢ 𝐵 = ∩ { 𝑢 ∈ On ∣ ∃ 𝑣 ∈ ( 𝑅1 ‘ 𝑢 ) ¬ 𝑣 ∈ ( 𝐹 “ 𝑡 ) }
	onvf1odlem4.6	⊢ 𝐶 = ( 𝐺 ‘ ( ( 𝑅1 ‘ 𝐵 ) ∖ ( 𝐹 “ 𝑡 ) ) )
Assertion	onvf1odlem4	⊢ ( 𝜑 → ( ¬ ran 𝐹 ∈ V → ran 𝐹 = V ) )

Proof

Step	Hyp	Ref	Expression
1		onvf1odlem4.1	⊢ ( 𝜑 → ∀ 𝑧 ( 𝑧 ≠ ∅ → ( 𝐺 ‘ 𝑧 ) ∈ 𝑧 ) )
2		onvf1odlem4.2	⊢ 𝑀 = ∩ { 𝑥 ∈ On ∣ ∃ 𝑦 ∈ ( 𝑅1 ‘ 𝑥 ) ¬ 𝑦 ∈ ran 𝑤 }
3		onvf1odlem4.3	⊢ 𝑁 = ( 𝐺 ‘ ( ( 𝑅1 ‘ 𝑀 ) ∖ ran 𝑤 ) )
4		onvf1odlem4.4	⊢ 𝐹 = recs ( ( 𝑤 ∈ V ↦ 𝑁 ) )
5		onvf1odlem4.5	⊢ 𝐵 = ∩ { 𝑢 ∈ On ∣ ∃ 𝑣 ∈ ( 𝑅1 ‘ 𝑢 ) ¬ 𝑣 ∈ ( 𝐹 “ 𝑡 ) }
6		onvf1odlem4.6	⊢ 𝐶 = ( 𝐺 ‘ ( ( 𝑅1 ‘ 𝐵 ) ∖ ( 𝐹 “ 𝑡 ) ) )
7		eqv	⊢ ( ran 𝐹 = V ↔ ∀ 𝑣 𝑣 ∈ ran 𝐹 )
8		exnal	⊢ ( ∃ 𝑣 ¬ 𝑣 ∈ ran 𝐹 ↔ ¬ ∀ 𝑣 𝑣 ∈ ran 𝐹 )
9	4	tfr1	⊢ 𝐹 Fn On
10		fvelrnb	⊢ ( 𝐹 Fn On → ( 𝑠 ∈ ran 𝐹 ↔ ∃ 𝑡 ∈ On ( 𝐹 ‘ 𝑡 ) = 𝑠 ) )
11	9 10	ax-mp	⊢ ( 𝑠 ∈ ran 𝐹 ↔ ∃ 𝑡 ∈ On ( 𝐹 ‘ 𝑡 ) = 𝑠 )
12	2 3 4 5 6	onvf1odlem3	⊢ ( 𝑡 ∈ On → ( 𝐹 ‘ 𝑡 ) = 𝐶 )
13	12	adantl	⊢ ( ( 𝜑 ∧ 𝑡 ∈ On ) → ( 𝐹 ‘ 𝑡 ) = 𝐶 )
14		fnfun	⊢ ( 𝐹 Fn On → Fun 𝐹 )
15	9 14	ax-mp	⊢ Fun 𝐹
16		vex	⊢ 𝑡 ∈ V
17	16	funimaex	⊢ ( Fun 𝐹 → ( 𝐹 “ 𝑡 ) ∈ V )
18	15 17	ax-mp	⊢ ( 𝐹 “ 𝑡 ) ∈ V
19	1 5 6	onvf1odlem2	⊢ ( 𝜑 → ( ( 𝐹 “ 𝑡 ) ∈ V → 𝐶 ∈ ( ( 𝑅1 ‘ 𝐵 ) ∖ ( 𝐹 “ 𝑡 ) ) ) )
20	18 19	mpi	⊢ ( 𝜑 → 𝐶 ∈ ( ( 𝑅1 ‘ 𝐵 ) ∖ ( 𝐹 “ 𝑡 ) ) )
21	20	eldifad	⊢ ( 𝜑 → 𝐶 ∈ ( 𝑅1 ‘ 𝐵 ) )
22	21	adantr	⊢ ( ( 𝜑 ∧ 𝑡 ∈ On ) → 𝐶 ∈ ( 𝑅1 ‘ 𝐵 ) )
23	13 22	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑡 ∈ On ) → ( 𝐹 ‘ 𝑡 ) ∈ ( 𝑅1 ‘ 𝐵 ) )
24		rankr1ai	⊢ ( ( 𝐹 ‘ 𝑡 ) ∈ ( 𝑅1 ‘ 𝐵 ) → ( rank ‘ ( 𝐹 ‘ 𝑡 ) ) ∈ 𝐵 )
25		onvf1odlem1	⊢ ( ( 𝐹 “ 𝑡 ) ∈ V → ∃ 𝑢 ∈ On ∃ 𝑣 ∈ ( 𝑅1 ‘ 𝑢 ) ¬ 𝑣 ∈ ( 𝐹 “ 𝑡 ) )
26	18 25	ax-mp	⊢ ∃ 𝑢 ∈ On ∃ 𝑣 ∈ ( 𝑅1 ‘ 𝑢 ) ¬ 𝑣 ∈ ( 𝐹 “ 𝑡 )
27		onintrab2	⊢ ( ∃ 𝑢 ∈ On ∃ 𝑣 ∈ ( 𝑅1 ‘ 𝑢 ) ¬ 𝑣 ∈ ( 𝐹 “ 𝑡 ) ↔ ∩ { 𝑢 ∈ On ∣ ∃ 𝑣 ∈ ( 𝑅1 ‘ 𝑢 ) ¬ 𝑣 ∈ ( 𝐹 “ 𝑡 ) } ∈ On )
28	5	eleq1i	⊢ ( 𝐵 ∈ On ↔ ∩ { 𝑢 ∈ On ∣ ∃ 𝑣 ∈ ( 𝑅1 ‘ 𝑢 ) ¬ 𝑣 ∈ ( 𝐹 “ 𝑡 ) } ∈ On )
29	27 28	bitr4i	⊢ ( ∃ 𝑢 ∈ On ∃ 𝑣 ∈ ( 𝑅1 ‘ 𝑢 ) ¬ 𝑣 ∈ ( 𝐹 “ 𝑡 ) ↔ 𝐵 ∈ On )
30	26 29	mpbi	⊢ 𝐵 ∈ On
31	30	oneli	⊢ ( ( rank ‘ ( 𝐹 ‘ 𝑡 ) ) ∈ 𝐵 → ( rank ‘ ( 𝐹 ‘ 𝑡 ) ) ∈ On )
32		fveq2	⊢ ( 𝑢 = ( rank ‘ ( 𝐹 ‘ 𝑡 ) ) → ( 𝑅1 ‘ 𝑢 ) = ( 𝑅1 ‘ ( rank ‘ ( 𝐹 ‘ 𝑡 ) ) ) )
33	32	rexeqdv	⊢ ( 𝑢 = ( rank ‘ ( 𝐹 ‘ 𝑡 ) ) → ( ∃ 𝑣 ∈ ( 𝑅1 ‘ 𝑢 ) ¬ 𝑣 ∈ ( 𝐹 “ 𝑡 ) ↔ ∃ 𝑣 ∈ ( 𝑅1 ‘ ( rank ‘ ( 𝐹 ‘ 𝑡 ) ) ) ¬ 𝑣 ∈ ( 𝐹 “ 𝑡 ) ) )
34	33	onnminsb	⊢ ( ( rank ‘ ( 𝐹 ‘ 𝑡 ) ) ∈ On → ( ( rank ‘ ( 𝐹 ‘ 𝑡 ) ) ∈ ∩ { 𝑢 ∈ On ∣ ∃ 𝑣 ∈ ( 𝑅1 ‘ 𝑢 ) ¬ 𝑣 ∈ ( 𝐹 “ 𝑡 ) } → ¬ ∃ 𝑣 ∈ ( 𝑅1 ‘ ( rank ‘ ( 𝐹 ‘ 𝑡 ) ) ) ¬ 𝑣 ∈ ( 𝐹 “ 𝑡 ) ) )
35	5	eleq2i	⊢ ( ( rank ‘ ( 𝐹 ‘ 𝑡 ) ) ∈ 𝐵 ↔ ( rank ‘ ( 𝐹 ‘ 𝑡 ) ) ∈ ∩ { 𝑢 ∈ On ∣ ∃ 𝑣 ∈ ( 𝑅1 ‘ 𝑢 ) ¬ 𝑣 ∈ ( 𝐹 “ 𝑡 ) } )
36		dfral2	⊢ ( ∀ 𝑣 ∈ ( 𝑅1 ‘ ( rank ‘ ( 𝐹 ‘ 𝑡 ) ) ) 𝑣 ∈ ( 𝐹 “ 𝑡 ) ↔ ¬ ∃ 𝑣 ∈ ( 𝑅1 ‘ ( rank ‘ ( 𝐹 ‘ 𝑡 ) ) ) ¬ 𝑣 ∈ ( 𝐹 “ 𝑡 ) )
37	34 35 36	3imtr4g	⊢ ( ( rank ‘ ( 𝐹 ‘ 𝑡 ) ) ∈ On → ( ( rank ‘ ( 𝐹 ‘ 𝑡 ) ) ∈ 𝐵 → ∀ 𝑣 ∈ ( 𝑅1 ‘ ( rank ‘ ( 𝐹 ‘ 𝑡 ) ) ) 𝑣 ∈ ( 𝐹 “ 𝑡 ) ) )
38	31 37	mpcom	⊢ ( ( rank ‘ ( 𝐹 ‘ 𝑡 ) ) ∈ 𝐵 → ∀ 𝑣 ∈ ( 𝑅1 ‘ ( rank ‘ ( 𝐹 ‘ 𝑡 ) ) ) 𝑣 ∈ ( 𝐹 “ 𝑡 ) )
39		imassrn	⊢ ( 𝐹 “ 𝑡 ) ⊆ ran 𝐹
40	39	sseli	⊢ ( 𝑣 ∈ ( 𝐹 “ 𝑡 ) → 𝑣 ∈ ran 𝐹 )
41	40	ralimi	⊢ ( ∀ 𝑣 ∈ ( 𝑅1 ‘ ( rank ‘ ( 𝐹 ‘ 𝑡 ) ) ) 𝑣 ∈ ( 𝐹 “ 𝑡 ) → ∀ 𝑣 ∈ ( 𝑅1 ‘ ( rank ‘ ( 𝐹 ‘ 𝑡 ) ) ) 𝑣 ∈ ran 𝐹 )
42	38 41	syl	⊢ ( ( rank ‘ ( 𝐹 ‘ 𝑡 ) ) ∈ 𝐵 → ∀ 𝑣 ∈ ( 𝑅1 ‘ ( rank ‘ ( 𝐹 ‘ 𝑡 ) ) ) 𝑣 ∈ ran 𝐹 )
43	23 24 42	3syl	⊢ ( ( 𝜑 ∧ 𝑡 ∈ On ) → ∀ 𝑣 ∈ ( 𝑅1 ‘ ( rank ‘ ( 𝐹 ‘ 𝑡 ) ) ) 𝑣 ∈ ran 𝐹 )
44		2fveq3	⊢ ( ( 𝐹 ‘ 𝑡 ) = 𝑠 → ( 𝑅1 ‘ ( rank ‘ ( 𝐹 ‘ 𝑡 ) ) ) = ( 𝑅1 ‘ ( rank ‘ 𝑠 ) ) )
45	44	raleqdv	⊢ ( ( 𝐹 ‘ 𝑡 ) = 𝑠 → ( ∀ 𝑣 ∈ ( 𝑅1 ‘ ( rank ‘ ( 𝐹 ‘ 𝑡 ) ) ) 𝑣 ∈ ran 𝐹 ↔ ∀ 𝑣 ∈ ( 𝑅1 ‘ ( rank ‘ 𝑠 ) ) 𝑣 ∈ ran 𝐹 ) )
46	43 45	syl5ibcom	⊢ ( ( 𝜑 ∧ 𝑡 ∈ On ) → ( ( 𝐹 ‘ 𝑡 ) = 𝑠 → ∀ 𝑣 ∈ ( 𝑅1 ‘ ( rank ‘ 𝑠 ) ) 𝑣 ∈ ran 𝐹 ) )
47	46	rexlimdva	⊢ ( 𝜑 → ( ∃ 𝑡 ∈ On ( 𝐹 ‘ 𝑡 ) = 𝑠 → ∀ 𝑣 ∈ ( 𝑅1 ‘ ( rank ‘ 𝑠 ) ) 𝑣 ∈ ran 𝐹 ) )
48	11 47	biimtrid	⊢ ( 𝜑 → ( 𝑠 ∈ ran 𝐹 → ∀ 𝑣 ∈ ( 𝑅1 ‘ ( rank ‘ 𝑠 ) ) 𝑣 ∈ ran 𝐹 ) )
49	48	imp	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ran 𝐹 ) → ∀ 𝑣 ∈ ( 𝑅1 ‘ ( rank ‘ 𝑠 ) ) 𝑣 ∈ ran 𝐹 )
50		df-ral	⊢ ( ∀ 𝑣 ∈ ( 𝑅1 ‘ ( rank ‘ 𝑠 ) ) 𝑣 ∈ ran 𝐹 ↔ ∀ 𝑣 ( 𝑣 ∈ ( 𝑅1 ‘ ( rank ‘ 𝑠 ) ) → 𝑣 ∈ ran 𝐹 ) )
51	49 50	sylib	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ran 𝐹 ) → ∀ 𝑣 ( 𝑣 ∈ ( 𝑅1 ‘ ( rank ‘ 𝑠 ) ) → 𝑣 ∈ ran 𝐹 ) )
52	51	19.21bi	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ran 𝐹 ) → ( 𝑣 ∈ ( 𝑅1 ‘ ( rank ‘ 𝑠 ) ) → 𝑣 ∈ ran 𝐹 ) )
53	52	con3d	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ran 𝐹 ) → ( ¬ 𝑣 ∈ ran 𝐹 → ¬ 𝑣 ∈ ( 𝑅1 ‘ ( rank ‘ 𝑠 ) ) ) )
54		rankon	⊢ ( rank ‘ 𝑠 ) ∈ On
55		vex	⊢ 𝑣 ∈ V
56	55	ssrankr1	⊢ ( ( rank ‘ 𝑠 ) ∈ On → ( ( rank ‘ 𝑠 ) ⊆ ( rank ‘ 𝑣 ) ↔ ¬ 𝑣 ∈ ( 𝑅1 ‘ ( rank ‘ 𝑠 ) ) ) )
57	54 56	ax-mp	⊢ ( ( rank ‘ 𝑠 ) ⊆ ( rank ‘ 𝑣 ) ↔ ¬ 𝑣 ∈ ( 𝑅1 ‘ ( rank ‘ 𝑠 ) ) )
58	53 57	imbitrrdi	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ran 𝐹 ) → ( ¬ 𝑣 ∈ ran 𝐹 → ( rank ‘ 𝑠 ) ⊆ ( rank ‘ 𝑣 ) ) )
59	58	impancom	⊢ ( ( 𝜑 ∧ ¬ 𝑣 ∈ ran 𝐹 ) → ( 𝑠 ∈ ran 𝐹 → ( rank ‘ 𝑠 ) ⊆ ( rank ‘ 𝑣 ) ) )
60	59	ralrimiv	⊢ ( ( 𝜑 ∧ ¬ 𝑣 ∈ ran 𝐹 ) → ∀ 𝑠 ∈ ran 𝐹 ( rank ‘ 𝑠 ) ⊆ ( rank ‘ 𝑣 ) )
61		rankon	⊢ ( rank ‘ 𝑣 ) ∈ On
62		sseq2	⊢ ( 𝑟 = ( rank ‘ 𝑣 ) → ( ( rank ‘ 𝑠 ) ⊆ 𝑟 ↔ ( rank ‘ 𝑠 ) ⊆ ( rank ‘ 𝑣 ) ) )
63	62	ralbidv	⊢ ( 𝑟 = ( rank ‘ 𝑣 ) → ( ∀ 𝑠 ∈ ran 𝐹 ( rank ‘ 𝑠 ) ⊆ 𝑟 ↔ ∀ 𝑠 ∈ ran 𝐹 ( rank ‘ 𝑠 ) ⊆ ( rank ‘ 𝑣 ) ) )
64	63	rspcev	⊢ ( ( ( rank ‘ 𝑣 ) ∈ On ∧ ∀ 𝑠 ∈ ran 𝐹 ( rank ‘ 𝑠 ) ⊆ ( rank ‘ 𝑣 ) ) → ∃ 𝑟 ∈ On ∀ 𝑠 ∈ ran 𝐹 ( rank ‘ 𝑠 ) ⊆ 𝑟 )
65	61 64	mpan	⊢ ( ∀ 𝑠 ∈ ran 𝐹 ( rank ‘ 𝑠 ) ⊆ ( rank ‘ 𝑣 ) → ∃ 𝑟 ∈ On ∀ 𝑠 ∈ ran 𝐹 ( rank ‘ 𝑠 ) ⊆ 𝑟 )
66		bndrank	⊢ ( ∃ 𝑟 ∈ On ∀ 𝑠 ∈ ran 𝐹 ( rank ‘ 𝑠 ) ⊆ 𝑟 → ran 𝐹 ∈ V )
67	60 65 66	3syl	⊢ ( ( 𝜑 ∧ ¬ 𝑣 ∈ ran 𝐹 ) → ran 𝐹 ∈ V )
68	67	expcom	⊢ ( ¬ 𝑣 ∈ ran 𝐹 → ( 𝜑 → ran 𝐹 ∈ V ) )
69	68	exlimiv	⊢ ( ∃ 𝑣 ¬ 𝑣 ∈ ran 𝐹 → ( 𝜑 → ran 𝐹 ∈ V ) )
70	8 69	sylbir	⊢ ( ¬ ∀ 𝑣 𝑣 ∈ ran 𝐹 → ( 𝜑 → ran 𝐹 ∈ V ) )
71	7 70	sylnbi	⊢ ( ¬ ran 𝐹 = V → ( 𝜑 → ran 𝐹 ∈ V ) )
72	71	com12	⊢ ( 𝜑 → ( ¬ ran 𝐹 = V → ran 𝐹 ∈ V ) )
73	72	con1d	⊢ ( 𝜑 → ( ¬ ran 𝐹 ∈ V → ran 𝐹 = V ) )