Definition df-fnl 35804

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.)

Assertion

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

Detailed syntax breakdown of Definition df-fnl

Step	Hyp	Ref	Expression
1		cfnl 35795	. 2 class 𝐹𝐿
2		vx	. . . 4 setvar 𝑥
3		cvv 3450	. . . 4 class V
4	2	cv 1569	. . . . . . . 8 class 𝑥
5	4	cdm 5647	. . . . . . 7 class dom 𝑥
6		ck3 35794	. . . . . . 7 class 𝐾3
7	5, 6	cfv 6527	. . . . . 6 class (𝐾3‘dom 𝑥)
8		c0 4278	. . . . . 6 class ∅
9	7, 8	wceq 1570	. . . . 5 wff (𝐾3‘dom 𝑥) = ∅
10	4	crn 5648	. . . . 5 class ran 𝑥
11		ck1 35792	. . . . . . . . 9 class 𝐾1
12	5, 11	cfv 6527	. . . . . . . 8 class (𝐾1‘dom 𝑥)
13	12, 4	cfv 6527	. . . . . . 7 class (𝑥‘(𝐾1‘dom 𝑥))
14		ck2 35793	. . . . . . . . 9 class 𝐾2
15	5, 14	cfv 6527	. . . . . . . 8 class (𝐾2‘dom 𝑥)
16	15, 4	cfv 6527	. . . . . . 7 class (𝑥‘(𝐾2‘dom 𝑥))
17	7, 13, 16	cotp 4591	. . . . . 6 class ⟨(𝐾3‘dom 𝑥), (𝑥‘(𝐾1‘dom 𝑥)), (𝑥‘(𝐾2‘dom 𝑥))⟩
18		cgdlopc 35776	. . . . . 6 class ℱ
19	17, 18	cfv 6527	. . . . 5 class (ℱ ‘⟨(𝐾3‘dom 𝑥), (𝑥‘(𝐾1‘dom 𝑥)), (𝑥‘(𝐾2‘dom 𝑥))⟩)
20	9, 10, 19	cif 4481	. . . 4 class if((𝐾3‘dom 𝑥) = ∅, ran 𝑥, (ℱ ‘⟨(𝐾3‘dom 𝑥), (𝑥‘(𝐾1‘dom 𝑥)), (𝑥‘(𝐾2‘dom 𝑥))⟩))
21	2, 3, 20	cmpt 5185	. . 3 class (𝑥 ∈ V ↦ if((𝐾3‘dom 𝑥) = ∅, ran 𝑥, (ℱ ‘⟨(𝐾3‘dom 𝑥), (𝑥‘(𝐾1‘dom 𝑥)), (𝑥‘(𝐾2‘dom 𝑥))⟩)))
22	21	crecs 8356	. 2 class recs((𝑥 ∈ V ↦ if((𝐾3‘dom 𝑥) = ∅, ran 𝑥, (ℱ ‘⟨(𝐾3‘dom 𝑥), (𝑥‘(𝐾1‘dom 𝑥)), (𝑥‘(𝐾2‘dom 𝑥))⟩))))
23	1, 22	wceq 1570	1 wff 𝐹𝐿 = recs((𝑥 ∈ V ↦ if((𝐾3‘dom 𝑥) = ∅, ran 𝑥, (ℱ ‘⟨(𝐾3‘dom 𝑥), (𝑥‘(𝐾1‘dom 𝑥)), (𝑥‘(𝐾2‘dom 𝑥))⟩))))

This definition is used by: (None)