Definition df-l

Description: Define the class of all constructible sets. Definition 15.15 of TakeutiZaring p. 158. (Contributed by BTernaryTau, 3-Sep-2026)

	Ref	Expression
Assertion	df-l	⊢ 𝐿 = ( 𝐹𝐿 “ On )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cl	⊢ 𝐿
1		cfnl	⊢ 𝐹𝐿
2		con0	⊢ On
3	1 2	cima	⊢ ( 𝐹𝐿 “ On )
4	0 3	wceq	⊢ 𝐿 = ( 𝐹𝐿 “ On )