Definition df-fnl

Description: Define a function whose range contains all and only the constructible sets. Based on Definition 15.13 of TakeutiZaring p. 158. (Contributed by BTernaryTau, 3-Sep-2026)

	Ref	Expression
Assertion	df-fnl	⊢ 𝐹𝐿 = recs ( ( 𝑥 ∈ V ↦ if ( ( 𝐾3 ‘ dom 𝑥 ) = ∅ , ran 𝑥 , ( ℱ ‘ ⟨ ( 𝐾3 ‘ dom 𝑥 ) , ( 𝑥 ‘ ( 𝐾1 ‘ dom 𝑥 ) ) , ( 𝑥 ‘ ( 𝐾2 ‘ dom 𝑥 ) ) ⟩ ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cfnl	⊢ 𝐹𝐿
1		vx	⊢ 𝑥
2		cvv	⊢ V
3		ck3	⊢ 𝐾3
4	1	cv	⊢ 𝑥
5	4	cdm	⊢ dom 𝑥
6	5 3	cfv	⊢ ( 𝐾3 ‘ dom 𝑥 )
7		c0	⊢ ∅
8	6 7	wceq	⊢ ( 𝐾3 ‘ dom 𝑥 ) = ∅
9	4	crn	⊢ ran 𝑥
10		cgdlopc	⊢ ℱ
11		ck1	⊢ 𝐾1
12	5 11	cfv	⊢ ( 𝐾1 ‘ dom 𝑥 )
13	12 4	cfv	⊢ ( 𝑥 ‘ ( 𝐾1 ‘ dom 𝑥 ) )
14		ck2	⊢ 𝐾2
15	5 14	cfv	⊢ ( 𝐾2 ‘ dom 𝑥 )
16	15 4	cfv	⊢ ( 𝑥 ‘ ( 𝐾2 ‘ dom 𝑥 ) )
17	6 13 16	cotp	⊢ ⟨ ( 𝐾3 ‘ dom 𝑥 ) , ( 𝑥 ‘ ( 𝐾1 ‘ dom 𝑥 ) ) , ( 𝑥 ‘ ( 𝐾2 ‘ dom 𝑥 ) ) ⟩
18	17 10	cfv	⊢ ( ℱ ‘ ⟨ ( 𝐾3 ‘ dom 𝑥 ) , ( 𝑥 ‘ ( 𝐾1 ‘ dom 𝑥 ) ) , ( 𝑥 ‘ ( 𝐾2 ‘ dom 𝑥 ) ) ⟩ )
19	8 9 18	cif	⊢ if ( ( 𝐾3 ‘ dom 𝑥 ) = ∅ , ran 𝑥 , ( ℱ ‘ ⟨ ( 𝐾3 ‘ dom 𝑥 ) , ( 𝑥 ‘ ( 𝐾1 ‘ dom 𝑥 ) ) , ( 𝑥 ‘ ( 𝐾2 ‘ dom 𝑥 ) ) ⟩ ) )
20	1 2 19	cmpt	⊢ ( 𝑥 ∈ V ↦ if ( ( 𝐾3 ‘ dom 𝑥 ) = ∅ , ran 𝑥 , ( ℱ ‘ ⟨ ( 𝐾3 ‘ dom 𝑥 ) , ( 𝑥 ‘ ( 𝐾1 ‘ dom 𝑥 ) ) , ( 𝑥 ‘ ( 𝐾2 ‘ dom 𝑥 ) ) ⟩ ) ) )
21	20	crecs	⊢ recs ( ( 𝑥 ∈ V ↦ if ( ( 𝐾3 ‘ dom 𝑥 ) = ∅ , ran 𝑥 , ( ℱ ‘ ⟨ ( 𝐾3 ‘ dom 𝑥 ) , ( 𝑥 ‘ ( 𝐾1 ‘ dom 𝑥 ) ) , ( 𝑥 ‘ ( 𝐾2 ‘ dom 𝑥 ) ) ⟩ ) ) ) )
22	0 21	wceq	⊢ 𝐹𝐿 = recs ( ( 𝑥 ∈ V ↦ if ( ( 𝐾3 ‘ dom 𝑥 ) = ∅ , ran 𝑥 , ( ℱ ‘ ⟨ ( 𝐾3 ‘ dom 𝑥 ) , ( 𝑥 ‘ ( 𝐾1 ‘ dom 𝑥 ) ) , ( 𝑥 ‘ ( 𝐾2 ‘ dom 𝑥 ) ) ⟩ ) ) ) )