Definition df-fne

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

	Ref	Expression
Assertion	df-fne	|- Fne = { <. x , y >. | ( U. x = U. y /\ A. z e. x z C_ U. ( y i^i ~P z ) ) }

Detailed syntax breakdown

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