Metamath Proof Explorer

Theorem isfne4b

Description: A condition for a topology to be finer than another. (Contributed by Jeff Hankins, 28-Sep-2009) (Revised by Mario Carneiro, 11-Sep-2015)

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

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 simpr ⊢ B ∈ V ∧ X = Y → X = Y
5 4 1 2 3eqtr3g ⊢ B ∈ V ∧ X = Y → ⋃ A = ⋃ B
6 uniexg ⊢ B ∈ V → ⋃ B ∈ V
7 6 adantr ⊢ B ∈ V ∧ X = Y → ⋃ B ∈ V
8 5 7 eqeltrd ⊢ B ∈ V ∧ X = Y → ⋃ A ∈ V
9 uniexb ⊢ A ∈ V ↔ ⋃ A ∈ V
10 8 9 sylibr ⊢ B ∈ V ∧ X = Y → A ∈ V
11 simpl ⊢ B ∈ V ∧ X = Y → B ∈ V
12 tgss3 ⊢ A ∈ V ∧ B ∈ V → topGen ⁡ A ⊆ topGen ⁡ B ↔ A ⊆ topGen ⁡ B
13 10 11 12 syl2anc ⊢ B ∈ V ∧ X = Y → topGen ⁡ A ⊆ topGen ⁡ B ↔ A ⊆ topGen ⁡ B
14 13 pm5.32da ⊢ B ∈ V → X = Y ∧ topGen ⁡ A ⊆ topGen ⁡ B ↔ X = Y ∧ A ⊆ topGen ⁡ B
15 3 14 bitr4id ⊢ B ∈ V → A Fne B ↔ X = Y ∧ topGen ⁡ A ⊆ topGen ⁡ B