Definition df-goeq 31340

Description: Define the Godel-set of equality. Here the arguments x = <. N , P >. correspond to v_N and v_P , so ( (/) =g 1o ) actually means v₀ = v₁ , not 0 = 1. Here we use the trick mentioned in ax-ext 2602 to introduce equality as a defined notion in terms of e.g. The expression suc ( u u. v ) = max ( u , v ) + 1 here is a convenient way of getting a dummy variable distinct from u and v. (Contributed by Mario Carneiro, 14-Jul-2013.)

Assertion

Ref	Expression
df-goeq	|- =g = ( u e. om , v e. om |-> [_ suc ( u u. v ) / w ]_ A.g w ( ( w e.g u ) <->g ( w e.g v ) ) )

Distinct variable group:   v, u, w

Detailed syntax breakdown of Definition df-goeq

Step	Hyp	Ref	Expression
1		cgoq 31333	. 2 class =g
2		vu	. . 3 setvar u
3		vv	. . 3 setvar v
4		com 7065	. . 3 class om
5		vw	. . . 4 setvar w
6	2	cv 1482	. . . . . 6 class u
7	3	cv 1482	. . . . . 6 class v
8	6, 7	cun 3572	. . . . 5 class ( u u. v )
9	8	csuc 5725	. . . 4 class suc ( u u. v )
10	5	cv 1482	. . . . . . 7 class w
11		cgoe 31315	. . . . . . 7 class e.g
12	10, 6, 11	co 6650	. . . . . 6 class ( w e.g u )
13	10, 7, 11	co 6650	. . . . . 6 class ( w e.g v )
14		cgob 31332	. . . . . 6 class <->g
15	12, 13, 14	co 6650	. . . . 5 class ( ( w e.g u ) <->g ( w e.g v ) )
16	15, 10	cgol 31317	. . . 4 class A.g w ( ( w e.g u ) <->g ( w e.g v ) )
17	5, 9, 16	csb 3533	. . 3 class [_ suc ( u u. v ) / w ]_ A.g w ( ( w e.g u ) <->g ( w e.g v ) )
18	2, 3, 4, 4, 17	cmpt2 6652	. 2 class ( u e. om , v e. om |-> [_ suc ( u u. v ) / w ]_ A.g w ( ( w e.g u ) <->g ( w e.g v ) ) )
19	1, 18	wceq 1483	1 wff =g = ( u e. om , v e. om |-> [_ suc ( u u. v ) / w ]_ A.g w ( ( w e.g u ) <->g ( w e.g v ) ) )

This definition is referenced by: (None)