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

Definition df-fne 34263
Description: Define the fineness relation for covers. (Contributed by Jeff Hankins, 28-Sep-2009.)
Assertion
Ref Expression
df-fne Fne = {⟨𝑥, 𝑦⟩ ∣ ( 𝑥 = 𝑦 ∧ ∀𝑧𝑥 𝑧 (𝑦 ∩ 𝒫 𝑧))}
Distinct variable group:   𝑥,𝑦,𝑧

Detailed syntax breakdown of Definition df-fne
StepHypRef Expression
1 cfne 34262 . 2 class Fne
2 vx . . . . . . 7 setvar 𝑥
32cv 1542 . . . . . 6 class 𝑥
43cuni 4819 . . . . 5 class 𝑥
5 vy . . . . . . 7 setvar 𝑦
65cv 1542 . . . . . 6 class 𝑦
76cuni 4819 . . . . 5 class 𝑦
84, 7wceq 1543 . . . 4 wff 𝑥 = 𝑦
9 vz . . . . . . 7 setvar 𝑧
109cv 1542 . . . . . 6 class 𝑧
1110cpw 4513 . . . . . . . 8 class 𝒫 𝑧
126, 11cin 3865 . . . . . . 7 class (𝑦 ∩ 𝒫 𝑧)
1312cuni 4819 . . . . . 6 class (𝑦 ∩ 𝒫 𝑧)
1410, 13wss 3866 . . . . 5 wff 𝑧 (𝑦 ∩ 𝒫 𝑧)
1514, 9, 3wral 3061 . . . 4 wff 𝑧𝑥 𝑧 (𝑦 ∩ 𝒫 𝑧)
168, 15wa 399 . . 3 wff ( 𝑥 = 𝑦 ∧ ∀𝑧𝑥 𝑧 (𝑦 ∩ 𝒫 𝑧))
1716, 2, 5copab 5115 . 2 class {⟨𝑥, 𝑦⟩ ∣ ( 𝑥 = 𝑦 ∧ ∀𝑧𝑥 𝑧 (𝑦 ∩ 𝒫 𝑧))}
181, 17wceq 1543 1 wff Fne = {⟨𝑥, 𝑦⟩ ∣ ( 𝑥 = 𝑦 ∧ ∀𝑧𝑥 𝑧 (𝑦 ∩ 𝒫 𝑧))}
Colors of variables: wff setvar class
This definition is referenced by:  fnerel  34264  isfne  34265
  Copyright terms: Public domain W3C validator