# Metamath Proof Explorer

## 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}\phantom{\rule{.4em}{0ex}}\exists {w}\in {y}\phantom{\rule{.4em}{0ex}}{z}\subseteq {w}\right)\right\}$

### Detailed syntax breakdown

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