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

Theorem cnmpt21 21284
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
cnmpt21.j (𝜑𝐽 ∈ (TopOn‘𝑋))
cnmpt21.k (𝜑𝐾 ∈ (TopOn‘𝑌))
cnmpt21.a (𝜑 → (𝑥𝑋, 𝑦𝑌𝐴) ∈ ((𝐽 ×t 𝐾) Cn 𝐿))
cnmpt21.l (𝜑𝐿 ∈ (TopOn‘𝑍))
cnmpt21.b (𝜑 → (𝑧𝑍𝐵) ∈ (𝐿 Cn 𝑀))
cnmpt21.c (𝑧 = 𝐴𝐵 = 𝐶)
Assertion
Ref Expression
cnmpt21 (𝜑 → (𝑥𝑋, 𝑦𝑌𝐶) ∈ ((𝐽 ×t 𝐾) Cn 𝑀))
Distinct variable groups:   𝑧,𝐴   𝑧,𝐽   𝑥,𝑦,𝑧,𝐿   𝜑,𝑥,𝑦,𝑧   𝑥,𝑋,𝑦,𝑧   𝑥,𝑀,𝑦,𝑧   𝑥,𝑌,𝑦,𝑧   𝑧,𝐾   𝑥,𝑍,𝑦,𝑧   𝑥,𝐵,𝑦   𝑧,𝐶
Allowed substitution hints:   𝐴(𝑥,𝑦)   𝐵(𝑧)   𝐶(𝑥,𝑦)   𝐽(𝑥,𝑦)   𝐾(𝑥,𝑦)

Proof of Theorem cnmpt21
Dummy variables 𝑢 𝑣 𝑤 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-ov 6552 . . . . . . . . . 10 (𝑥(𝑥𝑋, 𝑦𝑌𝐴)𝑦) = ((𝑥𝑋, 𝑦𝑌𝐴)‘⟨𝑥, 𝑦⟩)
2 simprl 790 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝑋𝑦𝑌)) → 𝑥𝑋)
3 simprr 792 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝑋𝑦𝑌)) → 𝑦𝑌)
4 cnmpt21.j . . . . . . . . . . . . . . . 16 (𝜑𝐽 ∈ (TopOn‘𝑋))
5 cnmpt21.k . . . . . . . . . . . . . . . 16 (𝜑𝐾 ∈ (TopOn‘𝑌))
6 txtopon 21204 . . . . . . . . . . . . . . . 16 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝐽 ×t 𝐾) ∈ (TopOn‘(𝑋 × 𝑌)))
74, 5, 6syl2anc 691 . . . . . . . . . . . . . . 15 (𝜑 → (𝐽 ×t 𝐾) ∈ (TopOn‘(𝑋 × 𝑌)))
8 cnmpt21.l . . . . . . . . . . . . . . 15 (𝜑𝐿 ∈ (TopOn‘𝑍))
9 cnmpt21.a . . . . . . . . . . . . . . 15 (𝜑 → (𝑥𝑋, 𝑦𝑌𝐴) ∈ ((𝐽 ×t 𝐾) Cn 𝐿))
10 cnf2 20863 . . . . . . . . . . . . . . 15 (((𝐽 ×t 𝐾) ∈ (TopOn‘(𝑋 × 𝑌)) ∧ 𝐿 ∈ (TopOn‘𝑍) ∧ (𝑥𝑋, 𝑦𝑌𝐴) ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) → (𝑥𝑋, 𝑦𝑌𝐴):(𝑋 × 𝑌)⟶𝑍)
117, 8, 9, 10syl3anc 1318 . . . . . . . . . . . . . 14 (𝜑 → (𝑥𝑋, 𝑦𝑌𝐴):(𝑋 × 𝑌)⟶𝑍)
12 eqid 2610 . . . . . . . . . . . . . . 15 (𝑥𝑋, 𝑦𝑌𝐴) = (𝑥𝑋, 𝑦𝑌𝐴)
1312fmpt2 7126 . . . . . . . . . . . . . 14 (∀𝑥𝑋𝑦𝑌 𝐴𝑍 ↔ (𝑥𝑋, 𝑦𝑌𝐴):(𝑋 × 𝑌)⟶𝑍)
1411, 13sylibr 223 . . . . . . . . . . . . 13 (𝜑 → ∀𝑥𝑋𝑦𝑌 𝐴𝑍)
15 rsp2 2920 . . . . . . . . . . . . 13 (∀𝑥𝑋𝑦𝑌 𝐴𝑍 → ((𝑥𝑋𝑦𝑌) → 𝐴𝑍))
1614, 15syl 17 . . . . . . . . . . . 12 (𝜑 → ((𝑥𝑋𝑦𝑌) → 𝐴𝑍))
1716imp 444 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝑋𝑦𝑌)) → 𝐴𝑍)
1812ovmpt4g 6681 . . . . . . . . . . 11 ((𝑥𝑋𝑦𝑌𝐴𝑍) → (𝑥(𝑥𝑋, 𝑦𝑌𝐴)𝑦) = 𝐴)
192, 3, 17, 18syl3anc 1318 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝑋𝑦𝑌)) → (𝑥(𝑥𝑋, 𝑦𝑌𝐴)𝑦) = 𝐴)
201, 19syl5eqr 2658 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝑋𝑦𝑌)) → ((𝑥𝑋, 𝑦𝑌𝐴)‘⟨𝑥, 𝑦⟩) = 𝐴)
2120fveq2d 6107 . . . . . . . 8 ((𝜑 ∧ (𝑥𝑋𝑦𝑌)) → ((𝑧𝑍𝐵)‘((𝑥𝑋, 𝑦𝑌𝐴)‘⟨𝑥, 𝑦⟩)) = ((𝑧𝑍𝐵)‘𝐴))
22 cnmpt21.b . . . . . . . . . . . . . . 15 (𝜑 → (𝑧𝑍𝐵) ∈ (𝐿 Cn 𝑀))
23 cntop2 20855 . . . . . . . . . . . . . . 15 ((𝑧𝑍𝐵) ∈ (𝐿 Cn 𝑀) → 𝑀 ∈ Top)
2422, 23syl 17 . . . . . . . . . . . . . 14 (𝜑𝑀 ∈ Top)
25 eqid 2610 . . . . . . . . . . . . . . 15 𝑀 = 𝑀
2625toptopon 20548 . . . . . . . . . . . . . 14 (𝑀 ∈ Top ↔ 𝑀 ∈ (TopOn‘ 𝑀))
2724, 26sylib 207 . . . . . . . . . . . . 13 (𝜑𝑀 ∈ (TopOn‘ 𝑀))
28 cnf2 20863 . . . . . . . . . . . . 13 ((𝐿 ∈ (TopOn‘𝑍) ∧ 𝑀 ∈ (TopOn‘ 𝑀) ∧ (𝑧𝑍𝐵) ∈ (𝐿 Cn 𝑀)) → (𝑧𝑍𝐵):𝑍 𝑀)
298, 27, 22, 28syl3anc 1318 . . . . . . . . . . . 12 (𝜑 → (𝑧𝑍𝐵):𝑍 𝑀)
30 eqid 2610 . . . . . . . . . . . . 13 (𝑧𝑍𝐵) = (𝑧𝑍𝐵)
3130fmpt 6289 . . . . . . . . . . . 12 (∀𝑧𝑍 𝐵 𝑀 ↔ (𝑧𝑍𝐵):𝑍 𝑀)
3229, 31sylibr 223 . . . . . . . . . . 11 (𝜑 → ∀𝑧𝑍 𝐵 𝑀)
3332adantr 480 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝑋𝑦𝑌)) → ∀𝑧𝑍 𝐵 𝑀)
34 cnmpt21.c . . . . . . . . . . . 12 (𝑧 = 𝐴𝐵 = 𝐶)
3534eleq1d 2672 . . . . . . . . . . 11 (𝑧 = 𝐴 → (𝐵 𝑀𝐶 𝑀))
3635rspcv 3278 . . . . . . . . . 10 (𝐴𝑍 → (∀𝑧𝑍 𝐵 𝑀𝐶 𝑀))
3717, 33, 36sylc 63 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝑋𝑦𝑌)) → 𝐶 𝑀)
3834, 30fvmptg 6189 . . . . . . . . 9 ((𝐴𝑍𝐶 𝑀) → ((𝑧𝑍𝐵)‘𝐴) = 𝐶)
3917, 37, 38syl2anc 691 . . . . . . . 8 ((𝜑 ∧ (𝑥𝑋𝑦𝑌)) → ((𝑧𝑍𝐵)‘𝐴) = 𝐶)
4021, 39eqtrd 2644 . . . . . . 7 ((𝜑 ∧ (𝑥𝑋𝑦𝑌)) → ((𝑧𝑍𝐵)‘((𝑥𝑋, 𝑦𝑌𝐴)‘⟨𝑥, 𝑦⟩)) = 𝐶)
41 opelxpi 5072 . . . . . . . 8 ((𝑥𝑋𝑦𝑌) → ⟨𝑥, 𝑦⟩ ∈ (𝑋 × 𝑌))
42 fvco3 6185 . . . . . . . 8 (((𝑥𝑋, 𝑦𝑌𝐴):(𝑋 × 𝑌)⟶𝑍 ∧ ⟨𝑥, 𝑦⟩ ∈ (𝑋 × 𝑌)) → (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑥, 𝑦⟩) = ((𝑧𝑍𝐵)‘((𝑥𝑋, 𝑦𝑌𝐴)‘⟨𝑥, 𝑦⟩)))
4311, 41, 42syl2an 493 . . . . . . 7 ((𝜑 ∧ (𝑥𝑋𝑦𝑌)) → (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑥, 𝑦⟩) = ((𝑧𝑍𝐵)‘((𝑥𝑋, 𝑦𝑌𝐴)‘⟨𝑥, 𝑦⟩)))
44 df-ov 6552 . . . . . . . 8 (𝑥(𝑥𝑋, 𝑦𝑌𝐶)𝑦) = ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑥, 𝑦⟩)
45 eqid 2610 . . . . . . . . . 10 (𝑥𝑋, 𝑦𝑌𝐶) = (𝑥𝑋, 𝑦𝑌𝐶)
4645ovmpt4g 6681 . . . . . . . . 9 ((𝑥𝑋𝑦𝑌𝐶 𝑀) → (𝑥(𝑥𝑋, 𝑦𝑌𝐶)𝑦) = 𝐶)
472, 3, 37, 46syl3anc 1318 . . . . . . . 8 ((𝜑 ∧ (𝑥𝑋𝑦𝑌)) → (𝑥(𝑥𝑋, 𝑦𝑌𝐶)𝑦) = 𝐶)
4844, 47syl5eqr 2658 . . . . . . 7 ((𝜑 ∧ (𝑥𝑋𝑦𝑌)) → ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑥, 𝑦⟩) = 𝐶)
4940, 43, 483eqtr4d 2654 . . . . . 6 ((𝜑 ∧ (𝑥𝑋𝑦𝑌)) → (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑥, 𝑦⟩) = ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑥, 𝑦⟩))
5049ralrimivva 2954 . . . . 5 (𝜑 → ∀𝑥𝑋𝑦𝑌 (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑥, 𝑦⟩) = ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑥, 𝑦⟩))
51 nfv 1830 . . . . . 6 𝑢𝑦𝑌 (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑥, 𝑦⟩) = ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑥, 𝑦⟩)
52 nfcv 2751 . . . . . . 7 𝑥𝑌
53 nfcv 2751 . . . . . . . . . 10 𝑥(𝑧𝑍𝐵)
54 nfmpt21 6620 . . . . . . . . . 10 𝑥(𝑥𝑋, 𝑦𝑌𝐴)
5553, 54nfco 5209 . . . . . . . . 9 𝑥((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))
56 nfcv 2751 . . . . . . . . 9 𝑥𝑢, 𝑣
5755, 56nffv 6110 . . . . . . . 8 𝑥(((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑢, 𝑣⟩)
58 nfmpt21 6620 . . . . . . . . 9 𝑥(𝑥𝑋, 𝑦𝑌𝐶)
5958, 56nffv 6110 . . . . . . . 8 𝑥((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑢, 𝑣⟩)
6057, 59nfeq 2762 . . . . . . 7 𝑥(((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑢, 𝑣⟩) = ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑢, 𝑣⟩)
6152, 60nfral 2929 . . . . . 6 𝑥𝑣𝑌 (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑢, 𝑣⟩) = ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑢, 𝑣⟩)
62 nfv 1830 . . . . . . . 8 𝑣(((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑥, 𝑦⟩) = ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑥, 𝑦⟩)
63 nfcv 2751 . . . . . . . . . . 11 𝑦(𝑧𝑍𝐵)
64 nfmpt22 6621 . . . . . . . . . . 11 𝑦(𝑥𝑋, 𝑦𝑌𝐴)
6563, 64nfco 5209 . . . . . . . . . 10 𝑦((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))
66 nfcv 2751 . . . . . . . . . 10 𝑦𝑥, 𝑣
6765, 66nffv 6110 . . . . . . . . 9 𝑦(((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑥, 𝑣⟩)
68 nfmpt22 6621 . . . . . . . . . 10 𝑦(𝑥𝑋, 𝑦𝑌𝐶)
6968, 66nffv 6110 . . . . . . . . 9 𝑦((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑥, 𝑣⟩)
7067, 69nfeq 2762 . . . . . . . 8 𝑦(((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑥, 𝑣⟩) = ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑥, 𝑣⟩)
71 opeq2 4341 . . . . . . . . . 10 (𝑦 = 𝑣 → ⟨𝑥, 𝑦⟩ = ⟨𝑥, 𝑣⟩)
7271fveq2d 6107 . . . . . . . . 9 (𝑦 = 𝑣 → (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑥, 𝑦⟩) = (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑥, 𝑣⟩))
7371fveq2d 6107 . . . . . . . . 9 (𝑦 = 𝑣 → ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑥, 𝑦⟩) = ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑥, 𝑣⟩))
7472, 73eqeq12d 2625 . . . . . . . 8 (𝑦 = 𝑣 → ((((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑥, 𝑦⟩) = ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑥, 𝑦⟩) ↔ (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑥, 𝑣⟩) = ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑥, 𝑣⟩)))
7562, 70, 74cbvral 3143 . . . . . . 7 (∀𝑦𝑌 (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑥, 𝑦⟩) = ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑥, 𝑦⟩) ↔ ∀𝑣𝑌 (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑥, 𝑣⟩) = ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑥, 𝑣⟩))
76 opeq1 4340 . . . . . . . . . 10 (𝑥 = 𝑢 → ⟨𝑥, 𝑣⟩ = ⟨𝑢, 𝑣⟩)
7776fveq2d 6107 . . . . . . . . 9 (𝑥 = 𝑢 → (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑥, 𝑣⟩) = (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑢, 𝑣⟩))
7876fveq2d 6107 . . . . . . . . 9 (𝑥 = 𝑢 → ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑥, 𝑣⟩) = ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑢, 𝑣⟩))
7977, 78eqeq12d 2625 . . . . . . . 8 (𝑥 = 𝑢 → ((((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑥, 𝑣⟩) = ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑥, 𝑣⟩) ↔ (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑢, 𝑣⟩) = ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑢, 𝑣⟩)))
8079ralbidv 2969 . . . . . . 7 (𝑥 = 𝑢 → (∀𝑣𝑌 (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑥, 𝑣⟩) = ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑥, 𝑣⟩) ↔ ∀𝑣𝑌 (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑢, 𝑣⟩) = ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑢, 𝑣⟩)))
8175, 80syl5bb 271 . . . . . 6 (𝑥 = 𝑢 → (∀𝑦𝑌 (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑥, 𝑦⟩) = ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑥, 𝑦⟩) ↔ ∀𝑣𝑌 (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑢, 𝑣⟩) = ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑢, 𝑣⟩)))
8251, 61, 81cbvral 3143 . . . . 5 (∀𝑥𝑋𝑦𝑌 (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑥, 𝑦⟩) = ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑥, 𝑦⟩) ↔ ∀𝑢𝑋𝑣𝑌 (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑢, 𝑣⟩) = ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑢, 𝑣⟩))
8350, 82sylib 207 . . . 4 (𝜑 → ∀𝑢𝑋𝑣𝑌 (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑢, 𝑣⟩) = ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑢, 𝑣⟩))
84 fveq2 6103 . . . . . 6 (𝑤 = ⟨𝑢, 𝑣⟩ → (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘𝑤) = (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑢, 𝑣⟩))
85 fveq2 6103 . . . . . 6 (𝑤 = ⟨𝑢, 𝑣⟩ → ((𝑥𝑋, 𝑦𝑌𝐶)‘𝑤) = ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑢, 𝑣⟩))
8684, 85eqeq12d 2625 . . . . 5 (𝑤 = ⟨𝑢, 𝑣⟩ → ((((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘𝑤) = ((𝑥𝑋, 𝑦𝑌𝐶)‘𝑤) ↔ (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑢, 𝑣⟩) = ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑢, 𝑣⟩)))
8786ralxp 5185 . . . 4 (∀𝑤 ∈ (𝑋 × 𝑌)(((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘𝑤) = ((𝑥𝑋, 𝑦𝑌𝐶)‘𝑤) ↔ ∀𝑢𝑋𝑣𝑌 (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑢, 𝑣⟩) = ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑢, 𝑣⟩))
8883, 87sylibr 223 . . 3 (𝜑 → ∀𝑤 ∈ (𝑋 × 𝑌)(((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘𝑤) = ((𝑥𝑋, 𝑦𝑌𝐶)‘𝑤))
89 fco 5971 . . . . . 6 (((𝑧𝑍𝐵):𝑍 𝑀 ∧ (𝑥𝑋, 𝑦𝑌𝐴):(𝑋 × 𝑌)⟶𝑍) → ((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴)):(𝑋 × 𝑌)⟶ 𝑀)
9029, 11, 89syl2anc 691 . . . . 5 (𝜑 → ((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴)):(𝑋 × 𝑌)⟶ 𝑀)
91 ffn 5958 . . . . 5 (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴)):(𝑋 × 𝑌)⟶ 𝑀 → ((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴)) Fn (𝑋 × 𝑌))
9290, 91syl 17 . . . 4 (𝜑 → ((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴)) Fn (𝑋 × 𝑌))
9337ralrimivva 2954 . . . . . 6 (𝜑 → ∀𝑥𝑋𝑦𝑌 𝐶 𝑀)
9445fmpt2 7126 . . . . . 6 (∀𝑥𝑋𝑦𝑌 𝐶 𝑀 ↔ (𝑥𝑋, 𝑦𝑌𝐶):(𝑋 × 𝑌)⟶ 𝑀)
9593, 94sylib 207 . . . . 5 (𝜑 → (𝑥𝑋, 𝑦𝑌𝐶):(𝑋 × 𝑌)⟶ 𝑀)
96 ffn 5958 . . . . 5 ((𝑥𝑋, 𝑦𝑌𝐶):(𝑋 × 𝑌)⟶ 𝑀 → (𝑥𝑋, 𝑦𝑌𝐶) Fn (𝑋 × 𝑌))
9795, 96syl 17 . . . 4 (𝜑 → (𝑥𝑋, 𝑦𝑌𝐶) Fn (𝑋 × 𝑌))
98 eqfnfv 6219 . . . 4 ((((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴)) Fn (𝑋 × 𝑌) ∧ (𝑥𝑋, 𝑦𝑌𝐶) Fn (𝑋 × 𝑌)) → (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴)) = (𝑥𝑋, 𝑦𝑌𝐶) ↔ ∀𝑤 ∈ (𝑋 × 𝑌)(((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘𝑤) = ((𝑥𝑋, 𝑦𝑌𝐶)‘𝑤)))
9992, 97, 98syl2anc 691 . . 3 (𝜑 → (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴)) = (𝑥𝑋, 𝑦𝑌𝐶) ↔ ∀𝑤 ∈ (𝑋 × 𝑌)(((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘𝑤) = ((𝑥𝑋, 𝑦𝑌𝐶)‘𝑤)))
10088, 99mpbird 246 . 2 (𝜑 → ((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴)) = (𝑥𝑋, 𝑦𝑌𝐶))
101 cnco 20880 . . 3 (((𝑥𝑋, 𝑦𝑌𝐴) ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ (𝑧𝑍𝐵) ∈ (𝐿 Cn 𝑀)) → ((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴)) ∈ ((𝐽 ×t 𝐾) Cn 𝑀))
1029, 22, 101syl2anc 691 . 2 (𝜑 → ((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴)) ∈ ((𝐽 ×t 𝐾) Cn 𝑀))
103100, 102eqeltrrd 2689 1 (𝜑 → (𝑥𝑋, 𝑦𝑌𝐶) ∈ ((𝐽 ×t 𝐾) Cn 𝑀))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 195  wa 383   = wceq 1475  wcel 1977  wral 2896  cop 4131   cuni 4372  cmpt 4643   × cxp 5036  ccom 5042   Fn wfn 5799  wf 5800  cfv 5804  (class class class)co 6549  cmpt2 6551  Topctop 20517  TopOnctopon 20518   Cn ccn 20838   ×t ctx 21173
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-id 4953  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-fv 5812  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-1st 7059  df-2nd 7060  df-map 7746  df-topgen 15927  df-top 20521  df-bases 20522  df-topon 20523  df-cn 20841  df-tx 21175
This theorem is referenced by:  cnmpt21f  21285  xkofvcn  21297  xkohmeo  21428  qustgplem  21734  prdstmdd  21737  divcn  22479  htpycom  22583  htpycc  22587  reparphti  22605  pcocn  22625  pcohtpylem  22627  pcopt  22630  pcopt2  22631  pcoass  22632  pcorevlem  22634  dipcn  26959
  Copyright terms: Public domain W3C validator