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	Could not format assertion : No typesetting found for |- _FL = recs ( ( x e. _V |-> if ( ( _K3 ` dom x ) = (/) , ran x , ( ~F ` <. ( _K3 ` dom x ) , ( x ` ( _K1 ` dom x ) ) , ( x ` ( _K2 ` dom x ) ) >. ) ) ) ) with typecode |-

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cfnl	Could not format _FL : No typesetting found for class _FL with typecode class
1		vx	$$setvarx$$
2		cvv	$$class\mathrm{V}$$
3		ck3	Could not format _K3 : No typesetting found for class _K3 with typecode class
4	1	cv	$$setvarx$$
5	4	cdm	$$class\mathrm{dom}x$$
6	5 3	cfv	Could not format ( _K3 ` dom x ) : No typesetting found for class ( _K3 ` dom x ) with typecode class
7		c0	$$class\varnothing$$
8	6 7	wceq	Could not format ( _K3 ` dom x ) = (/) : No typesetting found for wff ( _K3 ` dom x ) = (/) with typecode wff
9	4	crn	$$class\mathrm{ran}x$$
10		cgdlopc	Could not format ~F : No typesetting found for class ~F with typecode class
11		ck1	Could not format _K1 : No typesetting found for class _K1 with typecode class
12	5 11	cfv	Could not format ( _K1 ` dom x ) : No typesetting found for class ( _K1 ` dom x ) with typecode class
13	12 4	cfv	Could not format ( x ` ( _K1 ` dom x ) ) : No typesetting found for class ( x ` ( _K1 ` dom x ) ) with typecode class
14		ck2	Could not format _K2 : No typesetting found for class _K2 with typecode class
15	5 14	cfv	Could not format ( _K2 ` dom x ) : No typesetting found for class ( _K2 ` dom x ) with typecode class
16	15 4	cfv	Could not format ( x ` ( _K2 ` dom x ) ) : No typesetting found for class ( x ` ( _K2 ` dom x ) ) with typecode class
17	6 13 16	cotp	Could not format <. ( _K3 ` dom x ) , ( x ` ( _K1 ` dom x ) ) , ( x ` ( _K2 ` dom x ) ) >. : No typesetting found for class <. ( _K3 ` dom x ) , ( x ` ( _K1 ` dom x ) ) , ( x ` ( _K2 ` dom x ) ) >. with typecode class
18	17 10	cfv	Could not format ( ~F ` <. ( _K3 ` dom x ) , ( x ` ( _K1 ` dom x ) ) , ( x ` ( _K2 ` dom x ) ) >. ) : No typesetting found for class ( ~F ` <. ( _K3 ` dom x ) , ( x ` ( _K1 ` dom x ) ) , ( x ` ( _K2 ` dom x ) ) >. ) with typecode class
19	8 9 18	cif	Could not format if ( ( _K3 ` dom x ) = (/) , ran x , ( ~F ` <. ( _K3 ` dom x ) , ( x ` ( _K1 ` dom x ) ) , ( x ` ( _K2 ` dom x ) ) >. ) ) : No typesetting found for class if ( ( _K3 ` dom x ) = (/) , ran x , ( ~F ` <. ( _K3 ` dom x ) , ( x ` ( _K1 ` dom x ) ) , ( x ` ( _K2 ` dom x ) ) >. ) ) with typecode class
20	1 2 19	cmpt	Could not format ( x e. _V |-> if ( ( _K3 ` dom x ) = (/) , ran x , ( ~F ` <. ( _K3 ` dom x ) , ( x ` ( _K1 ` dom x ) ) , ( x ` ( _K2 ` dom x ) ) >. ) ) ) : No typesetting found for class ( x e. _V |-> if ( ( _K3 ` dom x ) = (/) , ran x , ( ~F ` <. ( _K3 ` dom x ) , ( x ` ( _K1 ` dom x ) ) , ( x ` ( _K2 ` dom x ) ) >. ) ) ) with typecode class
21	20	crecs	Could not format recs ( ( x e. _V |-> if ( ( _K3 ` dom x ) = (/) , ran x , ( ~F ` <. ( _K3 ` dom x ) , ( x ` ( _K1 ` dom x ) ) , ( x ` ( _K2 ` dom x ) ) >. ) ) ) ) : No typesetting found for class recs ( ( x e. _V |-> if ( ( _K3 ` dom x ) = (/) , ran x , ( ~F ` <. ( _K3 ` dom x ) , ( x ` ( _K1 ` dom x ) ) , ( x ` ( _K2 ` dom x ) ) >. ) ) ) ) with typecode class
22	0 21	wceq	Could not format _FL = recs ( ( x e. _V |-> if ( ( _K3 ` dom x ) = (/) , ran x , ( ~F ` <. ( _K3 ` dom x ) , ( x ` ( _K1 ` dom x ) ) , ( x ` ( _K2 ` dom x ) ) >. ) ) ) ) : No typesetting found for wff _FL = recs ( ( x e. _V |-> if ( ( _K3 ` dom x ) = (/) , ran x , ( ~F ` <. ( _K3 ` dom x ) , ( x ` ( _K1 ` dom x ) ) , ( x ` ( _K2 ` dom x ) ) >. ) ) ) ) with typecode wff