Users' Mathboxes Mathbox for Jeff Hankins < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-fne Unicode version

Definition df-fne 26263
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
StepHypRef Expression
1 cfne 26259 . 2  class  Fne
2 vx . . . . . . 7  set  x
32cv 1622 . . . . . 6  class  x
43cuni 3827 . . . . 5  class  U. x
5 vy . . . . . . 7  set  y
65cv 1622 . . . . . 6  class  y
76cuni 3827 . . . . 5  class  U. y
84, 7wceq 1623 . . . 4  wff  U. x  =  U. y
9 vz . . . . . . 7  set  z
109cv 1622 . . . . . 6  class  z
1110cpw 3625 . . . . . . . 8  class  ~P z
126, 11cin 3151 . . . . . . 7  class  ( y  i^i  ~P z )
1312cuni 3827 . . . . . 6  class  U. (
y  i^i  ~P z
)
1410, 13wss 3152 . . . . 5  wff  z  C_  U. ( y  i^i  ~P z )
1514, 9, 3wral 2543 . . . 4  wff  A. z  e.  x  z  C_  U. ( y  i^i  ~P z )
168, 15wa 358 . . 3  wff  ( U. x  =  U. y  /\  A. z  e.  x  z  C_  U. ( y  i^i  ~P z ) )
1716, 2, 5copab 4076 . 2  class  { <. x ,  y >.  |  ( U. x  =  U. y  /\  A. z  e.  x  z  C_  U. (
y  i^i  ~P z
) ) }
181, 17wceq 1623 1  wff  Fne  =  { <. x ,  y
>.  |  ( U. x  =  U. y  /\  A. z  e.  x  z  C_  U. ( y  i^i  ~P z ) ) }
Colors of variables: wff set class
This definition is referenced by:  fnerel  26267  isfne  26268
  Copyright terms: Public domain W3C validator