Theorem fnlfvk30

Description: The value of _FL when the value of _K3 is zero. Part of Proposition 15.14 of TakeutiZaring p. 158. (Contributed by BTernaryTau, 17-Oct-2026)

	Ref	Expression
Assertion	fnlfvk30	⊢ ( ( 𝐴 ∈ On ∧ ( 𝐾3 ‘ 𝐴 ) = ∅ ) → ( 𝐹𝐿 ‘ 𝐴 ) = ( 𝐹𝐿 “ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		df-fnl	⊢ 𝐹𝐿 = recs ( ( 𝑥 ∈ V ↦ if ( ( 𝐾3 ‘ dom 𝑥 ) = ∅ , ran 𝑥 , ( ℱ ‘ ⟨ ( 𝐾3 ‘ dom 𝑥 ) , ( 𝑥 ‘ ( 𝐾1 ‘ dom 𝑥 ) ) , ( 𝑥 ‘ ( 𝐾2 ‘ dom 𝑥 ) ) ⟩ ) ) ) )
2	1	tfr2	⊢ ( 𝐴 ∈ On → ( 𝐹𝐿 ‘ 𝐴 ) = ( ( 𝑥 ∈ V ↦ if ( ( 𝐾3 ‘ dom 𝑥 ) = ∅ , ran 𝑥 , ( ℱ ‘ ⟨ ( 𝐾3 ‘ dom 𝑥 ) , ( 𝑥 ‘ ( 𝐾1 ‘ dom 𝑥 ) ) , ( 𝑥 ‘ ( 𝐾2 ‘ dom 𝑥 ) ) ⟩ ) ) ) ‘ ( 𝐹𝐿 ↾ 𝐴 ) ) )
3	2	adantr	⊢ ( ( 𝐴 ∈ On ∧ ( 𝐾3 ‘ 𝐴 ) = ∅ ) → ( 𝐹𝐿 ‘ 𝐴 ) = ( ( 𝑥 ∈ V ↦ if ( ( 𝐾3 ‘ dom 𝑥 ) = ∅ , ran 𝑥 , ( ℱ ‘ ⟨ ( 𝐾3 ‘ dom 𝑥 ) , ( 𝑥 ‘ ( 𝐾1 ‘ dom 𝑥 ) ) , ( 𝑥 ‘ ( 𝐾2 ‘ dom 𝑥 ) ) ⟩ ) ) ) ‘ ( 𝐹𝐿 ↾ 𝐴 ) ) )
4		eqid	⊢ ( 𝑥 ∈ V ↦ if ( ( 𝐾3 ‘ dom 𝑥 ) = ∅ , ran 𝑥 , ( ℱ ‘ ⟨ ( 𝐾3 ‘ dom 𝑥 ) , ( 𝑥 ‘ ( 𝐾1 ‘ dom 𝑥 ) ) , ( 𝑥 ‘ ( 𝐾2 ‘ dom 𝑥 ) ) ⟩ ) ) ) = ( 𝑥 ∈ V ↦ if ( ( 𝐾3 ‘ dom 𝑥 ) = ∅ , ran 𝑥 , ( ℱ ‘ ⟨ ( 𝐾3 ‘ dom 𝑥 ) , ( 𝑥 ‘ ( 𝐾1 ‘ dom 𝑥 ) ) , ( 𝑥 ‘ ( 𝐾2 ‘ dom 𝑥 ) ) ⟩ ) ) )
5		dmeq	⊢ ( 𝑥 = ( 𝐹𝐿 ↾ 𝐴 ) → dom 𝑥 = dom ( 𝐹𝐿 ↾ 𝐴 ) )
6	5	adantl	⊢ ( ( ( 𝐴 ∈ On ∧ ( 𝐾3 ‘ 𝐴 ) = ∅ ) ∧ 𝑥 = ( 𝐹𝐿 ↾ 𝐴 ) ) → dom 𝑥 = dom ( 𝐹𝐿 ↾ 𝐴 ) )
7		onss	⊢ ( 𝐴 ∈ On → 𝐴 ⊆ On )
8	1	tfr1	⊢ 𝐹𝐿 Fn On
9	8	fndmi	⊢ dom 𝐹𝐿 = On
10	9	sseq2i	⊢ ( 𝐴 ⊆ dom 𝐹𝐿 ↔ 𝐴 ⊆ On )
11		ssdmres	⊢ ( 𝐴 ⊆ dom 𝐹𝐿 ↔ dom ( 𝐹𝐿 ↾ 𝐴 ) = 𝐴 )
12	10 11	bitr3i	⊢ ( 𝐴 ⊆ On ↔ dom ( 𝐹𝐿 ↾ 𝐴 ) = 𝐴 )
13	7 12	sylib	⊢ ( 𝐴 ∈ On → dom ( 𝐹𝐿 ↾ 𝐴 ) = 𝐴 )
14	13	ad2antrr	⊢ ( ( ( 𝐴 ∈ On ∧ ( 𝐾3 ‘ 𝐴 ) = ∅ ) ∧ 𝑥 = ( 𝐹𝐿 ↾ 𝐴 ) ) → dom ( 𝐹𝐿 ↾ 𝐴 ) = 𝐴 )
15	6 14	eqtrd	⊢ ( ( ( 𝐴 ∈ On ∧ ( 𝐾3 ‘ 𝐴 ) = ∅ ) ∧ 𝑥 = ( 𝐹𝐿 ↾ 𝐴 ) ) → dom 𝑥 = 𝐴 )
16	15	fveq2d	⊢ ( ( ( 𝐴 ∈ On ∧ ( 𝐾3 ‘ 𝐴 ) = ∅ ) ∧ 𝑥 = ( 𝐹𝐿 ↾ 𝐴 ) ) → ( 𝐾3 ‘ dom 𝑥 ) = ( 𝐾3 ‘ 𝐴 ) )
17		simplr	⊢ ( ( ( 𝐴 ∈ On ∧ ( 𝐾3 ‘ 𝐴 ) = ∅ ) ∧ 𝑥 = ( 𝐹𝐿 ↾ 𝐴 ) ) → ( 𝐾3 ‘ 𝐴 ) = ∅ )
18	16 17	eqtrd	⊢ ( ( ( 𝐴 ∈ On ∧ ( 𝐾3 ‘ 𝐴 ) = ∅ ) ∧ 𝑥 = ( 𝐹𝐿 ↾ 𝐴 ) ) → ( 𝐾3 ‘ dom 𝑥 ) = ∅ )
19	18	iftrued	⊢ ( ( ( 𝐴 ∈ On ∧ ( 𝐾3 ‘ 𝐴 ) = ∅ ) ∧ 𝑥 = ( 𝐹𝐿 ↾ 𝐴 ) ) → if ( ( 𝐾3 ‘ dom 𝑥 ) = ∅ , ran 𝑥 , ( ℱ ‘ ⟨ ( 𝐾3 ‘ dom 𝑥 ) , ( 𝑥 ‘ ( 𝐾1 ‘ dom 𝑥 ) ) , ( 𝑥 ‘ ( 𝐾2 ‘ dom 𝑥 ) ) ⟩ ) ) = ran 𝑥 )
20		rneq	⊢ ( 𝑥 = ( 𝐹𝐿 ↾ 𝐴 ) → ran 𝑥 = ran ( 𝐹𝐿 ↾ 𝐴 ) )
21		df-ima	⊢ ( 𝐹𝐿 “ 𝐴 ) = ran ( 𝐹𝐿 ↾ 𝐴 )
22	20 21	eqtr4di	⊢ ( 𝑥 = ( 𝐹𝐿 ↾ 𝐴 ) → ran 𝑥 = ( 𝐹𝐿 “ 𝐴 ) )
23	22	adantl	⊢ ( ( ( 𝐴 ∈ On ∧ ( 𝐾3 ‘ 𝐴 ) = ∅ ) ∧ 𝑥 = ( 𝐹𝐿 ↾ 𝐴 ) ) → ran 𝑥 = ( 𝐹𝐿 “ 𝐴 ) )
24	19 23	eqtrd	⊢ ( ( ( 𝐴 ∈ On ∧ ( 𝐾3 ‘ 𝐴 ) = ∅ ) ∧ 𝑥 = ( 𝐹𝐿 ↾ 𝐴 ) ) → if ( ( 𝐾3 ‘ dom 𝑥 ) = ∅ , ran 𝑥 , ( ℱ ‘ ⟨ ( 𝐾3 ‘ dom 𝑥 ) , ( 𝑥 ‘ ( 𝐾1 ‘ dom 𝑥 ) ) , ( 𝑥 ‘ ( 𝐾2 ‘ dom 𝑥 ) ) ⟩ ) ) = ( 𝐹𝐿 “ 𝐴 ) )
25		fnfun	⊢ ( 𝐹𝐿 Fn On → Fun 𝐹𝐿 )
26	8 25	ax-mp	⊢ Fun 𝐹𝐿
27		resfunexg	⊢ ( ( Fun 𝐹𝐿 ∧ 𝐴 ∈ On ) → ( 𝐹𝐿 ↾ 𝐴 ) ∈ V )
28	26 27	mpan	⊢ ( 𝐴 ∈ On → ( 𝐹𝐿 ↾ 𝐴 ) ∈ V )
29	28	adantr	⊢ ( ( 𝐴 ∈ On ∧ ( 𝐾3 ‘ 𝐴 ) = ∅ ) → ( 𝐹𝐿 ↾ 𝐴 ) ∈ V )
30		funimaexg	⊢ ( ( Fun 𝐹𝐿 ∧ 𝐴 ∈ On ) → ( 𝐹𝐿 “ 𝐴 ) ∈ V )
31	26 30	mpan	⊢ ( 𝐴 ∈ On → ( 𝐹𝐿 “ 𝐴 ) ∈ V )
32	31	adantr	⊢ ( ( 𝐴 ∈ On ∧ ( 𝐾3 ‘ 𝐴 ) = ∅ ) → ( 𝐹𝐿 “ 𝐴 ) ∈ V )
33	4 24 29 32	fvmptd2	⊢ ( ( 𝐴 ∈ On ∧ ( 𝐾3 ‘ 𝐴 ) = ∅ ) → ( ( 𝑥 ∈ V ↦ if ( ( 𝐾3 ‘ dom 𝑥 ) = ∅ , ran 𝑥 , ( ℱ ‘ ⟨ ( 𝐾3 ‘ dom 𝑥 ) , ( 𝑥 ‘ ( 𝐾1 ‘ dom 𝑥 ) ) , ( 𝑥 ‘ ( 𝐾2 ‘ dom 𝑥 ) ) ⟩ ) ) ) ‘ ( 𝐹𝐿 ↾ 𝐴 ) ) = ( 𝐹𝐿 “ 𝐴 ) )
34	3 33	eqtrd	⊢ ( ( 𝐴 ∈ On ∧ ( 𝐾3 ‘ 𝐴 ) = ∅ ) → ( 𝐹𝐿 ‘ 𝐴 ) = ( 𝐹𝐿 “ 𝐴 ) )