Metamath Proof Explorer

Theorem cnss2

Description: If the topology K is finer than J , then there are fewer continuous functions into K than into J from some other space. (Contributed by Mario Carneiro, 19-Mar-2015) (Revised by Mario Carneiro, 21-Aug-2015)

Ref Expression
Hypothesis cnss2.1 ⊢ 𝑌 = ∪ 𝐾
Assertion cnss2 ( ( 𝐿 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐿 ⊆ 𝐾 ) → ( 𝐽 Cn 𝐾 ) ⊆ ( 𝐽 Cn 𝐿 ) )

Proof

Step Hyp Ref Expression
1 cnss2.1 ⊢ 𝑌 = ∪ 𝐾
2 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
3 2 1 cnf ⊢ ( 𝑓 ∈ ( 𝐽 Cn 𝐾 ) → 𝑓 : ∪ 𝐽 ⟶ 𝑌 )
4 3 adantl ⊢ ( ( ( 𝐿 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐿 ⊆ 𝐾 ) ∧ 𝑓 ∈ ( 𝐽 Cn 𝐾 ) ) → 𝑓 : ∪ 𝐽 ⟶ 𝑌 )
5 simplr ⊢ ( ( ( 𝐿 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐿 ⊆ 𝐾 ) ∧ 𝑓 ∈ ( 𝐽 Cn 𝐾 ) ) → 𝐿 ⊆ 𝐾 )
6 cnima ⊢ ( ( 𝑓 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝑥 ∈ 𝐾 ) → ( ◡ 𝑓 “ 𝑥 ) ∈ 𝐽 )
7 6 ralrimiva ⊢ ( 𝑓 ∈ ( 𝐽 Cn 𝐾 ) → ∀ 𝑥 ∈ 𝐾 ( ◡ 𝑓 “ 𝑥 ) ∈ 𝐽 )
8 7 adantl ⊢ ( ( ( 𝐿 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐿 ⊆ 𝐾 ) ∧ 𝑓 ∈ ( 𝐽 Cn 𝐾 ) ) → ∀ 𝑥 ∈ 𝐾 ( ◡ 𝑓 “ 𝑥 ) ∈ 𝐽 )
9 ssralv ⊢ ( 𝐿 ⊆ 𝐾 → ( ∀ 𝑥 ∈ 𝐾 ( ◡ 𝑓 “ 𝑥 ) ∈ 𝐽 → ∀ 𝑥 ∈ 𝐿 ( ◡ 𝑓 “ 𝑥 ) ∈ 𝐽 ) )
10 5 8 9 sylc ⊢ ( ( ( 𝐿 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐿 ⊆ 𝐾 ) ∧ 𝑓 ∈ ( 𝐽 Cn 𝐾 ) ) → ∀ 𝑥 ∈ 𝐿 ( ◡ 𝑓 “ 𝑥 ) ∈ 𝐽 )
11 cntop1 ⊢ ( 𝑓 ∈ ( 𝐽 Cn 𝐾 ) → 𝐽 ∈ Top )
12 11 adantl ⊢ ( ( ( 𝐿 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐿 ⊆ 𝐾 ) ∧ 𝑓 ∈ ( 𝐽 Cn 𝐾 ) ) → 𝐽 ∈ Top )
13 toptopon2 ⊢ ( 𝐽 ∈ Top ↔ 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) )
14 12 13 sylib ⊢ ( ( ( 𝐿 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐿 ⊆ 𝐾 ) ∧ 𝑓 ∈ ( 𝐽 Cn 𝐾 ) ) → 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) )
15 simpll ⊢ ( ( ( 𝐿 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐿 ⊆ 𝐾 ) ∧ 𝑓 ∈ ( 𝐽 Cn 𝐾 ) ) → 𝐿 ∈ ( TopOn ‘ 𝑌 ) )
16 iscn ⊢ ( ( 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) ∧ 𝐿 ∈ ( TopOn ‘ 𝑌 ) ) → ( 𝑓 ∈ ( 𝐽 Cn 𝐿 ) ↔ ( 𝑓 : ∪ 𝐽 ⟶ 𝑌 ∧ ∀ 𝑥 ∈ 𝐿 ( ◡ 𝑓 “ 𝑥 ) ∈ 𝐽 ) ) )
17 14 15 16 syl2anc ⊢ ( ( ( 𝐿 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐿 ⊆ 𝐾 ) ∧ 𝑓 ∈ ( 𝐽 Cn 𝐾 ) ) → ( 𝑓 ∈ ( 𝐽 Cn 𝐿 ) ↔ ( 𝑓 : ∪ 𝐽 ⟶ 𝑌 ∧ ∀ 𝑥 ∈ 𝐿 ( ◡ 𝑓 “ 𝑥 ) ∈ 𝐽 ) ) )
18 4 10 17 mpbir2and ⊢ ( ( ( 𝐿 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐿 ⊆ 𝐾 ) ∧ 𝑓 ∈ ( 𝐽 Cn 𝐾 ) ) → 𝑓 ∈ ( 𝐽 Cn 𝐿 ) )
19 18 ex ⊢ ( ( 𝐿 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐿 ⊆ 𝐾 ) → ( 𝑓 ∈ ( 𝐽 Cn 𝐾 ) → 𝑓 ∈ ( 𝐽 Cn 𝐿 ) ) )
20 19 ssrdv ⊢ ( ( 𝐿 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐿 ⊆ 𝐾 ) → ( 𝐽 Cn 𝐾 ) ⊆ ( 𝐽 Cn 𝐿 ) )