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 30543 |
. . . . . . 7
⊢ (𝜑 → 𝐾:((0[,]1) × (0[,]1))⟶𝐵) |
9 | 8 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑋 ∈ (0[,]1)) → 𝐾:((0[,]1) × (0[,]1))⟶𝐵) |
10 | | ffn 5958 |
. . . . . 6
⊢ (𝐾:((0[,]1) ×
(0[,]1))⟶𝐵 →
𝐾 Fn ((0[,]1) ×
(0[,]1))) |
11 | 9, 10 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑋 ∈ (0[,]1)) → 𝐾 Fn ((0[,]1) ×
(0[,]1))) |
12 | | fnov 6666 |
. . . . 5
⊢ (𝐾 Fn ((0[,]1) × (0[,]1))
↔ 𝐾 = (𝑢 ∈ (0[,]1), 𝑣 ∈ (0[,]1) ↦ (𝑢𝐾𝑣))) |
13 | 11, 12 | sylib 207 |
. . . 4
⊢ ((𝜑 ∧ 𝑋 ∈ (0[,]1)) → 𝐾 = (𝑢 ∈ (0[,]1), 𝑣 ∈ (0[,]1) ↦ (𝑢𝐾𝑣))) |
14 | 13 | reseq1d 5316 |
. . 3
⊢ ((𝜑 ∧ 𝑋 ∈ (0[,]1)) → (𝐾 ↾ ({𝑋} × (0[,]1))) = ((𝑢 ∈ (0[,]1), 𝑣 ∈ (0[,]1) ↦ (𝑢𝐾𝑣)) ↾ ({𝑋} × (0[,]1)))) |
15 | | simpr 476 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑋 ∈ (0[,]1)) → 𝑋 ∈ (0[,]1)) |
16 | 15 | snssd 4281 |
. . . . 5
⊢ ((𝜑 ∧ 𝑋 ∈ (0[,]1)) → {𝑋} ⊆ (0[,]1)) |
17 | | ssid 3587 |
. . . . 5
⊢ (0[,]1)
⊆ (0[,]1) |
18 | | resmpt2 6656 |
. . . . 5
⊢ (({𝑋} ⊆ (0[,]1) ∧ (0[,]1)
⊆ (0[,]1)) → ((𝑢
∈ (0[,]1), 𝑣 ∈
(0[,]1) ↦ (𝑢𝐾𝑣)) ↾ ({𝑋} × (0[,]1))) = (𝑢 ∈ {𝑋}, 𝑣 ∈ (0[,]1) ↦ (𝑢𝐾𝑣))) |
19 | 16, 17, 18 | sylancl 693 |
. . . 4
⊢ ((𝜑 ∧ 𝑋 ∈ (0[,]1)) → ((𝑢 ∈ (0[,]1), 𝑣 ∈ (0[,]1) ↦ (𝑢𝐾𝑣)) ↾ ({𝑋} × (0[,]1))) = (𝑢 ∈ {𝑋}, 𝑣 ∈ (0[,]1) ↦ (𝑢𝐾𝑣))) |
20 | | elsni 4142 |
. . . . . . . 8
⊢ (𝑢 ∈ {𝑋} → 𝑢 = 𝑋) |
21 | 20 | 3ad2ant2 1076 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑋 ∈ (0[,]1)) ∧ 𝑢 ∈ {𝑋} ∧ 𝑣 ∈ (0[,]1)) → 𝑢 = 𝑋) |
22 | 21 | oveq1d 6564 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑋 ∈ (0[,]1)) ∧ 𝑢 ∈ {𝑋} ∧ 𝑣 ∈ (0[,]1)) → (𝑢𝐾𝑣) = (𝑋𝐾𝑣)) |
23 | | simp1r 1079 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑋 ∈ (0[,]1)) ∧ 𝑢 ∈ {𝑋} ∧ 𝑣 ∈ (0[,]1)) → 𝑋 ∈ (0[,]1)) |
24 | | simp3 1056 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑋 ∈ (0[,]1)) ∧ 𝑢 ∈ {𝑋} ∧ 𝑣 ∈ (0[,]1)) → 𝑣 ∈ (0[,]1)) |
25 | 1, 2, 3, 4, 5, 6, 7 | cvmlift2lem4 30542 |
. . . . . . 7
⊢ ((𝑋 ∈ (0[,]1) ∧ 𝑣 ∈ (0[,]1)) → (𝑋𝐾𝑣) = ((℩𝑓 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑓) = (𝑧 ∈ (0[,]1) ↦ (𝑋𝐺𝑧)) ∧ (𝑓‘0) = (𝐻‘𝑋)))‘𝑣)) |
26 | 23, 24, 25 | syl2anc 691 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑋 ∈ (0[,]1)) ∧ 𝑢 ∈ {𝑋} ∧ 𝑣 ∈ (0[,]1)) → (𝑋𝐾𝑣) = ((℩𝑓 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑓) = (𝑧 ∈ (0[,]1) ↦ (𝑋𝐺𝑧)) ∧ (𝑓‘0) = (𝐻‘𝑋)))‘𝑣)) |
27 | 22, 26 | eqtrd 2644 |
. . . . 5
⊢ (((𝜑 ∧ 𝑋 ∈ (0[,]1)) ∧ 𝑢 ∈ {𝑋} ∧ 𝑣 ∈ (0[,]1)) → (𝑢𝐾𝑣) = ((℩𝑓 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑓) = (𝑧 ∈ (0[,]1) ↦ (𝑋𝐺𝑧)) ∧ (𝑓‘0) = (𝐻‘𝑋)))‘𝑣)) |
28 | 27 | mpt2eq3dva 6617 |
. . . 4
⊢ ((𝜑 ∧ 𝑋 ∈ (0[,]1)) → (𝑢 ∈ {𝑋}, 𝑣 ∈ (0[,]1) ↦ (𝑢𝐾𝑣)) = (𝑢 ∈ {𝑋}, 𝑣 ∈ (0[,]1) ↦ ((℩𝑓 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑓) = (𝑧 ∈ (0[,]1) ↦ (𝑋𝐺𝑧)) ∧ (𝑓‘0) = (𝐻‘𝑋)))‘𝑣))) |
29 | 19, 28 | eqtrd 2644 |
. . 3
⊢ ((𝜑 ∧ 𝑋 ∈ (0[,]1)) → ((𝑢 ∈ (0[,]1), 𝑣 ∈ (0[,]1) ↦ (𝑢𝐾𝑣)) ↾ ({𝑋} × (0[,]1))) = (𝑢 ∈ {𝑋}, 𝑣 ∈ (0[,]1) ↦ ((℩𝑓 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑓) = (𝑧 ∈ (0[,]1) ↦ (𝑋𝐺𝑧)) ∧ (𝑓‘0) = (𝐻‘𝑋)))‘𝑣))) |
30 | 14, 29 | eqtrd 2644 |
. 2
⊢ ((𝜑 ∧ 𝑋 ∈ (0[,]1)) → (𝐾 ↾ ({𝑋} × (0[,]1))) = (𝑢 ∈ {𝑋}, 𝑣 ∈ (0[,]1) ↦ ((℩𝑓 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑓) = (𝑧 ∈ (0[,]1) ↦ (𝑋𝐺𝑧)) ∧ (𝑓‘0) = (𝐻‘𝑋)))‘𝑣))) |
31 | | eqid 2610 |
. . . 4
⊢ (II
↾t {𝑋}) =
(II ↾t {𝑋}) |
32 | | iitopon 22490 |
. . . . 5
⊢ II ∈
(TopOn‘(0[,]1)) |
33 | 32 | a1i 11 |
. . . 4
⊢ ((𝜑 ∧ 𝑋 ∈ (0[,]1)) → II ∈
(TopOn‘(0[,]1))) |
34 | | eqid 2610 |
. . . 4
⊢ (II
↾t (0[,]1)) = (II ↾t
(0[,]1)) |
35 | 17 | a1i 11 |
. . . 4
⊢ ((𝜑 ∧ 𝑋 ∈ (0[,]1)) → (0[,]1) ⊆
(0[,]1)) |
36 | 33, 33 | cnmpt2nd 21282 |
. . . . 5
⊢ ((𝜑 ∧ 𝑋 ∈ (0[,]1)) → (𝑢 ∈ (0[,]1), 𝑣 ∈ (0[,]1) ↦ 𝑣) ∈ ((II ×t II) Cn
II)) |
37 | | eqid 2610 |
. . . . . . 7
⊢
(℩𝑓
∈ (II Cn 𝐶)((𝐹 ∘ 𝑓) = (𝑧 ∈ (0[,]1) ↦ (𝑋𝐺𝑧)) ∧ (𝑓‘0) = (𝐻‘𝑋))) = (℩𝑓 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑓) = (𝑧 ∈ (0[,]1) ↦ (𝑋𝐺𝑧)) ∧ (𝑓‘0) = (𝐻‘𝑋))) |
38 | 1, 2, 3, 4, 5, 6, 37 | cvmlift2lem3 30541 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑋 ∈ (0[,]1)) →
((℩𝑓 ∈
(II Cn 𝐶)((𝐹 ∘ 𝑓) = (𝑧 ∈ (0[,]1) ↦ (𝑋𝐺𝑧)) ∧ (𝑓‘0) = (𝐻‘𝑋))) ∈ (II Cn 𝐶) ∧ (𝐹 ∘ (℩𝑓 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑓) = (𝑧 ∈ (0[,]1) ↦ (𝑋𝐺𝑧)) ∧ (𝑓‘0) = (𝐻‘𝑋)))) = (𝑧 ∈ (0[,]1) ↦ (𝑋𝐺𝑧)) ∧ ((℩𝑓 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑓) = (𝑧 ∈ (0[,]1) ↦ (𝑋𝐺𝑧)) ∧ (𝑓‘0) = (𝐻‘𝑋)))‘0) = (𝐻‘𝑋))) |
39 | 38 | simp1d 1066 |
. . . . 5
⊢ ((𝜑 ∧ 𝑋 ∈ (0[,]1)) → (℩𝑓 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑓) = (𝑧 ∈ (0[,]1) ↦ (𝑋𝐺𝑧)) ∧ (𝑓‘0) = (𝐻‘𝑋))) ∈ (II Cn 𝐶)) |
40 | 33, 33, 36, 39 | cnmpt21f 21285 |
. . . 4
⊢ ((𝜑 ∧ 𝑋 ∈ (0[,]1)) → (𝑢 ∈ (0[,]1), 𝑣 ∈ (0[,]1) ↦ ((℩𝑓 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑓) = (𝑧 ∈ (0[,]1) ↦ (𝑋𝐺𝑧)) ∧ (𝑓‘0) = (𝐻‘𝑋)))‘𝑣)) ∈ ((II ×t II) Cn
𝐶)) |
41 | 31, 33, 16, 34, 33, 35, 40 | cnmpt2res 21290 |
. . 3
⊢ ((𝜑 ∧ 𝑋 ∈ (0[,]1)) → (𝑢 ∈ {𝑋}, 𝑣 ∈ (0[,]1) ↦ ((℩𝑓 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑓) = (𝑧 ∈ (0[,]1) ↦ (𝑋𝐺𝑧)) ∧ (𝑓‘0) = (𝐻‘𝑋)))‘𝑣)) ∈ (((II ↾t {𝑋}) ×t (II
↾t (0[,]1))) Cn 𝐶)) |
42 | | iitop 22491 |
. . . . 5
⊢ II ∈
Top |
43 | | snex 4835 |
. . . . 5
⊢ {𝑋} ∈ V |
44 | | ovex 6577 |
. . . . 5
⊢ (0[,]1)
∈ V |
45 | | txrest 21244 |
. . . . 5
⊢ (((II
∈ Top ∧ II ∈ Top) ∧ ({𝑋} ∈ V ∧ (0[,]1) ∈ V)) →
((II ×t II) ↾t ({𝑋} × (0[,]1))) = ((II
↾t {𝑋})
×t (II ↾t (0[,]1)))) |
46 | 42, 42, 43, 44, 45 | mp4an 705 |
. . . 4
⊢ ((II
×t II) ↾t ({𝑋} × (0[,]1))) = ((II
↾t {𝑋})
×t (II ↾t (0[,]1))) |
47 | 46 | oveq1i 6559 |
. . 3
⊢ (((II
×t II) ↾t ({𝑋} × (0[,]1))) Cn 𝐶) = (((II ↾t {𝑋}) ×t (II
↾t (0[,]1))) Cn 𝐶) |
48 | 41, 47 | syl6eleqr 2699 |
. 2
⊢ ((𝜑 ∧ 𝑋 ∈ (0[,]1)) → (𝑢 ∈ {𝑋}, 𝑣 ∈ (0[,]1) ↦ ((℩𝑓 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑓) = (𝑧 ∈ (0[,]1) ↦ (𝑋𝐺𝑧)) ∧ (𝑓‘0) = (𝐻‘𝑋)))‘𝑣)) ∈ (((II ×t II)
↾t ({𝑋}
× (0[,]1))) Cn 𝐶)) |
49 | 30, 48 | eqeltrd 2688 |
1
⊢ ((𝜑 ∧ 𝑋 ∈ (0[,]1)) → (𝐾 ↾ ({𝑋} × (0[,]1))) ∈ (((II
×t II) ↾t ({𝑋} × (0[,]1))) Cn 𝐶)) |