Metamath Proof Explorer


Theorem cnmptcom

Description: The argument converse of a continuous function is continuous. (Contributed by Mario Carneiro, 6-Jun-2014)

Ref Expression
Hypotheses cnmptcom.3 ( 𝜑𝐽 ∈ ( TopOn ‘ 𝑋 ) )
cnmptcom.4 ( 𝜑𝐾 ∈ ( TopOn ‘ 𝑌 ) )
cnmptcom.6 ( 𝜑 → ( 𝑥𝑋 , 𝑦𝑌𝐴 ) ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝐿 ) )
Assertion cnmptcom ( 𝜑 → ( 𝑦𝑌 , 𝑥𝑋𝐴 ) ∈ ( ( 𝐾 ×t 𝐽 ) Cn 𝐿 ) )

Proof

Step Hyp Ref Expression
1 cnmptcom.3 ( 𝜑𝐽 ∈ ( TopOn ‘ 𝑋 ) )
2 cnmptcom.4 ( 𝜑𝐾 ∈ ( TopOn ‘ 𝑌 ) )
3 cnmptcom.6 ( 𝜑 → ( 𝑥𝑋 , 𝑦𝑌𝐴 ) ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝐿 ) )
4 txtopon ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) → ( 𝐽 ×t 𝐾 ) ∈ ( TopOn ‘ ( 𝑋 × 𝑌 ) ) )
5 1 2 4 syl2anc ( 𝜑 → ( 𝐽 ×t 𝐾 ) ∈ ( TopOn ‘ ( 𝑋 × 𝑌 ) ) )
6 cntop2 ( ( 𝑥𝑋 , 𝑦𝑌𝐴 ) ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝐿 ) → 𝐿 ∈ Top )
7 3 6 syl ( 𝜑𝐿 ∈ Top )
8 toptopon2 ( 𝐿 ∈ Top ↔ 𝐿 ∈ ( TopOn ‘ 𝐿 ) )
9 7 8 sylib ( 𝜑𝐿 ∈ ( TopOn ‘ 𝐿 ) )
10 cnf2 ( ( ( 𝐽 ×t 𝐾 ) ∈ ( TopOn ‘ ( 𝑋 × 𝑌 ) ) ∧ 𝐿 ∈ ( TopOn ‘ 𝐿 ) ∧ ( 𝑥𝑋 , 𝑦𝑌𝐴 ) ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝐿 ) ) → ( 𝑥𝑋 , 𝑦𝑌𝐴 ) : ( 𝑋 × 𝑌 ) ⟶ 𝐿 )
11 5 9 3 10 syl3anc ( 𝜑 → ( 𝑥𝑋 , 𝑦𝑌𝐴 ) : ( 𝑋 × 𝑌 ) ⟶ 𝐿 )
12 eqid ( 𝑥𝑋 , 𝑦𝑌𝐴 ) = ( 𝑥𝑋 , 𝑦𝑌𝐴 )
13 12 fmpo ( ∀ 𝑥𝑋𝑦𝑌 𝐴 𝐿 ↔ ( 𝑥𝑋 , 𝑦𝑌𝐴 ) : ( 𝑋 × 𝑌 ) ⟶ 𝐿 )
14 ralcom ( ∀ 𝑥𝑋𝑦𝑌 𝐴 𝐿 ↔ ∀ 𝑦𝑌𝑥𝑋 𝐴 𝐿 )
15 13 14 bitr3i ( ( 𝑥𝑋 , 𝑦𝑌𝐴 ) : ( 𝑋 × 𝑌 ) ⟶ 𝐿 ↔ ∀ 𝑦𝑌𝑥𝑋 𝐴 𝐿 )
16 11 15 sylib ( 𝜑 → ∀ 𝑦𝑌𝑥𝑋 𝐴 𝐿 )
17 eqid ( 𝑦𝑌 , 𝑥𝑋𝐴 ) = ( 𝑦𝑌 , 𝑥𝑋𝐴 )
18 17 fmpo ( ∀ 𝑦𝑌𝑥𝑋 𝐴 𝐿 ↔ ( 𝑦𝑌 , 𝑥𝑋𝐴 ) : ( 𝑌 × 𝑋 ) ⟶ 𝐿 )
19 16 18 sylib ( 𝜑 → ( 𝑦𝑌 , 𝑥𝑋𝐴 ) : ( 𝑌 × 𝑋 ) ⟶ 𝐿 )
20 19 ffnd ( 𝜑 → ( 𝑦𝑌 , 𝑥𝑋𝐴 ) Fn ( 𝑌 × 𝑋 ) )
21 fnov ( ( 𝑦𝑌 , 𝑥𝑋𝐴 ) Fn ( 𝑌 × 𝑋 ) ↔ ( 𝑦𝑌 , 𝑥𝑋𝐴 ) = ( 𝑧𝑌 , 𝑤𝑋 ↦ ( 𝑧 ( 𝑦𝑌 , 𝑥𝑋𝐴 ) 𝑤 ) ) )
22 20 21 sylib ( 𝜑 → ( 𝑦𝑌 , 𝑥𝑋𝐴 ) = ( 𝑧𝑌 , 𝑤𝑋 ↦ ( 𝑧 ( 𝑦𝑌 , 𝑥𝑋𝐴 ) 𝑤 ) ) )
23 nfcv 𝑦 𝑧
24 nfcv 𝑥 𝑧
25 nfcv 𝑥 𝑤
26 nfv 𝑦 𝜑
27 nfcv 𝑦 𝑥
28 nfmpo2 𝑦 ( 𝑥𝑋 , 𝑦𝑌𝐴 )
29 27 28 23 nfov 𝑦 ( 𝑥 ( 𝑥𝑋 , 𝑦𝑌𝐴 ) 𝑧 )
30 nfmpo1 𝑦 ( 𝑦𝑌 , 𝑥𝑋𝐴 )
31 23 30 27 nfov 𝑦 ( 𝑧 ( 𝑦𝑌 , 𝑥𝑋𝐴 ) 𝑥 )
32 29 31 nfeq 𝑦 ( 𝑥 ( 𝑥𝑋 , 𝑦𝑌𝐴 ) 𝑧 ) = ( 𝑧 ( 𝑦𝑌 , 𝑥𝑋𝐴 ) 𝑥 )
33 26 32 nfim 𝑦 ( 𝜑 → ( 𝑥 ( 𝑥𝑋 , 𝑦𝑌𝐴 ) 𝑧 ) = ( 𝑧 ( 𝑦𝑌 , 𝑥𝑋𝐴 ) 𝑥 ) )
34 nfv 𝑥 𝜑
35 nfmpo1 𝑥 ( 𝑥𝑋 , 𝑦𝑌𝐴 )
36 25 35 24 nfov 𝑥 ( 𝑤 ( 𝑥𝑋 , 𝑦𝑌𝐴 ) 𝑧 )
37 nfmpo2 𝑥 ( 𝑦𝑌 , 𝑥𝑋𝐴 )
38 24 37 25 nfov 𝑥 ( 𝑧 ( 𝑦𝑌 , 𝑥𝑋𝐴 ) 𝑤 )
39 36 38 nfeq 𝑥 ( 𝑤 ( 𝑥𝑋 , 𝑦𝑌𝐴 ) 𝑧 ) = ( 𝑧 ( 𝑦𝑌 , 𝑥𝑋𝐴 ) 𝑤 )
40 34 39 nfim 𝑥 ( 𝜑 → ( 𝑤 ( 𝑥𝑋 , 𝑦𝑌𝐴 ) 𝑧 ) = ( 𝑧 ( 𝑦𝑌 , 𝑥𝑋𝐴 ) 𝑤 ) )
41 oveq2 ( 𝑦 = 𝑧 → ( 𝑥 ( 𝑥𝑋 , 𝑦𝑌𝐴 ) 𝑦 ) = ( 𝑥 ( 𝑥𝑋 , 𝑦𝑌𝐴 ) 𝑧 ) )
42 oveq1 ( 𝑦 = 𝑧 → ( 𝑦 ( 𝑦𝑌 , 𝑥𝑋𝐴 ) 𝑥 ) = ( 𝑧 ( 𝑦𝑌 , 𝑥𝑋𝐴 ) 𝑥 ) )
43 41 42 eqeq12d ( 𝑦 = 𝑧 → ( ( 𝑥 ( 𝑥𝑋 , 𝑦𝑌𝐴 ) 𝑦 ) = ( 𝑦 ( 𝑦𝑌 , 𝑥𝑋𝐴 ) 𝑥 ) ↔ ( 𝑥 ( 𝑥𝑋 , 𝑦𝑌𝐴 ) 𝑧 ) = ( 𝑧 ( 𝑦𝑌 , 𝑥𝑋𝐴 ) 𝑥 ) ) )
44 43 imbi2d ( 𝑦 = 𝑧 → ( ( 𝜑 → ( 𝑥 ( 𝑥𝑋 , 𝑦𝑌𝐴 ) 𝑦 ) = ( 𝑦 ( 𝑦𝑌 , 𝑥𝑋𝐴 ) 𝑥 ) ) ↔ ( 𝜑 → ( 𝑥 ( 𝑥𝑋 , 𝑦𝑌𝐴 ) 𝑧 ) = ( 𝑧 ( 𝑦𝑌 , 𝑥𝑋𝐴 ) 𝑥 ) ) ) )
45 oveq1 ( 𝑥 = 𝑤 → ( 𝑥 ( 𝑥𝑋 , 𝑦𝑌𝐴 ) 𝑧 ) = ( 𝑤 ( 𝑥𝑋 , 𝑦𝑌𝐴 ) 𝑧 ) )
46 oveq2 ( 𝑥 = 𝑤 → ( 𝑧 ( 𝑦𝑌 , 𝑥𝑋𝐴 ) 𝑥 ) = ( 𝑧 ( 𝑦𝑌 , 𝑥𝑋𝐴 ) 𝑤 ) )
47 45 46 eqeq12d ( 𝑥 = 𝑤 → ( ( 𝑥 ( 𝑥𝑋 , 𝑦𝑌𝐴 ) 𝑧 ) = ( 𝑧 ( 𝑦𝑌 , 𝑥𝑋𝐴 ) 𝑥 ) ↔ ( 𝑤 ( 𝑥𝑋 , 𝑦𝑌𝐴 ) 𝑧 ) = ( 𝑧 ( 𝑦𝑌 , 𝑥𝑋𝐴 ) 𝑤 ) ) )
48 47 imbi2d ( 𝑥 = 𝑤 → ( ( 𝜑 → ( 𝑥 ( 𝑥𝑋 , 𝑦𝑌𝐴 ) 𝑧 ) = ( 𝑧 ( 𝑦𝑌 , 𝑥𝑋𝐴 ) 𝑥 ) ) ↔ ( 𝜑 → ( 𝑤 ( 𝑥𝑋 , 𝑦𝑌𝐴 ) 𝑧 ) = ( 𝑧 ( 𝑦𝑌 , 𝑥𝑋𝐴 ) 𝑤 ) ) ) )
49 rsp2 ( ∀ 𝑦𝑌𝑥𝑋 𝐴 𝐿 → ( ( 𝑦𝑌𝑥𝑋 ) → 𝐴 𝐿 ) )
50 49 16 syl11 ( ( 𝑦𝑌𝑥𝑋 ) → ( 𝜑𝐴 𝐿 ) )
51 12 ovmpt4g ( ( 𝑥𝑋𝑦𝑌𝐴 𝐿 ) → ( 𝑥 ( 𝑥𝑋 , 𝑦𝑌𝐴 ) 𝑦 ) = 𝐴 )
52 51 3com12 ( ( 𝑦𝑌𝑥𝑋𝐴 𝐿 ) → ( 𝑥 ( 𝑥𝑋 , 𝑦𝑌𝐴 ) 𝑦 ) = 𝐴 )
53 17 ovmpt4g ( ( 𝑦𝑌𝑥𝑋𝐴 𝐿 ) → ( 𝑦 ( 𝑦𝑌 , 𝑥𝑋𝐴 ) 𝑥 ) = 𝐴 )
54 52 53 eqtr4d ( ( 𝑦𝑌𝑥𝑋𝐴 𝐿 ) → ( 𝑥 ( 𝑥𝑋 , 𝑦𝑌𝐴 ) 𝑦 ) = ( 𝑦 ( 𝑦𝑌 , 𝑥𝑋𝐴 ) 𝑥 ) )
55 54 3expia ( ( 𝑦𝑌𝑥𝑋 ) → ( 𝐴 𝐿 → ( 𝑥 ( 𝑥𝑋 , 𝑦𝑌𝐴 ) 𝑦 ) = ( 𝑦 ( 𝑦𝑌 , 𝑥𝑋𝐴 ) 𝑥 ) ) )
56 50 55 syld ( ( 𝑦𝑌𝑥𝑋 ) → ( 𝜑 → ( 𝑥 ( 𝑥𝑋 , 𝑦𝑌𝐴 ) 𝑦 ) = ( 𝑦 ( 𝑦𝑌 , 𝑥𝑋𝐴 ) 𝑥 ) ) )
57 23 24 25 33 40 44 48 56 vtocl2gaf ( ( 𝑧𝑌𝑤𝑋 ) → ( 𝜑 → ( 𝑤 ( 𝑥𝑋 , 𝑦𝑌𝐴 ) 𝑧 ) = ( 𝑧 ( 𝑦𝑌 , 𝑥𝑋𝐴 ) 𝑤 ) ) )
58 57 com12 ( 𝜑 → ( ( 𝑧𝑌𝑤𝑋 ) → ( 𝑤 ( 𝑥𝑋 , 𝑦𝑌𝐴 ) 𝑧 ) = ( 𝑧 ( 𝑦𝑌 , 𝑥𝑋𝐴 ) 𝑤 ) ) )
59 58 3impib ( ( 𝜑𝑧𝑌𝑤𝑋 ) → ( 𝑤 ( 𝑥𝑋 , 𝑦𝑌𝐴 ) 𝑧 ) = ( 𝑧 ( 𝑦𝑌 , 𝑥𝑋𝐴 ) 𝑤 ) )
60 59 mpoeq3dva ( 𝜑 → ( 𝑧𝑌 , 𝑤𝑋 ↦ ( 𝑤 ( 𝑥𝑋 , 𝑦𝑌𝐴 ) 𝑧 ) ) = ( 𝑧𝑌 , 𝑤𝑋 ↦ ( 𝑧 ( 𝑦𝑌 , 𝑥𝑋𝐴 ) 𝑤 ) ) )
61 22 60 eqtr4d ( 𝜑 → ( 𝑦𝑌 , 𝑥𝑋𝐴 ) = ( 𝑧𝑌 , 𝑤𝑋 ↦ ( 𝑤 ( 𝑥𝑋 , 𝑦𝑌𝐴 ) 𝑧 ) ) )
62 2 1 cnmpt2nd ( 𝜑 → ( 𝑧𝑌 , 𝑤𝑋𝑤 ) ∈ ( ( 𝐾 ×t 𝐽 ) Cn 𝐽 ) )
63 2 1 cnmpt1st ( 𝜑 → ( 𝑧𝑌 , 𝑤𝑋𝑧 ) ∈ ( ( 𝐾 ×t 𝐽 ) Cn 𝐾 ) )
64 2 1 62 63 3 cnmpt22f ( 𝜑 → ( 𝑧𝑌 , 𝑤𝑋 ↦ ( 𝑤 ( 𝑥𝑋 , 𝑦𝑌𝐴 ) 𝑧 ) ) ∈ ( ( 𝐾 ×t 𝐽 ) Cn 𝐿 ) )
65 61 64 eqeltrd ( 𝜑 → ( 𝑦𝑌 , 𝑥𝑋𝐴 ) ∈ ( ( 𝐾 ×t 𝐽 ) Cn 𝐿 ) )