Metamath Proof Explorer

Theorem topssnei

Description: A finer topology has more neighborhoods. (Contributed by Mario Carneiro, 9-Apr-2015)

Ref Expression
Hypotheses tpnei.1 ⊢ 𝑋 = ∪ 𝐽
topssnei.2 ⊢ 𝑌 = ∪ 𝐾
Assertion topssnei ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝑋 = 𝑌 ) ∧ 𝐽 ⊆ 𝐾 ) → ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ⊆ ( ( nei ‘ 𝐾 ) ‘ 𝑆 ) )

Proof

Step Hyp Ref Expression
1 tpnei.1 ⊢ 𝑋 = ∪ 𝐽
2 topssnei.2 ⊢ 𝑌 = ∪ 𝐾
3 simpl2 ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝑋 = 𝑌 ) ∧ ( 𝐽 ⊆ 𝐾 ∧ 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) ) → 𝐾 ∈ Top )
4 simprl ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝑋 = 𝑌 ) ∧ ( 𝐽 ⊆ 𝐾 ∧ 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) ) → 𝐽 ⊆ 𝐾 )
5 simpl1 ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝑋 = 𝑌 ) ∧ ( 𝐽 ⊆ 𝐾 ∧ 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) ) → 𝐽 ∈ Top )
6 simprr ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝑋 = 𝑌 ) ∧ ( 𝐽 ⊆ 𝐾 ∧ 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) ) → 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) )
7 1 neii1 ⊢ ( ( 𝐽 ∈ Top ∧ 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) → 𝑥 ⊆ 𝑋 )
8 5 6 7 syl2anc ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝑋 = 𝑌 ) ∧ ( 𝐽 ⊆ 𝐾 ∧ 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) ) → 𝑥 ⊆ 𝑋 )
9 1 ntropn ⊢ ( ( 𝐽 ∈ Top ∧ 𝑥 ⊆ 𝑋 ) → ( ( int ‘ 𝐽 ) ‘ 𝑥 ) ∈ 𝐽 )
10 5 8 9 syl2anc ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝑋 = 𝑌 ) ∧ ( 𝐽 ⊆ 𝐾 ∧ 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) ) → ( ( int ‘ 𝐽 ) ‘ 𝑥 ) ∈ 𝐽 )
11 4 10 sseldd ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝑋 = 𝑌 ) ∧ ( 𝐽 ⊆ 𝐾 ∧ 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) ) → ( ( int ‘ 𝐽 ) ‘ 𝑥 ) ∈ 𝐾 )
12 1 neiss2 ⊢ ( ( 𝐽 ∈ Top ∧ 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) → 𝑆 ⊆ 𝑋 )
13 5 6 12 syl2anc ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝑋 = 𝑌 ) ∧ ( 𝐽 ⊆ 𝐾 ∧ 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) ) → 𝑆 ⊆ 𝑋 )
14 1 neiint ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑥 ⊆ 𝑋 ) → ( 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ↔ 𝑆 ⊆ ( ( int ‘ 𝐽 ) ‘ 𝑥 ) ) )
15 5 13 8 14 syl3anc ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝑋 = 𝑌 ) ∧ ( 𝐽 ⊆ 𝐾 ∧ 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) ) → ( 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ↔ 𝑆 ⊆ ( ( int ‘ 𝐽 ) ‘ 𝑥 ) ) )
16 6 15 mpbid ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝑋 = 𝑌 ) ∧ ( 𝐽 ⊆ 𝐾 ∧ 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) ) → 𝑆 ⊆ ( ( int ‘ 𝐽 ) ‘ 𝑥 ) )
17 opnneiss ⊢ ( ( 𝐾 ∈ Top ∧ ( ( int ‘ 𝐽 ) ‘ 𝑥 ) ∈ 𝐾 ∧ 𝑆 ⊆ ( ( int ‘ 𝐽 ) ‘ 𝑥 ) ) → ( ( int ‘ 𝐽 ) ‘ 𝑥 ) ∈ ( ( nei ‘ 𝐾 ) ‘ 𝑆 ) )
18 3 11 16 17 syl3anc ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝑋 = 𝑌 ) ∧ ( 𝐽 ⊆ 𝐾 ∧ 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) ) → ( ( int ‘ 𝐽 ) ‘ 𝑥 ) ∈ ( ( nei ‘ 𝐾 ) ‘ 𝑆 ) )
19 1 ntrss2 ⊢ ( ( 𝐽 ∈ Top ∧ 𝑥 ⊆ 𝑋 ) → ( ( int ‘ 𝐽 ) ‘ 𝑥 ) ⊆ 𝑥 )
20 5 8 19 syl2anc ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝑋 = 𝑌 ) ∧ ( 𝐽 ⊆ 𝐾 ∧ 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) ) → ( ( int ‘ 𝐽 ) ‘ 𝑥 ) ⊆ 𝑥 )
21 simpl3 ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝑋 = 𝑌 ) ∧ ( 𝐽 ⊆ 𝐾 ∧ 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) ) → 𝑋 = 𝑌 )
22 8 21 sseqtrd ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝑋 = 𝑌 ) ∧ ( 𝐽 ⊆ 𝐾 ∧ 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) ) → 𝑥 ⊆ 𝑌 )
23 2 ssnei2 ⊢ ( ( ( 𝐾 ∈ Top ∧ ( ( int ‘ 𝐽 ) ‘ 𝑥 ) ∈ ( ( nei ‘ 𝐾 ) ‘ 𝑆 ) ) ∧ ( ( ( int ‘ 𝐽 ) ‘ 𝑥 ) ⊆ 𝑥 ∧ 𝑥 ⊆ 𝑌 ) ) → 𝑥 ∈ ( ( nei ‘ 𝐾 ) ‘ 𝑆 ) )
24 3 18 20 22 23 syl22anc ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝑋 = 𝑌 ) ∧ ( 𝐽 ⊆ 𝐾 ∧ 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) ) → 𝑥 ∈ ( ( nei ‘ 𝐾 ) ‘ 𝑆 ) )
25 24 expr ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝑋 = 𝑌 ) ∧ 𝐽 ⊆ 𝐾 ) → ( 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) → 𝑥 ∈ ( ( nei ‘ 𝐾 ) ‘ 𝑆 ) ) )
26 25 ssrdv ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝑋 = 𝑌 ) ∧ 𝐽 ⊆ 𝐾 ) → ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ⊆ ( ( nei ‘ 𝐾 ) ‘ 𝑆 ) )