This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ∪ 𝑥 = ∪ 𝑦 ∧ ∀ 𝑧 ∈ 𝑥 𝑧 ⊆ ∪ ( 𝑦 ∩ 𝒫 𝑧 ) ) }

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 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ∪ 𝑥 = ∪ 𝑦 ∧ ∀ 𝑧 ∈ 𝑥 𝑧 ⊆ ∪ ( 𝑦 ∩ 𝒫 𝑧 ) ) }