Step | Hyp | Ref
| Expression |
1 | | cvmlift2.b |
. . . . . . . 8
⊢ 𝐵 = ∪
𝐶 |
2 | | cvmlift2.f |
. . . . . . . 8
⊢ (𝜑 → 𝐹 ∈ (𝐶 CovMap 𝐽)) |
3 | | cvmlift2.g |
. . . . . . . 8
⊢ (𝜑 → 𝐺 ∈ ((II ×t II) Cn
𝐽)) |
4 | | cvmlift2.p |
. . . . . . . 8
⊢ (𝜑 → 𝑃 ∈ 𝐵) |
5 | | cvmlift2.i |
. . . . . . . 8
⊢ (𝜑 → (𝐹‘𝑃) = (0𝐺0)) |
6 | | cvmlift2.h |
. . . . . . . 8
⊢ 𝐻 = (℩𝑓 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑓) = (𝑧 ∈ (0[,]1) ↦ (𝑧𝐺0)) ∧ (𝑓‘0) = 𝑃)) |
7 | | cvmlift2.k |
. . . . . . . 8
⊢ 𝐾 = (𝑥 ∈ (0[,]1), 𝑦 ∈ (0[,]1) ↦ ((℩𝑓 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑓) = (𝑧 ∈ (0[,]1) ↦ (𝑥𝐺𝑧)) ∧ (𝑓‘0) = (𝐻‘𝑥)))‘𝑦)) |
8 | 1, 2, 3, 4, 5, 6, 7 | cvmlift2lem5 32982 |
. . . . . . 7
⊢ (𝜑 → 𝐾:((0[,]1) × (0[,]1))⟶𝐵) |
9 | 8 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑋 ∈ (0[,]1)) → 𝐾:((0[,]1) × (0[,]1))⟶𝐵) |
10 | 9 | ffnd 6546 |
. . . . 5
⊢ ((𝜑 ∧ 𝑋 ∈ (0[,]1)) → 𝐾 Fn ((0[,]1) ×
(0[,]1))) |
11 | | fnov 7341 |
. . . . 5
⊢ (𝐾 Fn ((0[,]1) × (0[,]1))
↔ 𝐾 = (𝑢 ∈ (0[,]1), 𝑣 ∈ (0[,]1) ↦ (𝑢𝐾𝑣))) |
12 | 10, 11 | sylib 221 |
. . . 4
⊢ ((𝜑 ∧ 𝑋 ∈ (0[,]1)) → 𝐾 = (𝑢 ∈ (0[,]1), 𝑣 ∈ (0[,]1) ↦ (𝑢𝐾𝑣))) |
13 | 12 | reseq1d 5850 |
. . 3
⊢ ((𝜑 ∧ 𝑋 ∈ (0[,]1)) → (𝐾 ↾ ({𝑋} × (0[,]1))) = ((𝑢 ∈ (0[,]1), 𝑣 ∈ (0[,]1) ↦ (𝑢𝐾𝑣)) ↾ ({𝑋} × (0[,]1)))) |
14 | | simpr 488 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑋 ∈ (0[,]1)) → 𝑋 ∈ (0[,]1)) |
15 | 14 | snssd 4722 |
. . . . 5
⊢ ((𝜑 ∧ 𝑋 ∈ (0[,]1)) → {𝑋} ⊆ (0[,]1)) |
16 | | ssid 3923 |
. . . . 5
⊢ (0[,]1)
⊆ (0[,]1) |
17 | | resmpo 7330 |
. . . . 5
⊢ (({𝑋} ⊆ (0[,]1) ∧ (0[,]1)
⊆ (0[,]1)) → ((𝑢
∈ (0[,]1), 𝑣 ∈
(0[,]1) ↦ (𝑢𝐾𝑣)) ↾ ({𝑋} × (0[,]1))) = (𝑢 ∈ {𝑋}, 𝑣 ∈ (0[,]1) ↦ (𝑢𝐾𝑣))) |
18 | 15, 16, 17 | sylancl 589 |
. . . 4
⊢ ((𝜑 ∧ 𝑋 ∈ (0[,]1)) → ((𝑢 ∈ (0[,]1), 𝑣 ∈ (0[,]1) ↦ (𝑢𝐾𝑣)) ↾ ({𝑋} × (0[,]1))) = (𝑢 ∈ {𝑋}, 𝑣 ∈ (0[,]1) ↦ (𝑢𝐾𝑣))) |
19 | | elsni 4558 |
. . . . . . . 8
⊢ (𝑢 ∈ {𝑋} → 𝑢 = 𝑋) |
20 | 19 | 3ad2ant2 1136 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑋 ∈ (0[,]1)) ∧ 𝑢 ∈ {𝑋} ∧ 𝑣 ∈ (0[,]1)) → 𝑢 = 𝑋) |
21 | 20 | oveq1d 7228 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑋 ∈ (0[,]1)) ∧ 𝑢 ∈ {𝑋} ∧ 𝑣 ∈ (0[,]1)) → (𝑢𝐾𝑣) = (𝑋𝐾𝑣)) |
22 | | simp1r 1200 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑋 ∈ (0[,]1)) ∧ 𝑢 ∈ {𝑋} ∧ 𝑣 ∈ (0[,]1)) → 𝑋 ∈ (0[,]1)) |
23 | | simp3 1140 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑋 ∈ (0[,]1)) ∧ 𝑢 ∈ {𝑋} ∧ 𝑣 ∈ (0[,]1)) → 𝑣 ∈ (0[,]1)) |
24 | 1, 2, 3, 4, 5, 6, 7 | cvmlift2lem4 32981 |
. . . . . . 7
⊢ ((𝑋 ∈ (0[,]1) ∧ 𝑣 ∈ (0[,]1)) → (𝑋𝐾𝑣) = ((℩𝑓 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑓) = (𝑧 ∈ (0[,]1) ↦ (𝑋𝐺𝑧)) ∧ (𝑓‘0) = (𝐻‘𝑋)))‘𝑣)) |
25 | 22, 23, 24 | syl2anc 587 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑋 ∈ (0[,]1)) ∧ 𝑢 ∈ {𝑋} ∧ 𝑣 ∈ (0[,]1)) → (𝑋𝐾𝑣) = ((℩𝑓 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑓) = (𝑧 ∈ (0[,]1) ↦ (𝑋𝐺𝑧)) ∧ (𝑓‘0) = (𝐻‘𝑋)))‘𝑣)) |
26 | 21, 25 | eqtrd 2777 |
. . . . 5
⊢ (((𝜑 ∧ 𝑋 ∈ (0[,]1)) ∧ 𝑢 ∈ {𝑋} ∧ 𝑣 ∈ (0[,]1)) → (𝑢𝐾𝑣) = ((℩𝑓 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑓) = (𝑧 ∈ (0[,]1) ↦ (𝑋𝐺𝑧)) ∧ (𝑓‘0) = (𝐻‘𝑋)))‘𝑣)) |
27 | 26 | mpoeq3dva 7288 |
. . . 4
⊢ ((𝜑 ∧ 𝑋 ∈ (0[,]1)) → (𝑢 ∈ {𝑋}, 𝑣 ∈ (0[,]1) ↦ (𝑢𝐾𝑣)) = (𝑢 ∈ {𝑋}, 𝑣 ∈ (0[,]1) ↦ ((℩𝑓 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑓) = (𝑧 ∈ (0[,]1) ↦ (𝑋𝐺𝑧)) ∧ (𝑓‘0) = (𝐻‘𝑋)))‘𝑣))) |
28 | 18, 27 | eqtrd 2777 |
. . 3
⊢ ((𝜑 ∧ 𝑋 ∈ (0[,]1)) → ((𝑢 ∈ (0[,]1), 𝑣 ∈ (0[,]1) ↦ (𝑢𝐾𝑣)) ↾ ({𝑋} × (0[,]1))) = (𝑢 ∈ {𝑋}, 𝑣 ∈ (0[,]1) ↦ ((℩𝑓 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑓) = (𝑧 ∈ (0[,]1) ↦ (𝑋𝐺𝑧)) ∧ (𝑓‘0) = (𝐻‘𝑋)))‘𝑣))) |
29 | 13, 28 | eqtrd 2777 |
. 2
⊢ ((𝜑 ∧ 𝑋 ∈ (0[,]1)) → (𝐾 ↾ ({𝑋} × (0[,]1))) = (𝑢 ∈ {𝑋}, 𝑣 ∈ (0[,]1) ↦ ((℩𝑓 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑓) = (𝑧 ∈ (0[,]1) ↦ (𝑋𝐺𝑧)) ∧ (𝑓‘0) = (𝐻‘𝑋)))‘𝑣))) |
30 | | eqid 2737 |
. . . 4
⊢ (II
↾t {𝑋}) =
(II ↾t {𝑋}) |
31 | | iitopon 23776 |
. . . . 5
⊢ II ∈
(TopOn‘(0[,]1)) |
32 | 31 | a1i 11 |
. . . 4
⊢ ((𝜑 ∧ 𝑋 ∈ (0[,]1)) → II ∈
(TopOn‘(0[,]1))) |
33 | | eqid 2737 |
. . . 4
⊢ (II
↾t (0[,]1)) = (II ↾t
(0[,]1)) |
34 | 16 | a1i 11 |
. . . 4
⊢ ((𝜑 ∧ 𝑋 ∈ (0[,]1)) → (0[,]1) ⊆
(0[,]1)) |
35 | 32, 32 | cnmpt2nd 22566 |
. . . . 5
⊢ ((𝜑 ∧ 𝑋 ∈ (0[,]1)) → (𝑢 ∈ (0[,]1), 𝑣 ∈ (0[,]1) ↦ 𝑣) ∈ ((II ×t II) Cn
II)) |
36 | | eqid 2737 |
. . . . . . 7
⊢
(℩𝑓
∈ (II Cn 𝐶)((𝐹 ∘ 𝑓) = (𝑧 ∈ (0[,]1) ↦ (𝑋𝐺𝑧)) ∧ (𝑓‘0) = (𝐻‘𝑋))) = (℩𝑓 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑓) = (𝑧 ∈ (0[,]1) ↦ (𝑋𝐺𝑧)) ∧ (𝑓‘0) = (𝐻‘𝑋))) |
37 | 1, 2, 3, 4, 5, 6, 36 | cvmlift2lem3 32980 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑋 ∈ (0[,]1)) →
((℩𝑓 ∈
(II Cn 𝐶)((𝐹 ∘ 𝑓) = (𝑧 ∈ (0[,]1) ↦ (𝑋𝐺𝑧)) ∧ (𝑓‘0) = (𝐻‘𝑋))) ∈ (II Cn 𝐶) ∧ (𝐹 ∘ (℩𝑓 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑓) = (𝑧 ∈ (0[,]1) ↦ (𝑋𝐺𝑧)) ∧ (𝑓‘0) = (𝐻‘𝑋)))) = (𝑧 ∈ (0[,]1) ↦ (𝑋𝐺𝑧)) ∧ ((℩𝑓 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑓) = (𝑧 ∈ (0[,]1) ↦ (𝑋𝐺𝑧)) ∧ (𝑓‘0) = (𝐻‘𝑋)))‘0) = (𝐻‘𝑋))) |
38 | 37 | simp1d 1144 |
. . . . 5
⊢ ((𝜑 ∧ 𝑋 ∈ (0[,]1)) → (℩𝑓 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑓) = (𝑧 ∈ (0[,]1) ↦ (𝑋𝐺𝑧)) ∧ (𝑓‘0) = (𝐻‘𝑋))) ∈ (II Cn 𝐶)) |
39 | 32, 32, 35, 38 | cnmpt21f 22569 |
. . . 4
⊢ ((𝜑 ∧ 𝑋 ∈ (0[,]1)) → (𝑢 ∈ (0[,]1), 𝑣 ∈ (0[,]1) ↦ ((℩𝑓 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑓) = (𝑧 ∈ (0[,]1) ↦ (𝑋𝐺𝑧)) ∧ (𝑓‘0) = (𝐻‘𝑋)))‘𝑣)) ∈ ((II ×t II) Cn
𝐶)) |
40 | 30, 32, 15, 33, 32, 34, 39 | cnmpt2res 22574 |
. . 3
⊢ ((𝜑 ∧ 𝑋 ∈ (0[,]1)) → (𝑢 ∈ {𝑋}, 𝑣 ∈ (0[,]1) ↦ ((℩𝑓 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑓) = (𝑧 ∈ (0[,]1) ↦ (𝑋𝐺𝑧)) ∧ (𝑓‘0) = (𝐻‘𝑋)))‘𝑣)) ∈ (((II ↾t {𝑋}) ×t (II
↾t (0[,]1))) Cn 𝐶)) |
41 | | iitop 23777 |
. . . . 5
⊢ II ∈
Top |
42 | | snex 5324 |
. . . . 5
⊢ {𝑋} ∈ V |
43 | | ovex 7246 |
. . . . 5
⊢ (0[,]1)
∈ V |
44 | | txrest 22528 |
. . . . 5
⊢ (((II
∈ Top ∧ II ∈ Top) ∧ ({𝑋} ∈ V ∧ (0[,]1) ∈ V)) →
((II ×t II) ↾t ({𝑋} × (0[,]1))) = ((II
↾t {𝑋})
×t (II ↾t (0[,]1)))) |
45 | 41, 41, 42, 43, 44 | mp4an 693 |
. . . 4
⊢ ((II
×t II) ↾t ({𝑋} × (0[,]1))) = ((II
↾t {𝑋})
×t (II ↾t (0[,]1))) |
46 | 45 | oveq1i 7223 |
. . 3
⊢ (((II
×t II) ↾t ({𝑋} × (0[,]1))) Cn 𝐶) = (((II ↾t {𝑋}) ×t (II
↾t (0[,]1))) Cn 𝐶) |
47 | 40, 46 | eleqtrrdi 2849 |
. 2
⊢ ((𝜑 ∧ 𝑋 ∈ (0[,]1)) → (𝑢 ∈ {𝑋}, 𝑣 ∈ (0[,]1) ↦ ((℩𝑓 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑓) = (𝑧 ∈ (0[,]1) ↦ (𝑋𝐺𝑧)) ∧ (𝑓‘0) = (𝐻‘𝑋)))‘𝑣)) ∈ (((II ×t II)
↾t ({𝑋}
× (0[,]1))) Cn 𝐶)) |
48 | 29, 47 | eqeltrd 2838 |
1
⊢ ((𝜑 ∧ 𝑋 ∈ (0[,]1)) → (𝐾 ↾ ({𝑋} × (0[,]1))) ∈ (((II
×t II) ↾t ({𝑋} × (0[,]1))) Cn 𝐶)) |