Definition df-fne

Description: Define the fineness relation for covers. (Contributed by Jeff Hankins, 28-Sep-2009)

	Ref	Expression
Assertion	df-fne	$$⊢\mathrm{Fne}=\left\{⟨x,y⟩|\left(\bigcup x=\bigcup y\wedge \forall z\in xz\subseteq \bigcup \left(y\cap 𝒫z\right)\right)\right\}$$

Detailed syntax breakdown

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