Definition df-goeq

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_0 = v_1 , not 0 = 1 . Here we use the trick mentioned in ax-ext 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)

	Ref	Expression
Assertion	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 ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cgoq	|- =g
1		vu	|- u
2		com	|- _om
3		vv	|- v
4	1	cv	|- u
5	3	cv	|- v
6	4 5	cun	|- ( u u. v )
7	6	csuc	|- suc ( u u. v )
8		vw	|- w
9	8	cv	|- w
10		cgoe	|- e.g
11	9 4 10	co	|- ( w e.g u )
12		cgob	|- <->g
13	9 5 10	co	|- ( w e.g v )
14	11 13 12	co	|- ( ( w e.g u ) <->g ( w e.g v ) )
15	14 9	cgol	|- A.g w ( ( w e.g u ) <->g ( w e.g v ) )
16	8 7 15	csb	|- [_ suc ( u u. v ) / w ]_ A.g w ( ( w e.g u ) <->g ( w e.g v ) )
17	1 3 2 2 16	cmpo	|- ( u e. _om , v e. _om |-> [_ suc ( u u. v ) / w ]_ A.g w ( ( w e.g u ) <->g ( w e.g v ) ) )
18	0 17	wceq	|- =g = ( u e. _om , v e. _om |-> [_ suc ( u u. v ) / w ]_ A.g w ( ( w e.g u ) <->g ( w e.g v ) ) )