Theorem cnss1

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

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

Proof

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