Theorem onvf1odlem3

Description: Lemma for onvf1od . The value of F at an ordinal A . (Contributed by BTernaryTau, 2-Dec-2025)

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

Proof

Step	Hyp	Ref	Expression
1		onvf1odlem3.1	⊢ 𝑀 = ∩ { 𝑥 ∈ On ∣ ∃ 𝑦 ∈ ( 𝑅1 ‘ 𝑥 ) ¬ 𝑦 ∈ ran 𝑤 }
2		onvf1odlem3.2	⊢ 𝑁 = ( 𝐺 ‘ ( ( 𝑅1 ‘ 𝑀 ) ∖ ran 𝑤 ) )
3		onvf1odlem3.3	⊢ 𝐹 = recs ( ( 𝑤 ∈ V ↦ 𝑁 ) )
4		onvf1odlem3.4	⊢ 𝐵 = ∩ { 𝑢 ∈ On ∣ ∃ 𝑣 ∈ ( 𝑅1 ‘ 𝑢 ) ¬ 𝑣 ∈ ( 𝐹 “ 𝐴 ) }
5		onvf1odlem3.5	⊢ 𝐶 = ( 𝐺 ‘ ( ( 𝑅1 ‘ 𝐵 ) ∖ ( 𝐹 “ 𝐴 ) ) )
6	3	tfr2	⊢ ( 𝐴 ∈ On → ( 𝐹 ‘ 𝐴 ) = ( ( 𝑤 ∈ V ↦ 𝑁 ) ‘ ( 𝐹 ↾ 𝐴 ) ) )
7	3	tfr1	⊢ 𝐹 Fn On
8		fnfun	⊢ ( 𝐹 Fn On → Fun 𝐹 )
9	7 8	ax-mp	⊢ Fun 𝐹
10		resfunexg	⊢ ( ( Fun 𝐹 ∧ 𝐴 ∈ On ) → ( 𝐹 ↾ 𝐴 ) ∈ V )
11	9 10	mpan	⊢ ( 𝐴 ∈ On → ( 𝐹 ↾ 𝐴 ) ∈ V )
12		eleq1w	⊢ ( 𝑡 = 𝑣 → ( 𝑡 ∈ ran 𝑟 ↔ 𝑣 ∈ ran 𝑟 ) )
13	12	notbid	⊢ ( 𝑡 = 𝑣 → ( ¬ 𝑡 ∈ ran 𝑟 ↔ ¬ 𝑣 ∈ ran 𝑟 ) )
14	13	adantl	⊢ ( ( 𝑠 = 𝑢 ∧ 𝑡 = 𝑣 ) → ( ¬ 𝑡 ∈ ran 𝑟 ↔ ¬ 𝑣 ∈ ran 𝑟 ) )
15		fveq2	⊢ ( 𝑠 = 𝑢 → ( 𝑅1 ‘ 𝑠 ) = ( 𝑅1 ‘ 𝑢 ) )
16	15	adantr	⊢ ( ( 𝑠 = 𝑢 ∧ 𝑡 = 𝑣 ) → ( 𝑅1 ‘ 𝑠 ) = ( 𝑅1 ‘ 𝑢 ) )
17	14 16	cbvrexdva2	⊢ ( 𝑠 = 𝑢 → ( ∃ 𝑡 ∈ ( 𝑅1 ‘ 𝑠 ) ¬ 𝑡 ∈ ran 𝑟 ↔ ∃ 𝑣 ∈ ( 𝑅1 ‘ 𝑢 ) ¬ 𝑣 ∈ ran 𝑟 ) )
18	17	cbvrabv	⊢ { 𝑠 ∈ On ∣ ∃ 𝑡 ∈ ( 𝑅1 ‘ 𝑠 ) ¬ 𝑡 ∈ ran 𝑟 } = { 𝑢 ∈ On ∣ ∃ 𝑣 ∈ ( 𝑅1 ‘ 𝑢 ) ¬ 𝑣 ∈ ran 𝑟 }
19		rneq	⊢ ( 𝑟 = ( 𝐹 ↾ 𝐴 ) → ran 𝑟 = ran ( 𝐹 ↾ 𝐴 ) )
20		df-ima	⊢ ( 𝐹 “ 𝐴 ) = ran ( 𝐹 ↾ 𝐴 )
21	19 20	eqtr4di	⊢ ( 𝑟 = ( 𝐹 ↾ 𝐴 ) → ran 𝑟 = ( 𝐹 “ 𝐴 ) )
22	21	eleq2d	⊢ ( 𝑟 = ( 𝐹 ↾ 𝐴 ) → ( 𝑣 ∈ ran 𝑟 ↔ 𝑣 ∈ ( 𝐹 “ 𝐴 ) ) )
23	22	notbid	⊢ ( 𝑟 = ( 𝐹 ↾ 𝐴 ) → ( ¬ 𝑣 ∈ ran 𝑟 ↔ ¬ 𝑣 ∈ ( 𝐹 “ 𝐴 ) ) )
24	23	rexbidv	⊢ ( 𝑟 = ( 𝐹 ↾ 𝐴 ) → ( ∃ 𝑣 ∈ ( 𝑅1 ‘ 𝑢 ) ¬ 𝑣 ∈ ran 𝑟 ↔ ∃ 𝑣 ∈ ( 𝑅1 ‘ 𝑢 ) ¬ 𝑣 ∈ ( 𝐹 “ 𝐴 ) ) )
25	24	rabbidv	⊢ ( 𝑟 = ( 𝐹 ↾ 𝐴 ) → { 𝑢 ∈ On ∣ ∃ 𝑣 ∈ ( 𝑅1 ‘ 𝑢 ) ¬ 𝑣 ∈ ran 𝑟 } = { 𝑢 ∈ On ∣ ∃ 𝑣 ∈ ( 𝑅1 ‘ 𝑢 ) ¬ 𝑣 ∈ ( 𝐹 “ 𝐴 ) } )
26	18 25	eqtrid	⊢ ( 𝑟 = ( 𝐹 ↾ 𝐴 ) → { 𝑠 ∈ On ∣ ∃ 𝑡 ∈ ( 𝑅1 ‘ 𝑠 ) ¬ 𝑡 ∈ ran 𝑟 } = { 𝑢 ∈ On ∣ ∃ 𝑣 ∈ ( 𝑅1 ‘ 𝑢 ) ¬ 𝑣 ∈ ( 𝐹 “ 𝐴 ) } )
27	26	inteqd	⊢ ( 𝑟 = ( 𝐹 ↾ 𝐴 ) → ∩ { 𝑠 ∈ On ∣ ∃ 𝑡 ∈ ( 𝑅1 ‘ 𝑠 ) ¬ 𝑡 ∈ ran 𝑟 } = ∩ { 𝑢 ∈ On ∣ ∃ 𝑣 ∈ ( 𝑅1 ‘ 𝑢 ) ¬ 𝑣 ∈ ( 𝐹 “ 𝐴 ) } )
28	27 4	eqtr4di	⊢ ( 𝑟 = ( 𝐹 ↾ 𝐴 ) → ∩ { 𝑠 ∈ On ∣ ∃ 𝑡 ∈ ( 𝑅1 ‘ 𝑠 ) ¬ 𝑡 ∈ ran 𝑟 } = 𝐵 )
29	28	fveq2d	⊢ ( 𝑟 = ( 𝐹 ↾ 𝐴 ) → ( 𝑅1 ‘ ∩ { 𝑠 ∈ On ∣ ∃ 𝑡 ∈ ( 𝑅1 ‘ 𝑠 ) ¬ 𝑡 ∈ ran 𝑟 } ) = ( 𝑅1 ‘ 𝐵 ) )
30	29 21	difeq12d	⊢ ( 𝑟 = ( 𝐹 ↾ 𝐴 ) → ( ( 𝑅1 ‘ ∩ { 𝑠 ∈ On ∣ ∃ 𝑡 ∈ ( 𝑅1 ‘ 𝑠 ) ¬ 𝑡 ∈ ran 𝑟 } ) ∖ ran 𝑟 ) = ( ( 𝑅1 ‘ 𝐵 ) ∖ ( 𝐹 “ 𝐴 ) ) )
31	30	fveq2d	⊢ ( 𝑟 = ( 𝐹 ↾ 𝐴 ) → ( 𝐺 ‘ ( ( 𝑅1 ‘ ∩ { 𝑠 ∈ On ∣ ∃ 𝑡 ∈ ( 𝑅1 ‘ 𝑠 ) ¬ 𝑡 ∈ ran 𝑟 } ) ∖ ran 𝑟 ) ) = ( 𝐺 ‘ ( ( 𝑅1 ‘ 𝐵 ) ∖ ( 𝐹 “ 𝐴 ) ) ) )
32	31 5	eqtr4di	⊢ ( 𝑟 = ( 𝐹 ↾ 𝐴 ) → ( 𝐺 ‘ ( ( 𝑅1 ‘ ∩ { 𝑠 ∈ On ∣ ∃ 𝑡 ∈ ( 𝑅1 ‘ 𝑠 ) ¬ 𝑡 ∈ ran 𝑟 } ) ∖ ran 𝑟 ) ) = 𝐶 )
33		eleq1w	⊢ ( 𝑦 = 𝑡 → ( 𝑦 ∈ ran 𝑤 ↔ 𝑡 ∈ ran 𝑤 ) )
34	33	notbid	⊢ ( 𝑦 = 𝑡 → ( ¬ 𝑦 ∈ ran 𝑤 ↔ ¬ 𝑡 ∈ ran 𝑤 ) )
35	34	adantl	⊢ ( ( 𝑥 = 𝑠 ∧ 𝑦 = 𝑡 ) → ( ¬ 𝑦 ∈ ran 𝑤 ↔ ¬ 𝑡 ∈ ran 𝑤 ) )
36		fveq2	⊢ ( 𝑥 = 𝑠 → ( 𝑅1 ‘ 𝑥 ) = ( 𝑅1 ‘ 𝑠 ) )
37	36	adantr	⊢ ( ( 𝑥 = 𝑠 ∧ 𝑦 = 𝑡 ) → ( 𝑅1 ‘ 𝑥 ) = ( 𝑅1 ‘ 𝑠 ) )
38	35 37	cbvrexdva2	⊢ ( 𝑥 = 𝑠 → ( ∃ 𝑦 ∈ ( 𝑅1 ‘ 𝑥 ) ¬ 𝑦 ∈ ran 𝑤 ↔ ∃ 𝑡 ∈ ( 𝑅1 ‘ 𝑠 ) ¬ 𝑡 ∈ ran 𝑤 ) )
39	38	cbvrabv	⊢ { 𝑥 ∈ On ∣ ∃ 𝑦 ∈ ( 𝑅1 ‘ 𝑥 ) ¬ 𝑦 ∈ ran 𝑤 } = { 𝑠 ∈ On ∣ ∃ 𝑡 ∈ ( 𝑅1 ‘ 𝑠 ) ¬ 𝑡 ∈ ran 𝑤 }
40		rneq	⊢ ( 𝑤 = 𝑟 → ran 𝑤 = ran 𝑟 )
41	40	eleq2d	⊢ ( 𝑤 = 𝑟 → ( 𝑡 ∈ ran 𝑤 ↔ 𝑡 ∈ ran 𝑟 ) )
42	41	notbid	⊢ ( 𝑤 = 𝑟 → ( ¬ 𝑡 ∈ ran 𝑤 ↔ ¬ 𝑡 ∈ ran 𝑟 ) )
43	42	rexbidv	⊢ ( 𝑤 = 𝑟 → ( ∃ 𝑡 ∈ ( 𝑅1 ‘ 𝑠 ) ¬ 𝑡 ∈ ran 𝑤 ↔ ∃ 𝑡 ∈ ( 𝑅1 ‘ 𝑠 ) ¬ 𝑡 ∈ ran 𝑟 ) )
44	43	rabbidv	⊢ ( 𝑤 = 𝑟 → { 𝑠 ∈ On ∣ ∃ 𝑡 ∈ ( 𝑅1 ‘ 𝑠 ) ¬ 𝑡 ∈ ran 𝑤 } = { 𝑠 ∈ On ∣ ∃ 𝑡 ∈ ( 𝑅1 ‘ 𝑠 ) ¬ 𝑡 ∈ ran 𝑟 } )
45	39 44	eqtrid	⊢ ( 𝑤 = 𝑟 → { 𝑥 ∈ On ∣ ∃ 𝑦 ∈ ( 𝑅1 ‘ 𝑥 ) ¬ 𝑦 ∈ ran 𝑤 } = { 𝑠 ∈ On ∣ ∃ 𝑡 ∈ ( 𝑅1 ‘ 𝑠 ) ¬ 𝑡 ∈ ran 𝑟 } )
46	45	inteqd	⊢ ( 𝑤 = 𝑟 → ∩ { 𝑥 ∈ On ∣ ∃ 𝑦 ∈ ( 𝑅1 ‘ 𝑥 ) ¬ 𝑦 ∈ ran 𝑤 } = ∩ { 𝑠 ∈ On ∣ ∃ 𝑡 ∈ ( 𝑅1 ‘ 𝑠 ) ¬ 𝑡 ∈ ran 𝑟 } )
47	1 46	eqtrid	⊢ ( 𝑤 = 𝑟 → 𝑀 = ∩ { 𝑠 ∈ On ∣ ∃ 𝑡 ∈ ( 𝑅1 ‘ 𝑠 ) ¬ 𝑡 ∈ ran 𝑟 } )
48	47	fveq2d	⊢ ( 𝑤 = 𝑟 → ( 𝑅1 ‘ 𝑀 ) = ( 𝑅1 ‘ ∩ { 𝑠 ∈ On ∣ ∃ 𝑡 ∈ ( 𝑅1 ‘ 𝑠 ) ¬ 𝑡 ∈ ran 𝑟 } ) )
49	48 40	difeq12d	⊢ ( 𝑤 = 𝑟 → ( ( 𝑅1 ‘ 𝑀 ) ∖ ran 𝑤 ) = ( ( 𝑅1 ‘ ∩ { 𝑠 ∈ On ∣ ∃ 𝑡 ∈ ( 𝑅1 ‘ 𝑠 ) ¬ 𝑡 ∈ ran 𝑟 } ) ∖ ran 𝑟 ) )
50	49	fveq2d	⊢ ( 𝑤 = 𝑟 → ( 𝐺 ‘ ( ( 𝑅1 ‘ 𝑀 ) ∖ ran 𝑤 ) ) = ( 𝐺 ‘ ( ( 𝑅1 ‘ ∩ { 𝑠 ∈ On ∣ ∃ 𝑡 ∈ ( 𝑅1 ‘ 𝑠 ) ¬ 𝑡 ∈ ran 𝑟 } ) ∖ ran 𝑟 ) ) )
51	2 50	eqtrid	⊢ ( 𝑤 = 𝑟 → 𝑁 = ( 𝐺 ‘ ( ( 𝑅1 ‘ ∩ { 𝑠 ∈ On ∣ ∃ 𝑡 ∈ ( 𝑅1 ‘ 𝑠 ) ¬ 𝑡 ∈ ran 𝑟 } ) ∖ ran 𝑟 ) ) )
52	51	cbvmptv	⊢ ( 𝑤 ∈ V ↦ 𝑁 ) = ( 𝑟 ∈ V ↦ ( 𝐺 ‘ ( ( 𝑅1 ‘ ∩ { 𝑠 ∈ On ∣ ∃ 𝑡 ∈ ( 𝑅1 ‘ 𝑠 ) ¬ 𝑡 ∈ ran 𝑟 } ) ∖ ran 𝑟 ) ) )
53	5	fvexi	⊢ 𝐶 ∈ V
54	32 52 53	fvmpt	⊢ ( ( 𝐹 ↾ 𝐴 ) ∈ V → ( ( 𝑤 ∈ V ↦ 𝑁 ) ‘ ( 𝐹 ↾ 𝐴 ) ) = 𝐶 )
55	11 54	syl	⊢ ( 𝐴 ∈ On → ( ( 𝑤 ∈ V ↦ 𝑁 ) ‘ ( 𝐹 ↾ 𝐴 ) ) = 𝐶 )
56	6 55	eqtrd	⊢ ( 𝐴 ∈ On → ( 𝐹 ‘ 𝐴 ) = 𝐶 )