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 ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) → ( ( I ↾ 𝑋 ) ∈ ( 𝐽 Cn 𝐾 ) ↔ 𝐾𝐽 ) )

Proof

Step Hyp Ref Expression
1 iscn ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) → ( ( I ↾ 𝑋 ) ∈ ( 𝐽 Cn 𝐾 ) ↔ ( ( I ↾ 𝑋 ) : 𝑋𝑋 ∧ ∀ 𝑥𝐾 ( ( I ↾ 𝑋 ) “ 𝑥 ) ∈ 𝐽 ) ) )
2 f1oi ( I ↾ 𝑋 ) : 𝑋1-1-onto𝑋
3 f1of ( ( I ↾ 𝑋 ) : 𝑋1-1-onto𝑋 → ( I ↾ 𝑋 ) : 𝑋𝑋 )
4 2 3 ax-mp ( I ↾ 𝑋 ) : 𝑋𝑋
5 4 biantrur ( ∀ 𝑥𝐾 ( ( I ↾ 𝑋 ) “ 𝑥 ) ∈ 𝐽 ↔ ( ( I ↾ 𝑋 ) : 𝑋𝑋 ∧ ∀ 𝑥𝐾 ( ( I ↾ 𝑋 ) “ 𝑥 ) ∈ 𝐽 ) )
6 1 5 bitr4di ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) → ( ( I ↾ 𝑋 ) ∈ ( 𝐽 Cn 𝐾 ) ↔ ∀ 𝑥𝐾 ( ( I ↾ 𝑋 ) “ 𝑥 ) ∈ 𝐽 ) )
7 cnvresid ( I ↾ 𝑋 ) = ( I ↾ 𝑋 )
8 7 imaeq1i ( ( I ↾ 𝑋 ) “ 𝑥 ) = ( ( I ↾ 𝑋 ) “ 𝑥 )
9 elssuni ( 𝑥𝐾𝑥 𝐾 )
10 9 adantl ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ 𝑥𝐾 ) → 𝑥 𝐾 )
11 toponuni ( 𝐾 ∈ ( TopOn ‘ 𝑋 ) → 𝑋 = 𝐾 )
12 11 ad2antlr ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ 𝑥𝐾 ) → 𝑋 = 𝐾 )
13 10 12 sseqtrrd ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ 𝑥𝐾 ) → 𝑥𝑋 )
14 resiima ( 𝑥𝑋 → ( ( I ↾ 𝑋 ) “ 𝑥 ) = 𝑥 )
15 13 14 syl ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ 𝑥𝐾 ) → ( ( I ↾ 𝑋 ) “ 𝑥 ) = 𝑥 )
16 8 15 syl5eq ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ 𝑥𝐾 ) → ( ( I ↾ 𝑋 ) “ 𝑥 ) = 𝑥 )
17 16 eleq1d ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ 𝑥𝐾 ) → ( ( ( I ↾ 𝑋 ) “ 𝑥 ) ∈ 𝐽𝑥𝐽 ) )
18 17 ralbidva ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) → ( ∀ 𝑥𝐾 ( ( I ↾ 𝑋 ) “ 𝑥 ) ∈ 𝐽 ↔ ∀ 𝑥𝐾 𝑥𝐽 ) )
19 dfss3 ( 𝐾𝐽 ↔ ∀ 𝑥𝐾 𝑥𝐽 )
20 18 19 bitr4di ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) → ( ∀ 𝑥𝐾 ( ( I ↾ 𝑋 ) “ 𝑥 ) ∈ 𝐽𝐾𝐽 ) )
21 6 20 bitrd ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) → ( ( I ↾ 𝑋 ) ∈ ( 𝐽 Cn 𝐾 ) ↔ 𝐾𝐽 ) )