ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  cnmpt21 GIF version

Theorem cnmpt21 13085
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 5856 . . . . . . . . . 10 (𝑥(𝑥𝑋, 𝑦𝑌𝐴)𝑦) = ((𝑥𝑋, 𝑦𝑌𝐴)‘⟨𝑥, 𝑦⟩)
2 simprl 526 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝑋𝑦𝑌)) → 𝑥𝑋)
3 simprr 527 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝑋𝑦𝑌)) → 𝑦𝑌)
4 cnmpt21.j . . . . . . . . . . . . . . . 16 (𝜑𝐽 ∈ (TopOn‘𝑋))
5 cnmpt21.k . . . . . . . . . . . . . . . 16 (𝜑𝐾 ∈ (TopOn‘𝑌))
6 txtopon 13056 . . . . . . . . . . . . . . . 16 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝐽 ×t 𝐾) ∈ (TopOn‘(𝑋 × 𝑌)))
74, 5, 6syl2anc 409 . . . . . . . . . . . . . . 15 (𝜑 → (𝐽 ×t 𝐾) ∈ (TopOn‘(𝑋 × 𝑌)))
8 cnmpt21.l . . . . . . . . . . . . . . 15 (𝜑𝐿 ∈ (TopOn‘𝑍))
9 cnmpt21.a . . . . . . . . . . . . . . 15 (𝜑 → (𝑥𝑋, 𝑦𝑌𝐴) ∈ ((𝐽 ×t 𝐾) Cn 𝐿))
10 cnf2 12999 . . . . . . . . . . . . . . 15 (((𝐽 ×t 𝐾) ∈ (TopOn‘(𝑋 × 𝑌)) ∧ 𝐿 ∈ (TopOn‘𝑍) ∧ (𝑥𝑋, 𝑦𝑌𝐴) ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) → (𝑥𝑋, 𝑦𝑌𝐴):(𝑋 × 𝑌)⟶𝑍)
117, 8, 9, 10syl3anc 1233 . . . . . . . . . . . . . 14 (𝜑 → (𝑥𝑋, 𝑦𝑌𝐴):(𝑋 × 𝑌)⟶𝑍)
12 eqid 2170 . . . . . . . . . . . . . . 15 (𝑥𝑋, 𝑦𝑌𝐴) = (𝑥𝑋, 𝑦𝑌𝐴)
1312fmpo 6180 . . . . . . . . . . . . . 14 (∀𝑥𝑋𝑦𝑌 𝐴𝑍 ↔ (𝑥𝑋, 𝑦𝑌𝐴):(𝑋 × 𝑌)⟶𝑍)
1411, 13sylibr 133 . . . . . . . . . . . . 13 (𝜑 → ∀𝑥𝑋𝑦𝑌 𝐴𝑍)
15 rsp2 2520 . . . . . . . . . . . . 13 (∀𝑥𝑋𝑦𝑌 𝐴𝑍 → ((𝑥𝑋𝑦𝑌) → 𝐴𝑍))
1614, 15syl 14 . . . . . . . . . . . 12 (𝜑 → ((𝑥𝑋𝑦𝑌) → 𝐴𝑍))
1716imp 123 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝑋𝑦𝑌)) → 𝐴𝑍)
1812ovmpt4g 5975 . . . . . . . . . . 11 ((𝑥𝑋𝑦𝑌𝐴𝑍) → (𝑥(𝑥𝑋, 𝑦𝑌𝐴)𝑦) = 𝐴)
192, 3, 17, 18syl3anc 1233 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝑋𝑦𝑌)) → (𝑥(𝑥𝑋, 𝑦𝑌𝐴)𝑦) = 𝐴)
201, 19eqtr3id 2217 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝑋𝑦𝑌)) → ((𝑥𝑋, 𝑦𝑌𝐴)‘⟨𝑥, 𝑦⟩) = 𝐴)
2120fveq2d 5500 . . . . . . . 8 ((𝜑 ∧ (𝑥𝑋𝑦𝑌)) → ((𝑧𝑍𝐵)‘((𝑥𝑋, 𝑦𝑌𝐴)‘⟨𝑥, 𝑦⟩)) = ((𝑧𝑍𝐵)‘𝐴))
22 eqid 2170 . . . . . . . . 9 (𝑧𝑍𝐵) = (𝑧𝑍𝐵)
23 cnmpt21.c . . . . . . . . 9 (𝑧 = 𝐴𝐵 = 𝐶)
2423eleq1d 2239 . . . . . . . . . 10 (𝑧 = 𝐴 → (𝐵 𝑀𝐶 𝑀))
25 cnmpt21.b . . . . . . . . . . . . . . 15 (𝜑 → (𝑧𝑍𝐵) ∈ (𝐿 Cn 𝑀))
26 cntop2 12996 . . . . . . . . . . . . . . 15 ((𝑧𝑍𝐵) ∈ (𝐿 Cn 𝑀) → 𝑀 ∈ Top)
2725, 26syl 14 . . . . . . . . . . . . . 14 (𝜑𝑀 ∈ Top)
28 toptopon2 12811 . . . . . . . . . . . . . 14 (𝑀 ∈ Top ↔ 𝑀 ∈ (TopOn‘ 𝑀))
2927, 28sylib 121 . . . . . . . . . . . . 13 (𝜑𝑀 ∈ (TopOn‘ 𝑀))
30 cnf2 12999 . . . . . . . . . . . . 13 ((𝐿 ∈ (TopOn‘𝑍) ∧ 𝑀 ∈ (TopOn‘ 𝑀) ∧ (𝑧𝑍𝐵) ∈ (𝐿 Cn 𝑀)) → (𝑧𝑍𝐵):𝑍 𝑀)
318, 29, 25, 30syl3anc 1233 . . . . . . . . . . . 12 (𝜑 → (𝑧𝑍𝐵):𝑍 𝑀)
3222fmpt 5646 . . . . . . . . . . . 12 (∀𝑧𝑍 𝐵 𝑀 ↔ (𝑧𝑍𝐵):𝑍 𝑀)
3331, 32sylibr 133 . . . . . . . . . . 11 (𝜑 → ∀𝑧𝑍 𝐵 𝑀)
3433adantr 274 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝑋𝑦𝑌)) → ∀𝑧𝑍 𝐵 𝑀)
3524, 34, 17rspcdva 2839 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝑋𝑦𝑌)) → 𝐶 𝑀)
3622, 23, 17, 35fvmptd3 5589 . . . . . . . 8 ((𝜑 ∧ (𝑥𝑋𝑦𝑌)) → ((𝑧𝑍𝐵)‘𝐴) = 𝐶)
3721, 36eqtrd 2203 . . . . . . 7 ((𝜑 ∧ (𝑥𝑋𝑦𝑌)) → ((𝑧𝑍𝐵)‘((𝑥𝑋, 𝑦𝑌𝐴)‘⟨𝑥, 𝑦⟩)) = 𝐶)
38 opelxpi 4643 . . . . . . . 8 ((𝑥𝑋𝑦𝑌) → ⟨𝑥, 𝑦⟩ ∈ (𝑋 × 𝑌))
39 fvco3 5567 . . . . . . . 8 (((𝑥𝑋, 𝑦𝑌𝐴):(𝑋 × 𝑌)⟶𝑍 ∧ ⟨𝑥, 𝑦⟩ ∈ (𝑋 × 𝑌)) → (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑥, 𝑦⟩) = ((𝑧𝑍𝐵)‘((𝑥𝑋, 𝑦𝑌𝐴)‘⟨𝑥, 𝑦⟩)))
4011, 38, 39syl2an 287 . . . . . . 7 ((𝜑 ∧ (𝑥𝑋𝑦𝑌)) → (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑥, 𝑦⟩) = ((𝑧𝑍𝐵)‘((𝑥𝑋, 𝑦𝑌𝐴)‘⟨𝑥, 𝑦⟩)))
41 df-ov 5856 . . . . . . . 8 (𝑥(𝑥𝑋, 𝑦𝑌𝐶)𝑦) = ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑥, 𝑦⟩)
42 eqid 2170 . . . . . . . . . 10 (𝑥𝑋, 𝑦𝑌𝐶) = (𝑥𝑋, 𝑦𝑌𝐶)
4342ovmpt4g 5975 . . . . . . . . 9 ((𝑥𝑋𝑦𝑌𝐶 𝑀) → (𝑥(𝑥𝑋, 𝑦𝑌𝐶)𝑦) = 𝐶)
442, 3, 35, 43syl3anc 1233 . . . . . . . 8 ((𝜑 ∧ (𝑥𝑋𝑦𝑌)) → (𝑥(𝑥𝑋, 𝑦𝑌𝐶)𝑦) = 𝐶)
4541, 44eqtr3id 2217 . . . . . . 7 ((𝜑 ∧ (𝑥𝑋𝑦𝑌)) → ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑥, 𝑦⟩) = 𝐶)
4637, 40, 453eqtr4d 2213 . . . . . 6 ((𝜑 ∧ (𝑥𝑋𝑦𝑌)) → (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑥, 𝑦⟩) = ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑥, 𝑦⟩))
4746ralrimivva 2552 . . . . 5 (𝜑 → ∀𝑥𝑋𝑦𝑌 (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑥, 𝑦⟩) = ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑥, 𝑦⟩))
48 nfv 1521 . . . . . 6 𝑢𝑦𝑌 (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑥, 𝑦⟩) = ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑥, 𝑦⟩)
49 nfcv 2312 . . . . . . 7 𝑥𝑌
50 nfcv 2312 . . . . . . . . . 10 𝑥(𝑧𝑍𝐵)
51 nfmpo1 5920 . . . . . . . . . 10 𝑥(𝑥𝑋, 𝑦𝑌𝐴)
5250, 51nfco 4776 . . . . . . . . 9 𝑥((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))
53 nfcv 2312 . . . . . . . . 9 𝑥𝑢, 𝑣
5452, 53nffv 5506 . . . . . . . 8 𝑥(((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑢, 𝑣⟩)
55 nfmpo1 5920 . . . . . . . . 9 𝑥(𝑥𝑋, 𝑦𝑌𝐶)
5655, 53nffv 5506 . . . . . . . 8 𝑥((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑢, 𝑣⟩)
5754, 56nfeq 2320 . . . . . . 7 𝑥(((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑢, 𝑣⟩) = ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑢, 𝑣⟩)
5849, 57nfralxy 2508 . . . . . 6 𝑥𝑣𝑌 (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑢, 𝑣⟩) = ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑢, 𝑣⟩)
59 nfv 1521 . . . . . . . 8 𝑣(((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑥, 𝑦⟩) = ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑥, 𝑦⟩)
60 nfcv 2312 . . . . . . . . . . 11 𝑦(𝑧𝑍𝐵)
61 nfmpo2 5921 . . . . . . . . . . 11 𝑦(𝑥𝑋, 𝑦𝑌𝐴)
6260, 61nfco 4776 . . . . . . . . . 10 𝑦((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))
63 nfcv 2312 . . . . . . . . . 10 𝑦𝑥, 𝑣
6462, 63nffv 5506 . . . . . . . . 9 𝑦(((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑥, 𝑣⟩)
65 nfmpo2 5921 . . . . . . . . . 10 𝑦(𝑥𝑋, 𝑦𝑌𝐶)
6665, 63nffv 5506 . . . . . . . . 9 𝑦((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑥, 𝑣⟩)
6764, 66nfeq 2320 . . . . . . . 8 𝑦(((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑥, 𝑣⟩) = ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑥, 𝑣⟩)
68 opeq2 3766 . . . . . . . . . 10 (𝑦 = 𝑣 → ⟨𝑥, 𝑦⟩ = ⟨𝑥, 𝑣⟩)
6968fveq2d 5500 . . . . . . . . 9 (𝑦 = 𝑣 → (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑥, 𝑦⟩) = (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑥, 𝑣⟩))
7068fveq2d 5500 . . . . . . . . 9 (𝑦 = 𝑣 → ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑥, 𝑦⟩) = ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑥, 𝑣⟩))
7169, 70eqeq12d 2185 . . . . . . . 8 (𝑦 = 𝑣 → ((((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑥, 𝑦⟩) = ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑥, 𝑦⟩) ↔ (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑥, 𝑣⟩) = ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑥, 𝑣⟩)))
7259, 67, 71cbvral 2692 . . . . . . 7 (∀𝑦𝑌 (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑥, 𝑦⟩) = ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑥, 𝑦⟩) ↔ ∀𝑣𝑌 (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑥, 𝑣⟩) = ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑥, 𝑣⟩))
73 opeq1 3765 . . . . . . . . . 10 (𝑥 = 𝑢 → ⟨𝑥, 𝑣⟩ = ⟨𝑢, 𝑣⟩)
7473fveq2d 5500 . . . . . . . . 9 (𝑥 = 𝑢 → (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑥, 𝑣⟩) = (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑢, 𝑣⟩))
7573fveq2d 5500 . . . . . . . . 9 (𝑥 = 𝑢 → ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑥, 𝑣⟩) = ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑢, 𝑣⟩))
7674, 75eqeq12d 2185 . . . . . . . 8 (𝑥 = 𝑢 → ((((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑥, 𝑣⟩) = ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑥, 𝑣⟩) ↔ (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑢, 𝑣⟩) = ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑢, 𝑣⟩)))
7776ralbidv 2470 . . . . . . 7 (𝑥 = 𝑢 → (∀𝑣𝑌 (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑥, 𝑣⟩) = ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑥, 𝑣⟩) ↔ ∀𝑣𝑌 (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑢, 𝑣⟩) = ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑢, 𝑣⟩)))
7872, 77syl5bb 191 . . . . . 6 (𝑥 = 𝑢 → (∀𝑦𝑌 (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑥, 𝑦⟩) = ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑥, 𝑦⟩) ↔ ∀𝑣𝑌 (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑢, 𝑣⟩) = ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑢, 𝑣⟩)))
7948, 58, 78cbvral 2692 . . . . 5 (∀𝑥𝑋𝑦𝑌 (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑥, 𝑦⟩) = ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑥, 𝑦⟩) ↔ ∀𝑢𝑋𝑣𝑌 (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑢, 𝑣⟩) = ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑢, 𝑣⟩))
8047, 79sylib 121 . . . 4 (𝜑 → ∀𝑢𝑋𝑣𝑌 (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑢, 𝑣⟩) = ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑢, 𝑣⟩))
81 fveq2 5496 . . . . . 6 (𝑤 = ⟨𝑢, 𝑣⟩ → (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘𝑤) = (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑢, 𝑣⟩))
82 fveq2 5496 . . . . . 6 (𝑤 = ⟨𝑢, 𝑣⟩ → ((𝑥𝑋, 𝑦𝑌𝐶)‘𝑤) = ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑢, 𝑣⟩))
8381, 82eqeq12d 2185 . . . . 5 (𝑤 = ⟨𝑢, 𝑣⟩ → ((((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘𝑤) = ((𝑥𝑋, 𝑦𝑌𝐶)‘𝑤) ↔ (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑢, 𝑣⟩) = ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑢, 𝑣⟩)))
8483ralxp 4754 . . . 4 (∀𝑤 ∈ (𝑋 × 𝑌)(((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘𝑤) = ((𝑥𝑋, 𝑦𝑌𝐶)‘𝑤) ↔ ∀𝑢𝑋𝑣𝑌 (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑢, 𝑣⟩) = ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑢, 𝑣⟩))
8580, 84sylibr 133 . . 3 (𝜑 → ∀𝑤 ∈ (𝑋 × 𝑌)(((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘𝑤) = ((𝑥𝑋, 𝑦𝑌𝐶)‘𝑤))
86 fco 5363 . . . . . 6 (((𝑧𝑍𝐵):𝑍 𝑀 ∧ (𝑥𝑋, 𝑦𝑌𝐴):(𝑋 × 𝑌)⟶𝑍) → ((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴)):(𝑋 × 𝑌)⟶ 𝑀)
8731, 11, 86syl2anc 409 . . . . 5 (𝜑 → ((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴)):(𝑋 × 𝑌)⟶ 𝑀)
8887ffnd 5348 . . . 4 (𝜑 → ((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴)) Fn (𝑋 × 𝑌))
8935ralrimivva 2552 . . . . . 6 (𝜑 → ∀𝑥𝑋𝑦𝑌 𝐶 𝑀)
9042fmpo 6180 . . . . . 6 (∀𝑥𝑋𝑦𝑌 𝐶 𝑀 ↔ (𝑥𝑋, 𝑦𝑌𝐶):(𝑋 × 𝑌)⟶ 𝑀)
9189, 90sylib 121 . . . . 5 (𝜑 → (𝑥𝑋, 𝑦𝑌𝐶):(𝑋 × 𝑌)⟶ 𝑀)
9291ffnd 5348 . . . 4 (𝜑 → (𝑥𝑋, 𝑦𝑌𝐶) Fn (𝑋 × 𝑌))
93 eqfnfv 5593 . . . 4 ((((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴)) Fn (𝑋 × 𝑌) ∧ (𝑥𝑋, 𝑦𝑌𝐶) Fn (𝑋 × 𝑌)) → (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴)) = (𝑥𝑋, 𝑦𝑌𝐶) ↔ ∀𝑤 ∈ (𝑋 × 𝑌)(((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘𝑤) = ((𝑥𝑋, 𝑦𝑌𝐶)‘𝑤)))
9488, 92, 93syl2anc 409 . . 3 (𝜑 → (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴)) = (𝑥𝑋, 𝑦𝑌𝐶) ↔ ∀𝑤 ∈ (𝑋 × 𝑌)(((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘𝑤) = ((𝑥𝑋, 𝑦𝑌𝐶)‘𝑤)))
9585, 94mpbird 166 . 2 (𝜑 → ((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴)) = (𝑥𝑋, 𝑦𝑌𝐶))
96 cnco 13015 . . 3 (((𝑥𝑋, 𝑦𝑌𝐴) ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ (𝑧𝑍𝐵) ∈ (𝐿 Cn 𝑀)) → ((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴)) ∈ ((𝐽 ×t 𝐾) Cn 𝑀))
979, 25, 96syl2anc 409 . 2 (𝜑 → ((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴)) ∈ ((𝐽 ×t 𝐾) Cn 𝑀))
9895, 97eqeltrrd 2248 1 (𝜑 → (𝑥𝑋, 𝑦𝑌𝐶) ∈ ((𝐽 ×t 𝐾) Cn 𝑀))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  wb 104   = wceq 1348  wcel 2141  wral 2448  cop 3586   cuni 3796  cmpt 4050   × cxp 4609  ccom 4615   Fn wfn 5193  wf 5194  cfv 5198  (class class class)co 5853  cmpo 5855  Topctop 12789  TopOnctopon 12802   Cn ccn 12979   ×t ctx 13046
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 609  ax-in2 610  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-13 2143  ax-14 2144  ax-ext 2152  ax-coll 4104  ax-sep 4107  ax-pow 4160  ax-pr 4194  ax-un 4418  ax-setind 4521
This theorem depends on definitions:  df-bi 116  df-3an 975  df-tru 1351  df-fal 1354  df-nf 1454  df-sb 1756  df-eu 2022  df-mo 2023  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-ne 2341  df-ral 2453  df-rex 2454  df-reu 2455  df-rab 2457  df-v 2732  df-sbc 2956  df-csb 3050  df-dif 3123  df-un 3125  df-in 3127  df-ss 3134  df-pw 3568  df-sn 3589  df-pr 3590  df-op 3592  df-uni 3797  df-iun 3875  df-br 3990  df-opab 4051  df-mpt 4052  df-id 4278  df-xp 4617  df-rel 4618  df-cnv 4619  df-co 4620  df-dm 4621  df-rn 4622  df-res 4623  df-ima 4624  df-iota 5160  df-fun 5200  df-fn 5201  df-f 5202  df-f1 5203  df-fo 5204  df-f1o 5205  df-fv 5206  df-ov 5856  df-oprab 5857  df-mpo 5858  df-1st 6119  df-2nd 6120  df-map 6628  df-topgen 12600  df-top 12790  df-topon 12803  df-bases 12835  df-cn 12982  df-tx 13047
This theorem is referenced by:  cnmpt21f  13086  divcnap  13349
  Copyright terms: Public domain W3C validator