Definition df-fne

Description: Define the fineness relation for covers. (Contributed by Jeff Hankins, 28-Sep-2009)

	Ref	Expression
Assertion	df-fne	⊢ Fne = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ∪ 𝑥 = ∪ 𝑦 ∧ ∀ 𝑧 ∈ 𝑥 𝑧 ⊆ ∪ ( 𝑦 ∩ 𝒫 𝑧 ) ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cfne	⊢ Fne
1		vx	⊢ 𝑥
2		vy	⊢ 𝑦
3	1	cv	⊢ 𝑥
4	3	cuni	⊢ ∪ 𝑥
5	2	cv	⊢ 𝑦
6	5	cuni	⊢ ∪ 𝑦
7	4 6	wceq	⊢ ∪ 𝑥 = ∪ 𝑦
8		vz	⊢ 𝑧
9	8	cv	⊢ 𝑧
10	9	cpw	⊢ 𝒫 𝑧
11	5 10	cin	⊢ ( 𝑦 ∩ 𝒫 𝑧 )
12	11	cuni	⊢ ∪ ( 𝑦 ∩ 𝒫 𝑧 )
13	9 12	wss	⊢ 𝑧 ⊆ ∪ ( 𝑦 ∩ 𝒫 𝑧 )
14	13 8 3	wral	⊢ ∀ 𝑧 ∈ 𝑥 𝑧 ⊆ ∪ ( 𝑦 ∩ 𝒫 𝑧 )
15	7 14	wa	⊢ ( ∪ 𝑥 = ∪ 𝑦 ∧ ∀ 𝑧 ∈ 𝑥 𝑧 ⊆ ∪ ( 𝑦 ∩ 𝒫 𝑧 ) )
16	15 1 2	copab	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ∪ 𝑥 = ∪ 𝑦 ∧ ∀ 𝑧 ∈ 𝑥 𝑧 ⊆ ∪ ( 𝑦 ∩ 𝒫 𝑧 ) ) }
17	0 16	wceq	⊢ Fne = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ∪ 𝑥 = ∪ 𝑦 ∧ ∀ 𝑧 ∈ 𝑥 𝑧 ⊆ ∪ ( 𝑦 ∩ 𝒫 𝑧 ) ) }