Metamath Proof Explorer

Theorem isfne2

Description: The predicate " B is finer than A ". (Contributed by Jeff Hankins, 28-Sep-2009) (Proof shortened by Mario Carneiro, 11-Sep-2015)

Ref Expression
Hypotheses isfne.1 ⊢ X = ⋃ A
isfne.2 ⊢ Y = ⋃ B
Assertion isfne2 ⊢ B ∈ C → A Fne B ↔ X = Y ∧ ∀ x ∈ A ∀ y ∈ x ∃ z ∈ B y ∈ z ∧ z ⊆ x

Proof

Step Hyp Ref Expression
1 isfne.1 ⊢ X = ⋃ A
2 isfne.2 ⊢ Y = ⋃ B
3 1 2 isfne4 ⊢ A Fne B ↔ X = Y ∧ A ⊆ topGen ⁡ B
4 dfss3 ⊢ A ⊆ topGen ⁡ B ↔ ∀ x ∈ A x ∈ topGen ⁡ B
5 eltg2b ⊢ B ∈ C → x ∈ topGen ⁡ B ↔ ∀ y ∈ x ∃ z ∈ B y ∈ z ∧ z ⊆ x
6 5 ralbidv ⊢ B ∈ C → ∀ x ∈ A x ∈ topGen ⁡ B ↔ ∀ x ∈ A ∀ y ∈ x ∃ z ∈ B y ∈ z ∧ z ⊆ x
7 4 6 bitrid ⊢ B ∈ C → A ⊆ topGen ⁡ B ↔ ∀ x ∈ A ∀ y ∈ x ∃ z ∈ B y ∈ z ∧ z ⊆ x
8 7 anbi2d ⊢ B ∈ C → X = Y ∧ A ⊆ topGen ⁡ B ↔ X = Y ∧ ∀ x ∈ A ∀ y ∈ x ∃ z ∈ B y ∈ z ∧ z ⊆ x
9 3 8 bitrid ⊢ B ∈ C → A Fne B ↔ X = Y ∧ ∀ x ∈ A ∀ y ∈ x ∃ z ∈ B y ∈ z ∧ z ⊆ x