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 𝑋 ) )