Metamath Proof Explorer


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 | x = y z x z y 𝒫 z

Detailed syntax breakdown

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 𝒫 z
12 11 cuni class y 𝒫 z
13 9 12 wss wff z y 𝒫 z
14 13 8 3 wral wff z x z y 𝒫 z
15 7 14 wa wff x = y z x z y 𝒫 z
16 15 1 2 copab class x y | x = y z x z y 𝒫 z
17 0 16 wceq wff Fne = x y | x = y z x z y 𝒫 z