This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cnindis

Description: Every function is continuous when the codomain is indiscrete (trivial). (Contributed by Mario Carneiro, 9-Apr-2015) (Revised by Mario Carneiro, 21-Aug-2015)

Ref Expression
Assertion cnindis ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑉 ) → ( 𝐽 Cn { ∅ , 𝐴 } ) = ( 𝐴 ↑m 𝑋 ) )

Proof

Step Hyp Ref Expression
1 elpri ⊢ ( 𝑥 ∈ { ∅ , 𝐴 } → ( 𝑥 = ∅ ∨ 𝑥 = 𝐴 ) )
2 topontop ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝐽 ∈ Top )
3 2 ad2antrr ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑓 : 𝑋 ⟶ 𝐴 ) → 𝐽 ∈ Top )
4 0opn ⊢ ( 𝐽 ∈ Top → ∅ ∈ 𝐽 )
5 3 4 syl ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑓 : 𝑋 ⟶ 𝐴 ) → ∅ ∈ 𝐽 )
6 imaeq2 ⊢ ( 𝑥 = ∅ → ( ◡ 𝑓 “ 𝑥 ) = ( ◡ 𝑓 “ ∅ ) )
7 ima0 ⊢ ( ◡ 𝑓 “ ∅ ) = ∅
8 6 7 eqtrdi ⊢ ( 𝑥 = ∅ → ( ◡ 𝑓 “ 𝑥 ) = ∅ )
9 8 eleq1d ⊢ ( 𝑥 = ∅ → ( ( ◡ 𝑓 “ 𝑥 ) ∈ 𝐽 ↔ ∅ ∈ 𝐽 ) )
10 5 9 syl5ibrcom ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑓 : 𝑋 ⟶ 𝐴 ) → ( 𝑥 = ∅ → ( ◡ 𝑓 “ 𝑥 ) ∈ 𝐽 ) )
11 fimacnv ⊢ ( 𝑓 : 𝑋 ⟶ 𝐴 → ( ◡ 𝑓 “ 𝐴 ) = 𝑋 )
12 11 adantl ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑓 : 𝑋 ⟶ 𝐴 ) → ( ◡ 𝑓 “ 𝐴 ) = 𝑋 )
13 toponmax ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝑋 ∈ 𝐽 )
14 13 ad2antrr ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑓 : 𝑋 ⟶ 𝐴 ) → 𝑋 ∈ 𝐽 )
15 12 14 eqeltrd ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑓 : 𝑋 ⟶ 𝐴 ) → ( ◡ 𝑓 “ 𝐴 ) ∈ 𝐽 )
16 imaeq2 ⊢ ( 𝑥 = 𝐴 → ( ◡ 𝑓 “ 𝑥 ) = ( ◡ 𝑓 “ 𝐴 ) )
17 16 eleq1d ⊢ ( 𝑥 = 𝐴 → ( ( ◡ 𝑓 “ 𝑥 ) ∈ 𝐽 ↔ ( ◡ 𝑓 “ 𝐴 ) ∈ 𝐽 ) )
18 15 17 syl5ibrcom ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑓 : 𝑋 ⟶ 𝐴 ) → ( 𝑥 = 𝐴 → ( ◡ 𝑓 “ 𝑥 ) ∈ 𝐽 ) )
19 10 18 jaod ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑓 : 𝑋 ⟶ 𝐴 ) → ( ( 𝑥 = ∅ ∨ 𝑥 = 𝐴 ) → ( ◡ 𝑓 “ 𝑥 ) ∈ 𝐽 ) )
20 1 19 syl5 ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑓 : 𝑋 ⟶ 𝐴 ) → ( 𝑥 ∈ { ∅ , 𝐴 } → ( ◡ 𝑓 “ 𝑥 ) ∈ 𝐽 ) )
21 20 ralrimiv ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑓 : 𝑋 ⟶ 𝐴 ) → ∀ 𝑥 ∈ { ∅ , 𝐴 } ( ◡ 𝑓 “ 𝑥 ) ∈ 𝐽 )
22 21 ex ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑉 ) → ( 𝑓 : 𝑋 ⟶ 𝐴 → ∀ 𝑥 ∈ { ∅ , 𝐴 } ( ◡ 𝑓 “ 𝑥 ) ∈ 𝐽 ) )
23 22 pm4.71d ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑉 ) → ( 𝑓 : 𝑋 ⟶ 𝐴 ↔ ( 𝑓 : 𝑋 ⟶ 𝐴 ∧ ∀ 𝑥 ∈ { ∅ , 𝐴 } ( ◡ 𝑓 “ 𝑥 ) ∈ 𝐽 ) ) )
24 id ⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ 𝑉 )
25 elmapg ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐽 ) → ( 𝑓 ∈ ( 𝐴 ↑m 𝑋 ) ↔ 𝑓 : 𝑋 ⟶ 𝐴 ) )
26 24 13 25 syl2anr ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑉 ) → ( 𝑓 ∈ ( 𝐴 ↑m 𝑋 ) ↔ 𝑓 : 𝑋 ⟶ 𝐴 ) )
27 indistopon ⊢ ( 𝐴 ∈ 𝑉 → { ∅ , 𝐴 } ∈ ( TopOn ‘ 𝐴 ) )
28 iscn ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ { ∅ , 𝐴 } ∈ ( TopOn ‘ 𝐴 ) ) → ( 𝑓 ∈ ( 𝐽 Cn { ∅ , 𝐴 } ) ↔ ( 𝑓 : 𝑋 ⟶ 𝐴 ∧ ∀ 𝑥 ∈ { ∅ , 𝐴 } ( ◡ 𝑓 “ 𝑥 ) ∈ 𝐽 ) ) )
29 27 28 sylan2 ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑉 ) → ( 𝑓 ∈ ( 𝐽 Cn { ∅ , 𝐴 } ) ↔ ( 𝑓 : 𝑋 ⟶ 𝐴 ∧ ∀ 𝑥 ∈ { ∅ , 𝐴 } ( ◡ 𝑓 “ 𝑥 ) ∈ 𝐽 ) ) )
30 23 26 29 3bitr4rd ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑉 ) → ( 𝑓 ∈ ( 𝐽 Cn { ∅ , 𝐴 } ) ↔ 𝑓 ∈ ( 𝐴 ↑m 𝑋 ) ) )
31 30 eqrdv ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑉 ) → ( 𝐽 Cn { ∅ , 𝐴 } ) = ( 𝐴 ↑m 𝑋 ) )