Step | Hyp | Ref
| Expression |
1 | | cnextval 21675 |
. . 3
⊢ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top) → (𝐽CnExt𝐾) = (𝑓 ∈ (∪ 𝐾 ↑pm
∪ 𝐽) ↦ ∪ 𝑥 ∈ ((cls‘𝐽)‘dom 𝑓)({𝑥} × ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t dom 𝑓))‘𝑓)))) |
2 | 1 | adantr 480 |
. 2
⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐹:𝐴⟶𝐵 ∧ 𝐴 ⊆ 𝑋)) → (𝐽CnExt𝐾) = (𝑓 ∈ (∪ 𝐾 ↑pm
∪ 𝐽) ↦ ∪ 𝑥 ∈ ((cls‘𝐽)‘dom 𝑓)({𝑥} × ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t dom 𝑓))‘𝑓)))) |
3 | | simpr 476 |
. . . . . 6
⊢ ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐹:𝐴⟶𝐵 ∧ 𝐴 ⊆ 𝑋)) ∧ 𝑓 = 𝐹) → 𝑓 = 𝐹) |
4 | 3 | dmeqd 5248 |
. . . . 5
⊢ ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐹:𝐴⟶𝐵 ∧ 𝐴 ⊆ 𝑋)) ∧ 𝑓 = 𝐹) → dom 𝑓 = dom 𝐹) |
5 | | simplrl 796 |
. . . . . 6
⊢ ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐹:𝐴⟶𝐵 ∧ 𝐴 ⊆ 𝑋)) ∧ 𝑓 = 𝐹) → 𝐹:𝐴⟶𝐵) |
6 | | fdm 5964 |
. . . . . 6
⊢ (𝐹:𝐴⟶𝐵 → dom 𝐹 = 𝐴) |
7 | 5, 6 | syl 17 |
. . . . 5
⊢ ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐹:𝐴⟶𝐵 ∧ 𝐴 ⊆ 𝑋)) ∧ 𝑓 = 𝐹) → dom 𝐹 = 𝐴) |
8 | 4, 7 | eqtrd 2644 |
. . . 4
⊢ ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐹:𝐴⟶𝐵 ∧ 𝐴 ⊆ 𝑋)) ∧ 𝑓 = 𝐹) → dom 𝑓 = 𝐴) |
9 | 8 | fveq2d 6107 |
. . 3
⊢ ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐹:𝐴⟶𝐵 ∧ 𝐴 ⊆ 𝑋)) ∧ 𝑓 = 𝐹) → ((cls‘𝐽)‘dom 𝑓) = ((cls‘𝐽)‘𝐴)) |
10 | 8 | oveq2d 6565 |
. . . . . 6
⊢ ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐹:𝐴⟶𝐵 ∧ 𝐴 ⊆ 𝑋)) ∧ 𝑓 = 𝐹) → (((nei‘𝐽)‘{𝑥}) ↾t dom 𝑓) = (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)) |
11 | 10 | oveq2d 6565 |
. . . . 5
⊢ ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐹:𝐴⟶𝐵 ∧ 𝐴 ⊆ 𝑋)) ∧ 𝑓 = 𝐹) → (𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t dom 𝑓)) = (𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))) |
12 | 11, 3 | fveq12d 6109 |
. . . 4
⊢ ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐹:𝐴⟶𝐵 ∧ 𝐴 ⊆ 𝑋)) ∧ 𝑓 = 𝐹) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t dom 𝑓))‘𝑓) = ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹)) |
13 | 12 | xpeq2d 5063 |
. . 3
⊢ ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐹:𝐴⟶𝐵 ∧ 𝐴 ⊆ 𝑋)) ∧ 𝑓 = 𝐹) → ({𝑥} × ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t dom 𝑓))‘𝑓)) = ({𝑥} × ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹))) |
14 | 9, 13 | iuneq12d 4482 |
. 2
⊢ ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐹:𝐴⟶𝐵 ∧ 𝐴 ⊆ 𝑋)) ∧ 𝑓 = 𝐹) → ∪
𝑥 ∈ ((cls‘𝐽)‘dom 𝑓)({𝑥} × ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t dom 𝑓))‘𝑓)) = ∪
𝑥 ∈ ((cls‘𝐽)‘𝐴)({𝑥} × ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹))) |
15 | | uniexg 6853 |
. . . 4
⊢ (𝐾 ∈ Top → ∪ 𝐾
∈ V) |
16 | 15 | ad2antlr 759 |
. . 3
⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐹:𝐴⟶𝐵 ∧ 𝐴 ⊆ 𝑋)) → ∪ 𝐾 ∈ V) |
17 | | uniexg 6853 |
. . . 4
⊢ (𝐽 ∈ Top → ∪ 𝐽
∈ V) |
18 | 17 | ad2antrr 758 |
. . 3
⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐹:𝐴⟶𝐵 ∧ 𝐴 ⊆ 𝑋)) → ∪ 𝐽 ∈ V) |
19 | | eqid 2610 |
. . . . . 6
⊢ 𝐴 = 𝐴 |
20 | | cnextfval.2 |
. . . . . 6
⊢ 𝐵 = ∪
𝐾 |
21 | 19, 20 | feq23i 5952 |
. . . . 5
⊢ (𝐹:𝐴⟶𝐵 ↔ 𝐹:𝐴⟶∪ 𝐾) |
22 | 21 | biimpi 205 |
. . . 4
⊢ (𝐹:𝐴⟶𝐵 → 𝐹:𝐴⟶∪ 𝐾) |
23 | 22 | ad2antrl 760 |
. . 3
⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐹:𝐴⟶𝐵 ∧ 𝐴 ⊆ 𝑋)) → 𝐹:𝐴⟶∪ 𝐾) |
24 | | cnextfval.1 |
. . . . . 6
⊢ 𝑋 = ∪
𝐽 |
25 | 24 | sseq2i 3593 |
. . . . 5
⊢ (𝐴 ⊆ 𝑋 ↔ 𝐴 ⊆ ∪ 𝐽) |
26 | 25 | biimpi 205 |
. . . 4
⊢ (𝐴 ⊆ 𝑋 → 𝐴 ⊆ ∪ 𝐽) |
27 | 26 | ad2antll 761 |
. . 3
⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐹:𝐴⟶𝐵 ∧ 𝐴 ⊆ 𝑋)) → 𝐴 ⊆ ∪ 𝐽) |
28 | | elpm2r 7761 |
. . 3
⊢ (((∪ 𝐾
∈ V ∧ ∪ 𝐽 ∈ V) ∧ (𝐹:𝐴⟶∪ 𝐾 ∧ 𝐴 ⊆ ∪ 𝐽)) → 𝐹 ∈ (∪ 𝐾 ↑pm
∪ 𝐽)) |
29 | 16, 18, 23, 27, 28 | syl22anc 1319 |
. 2
⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐹:𝐴⟶𝐵 ∧ 𝐴 ⊆ 𝑋)) → 𝐹 ∈ (∪ 𝐾 ↑pm
∪ 𝐽)) |
30 | | fvex 6113 |
. . . 4
⊢
((cls‘𝐽)‘𝐴) ∈ V |
31 | | snex 4835 |
. . . . 5
⊢ {𝑥} ∈ V |
32 | | fvex 6113 |
. . . . 5
⊢ ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ∈ V |
33 | 31, 32 | xpex 6860 |
. . . 4
⊢ ({𝑥} × ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹)) ∈ V |
34 | 30, 33 | iunex 7039 |
. . 3
⊢ ∪ 𝑥 ∈ ((cls‘𝐽)‘𝐴)({𝑥} × ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹)) ∈ V |
35 | 34 | a1i 11 |
. 2
⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐹:𝐴⟶𝐵 ∧ 𝐴 ⊆ 𝑋)) → ∪ 𝑥 ∈ ((cls‘𝐽)‘𝐴)({𝑥} × ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹)) ∈ V) |
36 | 2, 14, 29, 35 | fvmptd 6197 |
1
⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐹:𝐴⟶𝐵 ∧ 𝐴 ⊆ 𝑋)) → ((𝐽CnExt𝐾)‘𝐹) = ∪
𝑥 ∈ ((cls‘𝐽)‘𝐴)({𝑥} × ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹))) |