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

Theorem cnmpt21 22950
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 7353 . . . . . . . . . 10 (𝑥(𝑥𝑋, 𝑦𝑌𝐴)𝑦) = ((𝑥𝑋, 𝑦𝑌𝐴)‘⟨𝑥, 𝑦⟩)
2 simprl 770 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝑋𝑦𝑌)) → 𝑥𝑋)
3 simprr 772 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝑋𝑦𝑌)) → 𝑦𝑌)
4 cnmpt21.j . . . . . . . . . . . . . . . 16 (𝜑𝐽 ∈ (TopOn‘𝑋))
5 cnmpt21.k . . . . . . . . . . . . . . . 16 (𝜑𝐾 ∈ (TopOn‘𝑌))
6 txtopon 22870 . . . . . . . . . . . . . . . 16 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝐽 ×t 𝐾) ∈ (TopOn‘(𝑋 × 𝑌)))
74, 5, 6syl2anc 585 . . . . . . . . . . . . . . 15 (𝜑 → (𝐽 ×t 𝐾) ∈ (TopOn‘(𝑋 × 𝑌)))
8 cnmpt21.l . . . . . . . . . . . . . . 15 (𝜑𝐿 ∈ (TopOn‘𝑍))
9 cnmpt21.a . . . . . . . . . . . . . . 15 (𝜑 → (𝑥𝑋, 𝑦𝑌𝐴) ∈ ((𝐽 ×t 𝐾) Cn 𝐿))
10 cnf2 22528 . . . . . . . . . . . . . . 15 (((𝐽 ×t 𝐾) ∈ (TopOn‘(𝑋 × 𝑌)) ∧ 𝐿 ∈ (TopOn‘𝑍) ∧ (𝑥𝑋, 𝑦𝑌𝐴) ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) → (𝑥𝑋, 𝑦𝑌𝐴):(𝑋 × 𝑌)⟶𝑍)
117, 8, 9, 10syl3anc 1372 . . . . . . . . . . . . . 14 (𝜑 → (𝑥𝑋, 𝑦𝑌𝐴):(𝑋 × 𝑌)⟶𝑍)
12 eqid 2738 . . . . . . . . . . . . . . 15 (𝑥𝑋, 𝑦𝑌𝐴) = (𝑥𝑋, 𝑦𝑌𝐴)
1312fmpo 7989 . . . . . . . . . . . . . 14 (∀𝑥𝑋𝑦𝑌 𝐴𝑍 ↔ (𝑥𝑋, 𝑦𝑌𝐴):(𝑋 × 𝑌)⟶𝑍)
1411, 13sylibr 233 . . . . . . . . . . . . 13 (𝜑 → ∀𝑥𝑋𝑦𝑌 𝐴𝑍)
15 rsp2 3259 . . . . . . . . . . . . 13 (∀𝑥𝑋𝑦𝑌 𝐴𝑍 → ((𝑥𝑋𝑦𝑌) → 𝐴𝑍))
1614, 15syl 17 . . . . . . . . . . . 12 (𝜑 → ((𝑥𝑋𝑦𝑌) → 𝐴𝑍))
1716imp 408 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝑋𝑦𝑌)) → 𝐴𝑍)
1812ovmpt4g 7495 . . . . . . . . . . 11 ((𝑥𝑋𝑦𝑌𝐴𝑍) → (𝑥(𝑥𝑋, 𝑦𝑌𝐴)𝑦) = 𝐴)
192, 3, 17, 18syl3anc 1372 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝑋𝑦𝑌)) → (𝑥(𝑥𝑋, 𝑦𝑌𝐴)𝑦) = 𝐴)
201, 19eqtr3id 2792 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝑋𝑦𝑌)) → ((𝑥𝑋, 𝑦𝑌𝐴)‘⟨𝑥, 𝑦⟩) = 𝐴)
2120fveq2d 6842 . . . . . . . 8 ((𝜑 ∧ (𝑥𝑋𝑦𝑌)) → ((𝑧𝑍𝐵)‘((𝑥𝑋, 𝑦𝑌𝐴)‘⟨𝑥, 𝑦⟩)) = ((𝑧𝑍𝐵)‘𝐴))
22 eqid 2738 . . . . . . . . 9 (𝑧𝑍𝐵) = (𝑧𝑍𝐵)
23 cnmpt21.c . . . . . . . . 9 (𝑧 = 𝐴𝐵 = 𝐶)
2423eleq1d 2823 . . . . . . . . . 10 (𝑧 = 𝐴 → (𝐵 𝑀𝐶 𝑀))
25 cnmpt21.b . . . . . . . . . . . . . . 15 (𝜑 → (𝑧𝑍𝐵) ∈ (𝐿 Cn 𝑀))
26 cntop2 22520 . . . . . . . . . . . . . . 15 ((𝑧𝑍𝐵) ∈ (𝐿 Cn 𝑀) → 𝑀 ∈ Top)
2725, 26syl 17 . . . . . . . . . . . . . 14 (𝜑𝑀 ∈ Top)
28 toptopon2 22195 . . . . . . . . . . . . . 14 (𝑀 ∈ Top ↔ 𝑀 ∈ (TopOn‘ 𝑀))
2927, 28sylib 217 . . . . . . . . . . . . 13 (𝜑𝑀 ∈ (TopOn‘ 𝑀))
30 cnf2 22528 . . . . . . . . . . . . 13 ((𝐿 ∈ (TopOn‘𝑍) ∧ 𝑀 ∈ (TopOn‘ 𝑀) ∧ (𝑧𝑍𝐵) ∈ (𝐿 Cn 𝑀)) → (𝑧𝑍𝐵):𝑍 𝑀)
318, 29, 25, 30syl3anc 1372 . . . . . . . . . . . 12 (𝜑 → (𝑧𝑍𝐵):𝑍 𝑀)
3222fmpt 7053 . . . . . . . . . . . 12 (∀𝑧𝑍 𝐵 𝑀 ↔ (𝑧𝑍𝐵):𝑍 𝑀)
3331, 32sylibr 233 . . . . . . . . . . 11 (𝜑 → ∀𝑧𝑍 𝐵 𝑀)
3433adantr 482 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝑋𝑦𝑌)) → ∀𝑧𝑍 𝐵 𝑀)
3524, 34, 17rspcdva 3581 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝑋𝑦𝑌)) → 𝐶 𝑀)
3622, 23, 17, 35fvmptd3 6967 . . . . . . . 8 ((𝜑 ∧ (𝑥𝑋𝑦𝑌)) → ((𝑧𝑍𝐵)‘𝐴) = 𝐶)
3721, 36eqtrd 2778 . . . . . . 7 ((𝜑 ∧ (𝑥𝑋𝑦𝑌)) → ((𝑧𝑍𝐵)‘((𝑥𝑋, 𝑦𝑌𝐴)‘⟨𝑥, 𝑦⟩)) = 𝐶)
38 opelxpi 5668 . . . . . . . 8 ((𝑥𝑋𝑦𝑌) → ⟨𝑥, 𝑦⟩ ∈ (𝑋 × 𝑌))
39 fvco3 6936 . . . . . . . 8 (((𝑥𝑋, 𝑦𝑌𝐴):(𝑋 × 𝑌)⟶𝑍 ∧ ⟨𝑥, 𝑦⟩ ∈ (𝑋 × 𝑌)) → (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑥, 𝑦⟩) = ((𝑧𝑍𝐵)‘((𝑥𝑋, 𝑦𝑌𝐴)‘⟨𝑥, 𝑦⟩)))
4011, 38, 39syl2an 597 . . . . . . 7 ((𝜑 ∧ (𝑥𝑋𝑦𝑌)) → (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑥, 𝑦⟩) = ((𝑧𝑍𝐵)‘((𝑥𝑋, 𝑦𝑌𝐴)‘⟨𝑥, 𝑦⟩)))
41 df-ov 7353 . . . . . . . 8 (𝑥(𝑥𝑋, 𝑦𝑌𝐶)𝑦) = ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑥, 𝑦⟩)
42 eqid 2738 . . . . . . . . . 10 (𝑥𝑋, 𝑦𝑌𝐶) = (𝑥𝑋, 𝑦𝑌𝐶)
4342ovmpt4g 7495 . . . . . . . . 9 ((𝑥𝑋𝑦𝑌𝐶 𝑀) → (𝑥(𝑥𝑋, 𝑦𝑌𝐶)𝑦) = 𝐶)
442, 3, 35, 43syl3anc 1372 . . . . . . . 8 ((𝜑 ∧ (𝑥𝑋𝑦𝑌)) → (𝑥(𝑥𝑋, 𝑦𝑌𝐶)𝑦) = 𝐶)
4541, 44eqtr3id 2792 . . . . . . 7 ((𝜑 ∧ (𝑥𝑋𝑦𝑌)) → ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑥, 𝑦⟩) = 𝐶)
4637, 40, 453eqtr4d 2788 . . . . . 6 ((𝜑 ∧ (𝑥𝑋𝑦𝑌)) → (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑥, 𝑦⟩) = ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑥, 𝑦⟩))
4746ralrimivva 3196 . . . . 5 (𝜑 → ∀𝑥𝑋𝑦𝑌 (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑥, 𝑦⟩) = ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑥, 𝑦⟩))
48 nfv 1918 . . . . . 6 𝑢𝑦𝑌 (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑥, 𝑦⟩) = ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑥, 𝑦⟩)
49 nfcv 2906 . . . . . . 7 𝑥𝑌
50 nfcv 2906 . . . . . . . . . 10 𝑥(𝑧𝑍𝐵)
51 nfmpo1 7430 . . . . . . . . . 10 𝑥(𝑥𝑋, 𝑦𝑌𝐴)
5250, 51nfco 5818 . . . . . . . . 9 𝑥((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))
53 nfcv 2906 . . . . . . . . 9 𝑥𝑢, 𝑣
5452, 53nffv 6848 . . . . . . . 8 𝑥(((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑢, 𝑣⟩)
55 nfmpo1 7430 . . . . . . . . 9 𝑥(𝑥𝑋, 𝑦𝑌𝐶)
5655, 53nffv 6848 . . . . . . . 8 𝑥((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑢, 𝑣⟩)
5754, 56nfeq 2919 . . . . . . 7 𝑥(((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑢, 𝑣⟩) = ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑢, 𝑣⟩)
5849, 57nfralw 3293 . . . . . 6 𝑥𝑣𝑌 (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑢, 𝑣⟩) = ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑢, 𝑣⟩)
59 nfv 1918 . . . . . . . 8 𝑣(((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑥, 𝑦⟩) = ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑥, 𝑦⟩)
60 nfcv 2906 . . . . . . . . . . 11 𝑦(𝑧𝑍𝐵)
61 nfmpo2 7431 . . . . . . . . . . 11 𝑦(𝑥𝑋, 𝑦𝑌𝐴)
6260, 61nfco 5818 . . . . . . . . . 10 𝑦((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))
63 nfcv 2906 . . . . . . . . . 10 𝑦𝑥, 𝑣
6462, 63nffv 6848 . . . . . . . . 9 𝑦(((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑥, 𝑣⟩)
65 nfmpo2 7431 . . . . . . . . . 10 𝑦(𝑥𝑋, 𝑦𝑌𝐶)
6665, 63nffv 6848 . . . . . . . . 9 𝑦((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑥, 𝑣⟩)
6764, 66nfeq 2919 . . . . . . . 8 𝑦(((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑥, 𝑣⟩) = ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑥, 𝑣⟩)
68 opeq2 4830 . . . . . . . . . 10 (𝑦 = 𝑣 → ⟨𝑥, 𝑦⟩ = ⟨𝑥, 𝑣⟩)
6968fveq2d 6842 . . . . . . . . 9 (𝑦 = 𝑣 → (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑥, 𝑦⟩) = (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑥, 𝑣⟩))
7068fveq2d 6842 . . . . . . . . 9 (𝑦 = 𝑣 → ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑥, 𝑦⟩) = ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑥, 𝑣⟩))
7169, 70eqeq12d 2754 . . . . . . . 8 (𝑦 = 𝑣 → ((((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑥, 𝑦⟩) = ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑥, 𝑦⟩) ↔ (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑥, 𝑣⟩) = ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑥, 𝑣⟩)))
7259, 67, 71cbvralw 3288 . . . . . . 7 (∀𝑦𝑌 (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑥, 𝑦⟩) = ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑥, 𝑦⟩) ↔ ∀𝑣𝑌 (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑥, 𝑣⟩) = ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑥, 𝑣⟩))
73 opeq1 4829 . . . . . . . . . 10 (𝑥 = 𝑢 → ⟨𝑥, 𝑣⟩ = ⟨𝑢, 𝑣⟩)
7473fveq2d 6842 . . . . . . . . 9 (𝑥 = 𝑢 → (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑥, 𝑣⟩) = (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑢, 𝑣⟩))
7573fveq2d 6842 . . . . . . . . 9 (𝑥 = 𝑢 → ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑥, 𝑣⟩) = ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑢, 𝑣⟩))
7674, 75eqeq12d 2754 . . . . . . . 8 (𝑥 = 𝑢 → ((((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑥, 𝑣⟩) = ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑥, 𝑣⟩) ↔ (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑢, 𝑣⟩) = ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑢, 𝑣⟩)))
7776ralbidv 3173 . . . . . . 7 (𝑥 = 𝑢 → (∀𝑣𝑌 (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑥, 𝑣⟩) = ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑥, 𝑣⟩) ↔ ∀𝑣𝑌 (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑢, 𝑣⟩) = ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑢, 𝑣⟩)))
7872, 77bitrid 283 . . . . . 6 (𝑥 = 𝑢 → (∀𝑦𝑌 (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑥, 𝑦⟩) = ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑥, 𝑦⟩) ↔ ∀𝑣𝑌 (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑢, 𝑣⟩) = ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑢, 𝑣⟩)))
7948, 58, 78cbvralw 3288 . . . . 5 (∀𝑥𝑋𝑦𝑌 (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑥, 𝑦⟩) = ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑥, 𝑦⟩) ↔ ∀𝑢𝑋𝑣𝑌 (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑢, 𝑣⟩) = ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑢, 𝑣⟩))
8047, 79sylib 217 . . . 4 (𝜑 → ∀𝑢𝑋𝑣𝑌 (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑢, 𝑣⟩) = ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑢, 𝑣⟩))
81 fveq2 6838 . . . . . 6 (𝑤 = ⟨𝑢, 𝑣⟩ → (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘𝑤) = (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑢, 𝑣⟩))
82 fveq2 6838 . . . . . 6 (𝑤 = ⟨𝑢, 𝑣⟩ → ((𝑥𝑋, 𝑦𝑌𝐶)‘𝑤) = ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑢, 𝑣⟩))
8381, 82eqeq12d 2754 . . . . 5 (𝑤 = ⟨𝑢, 𝑣⟩ → ((((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘𝑤) = ((𝑥𝑋, 𝑦𝑌𝐶)‘𝑤) ↔ (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑢, 𝑣⟩) = ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑢, 𝑣⟩)))
8483ralxp 5794 . . . 4 (∀𝑤 ∈ (𝑋 × 𝑌)(((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘𝑤) = ((𝑥𝑋, 𝑦𝑌𝐶)‘𝑤) ↔ ∀𝑢𝑋𝑣𝑌 (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘⟨𝑢, 𝑣⟩) = ((𝑥𝑋, 𝑦𝑌𝐶)‘⟨𝑢, 𝑣⟩))
8580, 84sylibr 233 . . 3 (𝜑 → ∀𝑤 ∈ (𝑋 × 𝑌)(((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘𝑤) = ((𝑥𝑋, 𝑦𝑌𝐶)‘𝑤))
86 fco 6688 . . . . . 6 (((𝑧𝑍𝐵):𝑍 𝑀 ∧ (𝑥𝑋, 𝑦𝑌𝐴):(𝑋 × 𝑌)⟶𝑍) → ((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴)):(𝑋 × 𝑌)⟶ 𝑀)
8731, 11, 86syl2anc 585 . . . . 5 (𝜑 → ((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴)):(𝑋 × 𝑌)⟶ 𝑀)
8887ffnd 6665 . . . 4 (𝜑 → ((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴)) Fn (𝑋 × 𝑌))
8935ralrimivva 3196 . . . . . 6 (𝜑 → ∀𝑥𝑋𝑦𝑌 𝐶 𝑀)
9042fmpo 7989 . . . . . 6 (∀𝑥𝑋𝑦𝑌 𝐶 𝑀 ↔ (𝑥𝑋, 𝑦𝑌𝐶):(𝑋 × 𝑌)⟶ 𝑀)
9189, 90sylib 217 . . . . 5 (𝜑 → (𝑥𝑋, 𝑦𝑌𝐶):(𝑋 × 𝑌)⟶ 𝑀)
9291ffnd 6665 . . . 4 (𝜑 → (𝑥𝑋, 𝑦𝑌𝐶) Fn (𝑋 × 𝑌))
93 eqfnfv 6978 . . . 4 ((((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴)) Fn (𝑋 × 𝑌) ∧ (𝑥𝑋, 𝑦𝑌𝐶) Fn (𝑋 × 𝑌)) → (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴)) = (𝑥𝑋, 𝑦𝑌𝐶) ↔ ∀𝑤 ∈ (𝑋 × 𝑌)(((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘𝑤) = ((𝑥𝑋, 𝑦𝑌𝐶)‘𝑤)))
9488, 92, 93syl2anc 585 . . 3 (𝜑 → (((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴)) = (𝑥𝑋, 𝑦𝑌𝐶) ↔ ∀𝑤 ∈ (𝑋 × 𝑌)(((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴))‘𝑤) = ((𝑥𝑋, 𝑦𝑌𝐶)‘𝑤)))
9585, 94mpbird 257 . 2 (𝜑 → ((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴)) = (𝑥𝑋, 𝑦𝑌𝐶))
96 cnco 22545 . . 3 (((𝑥𝑋, 𝑦𝑌𝐴) ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ (𝑧𝑍𝐵) ∈ (𝐿 Cn 𝑀)) → ((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴)) ∈ ((𝐽 ×t 𝐾) Cn 𝑀))
979, 25, 96syl2anc 585 . 2 (𝜑 → ((𝑧𝑍𝐵) ∘ (𝑥𝑋, 𝑦𝑌𝐴)) ∈ ((𝐽 ×t 𝐾) Cn 𝑀))
9895, 97eqeltrrd 2840 1 (𝜑 → (𝑥𝑋, 𝑦𝑌𝐶) ∈ ((𝐽 ×t 𝐾) Cn 𝑀))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 397   = wceq 1542  wcel 2107  wral 3063  cop 4591   cuni 4864  cmpt 5187   × cxp 5629  ccom 5635   Fn wfn 6487  wf 6488  cfv 6492  (class class class)co 7350  cmpo 7352  Topctop 22170  TopOnctopon 22187   Cn ccn 22503   ×t ctx 22839
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2709  ax-sep 5255  ax-nul 5262  ax-pow 5319  ax-pr 5383  ax-un 7663
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2888  df-ne 2943  df-ral 3064  df-rex 3073  df-rab 3407  df-v 3446  df-sbc 3739  df-csb 3855  df-dif 3912  df-un 3914  df-in 3916  df-ss 3926  df-nul 4282  df-if 4486  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4865  df-iun 4955  df-br 5105  df-opab 5167  df-mpt 5188  df-id 5529  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-iota 6444  df-fun 6494  df-fn 6495  df-f 6496  df-fv 6500  df-ov 7353  df-oprab 7354  df-mpo 7355  df-1st 7912  df-2nd 7913  df-map 8701  df-topgen 17261  df-top 22171  df-topon 22188  df-bases 22224  df-cn 22506  df-tx 22841
This theorem is referenced by:  cnmpt21f  22951  xkofvcn  22963  xkohmeo  23094  qustgplem  23400  prdstmdd  23403  divcn  24159  htpycom  24267  htpycc  24271  reparphti  24288  pcocn  24308  pcohtpylem  24310  pcopt  24313  pcopt2  24314  pcoass  24315  pcorevlem  24317  dipcn  29467
  Copyright terms: Public domain W3C validator