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 ) ) )

Metamath Proof Explorer

Definition df-goeq

Detailed syntax breakdown