Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Jeff Hankins
Refinements
df-fne
Next ⟩
fnerel
Metamath Proof Explorer
Ascii
Unicode
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