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

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