MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  cnmpt11 Structured version   Visualization version   GIF version

Theorem cnmpt11 21376
Description: The composition of continuous functions is continuous. (Contributed by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro, 22-Aug-2015.)
Hypotheses
Ref Expression
cnmptid.j (𝜑𝐽 ∈ (TopOn‘𝑋))
cnmpt11.a (𝜑 → (𝑥𝑋𝐴) ∈ (𝐽 Cn 𝐾))
cnmpt11.k (𝜑𝐾 ∈ (TopOn‘𝑌))
cnmpt11.b (𝜑 → (𝑦𝑌𝐵) ∈ (𝐾 Cn 𝐿))
cnmpt11.c (𝑦 = 𝐴𝐵 = 𝐶)
Assertion
Ref Expression
cnmpt11 (𝜑 → (𝑥𝑋𝐶) ∈ (𝐽 Cn 𝐿))
Distinct variable groups:   𝑦,𝐴   𝑥,𝑦   𝜑,𝑥   𝑥,𝐽,𝑦   𝑥,𝑋,𝑦   𝑥,𝑌,𝑦   𝑥,𝐾,𝑦   𝑥,𝐿,𝑦   𝑥,𝐵   𝑦,𝐶
Allowed substitution hints:   𝜑(𝑦)   𝐴(𝑥)   𝐵(𝑦)   𝐶(𝑥)

Proof of Theorem cnmpt11
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 simpr 477 . . . . . . . . 9 ((𝜑𝑥𝑋) → 𝑥𝑋)
2 cnmptid.j . . . . . . . . . . . 12 (𝜑𝐽 ∈ (TopOn‘𝑋))
3 cnmpt11.k . . . . . . . . . . . 12 (𝜑𝐾 ∈ (TopOn‘𝑌))
4 cnmpt11.a . . . . . . . . . . . 12 (𝜑 → (𝑥𝑋𝐴) ∈ (𝐽 Cn 𝐾))
5 cnf2 20963 . . . . . . . . . . . 12 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ (𝑥𝑋𝐴) ∈ (𝐽 Cn 𝐾)) → (𝑥𝑋𝐴):𝑋𝑌)
62, 3, 4, 5syl3anc 1323 . . . . . . . . . . 11 (𝜑 → (𝑥𝑋𝐴):𝑋𝑌)
7 eqid 2621 . . . . . . . . . . . 12 (𝑥𝑋𝐴) = (𝑥𝑋𝐴)
87fmpt 6337 . . . . . . . . . . 11 (∀𝑥𝑋 𝐴𝑌 ↔ (𝑥𝑋𝐴):𝑋𝑌)
96, 8sylibr 224 . . . . . . . . . 10 (𝜑 → ∀𝑥𝑋 𝐴𝑌)
109r19.21bi 2927 . . . . . . . . 9 ((𝜑𝑥𝑋) → 𝐴𝑌)
117fvmpt2 6248 . . . . . . . . 9 ((𝑥𝑋𝐴𝑌) → ((𝑥𝑋𝐴)‘𝑥) = 𝐴)
121, 10, 11syl2anc 692 . . . . . . . 8 ((𝜑𝑥𝑋) → ((𝑥𝑋𝐴)‘𝑥) = 𝐴)
1312fveq2d 6152 . . . . . . 7 ((𝜑𝑥𝑋) → ((𝑦𝑌𝐵)‘((𝑥𝑋𝐴)‘𝑥)) = ((𝑦𝑌𝐵)‘𝐴))
14 cnmpt11.b . . . . . . . . . . . . . 14 (𝜑 → (𝑦𝑌𝐵) ∈ (𝐾 Cn 𝐿))
15 cntop2 20955 . . . . . . . . . . . . . 14 ((𝑦𝑌𝐵) ∈ (𝐾 Cn 𝐿) → 𝐿 ∈ Top)
1614, 15syl 17 . . . . . . . . . . . . 13 (𝜑𝐿 ∈ Top)
17 eqid 2621 . . . . . . . . . . . . . 14 𝐿 = 𝐿
1817toptopon 20648 . . . . . . . . . . . . 13 (𝐿 ∈ Top ↔ 𝐿 ∈ (TopOn‘ 𝐿))
1916, 18sylib 208 . . . . . . . . . . . 12 (𝜑𝐿 ∈ (TopOn‘ 𝐿))
20 cnf2 20963 . . . . . . . . . . . 12 ((𝐾 ∈ (TopOn‘𝑌) ∧ 𝐿 ∈ (TopOn‘ 𝐿) ∧ (𝑦𝑌𝐵) ∈ (𝐾 Cn 𝐿)) → (𝑦𝑌𝐵):𝑌 𝐿)
213, 19, 14, 20syl3anc 1323 . . . . . . . . . . 11 (𝜑 → (𝑦𝑌𝐵):𝑌 𝐿)
22 eqid 2621 . . . . . . . . . . . 12 (𝑦𝑌𝐵) = (𝑦𝑌𝐵)
2322fmpt 6337 . . . . . . . . . . 11 (∀𝑦𝑌 𝐵 𝐿 ↔ (𝑦𝑌𝐵):𝑌 𝐿)
2421, 23sylibr 224 . . . . . . . . . 10 (𝜑 → ∀𝑦𝑌 𝐵 𝐿)
2524adantr 481 . . . . . . . . 9 ((𝜑𝑥𝑋) → ∀𝑦𝑌 𝐵 𝐿)
26 cnmpt11.c . . . . . . . . . . 11 (𝑦 = 𝐴𝐵 = 𝐶)
2726eleq1d 2683 . . . . . . . . . 10 (𝑦 = 𝐴 → (𝐵 𝐿𝐶 𝐿))
2827rspcv 3291 . . . . . . . . 9 (𝐴𝑌 → (∀𝑦𝑌 𝐵 𝐿𝐶 𝐿))
2910, 25, 28sylc 65 . . . . . . . 8 ((𝜑𝑥𝑋) → 𝐶 𝐿)
3026, 22fvmptg 6237 . . . . . . . 8 ((𝐴𝑌𝐶 𝐿) → ((𝑦𝑌𝐵)‘𝐴) = 𝐶)
3110, 29, 30syl2anc 692 . . . . . . 7 ((𝜑𝑥𝑋) → ((𝑦𝑌𝐵)‘𝐴) = 𝐶)
3213, 31eqtrd 2655 . . . . . 6 ((𝜑𝑥𝑋) → ((𝑦𝑌𝐵)‘((𝑥𝑋𝐴)‘𝑥)) = 𝐶)
33 fvco3 6232 . . . . . . 7 (((𝑥𝑋𝐴):𝑋𝑌𝑥𝑋) → (((𝑦𝑌𝐵) ∘ (𝑥𝑋𝐴))‘𝑥) = ((𝑦𝑌𝐵)‘((𝑥𝑋𝐴)‘𝑥)))
346, 33sylan 488 . . . . . 6 ((𝜑𝑥𝑋) → (((𝑦𝑌𝐵) ∘ (𝑥𝑋𝐴))‘𝑥) = ((𝑦𝑌𝐵)‘((𝑥𝑋𝐴)‘𝑥)))
35 eqid 2621 . . . . . . . 8 (𝑥𝑋𝐶) = (𝑥𝑋𝐶)
3635fvmpt2 6248 . . . . . . 7 ((𝑥𝑋𝐶 𝐿) → ((𝑥𝑋𝐶)‘𝑥) = 𝐶)
371, 29, 36syl2anc 692 . . . . . 6 ((𝜑𝑥𝑋) → ((𝑥𝑋𝐶)‘𝑥) = 𝐶)
3832, 34, 373eqtr4d 2665 . . . . 5 ((𝜑𝑥𝑋) → (((𝑦𝑌𝐵) ∘ (𝑥𝑋𝐴))‘𝑥) = ((𝑥𝑋𝐶)‘𝑥))
3938ralrimiva 2960 . . . 4 (𝜑 → ∀𝑥𝑋 (((𝑦𝑌𝐵) ∘ (𝑥𝑋𝐴))‘𝑥) = ((𝑥𝑋𝐶)‘𝑥))
40 nfv 1840 . . . . 5 𝑧(((𝑦𝑌𝐵) ∘ (𝑥𝑋𝐴))‘𝑥) = ((𝑥𝑋𝐶)‘𝑥)
41 nfcv 2761 . . . . . . . 8 𝑥(𝑦𝑌𝐵)
42 nfmpt1 4707 . . . . . . . 8 𝑥(𝑥𝑋𝐴)
4341, 42nfco 5247 . . . . . . 7 𝑥((𝑦𝑌𝐵) ∘ (𝑥𝑋𝐴))
44 nfcv 2761 . . . . . . 7 𝑥𝑧
4543, 44nffv 6155 . . . . . 6 𝑥(((𝑦𝑌𝐵) ∘ (𝑥𝑋𝐴))‘𝑧)
46 nfmpt1 4707 . . . . . . 7 𝑥(𝑥𝑋𝐶)
4746, 44nffv 6155 . . . . . 6 𝑥((𝑥𝑋𝐶)‘𝑧)
4845, 47nfeq 2772 . . . . 5 𝑥(((𝑦𝑌𝐵) ∘ (𝑥𝑋𝐴))‘𝑧) = ((𝑥𝑋𝐶)‘𝑧)
49 fveq2 6148 . . . . . 6 (𝑥 = 𝑧 → (((𝑦𝑌𝐵) ∘ (𝑥𝑋𝐴))‘𝑥) = (((𝑦𝑌𝐵) ∘ (𝑥𝑋𝐴))‘𝑧))
50 fveq2 6148 . . . . . 6 (𝑥 = 𝑧 → ((𝑥𝑋𝐶)‘𝑥) = ((𝑥𝑋𝐶)‘𝑧))
5149, 50eqeq12d 2636 . . . . 5 (𝑥 = 𝑧 → ((((𝑦𝑌𝐵) ∘ (𝑥𝑋𝐴))‘𝑥) = ((𝑥𝑋𝐶)‘𝑥) ↔ (((𝑦𝑌𝐵) ∘ (𝑥𝑋𝐴))‘𝑧) = ((𝑥𝑋𝐶)‘𝑧)))
5240, 48, 51cbvral 3155 . . . 4 (∀𝑥𝑋 (((𝑦𝑌𝐵) ∘ (𝑥𝑋𝐴))‘𝑥) = ((𝑥𝑋𝐶)‘𝑥) ↔ ∀𝑧𝑋 (((𝑦𝑌𝐵) ∘ (𝑥𝑋𝐴))‘𝑧) = ((𝑥𝑋𝐶)‘𝑧))
5339, 52sylib 208 . . 3 (𝜑 → ∀𝑧𝑋 (((𝑦𝑌𝐵) ∘ (𝑥𝑋𝐴))‘𝑧) = ((𝑥𝑋𝐶)‘𝑧))
54 fco 6015 . . . . . 6 (((𝑦𝑌𝐵):𝑌 𝐿 ∧ (𝑥𝑋𝐴):𝑋𝑌) → ((𝑦𝑌𝐵) ∘ (𝑥𝑋𝐴)):𝑋 𝐿)
5521, 6, 54syl2anc 692 . . . . 5 (𝜑 → ((𝑦𝑌𝐵) ∘ (𝑥𝑋𝐴)):𝑋 𝐿)
56 ffn 6002 . . . . 5 (((𝑦𝑌𝐵) ∘ (𝑥𝑋𝐴)):𝑋 𝐿 → ((𝑦𝑌𝐵) ∘ (𝑥𝑋𝐴)) Fn 𝑋)
5755, 56syl 17 . . . 4 (𝜑 → ((𝑦𝑌𝐵) ∘ (𝑥𝑋𝐴)) Fn 𝑋)
5829, 35fmptd 6340 . . . . 5 (𝜑 → (𝑥𝑋𝐶):𝑋 𝐿)
59 ffn 6002 . . . . 5 ((𝑥𝑋𝐶):𝑋 𝐿 → (𝑥𝑋𝐶) Fn 𝑋)
6058, 59syl 17 . . . 4 (𝜑 → (𝑥𝑋𝐶) Fn 𝑋)
61 eqfnfv 6267 . . . 4 ((((𝑦𝑌𝐵) ∘ (𝑥𝑋𝐴)) Fn 𝑋 ∧ (𝑥𝑋𝐶) Fn 𝑋) → (((𝑦𝑌𝐵) ∘ (𝑥𝑋𝐴)) = (𝑥𝑋𝐶) ↔ ∀𝑧𝑋 (((𝑦𝑌𝐵) ∘ (𝑥𝑋𝐴))‘𝑧) = ((𝑥𝑋𝐶)‘𝑧)))
6257, 60, 61syl2anc 692 . . 3 (𝜑 → (((𝑦𝑌𝐵) ∘ (𝑥𝑋𝐴)) = (𝑥𝑋𝐶) ↔ ∀𝑧𝑋 (((𝑦𝑌𝐵) ∘ (𝑥𝑋𝐴))‘𝑧) = ((𝑥𝑋𝐶)‘𝑧)))
6353, 62mpbird 247 . 2 (𝜑 → ((𝑦𝑌𝐵) ∘ (𝑥𝑋𝐴)) = (𝑥𝑋𝐶))
64 cnco 20980 . . 3 (((𝑥𝑋𝐴) ∈ (𝐽 Cn 𝐾) ∧ (𝑦𝑌𝐵) ∈ (𝐾 Cn 𝐿)) → ((𝑦𝑌𝐵) ∘ (𝑥𝑋𝐴)) ∈ (𝐽 Cn 𝐿))
654, 14, 64syl2anc 692 . 2 (𝜑 → ((𝑦𝑌𝐵) ∘ (𝑥𝑋𝐴)) ∈ (𝐽 Cn 𝐿))
6663, 65eqeltrrd 2699 1 (𝜑 → (𝑥𝑋𝐶) ∈ (𝐽 Cn 𝐿))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384   = wceq 1480  wcel 1987  wral 2907   cuni 4402  cmpt 4673  ccom 5078   Fn wfn 5842  wf 5843  cfv 5847  (class class class)co 6604  Topctop 20617  TopOnctopon 20618   Cn ccn 20938
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4741  ax-nul 4749  ax-pow 4803  ax-pr 4867  ax-un 6902
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2912  df-rex 2913  df-rab 2916  df-v 3188  df-sbc 3418  df-csb 3515  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-nul 3892  df-if 4059  df-pw 4132  df-sn 4149  df-pr 4151  df-op 4155  df-uni 4403  df-br 4614  df-opab 4674  df-mpt 4675  df-id 4989  df-xp 5080  df-rel 5081  df-cnv 5082  df-co 5083  df-dm 5084  df-rn 5085  df-res 5086  df-ima 5087  df-iota 5810  df-fun 5849  df-fn 5850  df-f 5851  df-fv 5855  df-ov 6607  df-oprab 6608  df-mpt2 6609  df-map 7804  df-top 20621  df-topon 20623  df-cn 20941
This theorem is referenced by:  cnmpt11f  21377  cnmptkp  21393  cnmptk1  21394  cnmpt1k  21395  ptunhmeo  21521  tmdgsum  21809  icchmeo  22648  evth2  22667  sinccvglem  31271  poimir  33071  broucube  33072
  Copyright terms: Public domain W3C validator