Metamath Proof Explorer

Theorem isfne4

Description: The predicate " B is finer than A " in terms of the topology generation function. (Contributed by Mario Carneiro, 11-Sep-2015)

Ref Expression
Hypotheses isfne.1 ⊢ X = ⋃ A
isfne.2 ⊢ Y = ⋃ B
Assertion isfne4 ⊢ A Fne B ↔ X = Y ∧ A ⊆ topGen ⁡ B

Proof

Step Hyp Ref Expression
1 isfne.1 ⊢ X = ⋃ A
2 isfne.2 ⊢ Y = ⋃ B
3 fnerel ⊢ Rel ⁡ Fne
4 3 brrelex2i ⊢ A Fne B → B ∈ V
5 simpl ⊢ X = Y ∧ A ⊆ topGen ⁡ B → X = Y
6 5 1 2 3eqtr3g ⊢ X = Y ∧ A ⊆ topGen ⁡ B → ⋃ A = ⋃ B
7 fvex ⊢ topGen ⁡ B ∈ V
8 7 ssex ⊢ A ⊆ topGen ⁡ B → A ∈ V
9 8 adantl ⊢ X = Y ∧ A ⊆ topGen ⁡ B → A ∈ V
10 9 uniexd ⊢ X = Y ∧ A ⊆ topGen ⁡ B → ⋃ A ∈ V
11 6 10 eqeltrrd ⊢ X = Y ∧ A ⊆ topGen ⁡ B → ⋃ B ∈ V
12 uniexb ⊢ B ∈ V ↔ ⋃ B ∈ V
13 11 12 sylibr ⊢ X = Y ∧ A ⊆ topGen ⁡ B → B ∈ V
14 1 2 isfne ⊢ B ∈ V → A Fne B ↔ X = Y ∧ ∀ x ∈ A x ⊆ ⋃ B ∩ 𝒫 x
15 dfss3 ⊢ A ⊆ topGen ⁡ B ↔ ∀ x ∈ A x ∈ topGen ⁡ B
16 eltg ⊢ B ∈ V → x ∈ topGen ⁡ B ↔ x ⊆ ⋃ B ∩ 𝒫 x
17 16 ralbidv ⊢ B ∈ V → ∀ x ∈ A x ∈ topGen ⁡ B ↔ ∀ x ∈ A x ⊆ ⋃ B ∩ 𝒫 x
18 15 17 syl5bb ⊢ B ∈ V → A ⊆ topGen ⁡ B ↔ ∀ x ∈ A x ⊆ ⋃ B ∩ 𝒫 x
19 18 anbi2d ⊢ B ∈ V → X = Y ∧ A ⊆ topGen ⁡ B ↔ X = Y ∧ ∀ x ∈ A x ⊆ ⋃ B ∩ 𝒫 x
20 14 19 bitr4d ⊢ B ∈ V → A Fne B ↔ X = Y ∧ A ⊆ topGen ⁡ B
21 4 13 20 pm5.21nii ⊢ A Fne B ↔ X = Y ∧ A ⊆ topGen ⁡ B