Step | Hyp | Ref
| Expression |
1 | | df-ov 6908 |
. 2
⊢ (𝑅𝑂𝑆) = (𝑂‘〈𝑅, 𝑆〉) |
2 | | flfcnp2.j |
. . . . 5
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) |
3 | | flfcnp2.k |
. . . . 5
⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌)) |
4 | | txtopon 21765 |
. . . . 5
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝐽 ×t 𝐾) ∈ (TopOn‘(𝑋 × 𝑌))) |
5 | 2, 3, 4 | syl2anc 579 |
. . . 4
⊢ (𝜑 → (𝐽 ×t 𝐾) ∈ (TopOn‘(𝑋 × 𝑌))) |
6 | | flfcnp2.l |
. . . 4
⊢ (𝜑 → 𝐿 ∈ (Fil‘𝑍)) |
7 | | flfcnp2.a |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑍) → 𝐴 ∈ 𝑋) |
8 | | flfcnp2.b |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑍) → 𝐵 ∈ 𝑌) |
9 | | opelxpi 5379 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) → 〈𝐴, 𝐵〉 ∈ (𝑋 × 𝑌)) |
10 | 7, 8, 9 | syl2anc 579 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑍) → 〈𝐴, 𝐵〉 ∈ (𝑋 × 𝑌)) |
11 | 10 | fmpttd 6634 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ 𝑍 ↦ 〈𝐴, 𝐵〉):𝑍⟶(𝑋 × 𝑌)) |
12 | | flfcnp2.r |
. . . . . 6
⊢ (𝜑 → 𝑅 ∈ ((𝐽 fLimf 𝐿)‘(𝑥 ∈ 𝑍 ↦ 𝐴))) |
13 | | flfcnp2.s |
. . . . . 6
⊢ (𝜑 → 𝑆 ∈ ((𝐾 fLimf 𝐿)‘(𝑥 ∈ 𝑍 ↦ 𝐵))) |
14 | 7 | fmpttd 6634 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ 𝑍 ↦ 𝐴):𝑍⟶𝑋) |
15 | 8 | fmpttd 6634 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ 𝑍 ↦ 𝐵):𝑍⟶𝑌) |
16 | | nfcv 2969 |
. . . . . . . 8
⊢
Ⅎ𝑦〈((𝑥 ∈ 𝑍 ↦ 𝐴)‘𝑥), ((𝑥 ∈ 𝑍 ↦ 𝐵)‘𝑥)〉 |
17 | | nffvmpt1 6444 |
. . . . . . . . 9
⊢
Ⅎ𝑥((𝑥 ∈ 𝑍 ↦ 𝐴)‘𝑦) |
18 | | nffvmpt1 6444 |
. . . . . . . . 9
⊢
Ⅎ𝑥((𝑥 ∈ 𝑍 ↦ 𝐵)‘𝑦) |
19 | 17, 18 | nfop 4639 |
. . . . . . . 8
⊢
Ⅎ𝑥〈((𝑥 ∈ 𝑍 ↦ 𝐴)‘𝑦), ((𝑥 ∈ 𝑍 ↦ 𝐵)‘𝑦)〉 |
20 | | fveq2 6433 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝑍 ↦ 𝐴)‘𝑥) = ((𝑥 ∈ 𝑍 ↦ 𝐴)‘𝑦)) |
21 | | fveq2 6433 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝑍 ↦ 𝐵)‘𝑥) = ((𝑥 ∈ 𝑍 ↦ 𝐵)‘𝑦)) |
22 | 20, 21 | opeq12d 4631 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → 〈((𝑥 ∈ 𝑍 ↦ 𝐴)‘𝑥), ((𝑥 ∈ 𝑍 ↦ 𝐵)‘𝑥)〉 = 〈((𝑥 ∈ 𝑍 ↦ 𝐴)‘𝑦), ((𝑥 ∈ 𝑍 ↦ 𝐵)‘𝑦)〉) |
23 | 16, 19, 22 | cbvmpt 4972 |
. . . . . . 7
⊢ (𝑥 ∈ 𝑍 ↦ 〈((𝑥 ∈ 𝑍 ↦ 𝐴)‘𝑥), ((𝑥 ∈ 𝑍 ↦ 𝐵)‘𝑥)〉) = (𝑦 ∈ 𝑍 ↦ 〈((𝑥 ∈ 𝑍 ↦ 𝐴)‘𝑦), ((𝑥 ∈ 𝑍 ↦ 𝐵)‘𝑦)〉) |
24 | 2, 3, 6, 14, 15, 23 | txflf 22180 |
. . . . . 6
⊢ (𝜑 → (〈𝑅, 𝑆〉 ∈ (((𝐽 ×t 𝐾) fLimf 𝐿)‘(𝑥 ∈ 𝑍 ↦ 〈((𝑥 ∈ 𝑍 ↦ 𝐴)‘𝑥), ((𝑥 ∈ 𝑍 ↦ 𝐵)‘𝑥)〉)) ↔ (𝑅 ∈ ((𝐽 fLimf 𝐿)‘(𝑥 ∈ 𝑍 ↦ 𝐴)) ∧ 𝑆 ∈ ((𝐾 fLimf 𝐿)‘(𝑥 ∈ 𝑍 ↦ 𝐵))))) |
25 | 12, 13, 24 | mpbir2and 704 |
. . . . 5
⊢ (𝜑 → 〈𝑅, 𝑆〉 ∈ (((𝐽 ×t 𝐾) fLimf 𝐿)‘(𝑥 ∈ 𝑍 ↦ 〈((𝑥 ∈ 𝑍 ↦ 𝐴)‘𝑥), ((𝑥 ∈ 𝑍 ↦ 𝐵)‘𝑥)〉))) |
26 | | simpr 479 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑍) → 𝑥 ∈ 𝑍) |
27 | | eqid 2825 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝑍 ↦ 𝐴) = (𝑥 ∈ 𝑍 ↦ 𝐴) |
28 | 27 | fvmpt2 6538 |
. . . . . . . . 9
⊢ ((𝑥 ∈ 𝑍 ∧ 𝐴 ∈ 𝑋) → ((𝑥 ∈ 𝑍 ↦ 𝐴)‘𝑥) = 𝐴) |
29 | 26, 7, 28 | syl2anc 579 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑍) → ((𝑥 ∈ 𝑍 ↦ 𝐴)‘𝑥) = 𝐴) |
30 | | eqid 2825 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝑍 ↦ 𝐵) = (𝑥 ∈ 𝑍 ↦ 𝐵) |
31 | 30 | fvmpt2 6538 |
. . . . . . . . 9
⊢ ((𝑥 ∈ 𝑍 ∧ 𝐵 ∈ 𝑌) → ((𝑥 ∈ 𝑍 ↦ 𝐵)‘𝑥) = 𝐵) |
32 | 26, 8, 31 | syl2anc 579 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑍) → ((𝑥 ∈ 𝑍 ↦ 𝐵)‘𝑥) = 𝐵) |
33 | 29, 32 | opeq12d 4631 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑍) → 〈((𝑥 ∈ 𝑍 ↦ 𝐴)‘𝑥), ((𝑥 ∈ 𝑍 ↦ 𝐵)‘𝑥)〉 = 〈𝐴, 𝐵〉) |
34 | 33 | mpteq2dva 4967 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ 𝑍 ↦ 〈((𝑥 ∈ 𝑍 ↦ 𝐴)‘𝑥), ((𝑥 ∈ 𝑍 ↦ 𝐵)‘𝑥)〉) = (𝑥 ∈ 𝑍 ↦ 〈𝐴, 𝐵〉)) |
35 | 34 | fveq2d 6437 |
. . . . 5
⊢ (𝜑 → (((𝐽 ×t 𝐾) fLimf 𝐿)‘(𝑥 ∈ 𝑍 ↦ 〈((𝑥 ∈ 𝑍 ↦ 𝐴)‘𝑥), ((𝑥 ∈ 𝑍 ↦ 𝐵)‘𝑥)〉)) = (((𝐽 ×t 𝐾) fLimf 𝐿)‘(𝑥 ∈ 𝑍 ↦ 〈𝐴, 𝐵〉))) |
36 | 25, 35 | eleqtrd 2908 |
. . . 4
⊢ (𝜑 → 〈𝑅, 𝑆〉 ∈ (((𝐽 ×t 𝐾) fLimf 𝐿)‘(𝑥 ∈ 𝑍 ↦ 〈𝐴, 𝐵〉))) |
37 | | flfcnp2.o |
. . . 4
⊢ (𝜑 → 𝑂 ∈ (((𝐽 ×t 𝐾) CnP 𝑁)‘〈𝑅, 𝑆〉)) |
38 | | flfcnp 22178 |
. . . 4
⊢ ((((𝐽 ×t 𝐾) ∈ (TopOn‘(𝑋 × 𝑌)) ∧ 𝐿 ∈ (Fil‘𝑍) ∧ (𝑥 ∈ 𝑍 ↦ 〈𝐴, 𝐵〉):𝑍⟶(𝑋 × 𝑌)) ∧ (〈𝑅, 𝑆〉 ∈ (((𝐽 ×t 𝐾) fLimf 𝐿)‘(𝑥 ∈ 𝑍 ↦ 〈𝐴, 𝐵〉)) ∧ 𝑂 ∈ (((𝐽 ×t 𝐾) CnP 𝑁)‘〈𝑅, 𝑆〉))) → (𝑂‘〈𝑅, 𝑆〉) ∈ ((𝑁 fLimf 𝐿)‘(𝑂 ∘ (𝑥 ∈ 𝑍 ↦ 〈𝐴, 𝐵〉)))) |
39 | 5, 6, 11, 36, 37, 38 | syl32anc 1501 |
. . 3
⊢ (𝜑 → (𝑂‘〈𝑅, 𝑆〉) ∈ ((𝑁 fLimf 𝐿)‘(𝑂 ∘ (𝑥 ∈ 𝑍 ↦ 〈𝐴, 𝐵〉)))) |
40 | | eqidd 2826 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ 𝑍 ↦ 〈𝐴, 𝐵〉) = (𝑥 ∈ 𝑍 ↦ 〈𝐴, 𝐵〉)) |
41 | | cnptop2 21418 |
. . . . . . . . 9
⊢ (𝑂 ∈ (((𝐽 ×t 𝐾) CnP 𝑁)‘〈𝑅, 𝑆〉) → 𝑁 ∈ Top) |
42 | 37, 41 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑁 ∈ Top) |
43 | | eqid 2825 |
. . . . . . . . 9
⊢ ∪ 𝑁 =
∪ 𝑁 |
44 | 43 | toptopon 21092 |
. . . . . . . 8
⊢ (𝑁 ∈ Top ↔ 𝑁 ∈ (TopOn‘∪ 𝑁)) |
45 | 42, 44 | sylib 210 |
. . . . . . 7
⊢ (𝜑 → 𝑁 ∈ (TopOn‘∪ 𝑁)) |
46 | | cnpf2 21425 |
. . . . . . 7
⊢ (((𝐽 ×t 𝐾) ∈ (TopOn‘(𝑋 × 𝑌)) ∧ 𝑁 ∈ (TopOn‘∪ 𝑁)
∧ 𝑂 ∈ (((𝐽 ×t 𝐾) CnP 𝑁)‘〈𝑅, 𝑆〉)) → 𝑂:(𝑋 × 𝑌)⟶∪ 𝑁) |
47 | 5, 45, 37, 46 | syl3anc 1494 |
. . . . . 6
⊢ (𝜑 → 𝑂:(𝑋 × 𝑌)⟶∪ 𝑁) |
48 | 47 | feqmptd 6496 |
. . . . 5
⊢ (𝜑 → 𝑂 = (𝑦 ∈ (𝑋 × 𝑌) ↦ (𝑂‘𝑦))) |
49 | | fveq2 6433 |
. . . . . 6
⊢ (𝑦 = 〈𝐴, 𝐵〉 → (𝑂‘𝑦) = (𝑂‘〈𝐴, 𝐵〉)) |
50 | | df-ov 6908 |
. . . . . 6
⊢ (𝐴𝑂𝐵) = (𝑂‘〈𝐴, 𝐵〉) |
51 | 49, 50 | syl6eqr 2879 |
. . . . 5
⊢ (𝑦 = 〈𝐴, 𝐵〉 → (𝑂‘𝑦) = (𝐴𝑂𝐵)) |
52 | 10, 40, 48, 51 | fmptco 6646 |
. . . 4
⊢ (𝜑 → (𝑂 ∘ (𝑥 ∈ 𝑍 ↦ 〈𝐴, 𝐵〉)) = (𝑥 ∈ 𝑍 ↦ (𝐴𝑂𝐵))) |
53 | 52 | fveq2d 6437 |
. . 3
⊢ (𝜑 → ((𝑁 fLimf 𝐿)‘(𝑂 ∘ (𝑥 ∈ 𝑍 ↦ 〈𝐴, 𝐵〉))) = ((𝑁 fLimf 𝐿)‘(𝑥 ∈ 𝑍 ↦ (𝐴𝑂𝐵)))) |
54 | 39, 53 | eleqtrd 2908 |
. 2
⊢ (𝜑 → (𝑂‘〈𝑅, 𝑆〉) ∈ ((𝑁 fLimf 𝐿)‘(𝑥 ∈ 𝑍 ↦ (𝐴𝑂𝐵)))) |
55 | 1, 54 | syl5eqel 2910 |
1
⊢ (𝜑 → (𝑅𝑂𝑆) ∈ ((𝑁 fLimf 𝐿)‘(𝑥 ∈ 𝑍 ↦ (𝐴𝑂𝐵)))) |