Definition df-ref

Description: Define the refinement relation. (Contributed by Jeff Hankins, 18-Jan-2010)

	Ref	Expression
Assertion	df-ref	|- Ref = { <. x , y >. | ( U. y = U. x /\ A. z e. x E. w e. y z C_ w ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cref	|- Ref
1		vx	|- x
2		vy	|- y
3	2	cv	|- y
4	3	cuni	|- U. y
5	1	cv	|- x
6	5	cuni	|- U. x
7	4 6	wceq	|- U. y = U. x
8		vz	|- z
9		vw	|- w
10	8	cv	|- z
11	9	cv	|- w
12	10 11	wss	|- z C_ w
13	12 9 3	wrex	|- E. w e. y z C_ w
14	13 8 5	wral	|- A. z e. x E. w e. y z C_ w
15	7 14	wa	|- ( U. y = U. x /\ A. z e. x E. w e. y z C_ w )
16	15 1 2	copab	|- { <. x , y >. | ( U. y = U. x /\ A. z e. x E. w e. y z C_ w ) }
17	0 16	wceq	|- Ref = { <. x , y >. | ( U. y = U. x /\ A. z e. x E. w e. y z C_ w ) }