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

Theorem cnmpt21 23679
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 7434 . . . . . . . . . 10 (𝑥(𝑥𝑋, 𝑦𝑌𝐴)𝑦) = ((𝑥𝑋, 𝑦𝑌𝐴)‘⟨𝑥, 𝑦⟩)
2 simprl 771 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝑋𝑦𝑌)) → 𝑥𝑋)
3 simprr 773 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝑋𝑦𝑌)) → 𝑦𝑌)
4 cnmpt21.j . . . . . . . . . . . . . . . 16 (𝜑𝐽 ∈ (TopOn‘𝑋))
5 cnmpt21.k . . . . . . . . . . . . . . . 16 (𝜑𝐾 ∈ (TopOn‘𝑌))
6 txtopon 23599 . . . . . . . . . . . . . . . 16 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝐽 ×t 𝐾) ∈ (TopOn‘(𝑋 × 𝑌)))
74, 5, 6syl2anc 584 . . . . . . . . . . . . . . 15 (𝜑 → (𝐽 ×t 𝐾) ∈ (TopOn‘(𝑋 × 𝑌)))
8 cnmpt21.l . . . . . . . . . . . . . . 15 (𝜑𝐿 ∈ (TopOn‘𝑍))
9 cnmpt21.a . . . . . . . . . . . . . . 15 (𝜑 → (𝑥𝑋, 𝑦𝑌𝐴) ∈ ((𝐽 ×t 𝐾) Cn 𝐿))
10 cnf2 23257 . . . . . . . . . . . . . . 15 (((𝐽 ×t 𝐾) ∈ (TopOn‘(𝑋 × 𝑌)) ∧ 𝐿 ∈ (TopOn‘𝑍) ∧ (𝑥𝑋, 𝑦𝑌𝐴) ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) → (𝑥𝑋, 𝑦𝑌𝐴):(𝑋 × 𝑌)⟶𝑍)
117, 8, 9, 10syl3anc 1373 . . . . . . . . . . . . . 14 (𝜑 → (𝑥𝑋, 𝑦𝑌𝐴):(𝑋 × 𝑌)⟶𝑍)
12 eqid 2737 . . . . . . . . . . . . . . 15 (𝑥𝑋, 𝑦𝑌𝐴) = (𝑥𝑋, 𝑦𝑌𝐴)
1312fmpo 8093 . . . . . . . . . . . . . 14 (∀𝑥𝑋𝑦𝑌 𝐴𝑍 ↔ (𝑥𝑋, 𝑦𝑌𝐴):(𝑋 × 𝑌)⟶𝑍)
1411, 13sylibr 234 . . . . . . . . . . . . 13 (𝜑 → ∀𝑥𝑋𝑦𝑌 𝐴𝑍)
15 rsp2 3277 . . . . . . . . . . . . 13 (∀𝑥𝑋𝑦𝑌 𝐴𝑍 → ((𝑥𝑋𝑦𝑌) → 𝐴𝑍))
1614, 15syl 17 . . . . . . . . . . . 12 (𝜑 → ((𝑥𝑋𝑦𝑌) → 𝐴𝑍))
1716imp 406 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝑋𝑦𝑌)) → 𝐴𝑍)
1812ovmpt4g 7580 . . . . . . . . . . 11 ((𝑥𝑋𝑦𝑌𝐴𝑍) → (𝑥(𝑥𝑋, 𝑦𝑌𝐴)𝑦) = 𝐴)
192, 3, 17, 18syl3anc 1373 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝑋𝑦𝑌)) → (𝑥(𝑥𝑋, 𝑦𝑌𝐴)𝑦) = 𝐴)
201, 19eqtr3id 2791 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝑋𝑦𝑌)) → ((𝑥𝑋, 𝑦𝑌𝐴)‘⟨𝑥, 𝑦⟩) = 𝐴)
2120fveq2d 6910 . . . . . . . 8 ((𝜑 ∧ (𝑥𝑋𝑦𝑌)) → ((𝑧𝑍𝐵)‘((𝑥𝑋, 𝑦𝑌𝐴)‘⟨𝑥, 𝑦⟩)) = ((𝑧𝑍𝐵)‘𝐴))
22 eqid 2737 . . . . . . . . 9 (𝑧𝑍𝐵) = (𝑧𝑍𝐵)
23 cnmpt21.c . . . . . . . . 9 (𝑧 = 𝐴𝐵 = 𝐶)
2423eleq1d 2826 . . . . . . . . . 10 (𝑧 = 𝐴 → (𝐵 𝑀𝐶 𝑀))
25 cnmpt21.b . . . . . . . . . . . . . . 15 (𝜑 → (𝑧𝑍𝐵) ∈ (𝐿 Cn 𝑀))
26 cntop2 23249 . . . . . . . . . . . . . . 15 ((𝑧𝑍𝐵) ∈ (𝐿 Cn 𝑀) → 𝑀 ∈ Top)
2725, 26syl 17 . . . . . . . . . . . . . 14 (𝜑𝑀 ∈ Top)
28 toptopon2 22924 . . . . . . . . . . . . . 14 (𝑀 ∈ Top ↔ 𝑀 ∈ (TopOn‘ 𝑀))
2927, 28sylib 218 . . . . . . . . . . . . 13 (𝜑𝑀 ∈ (TopOn‘ 𝑀))
30 cnf2 23257 . . . . . . . . . . . . 13 ((𝐿 ∈ (TopOn‘𝑍) ∧ 𝑀 ∈ (TopOn‘ 𝑀) ∧ (𝑧𝑍𝐵) ∈ (𝐿 Cn 𝑀)) → (𝑧𝑍𝐵):𝑍 𝑀)
318, 29, 25, 30syl3anc 1373 . . . . . . . . . . . 12 (𝜑 → (𝑧𝑍𝐵):𝑍 𝑀)
3222fmpt 7130 . . . . . . . . . . . 12 (∀𝑧𝑍 𝐵 𝑀 ↔ (𝑧𝑍𝐵):𝑍 𝑀)
3331, 32sylibr 234 . . . . . . . . . . 11 (𝜑 → ∀𝑧𝑍 𝐵 𝑀)
3433adantr 480 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝑋𝑦𝑌)) → ∀𝑧𝑍 𝐵 𝑀)
3524, 34, 17rspcdva 3623 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝑋𝑦𝑌)) → 𝐶 𝑀)
3622, 23, 17, 35fvmptd3 7039 . . . . . . . 8 ((𝜑 ∧ (𝑥𝑋𝑦𝑌)) → ((𝑧𝑍𝐵)‘𝐴) = 𝐶)
3721, 36eqtrd 2777 . . . . . . 7 ((𝜑 ∧ (𝑥𝑋𝑦𝑌)) → ((𝑧𝑍𝐵)‘((𝑥𝑋, 𝑦𝑌𝐴)‘⟨𝑥, 𝑦⟩)) = 𝐶)
38 opelxpi 5722 . . . . . . . 8 ((𝑥𝑋𝑦𝑌) → ⟨𝑥, 𝑦⟩ ∈ (𝑋 × 𝑌))
39 fvco3 7008 . . . . . . . 8 (((𝑥𝑋, 𝑦𝑌𝐴):(𝑋 × 𝑌)⟶𝑍 ∧ ⟨𝑥, 𝑦⟩ ∈ (𝑋 × 𝑌)) → (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑥, 𝑦⟩) = ((𝑧𝑍𝐵)‘((𝑥𝑋, 𝑦𝑌𝐴)‘⟨𝑥, 𝑦⟩)))
4011, 38, 39syl2an 596 . . . . . . 7 ((𝜑 ∧ (𝑥𝑋𝑦𝑌)) → (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑥, 𝑦⟩) = ((𝑧𝑍𝐵)‘((𝑥𝑋, 𝑦𝑌𝐴)‘⟨𝑥, 𝑦⟩)))
41 df-ov 7434 . . . . . . . 8 (𝑥(𝑥𝑋, 𝑦𝑌𝐶)𝑦) = ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑥, 𝑦⟩)
42 eqid 2737 . . . . . . . . . 10 (𝑥𝑋, 𝑦𝑌𝐶) = (𝑥𝑋, 𝑦𝑌𝐶)
4342ovmpt4g 7580 . . . . . . . . 9 ((𝑥𝑋𝑦𝑌𝐶 𝑀) → (𝑥(𝑥𝑋, 𝑦𝑌𝐶)𝑦) = 𝐶)
442, 3, 35, 43syl3anc 1373 . . . . . . . 8 ((𝜑 ∧ (𝑥𝑋𝑦𝑌)) → (𝑥(𝑥𝑋, 𝑦𝑌𝐶)𝑦) = 𝐶)
4541, 44eqtr3id 2791 . . . . . . 7 ((𝜑 ∧ (𝑥𝑋𝑦𝑌)) → ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑥, 𝑦⟩) = 𝐶)
4637, 40, 453eqtr4d 2787 . . . . . 6 ((𝜑 ∧ (𝑥𝑋𝑦𝑌)) → (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑥, 𝑦⟩) = ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑥, 𝑦⟩))
4746ralrimivva 3202 . . . . 5 (𝜑 → ∀𝑥𝑋𝑦𝑌 (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑥, 𝑦⟩) = ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑥, 𝑦⟩))
48 nfv 1914 . . . . . 6 𝑢𝑦𝑌 (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑥, 𝑦⟩) = ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑥, 𝑦⟩)
49 nfcv 2905 . . . . . . 7 𝑥𝑌
50 nfcv 2905 . . . . . . . . . 10 𝑥(𝑧𝑍𝐵)
51 nfmpo1 7513 . . . . . . . . . 10 𝑥(𝑥𝑋, 𝑦𝑌𝐴)
5250, 51nfco 5876 . . . . . . . . 9 𝑥((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))
53 nfcv 2905 . . . . . . . . 9 𝑥𝑢, 𝑣
5452, 53nffv 6916 . . . . . . . 8 𝑥(((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑢, 𝑣⟩)
55 nfmpo1 7513 . . . . . . . . 9 𝑥(𝑥𝑋, 𝑦𝑌𝐶)
5655, 53nffv 6916 . . . . . . . 8 𝑥((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑢, 𝑣⟩)
5754, 56nfeq 2919 . . . . . . 7 𝑥(((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑢, 𝑣⟩) = ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑢, 𝑣⟩)
5849, 57nfralw 3311 . . . . . 6 𝑥𝑣𝑌 (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑢, 𝑣⟩) = ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑢, 𝑣⟩)
59 nfv 1914 . . . . . . . 8 𝑣(((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑥, 𝑦⟩) = ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑥, 𝑦⟩)
60 nfcv 2905 . . . . . . . . . . 11 𝑦(𝑧𝑍𝐵)
61 nfmpo2 7514 . . . . . . . . . . 11 𝑦(𝑥𝑋, 𝑦𝑌𝐴)
6260, 61nfco 5876 . . . . . . . . . 10 𝑦((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))
63 nfcv 2905 . . . . . . . . . 10 𝑦𝑥, 𝑣
6462, 63nffv 6916 . . . . . . . . 9 𝑦(((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑥, 𝑣⟩)
65 nfmpo2 7514 . . . . . . . . . 10 𝑦(𝑥𝑋, 𝑦𝑌𝐶)
6665, 63nffv 6916 . . . . . . . . 9 𝑦((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑥, 𝑣⟩)
6764, 66nfeq 2919 . . . . . . . 8 𝑦(((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑥, 𝑣⟩) = ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑥, 𝑣⟩)
68 opeq2 4874 . . . . . . . . . 10 (𝑦 = 𝑣 → ⟨𝑥, 𝑦⟩ = ⟨𝑥, 𝑣⟩)
6968fveq2d 6910 . . . . . . . . 9 (𝑦 = 𝑣 → (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑥, 𝑦⟩) = (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑥, 𝑣⟩))
7068fveq2d 6910 . . . . . . . . 9 (𝑦 = 𝑣 → ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑥, 𝑦⟩) = ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑥, 𝑣⟩))
7169, 70eqeq12d 2753 . . . . . . . 8 (𝑦 = 𝑣 → ((((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑥, 𝑦⟩) = ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑥, 𝑦⟩) ↔ (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑥, 𝑣⟩) = ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑥, 𝑣⟩)))
7259, 67, 71cbvralw 3306 . . . . . . 7 (∀𝑦𝑌 (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑥, 𝑦⟩) = ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑥, 𝑦⟩) ↔ ∀𝑣𝑌 (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑥, 𝑣⟩) = ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑥, 𝑣⟩))
73 opeq1 4873 . . . . . . . . . 10 (𝑥 = 𝑢 → ⟨𝑥, 𝑣⟩ = ⟨𝑢, 𝑣⟩)
7473fveq2d 6910 . . . . . . . . 9 (𝑥 = 𝑢 → (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑥, 𝑣⟩) = (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑢, 𝑣⟩))
7573fveq2d 6910 . . . . . . . . 9 (𝑥 = 𝑢 → ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑥, 𝑣⟩) = ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑢, 𝑣⟩))
7674, 75eqeq12d 2753 . . . . . . . 8 (𝑥 = 𝑢 → ((((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑥, 𝑣⟩) = ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑥, 𝑣⟩) ↔ (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑢, 𝑣⟩) = ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑢, 𝑣⟩)))
7776ralbidv 3178 . . . . . . 7 (𝑥 = 𝑢 → (∀𝑣𝑌 (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑥, 𝑣⟩) = ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑥, 𝑣⟩) ↔ ∀𝑣𝑌 (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑢, 𝑣⟩) = ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑢, 𝑣⟩)))
7872, 77bitrid 283 . . . . . 6 (𝑥 = 𝑢 → (∀𝑦𝑌 (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑥, 𝑦⟩) = ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑥, 𝑦⟩) ↔ ∀𝑣𝑌 (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑢, 𝑣⟩) = ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑢, 𝑣⟩)))
7948, 58, 78cbvralw 3306 . . . . 5 (∀𝑥𝑋𝑦𝑌 (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑥, 𝑦⟩) = ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑥, 𝑦⟩) ↔ ∀𝑢𝑋𝑣𝑌 (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑢, 𝑣⟩) = ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑢, 𝑣⟩))
8047, 79sylib 218 . . . 4 (𝜑 → ∀𝑢𝑋𝑣𝑌 (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑢, 𝑣⟩) = ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑢, 𝑣⟩))
81 fveq2 6906 . . . . . 6 (𝑤 = ⟨𝑢, 𝑣⟩ → (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘𝑤) = (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑢, 𝑣⟩))
82 fveq2 6906 . . . . . 6 (𝑤 = ⟨𝑢, 𝑣⟩ → ((𝑥𝑋, 𝑦𝑌𝐶)‘𝑤) = ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑢, 𝑣⟩))
8381, 82eqeq12d 2753 . . . . 5 (𝑤 = ⟨𝑢, 𝑣⟩ → ((((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘𝑤) = ((𝑥𝑋, 𝑦𝑌𝐶)‘𝑤) ↔ (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑢, 𝑣⟩) = ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑢, 𝑣⟩)))
8483ralxp 5852 . . . 4 (∀𝑤 ∈ (𝑋 × 𝑌)(((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘𝑤) = ((𝑥𝑋, 𝑦𝑌𝐶)‘𝑤) ↔ ∀𝑢𝑋𝑣𝑌 (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑢, 𝑣⟩) = ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑢, 𝑣⟩))
8580, 84sylibr 234 . . 3 (𝜑 → ∀𝑤 ∈ (𝑋 × 𝑌)(((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘𝑤) = ((𝑥𝑋, 𝑦𝑌𝐶)‘𝑤))
86 fco 6760 . . . . . 6 (((𝑧𝑍𝐵):𝑍 𝑀 ∧ (𝑥𝑋, 𝑦𝑌𝐴):(𝑋 × 𝑌)⟶𝑍) → ((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴)):(𝑋 × 𝑌)⟶ 𝑀)
8731, 11, 86syl2anc 584 . . . . 5 (𝜑 → ((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴)):(𝑋 × 𝑌)⟶ 𝑀)
8887ffnd 6737 . . . 4 (𝜑 → ((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴)) Fn (𝑋 × 𝑌))
8935ralrimivva 3202 . . . . . 6 (𝜑 → ∀𝑥𝑋𝑦𝑌 𝐶 𝑀)
9042fmpo 8093 . . . . . 6 (∀𝑥𝑋𝑦𝑌 𝐶 𝑀 ↔ (𝑥𝑋, 𝑦𝑌𝐶):(𝑋 × 𝑌)⟶ 𝑀)
9189, 90sylib 218 . . . . 5 (𝜑 → (𝑥𝑋, 𝑦𝑌𝐶):(𝑋 × 𝑌)⟶ 𝑀)
9291ffnd 6737 . . . 4 (𝜑 → (𝑥𝑋, 𝑦𝑌𝐶) Fn (𝑋 × 𝑌))
93 eqfnfv 7051 . . . 4 ((((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴)) Fn (𝑋 × 𝑌) ∧ (𝑥𝑋, 𝑦𝑌𝐶) Fn (𝑋 × 𝑌)) → (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴)) = (𝑥𝑋, 𝑦𝑌𝐶) ↔ ∀𝑤 ∈ (𝑋 × 𝑌)(((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘𝑤) = ((𝑥𝑋, 𝑦𝑌𝐶)‘𝑤)))
9488, 92, 93syl2anc 584 . . 3 (𝜑 → (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴)) = (𝑥𝑋, 𝑦𝑌𝐶) ↔ ∀𝑤 ∈ (𝑋 × 𝑌)(((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘𝑤) = ((𝑥𝑋, 𝑦𝑌𝐶)‘𝑤)))
9585, 94mpbird 257 . 2 (𝜑 → ((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴)) = (𝑥𝑋, 𝑦𝑌𝐶))
96 cnco 23274 . . 3 (((𝑥𝑋, 𝑦𝑌𝐴) ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ (𝑧𝑍𝐵) ∈ (𝐿 Cn 𝑀)) → ((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴)) ∈ ((𝐽 ×t 𝐾) Cn 𝑀))
979, 25, 96syl2anc 584 . 2 (𝜑 → ((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴)) ∈ ((𝐽 ×t 𝐾) Cn 𝑀))
9895, 97eqeltrrd 2842 1 (𝜑 → (𝑥𝑋, 𝑦𝑌𝐶) ∈ ((𝐽 ×t 𝐾) Cn 𝑀))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395   = wceq 1540  wcel 2108  wral 3061  cop 4632   cuni 4907  cmpt 5225   × cxp 5683  ccom 5689   Fn wfn 6556  wf 6557  cfv 6561  (class class class)co 7431  cmpo 7433  Topctop 22899  TopOnctopon 22916   Cn ccn 23232   ×t ctx 23568
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-fv 6569  df-ov 7434  df-oprab 7435  df-mpo 7436  df-1st 8014  df-2nd 8015  df-map 8868  df-topgen 17488  df-top 22900  df-topon 22917  df-bases 22953  df-cn 23235  df-tx 23570
This theorem is referenced by:  cnmpt21f  23680  xkofvcn  23692  xkohmeo  23823  qustgplem  24129  prdstmdd  24132  divcnOLD  24890  divcn  24892  htpycom  25008  htpycc  25012  reparphti  25029  reparphtiOLD  25030  pcocn  25050  pcohtpylem  25052  pcopt  25055  pcopt2  25056  pcoass  25057  pcorevlem  25059  dipcn  30739
  Copyright terms: Public domain W3C validator