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

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

Proof

Step Hyp Ref Expression
1 isfne.1 ⊢ 𝑋 = ∪ 𝐴
2 isfne.2 ⊢ 𝑌 = ∪ 𝐵
3 1 2 isfne4 ⊢ ( 𝐴 Fne 𝐵 ↔ ( 𝑋 = 𝑌 ∧ 𝐴 ⊆ ( topGen ‘ 𝐵 ) ) )
4 simpr ⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝑋 = 𝑌 ) → 𝑋 = 𝑌 )
5 4 1 2 3eqtr3g ⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝑋 = 𝑌 ) → ∪ 𝐴 = ∪ 𝐵 )
6 uniexg ⊢ ( 𝐵 ∈ 𝑉 → ∪ 𝐵 ∈ V )
7 6 adantr ⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝑋 = 𝑌 ) → ∪ 𝐵 ∈ V )
8 5 7 eqeltrd ⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝑋 = 𝑌 ) → ∪ 𝐴 ∈ V )
9 uniexb ⊢ ( 𝐴 ∈ V ↔ ∪ 𝐴 ∈ V )
10 8 9 sylibr ⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝑋 = 𝑌 ) → 𝐴 ∈ V )
11 simpl ⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝑋 = 𝑌 ) → 𝐵 ∈ 𝑉 )
12 tgss3 ⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ 𝑉 ) → ( ( topGen ‘ 𝐴 ) ⊆ ( topGen ‘ 𝐵 ) ↔ 𝐴 ⊆ ( topGen ‘ 𝐵 ) ) )
13 10 11 12 syl2anc ⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝑋 = 𝑌 ) → ( ( topGen ‘ 𝐴 ) ⊆ ( topGen ‘ 𝐵 ) ↔ 𝐴 ⊆ ( topGen ‘ 𝐵 ) ) )
14 13 pm5.32da ⊢ ( 𝐵 ∈ 𝑉 → ( ( 𝑋 = 𝑌 ∧ ( topGen ‘ 𝐴 ) ⊆ ( topGen ‘ 𝐵 ) ) ↔ ( 𝑋 = 𝑌 ∧ 𝐴 ⊆ ( topGen ‘ 𝐵 ) ) ) )
15 3 14 bitr4id ⊢ ( 𝐵 ∈ 𝑉 → ( 𝐴 Fne 𝐵 ↔ ( 𝑋 = 𝑌 ∧ ( topGen ‘ 𝐴 ) ⊆ ( topGen ‘ 𝐵 ) ) ) )