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

Theorem cnmpt21 21522
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 6693 . . . . . . . . . 10 (𝑥(𝑥𝑋, 𝑦𝑌𝐴)𝑦) = ((𝑥𝑋, 𝑦𝑌𝐴)‘⟨𝑥, 𝑦⟩)
2 simprl 809 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝑋𝑦𝑌)) → 𝑥𝑋)
3 simprr 811 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝑋𝑦𝑌)) → 𝑦𝑌)
4 cnmpt21.j . . . . . . . . . . . . . . . 16 (𝜑𝐽 ∈ (TopOn‘𝑋))
5 cnmpt21.k . . . . . . . . . . . . . . . 16 (𝜑𝐾 ∈ (TopOn‘𝑌))
6 txtopon 21442 . . . . . . . . . . . . . . . 16 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝐽 ×t 𝐾) ∈ (TopOn‘(𝑋 × 𝑌)))
74, 5, 6syl2anc 694 . . . . . . . . . . . . . . 15 (𝜑 → (𝐽 ×t 𝐾) ∈ (TopOn‘(𝑋 × 𝑌)))
8 cnmpt21.l . . . . . . . . . . . . . . 15 (𝜑𝐿 ∈ (TopOn‘𝑍))
9 cnmpt21.a . . . . . . . . . . . . . . 15 (𝜑 → (𝑥𝑋, 𝑦𝑌𝐴) ∈ ((𝐽 ×t 𝐾) Cn 𝐿))
10 cnf2 21101 . . . . . . . . . . . . . . 15 (((𝐽 ×t 𝐾) ∈ (TopOn‘(𝑋 × 𝑌)) ∧ 𝐿 ∈ (TopOn‘𝑍) ∧ (𝑥𝑋, 𝑦𝑌𝐴) ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) → (𝑥𝑋, 𝑦𝑌𝐴):(𝑋 × 𝑌)⟶𝑍)
117, 8, 9, 10syl3anc 1366 . . . . . . . . . . . . . 14 (𝜑 → (𝑥𝑋, 𝑦𝑌𝐴):(𝑋 × 𝑌)⟶𝑍)
12 eqid 2651 . . . . . . . . . . . . . . 15 (𝑥𝑋, 𝑦𝑌𝐴) = (𝑥𝑋, 𝑦𝑌𝐴)
1312fmpt2 7282 . . . . . . . . . . . . . 14 (∀𝑥𝑋𝑦𝑌 𝐴𝑍 ↔ (𝑥𝑋, 𝑦𝑌𝐴):(𝑋 × 𝑌)⟶𝑍)
1411, 13sylibr 224 . . . . . . . . . . . . 13 (𝜑 → ∀𝑥𝑋𝑦𝑌 𝐴𝑍)
15 rsp2 2965 . . . . . . . . . . . . 13 (∀𝑥𝑋𝑦𝑌 𝐴𝑍 → ((𝑥𝑋𝑦𝑌) → 𝐴𝑍))
1614, 15syl 17 . . . . . . . . . . . 12 (𝜑 → ((𝑥𝑋𝑦𝑌) → 𝐴𝑍))
1716imp 444 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝑋𝑦𝑌)) → 𝐴𝑍)
1812ovmpt4g 6825 . . . . . . . . . . 11 ((𝑥𝑋𝑦𝑌𝐴𝑍) → (𝑥(𝑥𝑋, 𝑦𝑌𝐴)𝑦) = 𝐴)
192, 3, 17, 18syl3anc 1366 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝑋𝑦𝑌)) → (𝑥(𝑥𝑋, 𝑦𝑌𝐴)𝑦) = 𝐴)
201, 19syl5eqr 2699 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝑋𝑦𝑌)) → ((𝑥𝑋, 𝑦𝑌𝐴)‘⟨𝑥, 𝑦⟩) = 𝐴)
2120fveq2d 6233 . . . . . . . 8 ((𝜑 ∧ (𝑥𝑋𝑦𝑌)) → ((𝑧𝑍𝐵)‘((𝑥𝑋, 𝑦𝑌𝐴)‘⟨𝑥, 𝑦⟩)) = ((𝑧𝑍𝐵)‘𝐴))
22 cnmpt21.b . . . . . . . . . . . . . . 15 (𝜑 → (𝑧𝑍𝐵) ∈ (𝐿 Cn 𝑀))
23 cntop2 21093 . . . . . . . . . . . . . . 15 ((𝑧𝑍𝐵) ∈ (𝐿 Cn 𝑀) → 𝑀 ∈ Top)
2422, 23syl 17 . . . . . . . . . . . . . 14 (𝜑𝑀 ∈ Top)
25 eqid 2651 . . . . . . . . . . . . . . 15 𝑀 = 𝑀
2625toptopon 20770 . . . . . . . . . . . . . 14 (𝑀 ∈ Top ↔ 𝑀 ∈ (TopOn‘ 𝑀))
2724, 26sylib 208 . . . . . . . . . . . . 13 (𝜑𝑀 ∈ (TopOn‘ 𝑀))
28 cnf2 21101 . . . . . . . . . . . . 13 ((𝐿 ∈ (TopOn‘𝑍) ∧ 𝑀 ∈ (TopOn‘ 𝑀) ∧ (𝑧𝑍𝐵) ∈ (𝐿 Cn 𝑀)) → (𝑧𝑍𝐵):𝑍 𝑀)
298, 27, 22, 28syl3anc 1366 . . . . . . . . . . . 12 (𝜑 → (𝑧𝑍𝐵):𝑍 𝑀)
30 eqid 2651 . . . . . . . . . . . . 13 (𝑧𝑍𝐵) = (𝑧𝑍𝐵)
3130fmpt 6421 . . . . . . . . . . . 12 (∀𝑧𝑍 𝐵 𝑀 ↔ (𝑧𝑍𝐵):𝑍 𝑀)
3229, 31sylibr 224 . . . . . . . . . . 11 (𝜑 → ∀𝑧𝑍 𝐵 𝑀)
3332adantr 480 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝑋𝑦𝑌)) → ∀𝑧𝑍 𝐵 𝑀)
34 cnmpt21.c . . . . . . . . . . . 12 (𝑧 = 𝐴𝐵 = 𝐶)
3534eleq1d 2715 . . . . . . . . . . 11 (𝑧 = 𝐴 → (𝐵 𝑀𝐶 𝑀))
3635rspcv 3336 . . . . . . . . . 10 (𝐴𝑍 → (∀𝑧𝑍 𝐵 𝑀𝐶 𝑀))
3717, 33, 36sylc 65 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝑋𝑦𝑌)) → 𝐶 𝑀)
3834, 30fvmptg 6319 . . . . . . . . 9 ((𝐴𝑍𝐶 𝑀) → ((𝑧𝑍𝐵)‘𝐴) = 𝐶)
3917, 37, 38syl2anc 694 . . . . . . . 8 ((𝜑 ∧ (𝑥𝑋𝑦𝑌)) → ((𝑧𝑍𝐵)‘𝐴) = 𝐶)
4021, 39eqtrd 2685 . . . . . . 7 ((𝜑 ∧ (𝑥𝑋𝑦𝑌)) → ((𝑧𝑍𝐵)‘((𝑥𝑋, 𝑦𝑌𝐴)‘⟨𝑥, 𝑦⟩)) = 𝐶)
41 opelxpi 5182 . . . . . . . 8 ((𝑥𝑋𝑦𝑌) → ⟨𝑥, 𝑦⟩ ∈ (𝑋 × 𝑌))
42 fvco3 6314 . . . . . . . 8 (((𝑥𝑋, 𝑦𝑌𝐴):(𝑋 × 𝑌)⟶𝑍 ∧ ⟨𝑥, 𝑦⟩ ∈ (𝑋 × 𝑌)) → (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑥, 𝑦⟩) = ((𝑧𝑍𝐵)‘((𝑥𝑋, 𝑦𝑌𝐴)‘⟨𝑥, 𝑦⟩)))
4311, 41, 42syl2an 493 . . . . . . 7 ((𝜑 ∧ (𝑥𝑋𝑦𝑌)) → (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑥, 𝑦⟩) = ((𝑧𝑍𝐵)‘((𝑥𝑋, 𝑦𝑌𝐴)‘⟨𝑥, 𝑦⟩)))
44 df-ov 6693 . . . . . . . 8 (𝑥(𝑥𝑋, 𝑦𝑌𝐶)𝑦) = ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑥, 𝑦⟩)
45 eqid 2651 . . . . . . . . . 10 (𝑥𝑋, 𝑦𝑌𝐶) = (𝑥𝑋, 𝑦𝑌𝐶)
4645ovmpt4g 6825 . . . . . . . . 9 ((𝑥𝑋𝑦𝑌𝐶 𝑀) → (𝑥(𝑥𝑋, 𝑦𝑌𝐶)𝑦) = 𝐶)
472, 3, 37, 46syl3anc 1366 . . . . . . . 8 ((𝜑 ∧ (𝑥𝑋𝑦𝑌)) → (𝑥(𝑥𝑋, 𝑦𝑌𝐶)𝑦) = 𝐶)
4844, 47syl5eqr 2699 . . . . . . 7 ((𝜑 ∧ (𝑥𝑋𝑦𝑌)) → ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑥, 𝑦⟩) = 𝐶)
4940, 43, 483eqtr4d 2695 . . . . . 6 ((𝜑 ∧ (𝑥𝑋𝑦𝑌)) → (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑥, 𝑦⟩) = ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑥, 𝑦⟩))
5049ralrimivva 3000 . . . . 5 (𝜑 → ∀𝑥𝑋𝑦𝑌 (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑥, 𝑦⟩) = ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑥, 𝑦⟩))
51 nfv 1883 . . . . . 6 𝑢𝑦𝑌 (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑥, 𝑦⟩) = ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑥, 𝑦⟩)
52 nfcv 2793 . . . . . . 7 𝑥𝑌
53 nfcv 2793 . . . . . . . . . 10 𝑥(𝑧𝑍𝐵)
54 nfmpt21 6764 . . . . . . . . . 10 𝑥(𝑥𝑋, 𝑦𝑌𝐴)
5553, 54nfco 5320 . . . . . . . . 9 𝑥((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))
56 nfcv 2793 . . . . . . . . 9 𝑥𝑢, 𝑣
5755, 56nffv 6236 . . . . . . . 8 𝑥(((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑢, 𝑣⟩)
58 nfmpt21 6764 . . . . . . . . 9 𝑥(𝑥𝑋, 𝑦𝑌𝐶)
5958, 56nffv 6236 . . . . . . . 8 𝑥((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑢, 𝑣⟩)
6057, 59nfeq 2805 . . . . . . 7 𝑥(((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑢, 𝑣⟩) = ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑢, 𝑣⟩)
6152, 60nfral 2974 . . . . . 6 𝑥𝑣𝑌 (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑢, 𝑣⟩) = ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑢, 𝑣⟩)
62 nfv 1883 . . . . . . . 8 𝑣(((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑥, 𝑦⟩) = ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑥, 𝑦⟩)
63 nfcv 2793 . . . . . . . . . . 11 𝑦(𝑧𝑍𝐵)
64 nfmpt22 6765 . . . . . . . . . . 11 𝑦(𝑥𝑋, 𝑦𝑌𝐴)
6563, 64nfco 5320 . . . . . . . . . 10 𝑦((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))
66 nfcv 2793 . . . . . . . . . 10 𝑦𝑥, 𝑣
6765, 66nffv 6236 . . . . . . . . 9 𝑦(((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑥, 𝑣⟩)
68 nfmpt22 6765 . . . . . . . . . 10 𝑦(𝑥𝑋, 𝑦𝑌𝐶)
6968, 66nffv 6236 . . . . . . . . 9 𝑦((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑥, 𝑣⟩)
7067, 69nfeq 2805 . . . . . . . 8 𝑦(((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑥, 𝑣⟩) = ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑥, 𝑣⟩)
71 opeq2 4434 . . . . . . . . . 10 (𝑦 = 𝑣 → ⟨𝑥, 𝑦⟩ = ⟨𝑥, 𝑣⟩)
7271fveq2d 6233 . . . . . . . . 9 (𝑦 = 𝑣 → (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑥, 𝑦⟩) = (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑥, 𝑣⟩))
7371fveq2d 6233 . . . . . . . . 9 (𝑦 = 𝑣 → ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑥, 𝑦⟩) = ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑥, 𝑣⟩))
7472, 73eqeq12d 2666 . . . . . . . 8 (𝑦 = 𝑣 → ((((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑥, 𝑦⟩) = ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑥, 𝑦⟩) ↔ (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑥, 𝑣⟩) = ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑥, 𝑣⟩)))
7562, 70, 74cbvral 3197 . . . . . . 7 (∀𝑦𝑌 (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑥, 𝑦⟩) = ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑥, 𝑦⟩) ↔ ∀𝑣𝑌 (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑥, 𝑣⟩) = ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑥, 𝑣⟩))
76 opeq1 4433 . . . . . . . . . 10 (𝑥 = 𝑢 → ⟨𝑥, 𝑣⟩ = ⟨𝑢, 𝑣⟩)
7776fveq2d 6233 . . . . . . . . 9 (𝑥 = 𝑢 → (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑥, 𝑣⟩) = (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑢, 𝑣⟩))
7876fveq2d 6233 . . . . . . . . 9 (𝑥 = 𝑢 → ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑥, 𝑣⟩) = ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑢, 𝑣⟩))
7977, 78eqeq12d 2666 . . . . . . . 8 (𝑥 = 𝑢 → ((((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑥, 𝑣⟩) = ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑥, 𝑣⟩) ↔ (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑢, 𝑣⟩) = ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑢, 𝑣⟩)))
8079ralbidv 3015 . . . . . . 7 (𝑥 = 𝑢 → (∀𝑣𝑌 (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑥, 𝑣⟩) = ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑥, 𝑣⟩) ↔ ∀𝑣𝑌 (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑢, 𝑣⟩) = ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑢, 𝑣⟩)))
8175, 80syl5bb 272 . . . . . 6 (𝑥 = 𝑢 → (∀𝑦𝑌 (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑥, 𝑦⟩) = ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑥, 𝑦⟩) ↔ ∀𝑣𝑌 (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑢, 𝑣⟩) = ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑢, 𝑣⟩)))
8251, 61, 81cbvral 3197 . . . . 5 (∀𝑥𝑋𝑦𝑌 (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑥, 𝑦⟩) = ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑥, 𝑦⟩) ↔ ∀𝑢𝑋𝑣𝑌 (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑢, 𝑣⟩) = ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑢, 𝑣⟩))
8350, 82sylib 208 . . . 4 (𝜑 → ∀𝑢𝑋𝑣𝑌 (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑢, 𝑣⟩) = ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑢, 𝑣⟩))
84 fveq2 6229 . . . . . 6 (𝑤 = ⟨𝑢, 𝑣⟩ → (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘𝑤) = (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑢, 𝑣⟩))
85 fveq2 6229 . . . . . 6 (𝑤 = ⟨𝑢, 𝑣⟩ → ((𝑥𝑋, 𝑦𝑌𝐶)‘𝑤) = ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑢, 𝑣⟩))
8684, 85eqeq12d 2666 . . . . 5 (𝑤 = ⟨𝑢, 𝑣⟩ → ((((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘𝑤) = ((𝑥𝑋, 𝑦𝑌𝐶)‘𝑤) ↔ (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑢, 𝑣⟩) = ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑢, 𝑣⟩)))
8786ralxp 5296 . . . 4 (∀𝑤 ∈ (𝑋 × 𝑌)(((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘𝑤) = ((𝑥𝑋, 𝑦𝑌𝐶)‘𝑤) ↔ ∀𝑢𝑋𝑣𝑌 (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑢, 𝑣⟩) = ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑢, 𝑣⟩))
8883, 87sylibr 224 . . 3 (𝜑 → ∀𝑤 ∈ (𝑋 × 𝑌)(((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘𝑤) = ((𝑥𝑋, 𝑦𝑌𝐶)‘𝑤))
89 fco 6096 . . . . . 6 (((𝑧𝑍𝐵):𝑍 𝑀 ∧ (𝑥𝑋, 𝑦𝑌𝐴):(𝑋 × 𝑌)⟶𝑍) → ((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴)):(𝑋 × 𝑌)⟶ 𝑀)
9029, 11, 89syl2anc 694 . . . . 5 (𝜑 → ((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴)):(𝑋 × 𝑌)⟶ 𝑀)
91 ffn 6083 . . . . 5 (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴)):(𝑋 × 𝑌)⟶ 𝑀 → ((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴)) Fn (𝑋 × 𝑌))
9290, 91syl 17 . . . 4 (𝜑 → ((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴)) Fn (𝑋 × 𝑌))
9337ralrimivva 3000 . . . . . 6 (𝜑 → ∀𝑥𝑋𝑦𝑌 𝐶 𝑀)
9445fmpt2 7282 . . . . . 6 (∀𝑥𝑋𝑦𝑌 𝐶 𝑀 ↔ (𝑥𝑋, 𝑦𝑌𝐶):(𝑋 × 𝑌)⟶ 𝑀)
9593, 94sylib 208 . . . . 5 (𝜑 → (𝑥𝑋, 𝑦𝑌𝐶):(𝑋 × 𝑌)⟶ 𝑀)
96 ffn 6083 . . . . 5 ((𝑥𝑋, 𝑦𝑌𝐶):(𝑋 × 𝑌)⟶ 𝑀 → (𝑥𝑋, 𝑦𝑌𝐶) Fn (𝑋 × 𝑌))
9795, 96syl 17 . . . 4 (𝜑 → (𝑥𝑋, 𝑦𝑌𝐶) Fn (𝑋 × 𝑌))
98 eqfnfv 6351 . . . 4 ((((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴)) Fn (𝑋 × 𝑌) ∧ (𝑥𝑋, 𝑦𝑌𝐶) Fn (𝑋 × 𝑌)) → (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴)) = (𝑥𝑋, 𝑦𝑌𝐶) ↔ ∀𝑤 ∈ (𝑋 × 𝑌)(((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘𝑤) = ((𝑥𝑋, 𝑦𝑌𝐶)‘𝑤)))
9992, 97, 98syl2anc 694 . . 3 (𝜑 → (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴)) = (𝑥𝑋, 𝑦𝑌𝐶) ↔ ∀𝑤 ∈ (𝑋 × 𝑌)(((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘𝑤) = ((𝑥𝑋, 𝑦𝑌𝐶)‘𝑤)))
10088, 99mpbird 247 . 2 (𝜑 → ((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴)) = (𝑥𝑋, 𝑦𝑌𝐶))
101 cnco 21118 . . 3 (((𝑥𝑋, 𝑦𝑌𝐴) ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ (𝑧𝑍𝐵) ∈ (𝐿 Cn 𝑀)) → ((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴)) ∈ ((𝐽 ×t 𝐾) Cn 𝑀))
1029, 22, 101syl2anc 694 . 2 (𝜑 → ((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴)) ∈ ((𝐽 ×t 𝐾) Cn 𝑀))
103100, 102eqeltrrd 2731 1 (𝜑 → (𝑥𝑋, 𝑦𝑌𝐶) ∈ ((𝐽 ×t 𝐾) Cn 𝑀))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383   = wceq 1523  wcel 2030  wral 2941  cop 4216   cuni 4468  cmpt 4762   × cxp 5141  ccom 5147   Fn wfn 5921  wf 5922  cfv 5926  (class class class)co 6690  cmpt2 6692  Topctop 20746  TopOnctopon 20763   Cn ccn 21076   ×t ctx 21411
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-id 5053  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-fv 5934  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-1st 7210  df-2nd 7211  df-map 7901  df-topgen 16151  df-top 20747  df-topon 20764  df-bases 20798  df-cn 21079  df-tx 21413
This theorem is referenced by:  cnmpt21f  21523  xkofvcn  21535  xkohmeo  21666  qustgplem  21971  prdstmdd  21974  divcn  22718  htpycom  22822  htpycc  22826  reparphti  22843  pcocn  22863  pcohtpylem  22865  pcopt  22868  pcopt2  22869  pcoass  22870  pcorevlem  22872  dipcn  27703
  Copyright terms: Public domain W3C validator