Metamath Proof Explorer

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 
|- _FL = recs ( ( x e. _V |-> if ( ( _K3 ` dom x ) = (/) , ran x , ( ~F ` <. ( _K3 ` dom x ) , ( x ` ( _K1 ` dom x ) ) , ( x ` ( _K2 ` dom x ) ) >. ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cfnl 
 |-  _FL
1 vx 
 |-  x
2 cvv 
 |-  _V
3 ck3 
 |-  _K3
4 1 cv 
 |-  x
5 4 cdm 
 |-  dom x
6 5 3 cfv 
 |-  ( _K3 ` dom x )
7 c0 
 |-  (/)
8 6 7 wceq 
 |-  ( _K3 ` dom x ) = (/)
9 4 crn 
 |-  ran x
10 cgdlopc 
 |-  ~F
11 ck1 
 |-  _K1
12 5 11 cfv 
 |-  ( _K1 ` dom x )
13 12 4 cfv 
 |-  ( x ` ( _K1 ` dom x ) )
14 ck2 
 |-  _K2
15 5 14 cfv 
 |-  ( _K2 ` dom x )
16 15 4 cfv 
 |-  ( x ` ( _K2 ` dom x ) )
17 6 13 16 cotp 
 |-  <. ( _K3 ` dom x ) , ( x ` ( _K1 ` dom x ) ) , ( x ` ( _K2 ` dom x ) ) >.
18 17 10 cfv 
 |-  ( ~F ` <. ( _K3 ` dom x ) , ( x ` ( _K1 ` dom x ) ) , ( x ` ( _K2 ` dom x ) ) >. )
19 8 9 18 cif 
 |-  if ( ( _K3 ` dom x ) = (/) , ran x , ( ~F ` <. ( _K3 ` dom x ) , ( x ` ( _K1 ` dom x ) ) , ( x ` ( _K2 ` dom x ) ) >. ) )
20 1 2 19 cmpt 
 |-  ( x e. _V |-> if ( ( _K3 ` dom x ) = (/) , ran x , ( ~F ` <. ( _K3 ` dom x ) , ( x ` ( _K1 ` dom x ) ) , ( x ` ( _K2 ` dom x ) ) >. ) ) )
21 20 crecs 
 |-  recs ( ( x e. _V |-> if ( ( _K3 ` dom x ) = (/) , ran x , ( ~F ` <. ( _K3 ` dom x ) , ( x ` ( _K1 ` dom x ) ) , ( x ` ( _K2 ` dom x ) ) >. ) ) ) )
22 0 21 wceq 
 |-  _FL = recs ( ( x e. _V |-> if ( ( _K3 ` dom x ) = (/) , ran x , ( ~F ` <. ( _K3 ` dom x ) , ( x ` ( _K1 ` dom x ) ) , ( x ` ( _K2 ` dom x ) ) >. ) ) ) )