Definition df-fne 37125

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

Step	Hyp	Ref	Expression
1		cfne 37124	. 2 class Fne
2		vx	. . . . . . 7 setvar 𝑥
3	2	cv 1569	. . . . . 6 class 𝑥
4	3	cuni 4867	. . . . 5 class ∪ 𝑥
5		vy	. . . . . . 7 setvar 𝑦
6	5	cv 1569	. . . . . 6 class 𝑦
7	6	cuni 4867	. . . . 5 class ∪ 𝑦
8	4, 7	wceq 1570	. . . 4 wff ∪ 𝑥 = ∪ 𝑦
9		vz	. . . . . . 7 setvar 𝑧
10	9	cv 1569	. . . . . 6 class 𝑧
11	10	cpw 4557	. . . . . . . 8 class 𝒫 𝑧
12	6, 11	cin 3898	. . . . . . 7 class (𝑦 ∩ 𝒫 𝑧)
13	12	cuni 4867	. . . . . 6 class ∪ (𝑦 ∩ 𝒫 𝑧)
14	10, 13	wss 3899	. . . . 5 wff 𝑧 ⊆ ∪ (𝑦 ∩ 𝒫 𝑧)
15	14, 9, 3	wral 3077	. . . 4 wff ∀𝑧 ∈ 𝑥 𝑧 ⊆ ∪ (𝑦 ∩ 𝒫 𝑧)
16	8, 15	wa 401	. . 3 wff (∪ 𝑥 = ∪ 𝑦 ∧ ∀𝑧 ∈ 𝑥 𝑧 ⊆ ∪ (𝑦 ∩ 𝒫 𝑧))
17	16, 2, 5	copab 5167	. 2 class {⟨𝑥, 𝑦⟩ ∣ (∪ 𝑥 = ∪ 𝑦 ∧ ∀𝑧 ∈ 𝑥 𝑧 ⊆ ∪ (𝑦 ∩ 𝒫 𝑧))}
18	1, 17	wceq 1570	1 wff Fne = {⟨𝑥, 𝑦⟩ ∣ (∪ 𝑥 = ∪ 𝑦 ∧ ∀𝑧 ∈ 𝑥 𝑧 ⊆ ∪ (𝑦 ∩ 𝒫 𝑧))}

This definition is used by:  fnerel  37126  isfne  37127