Metamath Proof Explorer


Theorem cnconst2

Description: A constant function is continuous. (Contributed by Mario Carneiro, 19-Mar-2015)

Ref Expression
Assertion cnconst2 JTopOnXKTopOnYBYX×BJCnK

Proof

Step Hyp Ref Expression
1 fconst6g BYX×B:XY
2 1 3ad2ant3 JTopOnXKTopOnYBYX×B:XY
3 2 adantr JTopOnXKTopOnYBYxXX×B:XY
4 simpll3 JTopOnXKTopOnYBYxXyKBY
5 simplr JTopOnXKTopOnYBYxXyKxX
6 fvconst2g BYxXX×Bx=B
7 4 5 6 syl2anc JTopOnXKTopOnYBYxXyKX×Bx=B
8 7 eleq1d JTopOnXKTopOnYBYxXyKX×BxyBy
9 simpll1 JTopOnXKTopOnYBYxXyKByJTopOnX
10 toponmax JTopOnXXJ
11 9 10 syl JTopOnXKTopOnYBYxXyKByXJ
12 simplr JTopOnXKTopOnYBYxXyKByxX
13 df-ima X×BX=ranX×BX
14 ssid XX
15 xpssres XXX×BX=X×B
16 14 15 ax-mp X×BX=X×B
17 16 rneqi ranX×BX=ranX×B
18 rnxpss ranX×BB
19 17 18 eqsstri ranX×BXB
20 simprr JTopOnXKTopOnYBYxXyKByBy
21 20 snssd JTopOnXKTopOnYBYxXyKByBy
22 19 21 sstrid JTopOnXKTopOnYBYxXyKByranX×BXy
23 13 22 eqsstrid JTopOnXKTopOnYBYxXyKByX×BXy
24 eleq2 u=XxuxX
25 imaeq2 u=XX×Bu=X×BX
26 25 sseq1d u=XX×BuyX×BXy
27 24 26 anbi12d u=XxuX×BuyxXX×BXy
28 27 rspcev XJxXX×BXyuJxuX×Buy
29 11 12 23 28 syl12anc JTopOnXKTopOnYBYxXyKByuJxuX×Buy
30 29 expr JTopOnXKTopOnYBYxXyKByuJxuX×Buy
31 8 30 sylbid JTopOnXKTopOnYBYxXyKX×BxyuJxuX×Buy
32 31 ralrimiva JTopOnXKTopOnYBYxXyKX×BxyuJxuX×Buy
33 simpl1 JTopOnXKTopOnYBYxXJTopOnX
34 simpl2 JTopOnXKTopOnYBYxXKTopOnY
35 simpr JTopOnXKTopOnYBYxXxX
36 iscnp JTopOnXKTopOnYxXX×BJCnPKxX×B:XYyKX×BxyuJxuX×Buy
37 33 34 35 36 syl3anc JTopOnXKTopOnYBYxXX×BJCnPKxX×B:XYyKX×BxyuJxuX×Buy
38 3 32 37 mpbir2and JTopOnXKTopOnYBYxXX×BJCnPKx
39 38 ralrimiva JTopOnXKTopOnYBYxXX×BJCnPKx
40 cncnp JTopOnXKTopOnYX×BJCnKX×B:XYxXX×BJCnPKx
41 40 3adant3 JTopOnXKTopOnYBYX×BJCnKX×B:XYxXX×BJCnPKx
42 2 39 41 mpbir2and JTopOnXKTopOnYBYX×BJCnK