Proof of Theorem xkocnv
Step | Hyp | Ref
| Expression |
1 | | simprr 792 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) → 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)))) |
2 | | xkohmeo.x |
. . . . . . . . 9
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) |
3 | 2 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) → 𝐽 ∈ (TopOn‘𝑋)) |
4 | | xkohmeo.y |
. . . . . . . . 9
⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌)) |
5 | 4 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) → 𝐾 ∈ (TopOn‘𝑌)) |
6 | | txtopon 21204 |
. . . . . . . . . . . . . 14
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝐽 ×t 𝐾) ∈ (TopOn‘(𝑋 × 𝑌))) |
7 | 2, 4, 6 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐽 ×t 𝐾) ∈ (TopOn‘(𝑋 × 𝑌))) |
8 | 7 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) → (𝐽 ×t 𝐾) ∈ (TopOn‘(𝑋 × 𝑌))) |
9 | | xkohmeo.l |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐿 ∈ Top) |
10 | | eqid 2610 |
. . . . . . . . . . . . . . 15
⊢ ∪ 𝐿 =
∪ 𝐿 |
11 | 10 | toptopon 20548 |
. . . . . . . . . . . . . 14
⊢ (𝐿 ∈ Top ↔ 𝐿 ∈ (TopOn‘∪ 𝐿)) |
12 | 9, 11 | sylib 207 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐿 ∈ (TopOn‘∪ 𝐿)) |
13 | 12 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) → 𝐿 ∈ (TopOn‘∪ 𝐿)) |
14 | | simpr 476 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) → 𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) |
15 | | cnf2 20863 |
. . . . . . . . . . . 12
⊢ (((𝐽 ×t 𝐾) ∈ (TopOn‘(𝑋 × 𝑌)) ∧ 𝐿 ∈ (TopOn‘∪ 𝐿)
∧ 𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) → 𝑓:(𝑋 × 𝑌)⟶∪ 𝐿) |
16 | 8, 13, 14, 15 | syl3anc 1318 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) → 𝑓:(𝑋 × 𝑌)⟶∪ 𝐿) |
17 | | ffn 5958 |
. . . . . . . . . . 11
⊢ (𝑓:(𝑋 × 𝑌)⟶∪ 𝐿 → 𝑓 Fn (𝑋 × 𝑌)) |
18 | 16, 17 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) → 𝑓 Fn (𝑋 × 𝑌)) |
19 | | fnov 6666 |
. . . . . . . . . 10
⊢ (𝑓 Fn (𝑋 × 𝑌) ↔ 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))) |
20 | 18, 19 | sylib 207 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) → 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))) |
21 | 20, 14 | eqeltrrd 2689 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)) ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) |
22 | 3, 5, 21 | cnmpt2k 21301 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) → (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))) ∈ (𝐽 Cn (𝐿 ^ko 𝐾))) |
23 | 22 | adantrr 749 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) → (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))) ∈ (𝐽 Cn (𝐿 ^ko 𝐾))) |
24 | 1, 23 | eqeltrd 2688 |
. . . . 5
⊢ ((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) → 𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾))) |
25 | 20 | adantrr 749 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) → 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))) |
26 | | eqid 2610 |
. . . . . . 7
⊢ 𝑋 = 𝑋 |
27 | | nfv 1830 |
. . . . . . . . 9
⊢
Ⅎ𝑥𝜑 |
28 | | nfv 1830 |
. . . . . . . . . 10
⊢
Ⅎ𝑥 𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) |
29 | | nfmpt1 4675 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥(𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))) |
30 | 29 | nfeq2 2766 |
. . . . . . . . . 10
⊢
Ⅎ𝑥 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))) |
31 | 28, 30 | nfan 1816 |
. . . . . . . . 9
⊢
Ⅎ𝑥(𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)))) |
32 | 27, 31 | nfan 1816 |
. . . . . . . 8
⊢
Ⅎ𝑥(𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) |
33 | | nfv 1830 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑦𝜑 |
34 | | nfv 1830 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑦 𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) |
35 | | nfcv 2751 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑦𝑋 |
36 | | nfmpt1 4675 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑦(𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)) |
37 | 35, 36 | nfmpt 4674 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑦(𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))) |
38 | 37 | nfeq2 2766 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑦 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))) |
39 | 34, 38 | nfan 1816 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑦(𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)))) |
40 | 33, 39 | nfan 1816 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑦(𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) |
41 | | nfv 1830 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑦 𝑥 ∈ 𝑋 |
42 | 40, 41 | nfan 1816 |
. . . . . . . . . . 11
⊢
Ⅎ𝑦((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) ∧ 𝑥 ∈ 𝑋) |
43 | | simplrr 797 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)))) |
44 | 43 | fveq1d 6105 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → (𝑔‘𝑥) = ((𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)))‘𝑥)) |
45 | | simprl 790 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → 𝑥 ∈ 𝑋) |
46 | | toponmax 20543 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐾 ∈ (TopOn‘𝑌) → 𝑌 ∈ 𝐾) |
47 | 4, 46 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑌 ∈ 𝐾) |
48 | 47 | ad2antrr 758 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → 𝑌 ∈ 𝐾) |
49 | | mptexg 6389 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑌 ∈ 𝐾 → (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)) ∈ V) |
50 | 48, 49 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)) ∈ V) |
51 | | eqid 2610 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))) = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))) |
52 | 51 | fvmpt2 6200 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ 𝑋 ∧ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)) ∈ V) → ((𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)))‘𝑥) = (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))) |
53 | 45, 50, 52 | syl2anc 691 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → ((𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)))‘𝑥) = (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))) |
54 | 44, 53 | eqtrd 2644 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → (𝑔‘𝑥) = (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))) |
55 | 54 | fveq1d 6105 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → ((𝑔‘𝑥)‘𝑦) = ((𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))‘𝑦)) |
56 | | simprr 792 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → 𝑦 ∈ 𝑌) |
57 | | ovex 6577 |
. . . . . . . . . . . . . 14
⊢ (𝑥𝑓𝑦) ∈ V |
58 | | eqid 2610 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)) = (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)) |
59 | 58 | fvmpt2 6200 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ 𝑌 ∧ (𝑥𝑓𝑦) ∈ V) → ((𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))‘𝑦) = (𝑥𝑓𝑦)) |
60 | 56, 57, 59 | sylancl 693 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → ((𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))‘𝑦) = (𝑥𝑓𝑦)) |
61 | 55, 60 | eqtrd 2644 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → ((𝑔‘𝑥)‘𝑦) = (𝑥𝑓𝑦)) |
62 | 61 | expr 641 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) ∧ 𝑥 ∈ 𝑋) → (𝑦 ∈ 𝑌 → ((𝑔‘𝑥)‘𝑦) = (𝑥𝑓𝑦))) |
63 | 42, 62 | ralrimi 2940 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) ∧ 𝑥 ∈ 𝑋) → ∀𝑦 ∈ 𝑌 ((𝑔‘𝑥)‘𝑦) = (𝑥𝑓𝑦)) |
64 | | eqid 2610 |
. . . . . . . . . 10
⊢ 𝑌 = 𝑌 |
65 | 63, 64 | jctil 558 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) ∧ 𝑥 ∈ 𝑋) → (𝑌 = 𝑌 ∧ ∀𝑦 ∈ 𝑌 ((𝑔‘𝑥)‘𝑦) = (𝑥𝑓𝑦))) |
66 | 65 | ex 449 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) → (𝑥 ∈ 𝑋 → (𝑌 = 𝑌 ∧ ∀𝑦 ∈ 𝑌 ((𝑔‘𝑥)‘𝑦) = (𝑥𝑓𝑦)))) |
67 | 32, 66 | ralrimi 2940 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) → ∀𝑥 ∈ 𝑋 (𝑌 = 𝑌 ∧ ∀𝑦 ∈ 𝑌 ((𝑔‘𝑥)‘𝑦) = (𝑥𝑓𝑦))) |
68 | | mpt2eq123 6612 |
. . . . . . 7
⊢ ((𝑋 = 𝑋 ∧ ∀𝑥 ∈ 𝑋 (𝑌 = 𝑌 ∧ ∀𝑦 ∈ 𝑌 ((𝑔‘𝑥)‘𝑦) = (𝑥𝑓𝑦))) → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))) |
69 | 26, 67, 68 | sylancr 694 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))) |
70 | 25, 69 | eqtr4d 2647 |
. . . . 5
⊢ ((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) → 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦))) |
71 | 24, 70 | jca 553 |
. . . 4
⊢ ((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) → (𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾)) ∧ 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))) |
72 | | simprr 792 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾)) ∧ 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))) → 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦))) |
73 | 2 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾))) → 𝐽 ∈ (TopOn‘𝑋)) |
74 | 4 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾))) → 𝐾 ∈ (TopOn‘𝑌)) |
75 | 12 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾))) → 𝐿 ∈ (TopOn‘∪ 𝐿)) |
76 | | xkohmeo.k |
. . . . . . . . 9
⊢ (𝜑 → 𝐾 ∈ 𝑛-Locally
Comp) |
77 | 76 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾))) → 𝐾 ∈ 𝑛-Locally
Comp) |
78 | | nllytop 21086 |
. . . . . . . . . . . . . 14
⊢ (𝐾 ∈ 𝑛-Locally Comp
→ 𝐾 ∈
Top) |
79 | 77, 78 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾))) → 𝐾 ∈ Top) |
80 | 9 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾))) → 𝐿 ∈ Top) |
81 | | eqid 2610 |
. . . . . . . . . . . . . 14
⊢ (𝐿 ^ko 𝐾) = (𝐿 ^ko 𝐾) |
82 | 81 | xkotopon 21213 |
. . . . . . . . . . . . 13
⊢ ((𝐾 ∈ Top ∧ 𝐿 ∈ Top) → (𝐿 ^ko 𝐾) ∈ (TopOn‘(𝐾 Cn 𝐿))) |
83 | 79, 80, 82 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾))) → (𝐿 ^ko 𝐾) ∈ (TopOn‘(𝐾 Cn 𝐿))) |
84 | | simpr 476 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾))) → 𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾))) |
85 | | cnf2 20863 |
. . . . . . . . . . . 12
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ (𝐿 ^ko 𝐾) ∈ (TopOn‘(𝐾 Cn 𝐿)) ∧ 𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾))) → 𝑔:𝑋⟶(𝐾 Cn 𝐿)) |
86 | 73, 83, 84, 85 | syl3anc 1318 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾))) → 𝑔:𝑋⟶(𝐾 Cn 𝐿)) |
87 | 86 | feqmptd 6159 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾))) → 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑔‘𝑥))) |
88 | 4 | ad2antrr 758 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾))) ∧ 𝑥 ∈ 𝑋) → 𝐾 ∈ (TopOn‘𝑌)) |
89 | 12 | ad2antrr 758 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾))) ∧ 𝑥 ∈ 𝑋) → 𝐿 ∈ (TopOn‘∪ 𝐿)) |
90 | 86 | ffvelrnda 6267 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾))) ∧ 𝑥 ∈ 𝑋) → (𝑔‘𝑥) ∈ (𝐾 Cn 𝐿)) |
91 | | cnf2 20863 |
. . . . . . . . . . . . 13
⊢ ((𝐾 ∈ (TopOn‘𝑌) ∧ 𝐿 ∈ (TopOn‘∪ 𝐿)
∧ (𝑔‘𝑥) ∈ (𝐾 Cn 𝐿)) → (𝑔‘𝑥):𝑌⟶∪ 𝐿) |
92 | 88, 89, 90, 91 | syl3anc 1318 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾))) ∧ 𝑥 ∈ 𝑋) → (𝑔‘𝑥):𝑌⟶∪ 𝐿) |
93 | 92 | feqmptd 6159 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾))) ∧ 𝑥 ∈ 𝑋) → (𝑔‘𝑥) = (𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦))) |
94 | 93 | mpteq2dva 4672 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾))) → (𝑥 ∈ 𝑋 ↦ (𝑔‘𝑥)) = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))) |
95 | 87, 94 | eqtrd 2644 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾))) → 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))) |
96 | 95, 84 | eqeltrrd 2689 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾))) → (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦))) ∈ (𝐽 Cn (𝐿 ^ko 𝐾))) |
97 | 73, 74, 75, 77, 96 | cnmptk2 21299 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾))) → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)) ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) |
98 | 97 | adantrr 749 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾)) ∧ 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))) → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)) ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) |
99 | 72, 98 | eqeltrd 2688 |
. . . . 5
⊢ ((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾)) ∧ 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))) → 𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) |
100 | 95 | adantrr 749 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾)) ∧ 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))) → 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))) |
101 | | nfv 1830 |
. . . . . . . . 9
⊢
Ⅎ𝑥 𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾)) |
102 | | nfmpt21 6620 |
. . . . . . . . . 10
⊢
Ⅎ𝑥(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)) |
103 | 102 | nfeq2 2766 |
. . . . . . . . 9
⊢
Ⅎ𝑥 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)) |
104 | 101, 103 | nfan 1816 |
. . . . . . . 8
⊢
Ⅎ𝑥(𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾)) ∧ 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦))) |
105 | 27, 104 | nfan 1816 |
. . . . . . 7
⊢
Ⅎ𝑥(𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾)) ∧ 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))) |
106 | | nfv 1830 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑦 𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾)) |
107 | | nfmpt22 6621 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑦(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)) |
108 | 107 | nfeq2 2766 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑦 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)) |
109 | 106, 108 | nfan 1816 |
. . . . . . . . . . 11
⊢
Ⅎ𝑦(𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾)) ∧ 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦))) |
110 | 33, 109 | nfan 1816 |
. . . . . . . . . 10
⊢
Ⅎ𝑦(𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾)) ∧ 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))) |
111 | 110, 41 | nfan 1816 |
. . . . . . . . 9
⊢
Ⅎ𝑦((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾)) ∧ 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))) ∧ 𝑥 ∈ 𝑋) |
112 | 72 | oveqd 6566 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾)) ∧ 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))) → (𝑥𝑓𝑦) = (𝑥(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦))𝑦)) |
113 | | fvex 6113 |
. . . . . . . . . . . 12
⊢ ((𝑔‘𝑥)‘𝑦) ∈ V |
114 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)) |
115 | 114 | ovmpt4g 6681 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ∧ ((𝑔‘𝑥)‘𝑦) ∈ V) → (𝑥(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦))𝑦) = ((𝑔‘𝑥)‘𝑦)) |
116 | 113, 115 | mp3an3 1405 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌) → (𝑥(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦))𝑦) = ((𝑔‘𝑥)‘𝑦)) |
117 | 112, 116 | sylan9eq 2664 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾)) ∧ 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → (𝑥𝑓𝑦) = ((𝑔‘𝑥)‘𝑦)) |
118 | 117 | expr 641 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾)) ∧ 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))) ∧ 𝑥 ∈ 𝑋) → (𝑦 ∈ 𝑌 → (𝑥𝑓𝑦) = ((𝑔‘𝑥)‘𝑦))) |
119 | 111, 118 | ralrimi 2940 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾)) ∧ 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))) ∧ 𝑥 ∈ 𝑋) → ∀𝑦 ∈ 𝑌 (𝑥𝑓𝑦) = ((𝑔‘𝑥)‘𝑦)) |
120 | | mpteq12 4664 |
. . . . . . . 8
⊢ ((𝑌 = 𝑌 ∧ ∀𝑦 ∈ 𝑌 (𝑥𝑓𝑦) = ((𝑔‘𝑥)‘𝑦)) → (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)) = (𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦))) |
121 | 64, 119, 120 | sylancr 694 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾)) ∧ 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))) ∧ 𝑥 ∈ 𝑋) → (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)) = (𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦))) |
122 | 105, 121 | mpteq2da 4671 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾)) ∧ 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))) → (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))) = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))) |
123 | 100, 122 | eqtr4d 2647 |
. . . . 5
⊢ ((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾)) ∧ 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))) → 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)))) |
124 | 99, 123 | jca 553 |
. . . 4
⊢ ((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾)) ∧ 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))) → (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) |
125 | 71, 124 | impbida 873 |
. . 3
⊢ (𝜑 → ((𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)))) ↔ (𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾)) ∧ 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦))))) |
126 | 125 | opabbidv 4648 |
. 2
⊢ (𝜑 → {〈𝑔, 𝑓〉 ∣ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))} = {〈𝑔, 𝑓〉 ∣ (𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾)) ∧ 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))}) |
127 | | xkohmeo.f |
. . . . 5
⊢ 𝐹 = (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ↦ (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)))) |
128 | | df-mpt 4645 |
. . . . 5
⊢ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ↦ (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)))) = {〈𝑓, 𝑔〉 ∣ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))} |
129 | 127, 128 | eqtri 2632 |
. . . 4
⊢ 𝐹 = {〈𝑓, 𝑔〉 ∣ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))} |
130 | 129 | cnveqi 5219 |
. . 3
⊢ ◡𝐹 = ◡{〈𝑓, 𝑔〉 ∣ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))} |
131 | | cnvopab 5452 |
. . 3
⊢ ◡{〈𝑓, 𝑔〉 ∣ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))} = {〈𝑔, 𝑓〉 ∣ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))} |
132 | 130, 131 | eqtri 2632 |
. 2
⊢ ◡𝐹 = {〈𝑔, 𝑓〉 ∣ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))} |
133 | | df-mpt 4645 |
. 2
⊢ (𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾)) ↦ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦))) = {〈𝑔, 𝑓〉 ∣ (𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾)) ∧ 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))} |
134 | 126, 132,
133 | 3eqtr4g 2669 |
1
⊢ (𝜑 → ◡𝐹 = (𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾)) ↦ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))) |