Definition df-gdlop2

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

	Ref	Expression
Assertion	df-gdlop2	⊢ ℱ2 = ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥 ∩ E ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cgdlop2	⊢ ℱ2
1		vx	⊢ 𝑥
2		cvv	⊢ V
3		vy	⊢ 𝑦
4	1	cv	⊢ 𝑥
5		cep	⊢ E
6	4 5	cin	⊢ ( 𝑥 ∩ E )
7	1 3 2 2 6	cmpo	⊢ ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥 ∩ E ) )
8	0 7	wceq	⊢ ℱ2 = ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥 ∩ E ) )