Definition df-ref

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

	Ref	Expression
Assertion	df-ref	$$⊢\mathrm{Ref}=\left\{⟨x,y⟩|\left(\bigcup y=\bigcup x\wedge \forall z\in x\exists w\in yz\subseteq w\right)\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cref	$$class\mathrm{Ref}$$
1		vx	$$setvarx$$
2		vy	$$setvary$$
3	2	cv	$$setvary$$
4	3	cuni	$$class\bigcup y$$
5	1	cv	$$setvarx$$
6	5	cuni	$$class\bigcup x$$
7	4 6	wceq	$$wff\bigcup y=\bigcup x$$
8		vz	$$setvarz$$
9		vw	$$setvarw$$
10	8	cv	$$setvarz$$
11	9	cv	$$setvarw$$
12	10 11	wss	$$wffz\subseteq w$$
13	12 9 3	wrex	$$wff\exists w\in yz\subseteq w$$
14	13 8 5	wral	$$wff\forall z\in x\exists w\in yz\subseteq w$$
15	7 14	wa	$$wff\left(\bigcup y=\bigcup x\wedge \forall z\in x\exists w\in yz\subseteq w\right)$$
16	15 1 2	copab	$$class\left\{⟨x,y⟩|\left(\bigcup y=\bigcup x\wedge \forall z\in x\exists w\in yz\subseteq w\right)\right\}$$
17	0 16	wceq	$$wff\mathrm{Ref}=\left\{⟨x,y⟩|\left(\bigcup y=\bigcup x\wedge \forall z\in x\exists w\in yz\subseteq w\right)\right\}$$