Metamath Proof Explorer

Theorem isfne3

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

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

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 eltg3 ⊢ B ∈ C → x ∈ topGen ⁡ B ↔ ∃ y y ⊆ B ∧ x = ⋃ y
6 5 ralbidv ⊢ B ∈ C → ∀ x ∈ A x ∈ topGen ⁡ B ↔ ∀ x ∈ A ∃ y y ⊆ B ∧ x = ⋃ y
7 4 6 bitrid ⊢ B ∈ C → A ⊆ topGen ⁡ B ↔ ∀ x ∈ A ∃ y y ⊆ B ∧ x = ⋃ y
8 7 anbi2d ⊢ B ∈ C → X = Y ∧ A ⊆ topGen ⁡ B ↔ X = Y ∧ ∀ x ∈ A ∃ y y ⊆ B ∧ x = ⋃ y
9 3 8 bitrid ⊢ B ∈ C → A Fne B ↔ X = Y ∧ ∀ x ∈ A ∃ y y ⊆ B ∧ x = ⋃ y