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 ⊢ 𝑋 = ∪ 𝐴
isfne.2 ⊢ 𝑌 = ∪ 𝐵
Assertion isfne4 ( 𝐴 Fne 𝐵 ↔ ( 𝑋 = 𝑌 ∧ 𝐴 ⊆ ( topGen ‘ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 isfne.1 ⊢ 𝑋 = ∪ 𝐴
2 isfne.2 ⊢ 𝑌 = ∪ 𝐵
3 fnerel ⊢ Rel Fne
4 3 brrelex2i ⊢ ( 𝐴 Fne 𝐵 → 𝐵 ∈ V )
5 simpl ⊢ ( ( 𝑋 = 𝑌 ∧ 𝐴 ⊆ ( topGen ‘ 𝐵 ) ) → 𝑋 = 𝑌 )
6 5 1 2 3eqtr3g ⊢ ( ( 𝑋 = 𝑌 ∧ 𝐴 ⊆ ( topGen ‘ 𝐵 ) ) → ∪ 𝐴 = ∪ 𝐵 )
7 fvex ⊢ ( topGen ‘ 𝐵 ) ∈ V
8 7 ssex ⊢ ( 𝐴 ⊆ ( topGen ‘ 𝐵 ) → 𝐴 ∈ V )
9 8 adantl ⊢ ( ( 𝑋 = 𝑌 ∧ 𝐴 ⊆ ( topGen ‘ 𝐵 ) ) → 𝐴 ∈ V )
10 9 uniexd ⊢ ( ( 𝑋 = 𝑌 ∧ 𝐴 ⊆ ( topGen ‘ 𝐵 ) ) → ∪ 𝐴 ∈ V )
11 6 10 eqeltrrd ⊢ ( ( 𝑋 = 𝑌 ∧ 𝐴 ⊆ ( topGen ‘ 𝐵 ) ) → ∪ 𝐵 ∈ V )
12 uniexb ⊢ ( 𝐵 ∈ V ↔ ∪ 𝐵 ∈ V )
13 11 12 sylibr ⊢ ( ( 𝑋 = 𝑌 ∧ 𝐴 ⊆ ( topGen ‘ 𝐵 ) ) → 𝐵 ∈ V )
14 1 2 isfne ⊢ ( 𝐵 ∈ V → ( 𝐴 Fne 𝐵 ↔ ( 𝑋 = 𝑌 ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ⊆ ∪ ( 𝐵 ∩ 𝒫 𝑥 ) ) ) )
15 dfss3 ⊢ ( 𝐴 ⊆ ( topGen ‘ 𝐵 ) ↔ ∀ 𝑥 ∈ 𝐴 𝑥 ∈ ( topGen ‘ 𝐵 ) )
16 eltg ⊢ ( 𝐵 ∈ V → ( 𝑥 ∈ ( topGen ‘ 𝐵 ) ↔ 𝑥 ⊆ ∪ ( 𝐵 ∩ 𝒫 𝑥 ) ) )
17 16 ralbidv ⊢ ( 𝐵 ∈ V → ( ∀ 𝑥 ∈ 𝐴 𝑥 ∈ ( topGen ‘ 𝐵 ) ↔ ∀ 𝑥 ∈ 𝐴 𝑥 ⊆ ∪ ( 𝐵 ∩ 𝒫 𝑥 ) ) )
18 15 17 syl5bb ⊢ ( 𝐵 ∈ V → ( 𝐴 ⊆ ( topGen ‘ 𝐵 ) ↔ ∀ 𝑥 ∈ 𝐴 𝑥 ⊆ ∪ ( 𝐵 ∩ 𝒫 𝑥 ) ) )
19 18 anbi2d ⊢ ( 𝐵 ∈ V → ( ( 𝑋 = 𝑌 ∧ 𝐴 ⊆ ( topGen ‘ 𝐵 ) ) ↔ ( 𝑋 = 𝑌 ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ⊆ ∪ ( 𝐵 ∩ 𝒫 𝑥 ) ) ) )
20 14 19 bitr4d ⊢ ( 𝐵 ∈ V → ( 𝐴 Fne 𝐵 ↔ ( 𝑋 = 𝑌 ∧ 𝐴 ⊆ ( topGen ‘ 𝐵 ) ) ) )
21 4 13 20 pm5.21nii ⊢ ( 𝐴 Fne 𝐵 ↔ ( 𝑋 = 𝑌 ∧ 𝐴 ⊆ ( topGen ‘ 𝐵 ) ) )