df-fne

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

		Ref	Expression
	Assertion	df-fne	$⊢ Fne = \{⟨x, y⟩ \| (⋃ x = ⋃ y \land \forall z \in x z \subseteq ⋃ (y \cap 𝒫 z))\}$

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

Metamath Proof Explorer