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 𝐾 ) ↔ 𝐾 ⊆ 𝐽 ) )