Definition df-gdlop5

Description: Define the fifth Gödel operation. This function takes two arguments and returns the intersection of the first argument with the domain of the second argument (see df-in and df-dm ). Based on the fifth case of Definition 14.2 of TakeutiZaring p. 144. (Contributed by BTernaryTau, 2-Sep-2026)

	Ref	Expression
Assertion	df-gdlop5	Could not format assertion : No typesetting found for |- ~F5 = ( x e. _V , y e. _V |-> ( x i^i dom y ) ) with typecode |-

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cgdlop5	Could not format ~F5 : No typesetting found for class ~F5 with typecode class
1		vx	$$setvarx$$
2		cvv	$$class\mathrm{V}$$
3		vy	$$setvary$$
4	1	cv	$$setvarx$$
5	3	cv	$$setvary$$
6	5	cdm	$$class\mathrm{dom}y$$
7	4 6	cin	$$class\left(x\cap \mathrm{dom}y\right)$$
8	1 3 2 2 7	cmpo	$$class\left(x\in \mathrm{V},y\in \mathrm{V}⟼x\cap \mathrm{dom}y\right)$$
9	0 8	wceq	Could not format ~F5 = ( x e. _V , y e. _V |-> ( x i^i dom y ) ) : No typesetting found for wff ~F5 = ( x e. _V , y e. _V |-> ( x i^i dom y ) ) with typecode wff