Definition df-gdlop1

Description: Define the first Gödel operation. This function takes two arguments and returns the unordered pair containing both (see df-pr ). Based on the first case of Definition 14.2 of TakeutiZaring p. 144. (Contributed by BTernaryTau, 2-Sep-2026)

	Ref	Expression
Assertion	df-gdlop1	Could not format assertion : No typesetting found for |- ~F1 = ( x e. _V , y e. _V |-> { x , y } ) with typecode |-

Detailed syntax breakdown

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