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

Theorem cnmpt11 23686
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 484 . . . . . . . . 9 ((𝜑𝑥𝑋) → 𝑥𝑋)
2 cnmptid.j . . . . . . . . . . 11 (𝜑𝐽 ∈ (TopOn‘𝑋))
3 cnmpt11.k . . . . . . . . . . 11 (𝜑𝐾 ∈ (TopOn‘𝑌))
4 cnmpt11.a . . . . . . . . . . 11 (𝜑 → (𝑥𝑋𝐴) ∈ (𝐽 Cn 𝐾))
5 cnf2 23272 . . . . . . . . . . 11 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ (𝑥𝑋𝐴) ∈ (𝐽 Cn 𝐾)) → (𝑥𝑋𝐴):𝑋𝑌)
62, 3, 4, 5syl3anc 1370 . . . . . . . . . 10 (𝜑 → (𝑥𝑋𝐴):𝑋𝑌)
76fvmptelcdm 7132 . . . . . . . . 9 ((𝜑𝑥𝑋) → 𝐴𝑌)
8 eqid 2734 . . . . . . . . . 10 (𝑥𝑋𝐴) = (𝑥𝑋𝐴)
98fvmpt2 7026 . . . . . . . . 9 ((𝑥𝑋𝐴𝑌) → ((𝑥𝑋𝐴)‘𝑥) = 𝐴)
101, 7, 9syl2anc 584 . . . . . . . 8 ((𝜑𝑥𝑋) → ((𝑥𝑋𝐴)‘𝑥) = 𝐴)
1110fveq2d 6910 . . . . . . 7 ((𝜑𝑥𝑋) → ((𝑦𝑌𝐵)‘((𝑥𝑋𝐴)‘𝑥)) = ((𝑦𝑌𝐵)‘𝐴))
12 eqid 2734 . . . . . . . 8 (𝑦𝑌𝐵) = (𝑦𝑌𝐵)
13 cnmpt11.c . . . . . . . 8 (𝑦 = 𝐴𝐵 = 𝐶)
1413eleq1d 2823 . . . . . . . . 9 (𝑦 = 𝐴 → (𝐵 𝐿𝐶 𝐿))
15 cnmpt11.b . . . . . . . . . . . . . 14 (𝜑 → (𝑦𝑌𝐵) ∈ (𝐾 Cn 𝐿))
16 cntop2 23264 . . . . . . . . . . . . . 14 ((𝑦𝑌𝐵) ∈ (𝐾 Cn 𝐿) → 𝐿 ∈ Top)
1715, 16syl 17 . . . . . . . . . . . . 13 (𝜑𝐿 ∈ Top)
18 toptopon2 22939 . . . . . . . . . . . . 13 (𝐿 ∈ Top ↔ 𝐿 ∈ (TopOn‘ 𝐿))
1917, 18sylib 218 . . . . . . . . . . . 12 (𝜑𝐿 ∈ (TopOn‘ 𝐿))
20 cnf2 23272 . . . . . . . . . . . 12 ((𝐾 ∈ (TopOn‘𝑌) ∧ 𝐿 ∈ (TopOn‘ 𝐿) ∧ (𝑦𝑌𝐵) ∈ (𝐾 Cn 𝐿)) → (𝑦𝑌𝐵):𝑌 𝐿)
213, 19, 15, 20syl3anc 1370 . . . . . . . . . . 11 (𝜑 → (𝑦𝑌𝐵):𝑌 𝐿)
2212fmpt 7129 . . . . . . . . . . 11 (∀𝑦𝑌 𝐵 𝐿 ↔ (𝑦𝑌𝐵):𝑌 𝐿)
2321, 22sylibr 234 . . . . . . . . . 10 (𝜑 → ∀𝑦𝑌 𝐵 𝐿)
2423adantr 480 . . . . . . . . 9 ((𝜑𝑥𝑋) → ∀𝑦𝑌 𝐵 𝐿)
2514, 24, 7rspcdva 3622 . . . . . . . 8 ((𝜑𝑥𝑋) → 𝐶 𝐿)
2612, 13, 7, 25fvmptd3 7038 . . . . . . 7 ((𝜑𝑥𝑋) → ((𝑦𝑌𝐵)‘𝐴) = 𝐶)
2711, 26eqtrd 2774 . . . . . 6 ((𝜑𝑥𝑋) → ((𝑦𝑌𝐵)‘((𝑥𝑋𝐴)‘𝑥)) = 𝐶)
28 fvco3 7007 . . . . . . 7 (((𝑥𝑋𝐴):𝑋𝑌𝑥𝑋) → (((𝑦𝑌𝐵) ∘ (𝑥𝑋𝐴))‘𝑥) = ((𝑦𝑌𝐵)‘((𝑥𝑋𝐴)‘𝑥)))
296, 28sylan 580 . . . . . 6 ((𝜑𝑥𝑋) → (((𝑦𝑌𝐵) ∘ (𝑥𝑋𝐴))‘𝑥) = ((𝑦𝑌𝐵)‘((𝑥𝑋𝐴)‘𝑥)))
30 eqid 2734 . . . . . . . 8 (𝑥𝑋𝐶) = (𝑥𝑋𝐶)
3130fvmpt2 7026 . . . . . . 7 ((𝑥𝑋𝐶 𝐿) → ((𝑥𝑋𝐶)‘𝑥) = 𝐶)
321, 25, 31syl2anc 584 . . . . . 6 ((𝜑𝑥𝑋) → ((𝑥𝑋𝐶)‘𝑥) = 𝐶)
3327, 29, 323eqtr4d 2784 . . . . 5 ((𝜑𝑥𝑋) → (((𝑦𝑌𝐵) ∘ (𝑥𝑋𝐴))‘𝑥) = ((𝑥𝑋𝐶)‘𝑥))
3433ralrimiva 3143 . . . 4 (𝜑 → ∀𝑥𝑋 (((𝑦𝑌𝐵) ∘ (𝑥𝑋𝐴))‘𝑥) = ((𝑥𝑋𝐶)‘𝑥))
35 nfv 1911 . . . . 5 𝑧(((𝑦𝑌𝐵) ∘ (𝑥𝑋𝐴))‘𝑥) = ((𝑥𝑋𝐶)‘𝑥)
36 nfcv 2902 . . . . . . . 8 𝑥(𝑦𝑌𝐵)
37 nfmpt1 5255 . . . . . . . 8 𝑥(𝑥𝑋𝐴)
3836, 37nfco 5878 . . . . . . 7 𝑥((𝑦𝑌𝐵) ∘ (𝑥𝑋𝐴))
39 nfcv 2902 . . . . . . 7 𝑥𝑧
4038, 39nffv 6916 . . . . . 6 𝑥(((𝑦𝑌𝐵) ∘ (𝑥𝑋𝐴))‘𝑧)
41 nfmpt1 5255 . . . . . . 7 𝑥(𝑥𝑋𝐶)
4241, 39nffv 6916 . . . . . 6 𝑥((𝑥𝑋𝐶)‘𝑧)
4340, 42nfeq 2916 . . . . 5 𝑥(((𝑦𝑌𝐵) ∘ (𝑥𝑋𝐴))‘𝑧) = ((𝑥𝑋𝐶)‘𝑧)
44 fveq2 6906 . . . . . 6 (𝑥 = 𝑧 → (((𝑦𝑌𝐵) ∘ (𝑥𝑋𝐴))‘𝑥) = (((𝑦𝑌𝐵) ∘ (𝑥𝑋𝐴))‘𝑧))
45 fveq2 6906 . . . . . 6 (𝑥 = 𝑧 → ((𝑥𝑋𝐶)‘𝑥) = ((𝑥𝑋𝐶)‘𝑧))
4644, 45eqeq12d 2750 . . . . 5 (𝑥 = 𝑧 → ((((𝑦𝑌𝐵) ∘ (𝑥𝑋𝐴))‘𝑥) = ((𝑥𝑋𝐶)‘𝑥) ↔ (((𝑦𝑌𝐵) ∘ (𝑥𝑋𝐴))‘𝑧) = ((𝑥𝑋𝐶)‘𝑧)))
4735, 43, 46cbvralw 3303 . . . 4 (∀𝑥𝑋 (((𝑦𝑌𝐵) ∘ (𝑥𝑋𝐴))‘𝑥) = ((𝑥𝑋𝐶)‘𝑥) ↔ ∀𝑧𝑋 (((𝑦𝑌𝐵) ∘ (𝑥𝑋𝐴))‘𝑧) = ((𝑥𝑋𝐶)‘𝑧))
4834, 47sylib 218 . . 3 (𝜑 → ∀𝑧𝑋 (((𝑦𝑌𝐵) ∘ (𝑥𝑋𝐴))‘𝑧) = ((𝑥𝑋𝐶)‘𝑧))
49 fco 6760 . . . . . 6 (((𝑦𝑌𝐵):𝑌 𝐿 ∧ (𝑥𝑋𝐴):𝑋𝑌) → ((𝑦𝑌𝐵) ∘ (𝑥𝑋𝐴)):𝑋 𝐿)
5021, 6, 49syl2anc 584 . . . . 5 (𝜑 → ((𝑦𝑌𝐵) ∘ (𝑥𝑋𝐴)):𝑋 𝐿)
5150ffnd 6737 . . . 4 (𝜑 → ((𝑦𝑌𝐵) ∘ (𝑥𝑋𝐴)) Fn 𝑋)
5225fmpttd 7134 . . . . 5 (𝜑 → (𝑥𝑋𝐶):𝑋 𝐿)
5352ffnd 6737 . . . 4 (𝜑 → (𝑥𝑋𝐶) Fn 𝑋)
54 eqfnfv 7050 . . . 4 ((((𝑦𝑌𝐵) ∘ (𝑥𝑋𝐴)) Fn 𝑋 ∧ (𝑥𝑋𝐶) Fn 𝑋) → (((𝑦𝑌𝐵) ∘ (𝑥𝑋𝐴)) = (𝑥𝑋𝐶) ↔ ∀𝑧𝑋 (((𝑦𝑌𝐵) ∘ (𝑥𝑋𝐴))‘𝑧) = ((𝑥𝑋𝐶)‘𝑧)))
5551, 53, 54syl2anc 584 . . 3 (𝜑 → (((𝑦𝑌𝐵) ∘ (𝑥𝑋𝐴)) = (𝑥𝑋𝐶) ↔ ∀𝑧𝑋 (((𝑦𝑌𝐵) ∘ (𝑥𝑋𝐴))‘𝑧) = ((𝑥𝑋𝐶)‘𝑧)))
5648, 55mpbird 257 . 2 (𝜑 → ((𝑦𝑌𝐵) ∘ (𝑥𝑋𝐴)) = (𝑥𝑋𝐶))
57 cnco 23289 . . 3 (((𝑥𝑋𝐴) ∈ (𝐽 Cn 𝐾) ∧ (𝑦𝑌𝐵) ∈ (𝐾 Cn 𝐿)) → ((𝑦𝑌𝐵) ∘ (𝑥𝑋𝐴)) ∈ (𝐽 Cn 𝐿))
584, 15, 57syl2anc 584 . 2 (𝜑 → ((𝑦𝑌𝐵) ∘ (𝑥𝑋𝐴)) ∈ (𝐽 Cn 𝐿))
5956, 58eqeltrrd 2839 1 (𝜑 → (𝑥𝑋𝐶) ∈ (𝐽 Cn 𝐿))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395   = wceq 1536  wcel 2105  wral 3058   cuni 4911  cmpt 5230  ccom 5692   Fn wfn 6557  wf 6558  cfv 6562  (class class class)co 7430  Topctop 22914  TopOnctopon 22931   Cn ccn 23247
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5582  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-fv 6570  df-ov 7433  df-oprab 7434  df-mpo 7435  df-map 8866  df-top 22915  df-topon 22932  df-cn 23250
This theorem is referenced by:  cnmpt11f  23687  cnmptkp  23703  cnmptk1  23704  cnmpt1k  23705  ptunhmeo  23831  tmdgsum  24118  icchmeo  24984  icchmeoOLD  24985  evth2  25005  sinccvglem  35656  poimir  37639  broucube  37640
  Copyright terms: Public domain W3C validator