Definition df-gdlop8

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

	Ref	Expression
Assertion	df-gdlop8	⊢ ℱ8 = ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥 ∩ ( Cnv3 ‘ 𝑦 ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cgdlop8	⊢ ℱ8
1		vx	⊢ 𝑥
2		cvv	⊢ V
3		vy	⊢ 𝑦
4	1	cv	⊢ 𝑥
5		ccnv3	⊢ Cnv3
6	3	cv	⊢ 𝑦
7	6 5	cfv	⊢ ( Cnv3 ‘ 𝑦 )
8	4 7	cin	⊢ ( 𝑥 ∩ ( Cnv3 ‘ 𝑦 ) )
9	1 3 2 2 8	cmpo	⊢ ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥 ∩ ( Cnv3 ‘ 𝑦 ) ) )
10	0 9	wceq	⊢ ℱ8 = ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥 ∩ ( Cnv3 ‘ 𝑦 ) ) )