This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fneval

Description: Two covers are finer than each other iff they are both bases for the same topology. (Contributed by Mario Carneiro, 11-Sep-2015)

Ref Expression
Hypothesis fneval.1 ⊢ ∼ = ( Fne ∩ ◡ Fne )
Assertion fneval ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐴 ∼ 𝐵 ↔ ( topGen ‘ 𝐴 ) = ( topGen ‘ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 fneval.1 ⊢ ∼ = ( Fne ∩ ◡ Fne )
2 1 breqi ⊢ ( 𝐴 ∼ 𝐵 ↔ 𝐴 ( Fne ∩ ◡ Fne ) 𝐵 )
3 brin ⊢ ( 𝐴 ( Fne ∩ ◡ Fne ) 𝐵 ↔ ( 𝐴 Fne 𝐵 ∧ 𝐴 ◡ Fne 𝐵 ) )
4 fnerel ⊢ Rel Fne
5 4 relbrcnv ⊢ ( 𝐴 ◡ Fne 𝐵 ↔ 𝐵 Fne 𝐴 )
6 5 anbi2i ⊢ ( ( 𝐴 Fne 𝐵 ∧ 𝐴 ◡ Fne 𝐵 ) ↔ ( 𝐴 Fne 𝐵 ∧ 𝐵 Fne 𝐴 ) )
7 3 6 bitri ⊢ ( 𝐴 ( Fne ∩ ◡ Fne ) 𝐵 ↔ ( 𝐴 Fne 𝐵 ∧ 𝐵 Fne 𝐴 ) )
8 2 7 bitri ⊢ ( 𝐴 ∼ 𝐵 ↔ ( 𝐴 Fne 𝐵 ∧ 𝐵 Fne 𝐴 ) )
9 eqid ⊢ ∪ 𝐴 = ∪ 𝐴
10 eqid ⊢ ∪ 𝐵 = ∪ 𝐵
11 9 10 isfne4b ⊢ ( 𝐵 ∈ 𝑊 → ( 𝐴 Fne 𝐵 ↔ ( ∪ 𝐴 = ∪ 𝐵 ∧ ( topGen ‘ 𝐴 ) ⊆ ( topGen ‘ 𝐵 ) ) ) )
12 10 9 isfne4b ⊢ ( 𝐴 ∈ 𝑉 → ( 𝐵 Fne 𝐴 ↔ ( ∪ 𝐵 = ∪ 𝐴 ∧ ( topGen ‘ 𝐵 ) ⊆ ( topGen ‘ 𝐴 ) ) ) )
13 eqcom ⊢ ( ∪ 𝐵 = ∪ 𝐴 ↔ ∪ 𝐴 = ∪ 𝐵 )
14 13 anbi1i ⊢ ( ( ∪ 𝐵 = ∪ 𝐴 ∧ ( topGen ‘ 𝐵 ) ⊆ ( topGen ‘ 𝐴 ) ) ↔ ( ∪ 𝐴 = ∪ 𝐵 ∧ ( topGen ‘ 𝐵 ) ⊆ ( topGen ‘ 𝐴 ) ) )
15 12 14 bitrdi ⊢ ( 𝐴 ∈ 𝑉 → ( 𝐵 Fne 𝐴 ↔ ( ∪ 𝐴 = ∪ 𝐵 ∧ ( topGen ‘ 𝐵 ) ⊆ ( topGen ‘ 𝐴 ) ) ) )
16 11 15 bi2anan9r ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ( 𝐴 Fne 𝐵 ∧ 𝐵 Fne 𝐴 ) ↔ ( ( ∪ 𝐴 = ∪ 𝐵 ∧ ( topGen ‘ 𝐴 ) ⊆ ( topGen ‘ 𝐵 ) ) ∧ ( ∪ 𝐴 = ∪ 𝐵 ∧ ( topGen ‘ 𝐵 ) ⊆ ( topGen ‘ 𝐴 ) ) ) ) )
17 eqss ⊢ ( ( topGen ‘ 𝐴 ) = ( topGen ‘ 𝐵 ) ↔ ( ( topGen ‘ 𝐴 ) ⊆ ( topGen ‘ 𝐵 ) ∧ ( topGen ‘ 𝐵 ) ⊆ ( topGen ‘ 𝐴 ) ) )
18 17 anbi2i ⊢ ( ( ∪ 𝐴 = ∪ 𝐵 ∧ ( topGen ‘ 𝐴 ) = ( topGen ‘ 𝐵 ) ) ↔ ( ∪ 𝐴 = ∪ 𝐵 ∧ ( ( topGen ‘ 𝐴 ) ⊆ ( topGen ‘ 𝐵 ) ∧ ( topGen ‘ 𝐵 ) ⊆ ( topGen ‘ 𝐴 ) ) ) )
19 anandi ⊢ ( ( ∪ 𝐴 = ∪ 𝐵 ∧ ( ( topGen ‘ 𝐴 ) ⊆ ( topGen ‘ 𝐵 ) ∧ ( topGen ‘ 𝐵 ) ⊆ ( topGen ‘ 𝐴 ) ) ) ↔ ( ( ∪ 𝐴 = ∪ 𝐵 ∧ ( topGen ‘ 𝐴 ) ⊆ ( topGen ‘ 𝐵 ) ) ∧ ( ∪ 𝐴 = ∪ 𝐵 ∧ ( topGen ‘ 𝐵 ) ⊆ ( topGen ‘ 𝐴 ) ) ) )
20 18 19 bitri ⊢ ( ( ∪ 𝐴 = ∪ 𝐵 ∧ ( topGen ‘ 𝐴 ) = ( topGen ‘ 𝐵 ) ) ↔ ( ( ∪ 𝐴 = ∪ 𝐵 ∧ ( topGen ‘ 𝐴 ) ⊆ ( topGen ‘ 𝐵 ) ) ∧ ( ∪ 𝐴 = ∪ 𝐵 ∧ ( topGen ‘ 𝐵 ) ⊆ ( topGen ‘ 𝐴 ) ) ) )
21 16 20 bitr4di ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ( 𝐴 Fne 𝐵 ∧ 𝐵 Fne 𝐴 ) ↔ ( ∪ 𝐴 = ∪ 𝐵 ∧ ( topGen ‘ 𝐴 ) = ( topGen ‘ 𝐵 ) ) ) )
22 unieq ⊢ ( ( topGen ‘ 𝐴 ) = ( topGen ‘ 𝐵 ) → ∪ ( topGen ‘ 𝐴 ) = ∪ ( topGen ‘ 𝐵 ) )
23 unitg ⊢ ( 𝐴 ∈ 𝑉 → ∪ ( topGen ‘ 𝐴 ) = ∪ 𝐴 )
24 unitg ⊢ ( 𝐵 ∈ 𝑊 → ∪ ( topGen ‘ 𝐵 ) = ∪ 𝐵 )
25 23 24 eqeqan12d ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ∪ ( topGen ‘ 𝐴 ) = ∪ ( topGen ‘ 𝐵 ) ↔ ∪ 𝐴 = ∪ 𝐵 ) )
26 22 25 imbitrid ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ( topGen ‘ 𝐴 ) = ( topGen ‘ 𝐵 ) → ∪ 𝐴 = ∪ 𝐵 ) )
27 26 pm4.71rd ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ( topGen ‘ 𝐴 ) = ( topGen ‘ 𝐵 ) ↔ ( ∪ 𝐴 = ∪ 𝐵 ∧ ( topGen ‘ 𝐴 ) = ( topGen ‘ 𝐵 ) ) ) )
28 21 27 bitr4d ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ( 𝐴 Fne 𝐵 ∧ 𝐵 Fne 𝐴 ) ↔ ( topGen ‘ 𝐴 ) = ( topGen ‘ 𝐵 ) ) )
29 8 28 bitrid ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐴 ∼ 𝐵 ↔ ( topGen ‘ 𝐴 ) = ( topGen ‘ 𝐵 ) ) )