Definition df-fne 32332

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

Assertion

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

Distinct variable group:   x, y, z

Detailed syntax breakdown of Definition df-fne

Step	Hyp	Ref	Expression
1		cfne 32331	. 2 class Fne
2		vx	. . . . . . 7 setvar x
3	2	cv 1482	. . . . . 6 class x
4	3	cuni 4436	. . . . 5 class U. x
5		vy	. . . . . . 7 setvar y
6	5	cv 1482	. . . . . 6 class y
7	6	cuni 4436	. . . . 5 class U. y
8	4, 7	wceq 1483	. . . 4 wff U. x = U. y
9		vz	. . . . . . 7 setvar z
10	9	cv 1482	. . . . . 6 class z
11	10	cpw 4158	. . . . . . . 8 class ~P z
12	6, 11	cin 3573	. . . . . . 7 class ( y i^i ~P z )
13	12	cuni 4436	. . . . . 6 class U. ( y i^i ~P z )
14	10, 13	wss 3574	. . . . 5 wff z C_ U. ( y i^i ~P z )
15	14, 9, 3	wral 2912	. . . 4 wff A. z e. x z C_ U. ( y i^i ~P z )
16	8, 15	wa 384	. . 3 wff ( U. x = U. y /\ A. z e. x z C_ U. ( y i^i ~P z ) )
17	16, 2, 5	copab 4712	. 2 class { <. x , y >. | ( U. x = U. y /\ A. z e. x z C_ U. ( y i^i ~P z ) ) }
18	1, 17	wceq 1483	1 wff Fne = { <. x , y >. | ( U. x = U. y /\ A. z e. x z C_ U. ( y i^i ~P z ) ) }

This definition is referenced by:  fnerel  32333  isfne  32334