Metamath Proof Explorer

Theorem ssidcn

Description: The identity function is a continuous function from one topology to another topology on the same set iff the domain is finer than the codomain. (Contributed by Mario Carneiro, 21-Mar-2015) (Revised by Mario Carneiro, 21-Aug-2015)

Ref Expression
Assertion ssidcn ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ X → I ↾ X ∈ J Cn K ↔ K ⊆ J

Proof

Step Hyp Ref Expression
1 iscn ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ X → I ↾ X ∈ J Cn K ↔ I ↾ X : X ⟶ X ∧ ∀ x ∈ K I ↾ X -1 x ∈ J
2 f1oi ⊢ I ↾ X : X ⟶ 1-1 onto X
3 f1of ⊢ I ↾ X : X ⟶ 1-1 onto X → I ↾ X : X ⟶ X
4 2 3 ax-mp ⊢ I ↾ X : X ⟶ X
5 4 biantrur ⊢ ∀ x ∈ K I ↾ X -1 x ∈ J ↔ I ↾ X : X ⟶ X ∧ ∀ x ∈ K I ↾ X -1 x ∈ J
6 1 5 bitr4di ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ X → I ↾ X ∈ J Cn K ↔ ∀ x ∈ K I ↾ X -1 x ∈ J
7 cnvresid ⊢ I ↾ X -1 = I ↾ X
8 7 imaeq1i ⊢ I ↾ X -1 x = I ↾ X x
9 elssuni ⊢ x ∈ K → x ⊆ ⋃ K
10 9 adantl ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ X ∧ x ∈ K → x ⊆ ⋃ K
11 toponuni ⊢ K ∈ TopOn ⁡ X → X = ⋃ K
12 11 ad2antlr ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ X ∧ x ∈ K → X = ⋃ K
13 10 12 sseqtrrd ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ X ∧ x ∈ K → x ⊆ X
14 resiima ⊢ x ⊆ X → I ↾ X x = x
15 13 14 syl ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ X ∧ x ∈ K → I ↾ X x = x
16 8 15 syl5eq ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ X ∧ x ∈ K → I ↾ X -1 x = x
17 16 eleq1d ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ X ∧ x ∈ K → I ↾ X -1 x ∈ J ↔ x ∈ J
18 17 ralbidva ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ X → ∀ x ∈ K I ↾ X -1 x ∈ J ↔ ∀ x ∈ K x ∈ J
19 dfss3 ⊢ K ⊆ J ↔ ∀ x ∈ K x ∈ J
20 18 19 bitr4di ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ X → ∀ x ∈ K I ↾ X -1 x ∈ J ↔ K ⊆ J
21 6 20 bitrd ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ X → I ↾ X ∈ J Cn K ↔ K ⊆ J