Step | Hyp | Ref
| Expression |
1 | | cvmlift2.b |
. 2
⊢ 𝐵 = ∪
𝐶 |
2 | | iitop 22491 |
. . 3
⊢ II ∈
Top |
3 | | iiuni 22492 |
. . 3
⊢ (0[,]1) =
∪ II |
4 | 2, 2, 3, 3 | txunii 21206 |
. 2
⊢ ((0[,]1)
× (0[,]1)) = ∪ (II ×t
II) |
5 | | cvmlift2lem10.s |
. 2
⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 =
(◡𝐹 “ 𝑘) ∧ ∀𝑐 ∈ 𝑠 (∀𝑑 ∈ (𝑠 ∖ {𝑐})(𝑐 ∩ 𝑑) = ∅ ∧ (𝐹 ↾ 𝑐) ∈ ((𝐶 ↾t 𝑐)Homeo(𝐽 ↾t 𝑘))))}) |
6 | | cvmlift2.f |
. 2
⊢ (𝜑 → 𝐹 ∈ (𝐶 CovMap 𝐽)) |
7 | | cvmlift2.g |
. . 3
⊢ (𝜑 → 𝐺 ∈ ((II ×t II) Cn
𝐽)) |
8 | | cvmlift2.p |
. . 3
⊢ (𝜑 → 𝑃 ∈ 𝐵) |
9 | | cvmlift2.i |
. . 3
⊢ (𝜑 → (𝐹‘𝑃) = (0𝐺0)) |
10 | | cvmlift2.h |
. . 3
⊢ 𝐻 = (℩𝑓 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑓) = (𝑧 ∈ (0[,]1) ↦ (𝑧𝐺0)) ∧ (𝑓‘0) = 𝑃)) |
11 | | cvmlift2.k |
. . 3
⊢ 𝐾 = (𝑥 ∈ (0[,]1), 𝑦 ∈ (0[,]1) ↦ ((℩𝑓 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑓) = (𝑧 ∈ (0[,]1) ↦ (𝑥𝐺𝑧)) ∧ (𝑓‘0) = (𝐻‘𝑥)))‘𝑦)) |
12 | 1, 6, 7, 8, 9, 10,
11 | cvmlift2lem5 30543 |
. 2
⊢ (𝜑 → 𝐾:((0[,]1) × (0[,]1))⟶𝐵) |
13 | 1, 6, 7, 8, 9, 10,
11 | cvmlift2lem7 30545 |
. . 3
⊢ (𝜑 → (𝐹 ∘ 𝐾) = 𝐺) |
14 | 13, 7 | eqeltrd 2688 |
. 2
⊢ (𝜑 → (𝐹 ∘ 𝐾) ∈ ((II ×t II) Cn
𝐽)) |
15 | 2, 2 | txtopi 21203 |
. . 3
⊢ (II
×t II) ∈ Top |
16 | 15 | a1i 11 |
. 2
⊢ (𝜑 → (II ×t
II) ∈ Top) |
17 | | cvmlift2lem9.3 |
. . . . 5
⊢ (𝜑 → 𝑈 ∈ II) |
18 | | elssuni 4403 |
. . . . . 6
⊢ (𝑈 ∈ II → 𝑈 ⊆ ∪ II) |
19 | 18, 3 | syl6sseqr 3615 |
. . . . 5
⊢ (𝑈 ∈ II → 𝑈 ⊆
(0[,]1)) |
20 | 17, 19 | syl 17 |
. . . 4
⊢ (𝜑 → 𝑈 ⊆ (0[,]1)) |
21 | | cvmlift2lem9.7 |
. . . 4
⊢ (𝜑 → 𝑋 ∈ 𝑈) |
22 | 20, 21 | sseldd 3569 |
. . 3
⊢ (𝜑 → 𝑋 ∈ (0[,]1)) |
23 | | cvmlift2lem9.4 |
. . . . 5
⊢ (𝜑 → 𝑉 ∈ II) |
24 | | elssuni 4403 |
. . . . . 6
⊢ (𝑉 ∈ II → 𝑉 ⊆ ∪ II) |
25 | 24, 3 | syl6sseqr 3615 |
. . . . 5
⊢ (𝑉 ∈ II → 𝑉 ⊆
(0[,]1)) |
26 | 23, 25 | syl 17 |
. . . 4
⊢ (𝜑 → 𝑉 ⊆ (0[,]1)) |
27 | | cvmlift2lem9.8 |
. . . 4
⊢ (𝜑 → 𝑌 ∈ 𝑉) |
28 | 26, 27 | sseldd 3569 |
. . 3
⊢ (𝜑 → 𝑌 ∈ (0[,]1)) |
29 | | opelxpi 5072 |
. . 3
⊢ ((𝑋 ∈ (0[,]1) ∧ 𝑌 ∈ (0[,]1)) →
〈𝑋, 𝑌〉 ∈ ((0[,]1) ×
(0[,]1))) |
30 | 22, 28, 29 | syl2anc 691 |
. 2
⊢ (𝜑 → 〈𝑋, 𝑌〉 ∈ ((0[,]1) ×
(0[,]1))) |
31 | | cvmlift2lem9.2 |
. 2
⊢ (𝜑 → 𝑇 ∈ (𝑆‘𝑀)) |
32 | 12, 22, 28 | fovrnd 6704 |
. . . 4
⊢ (𝜑 → (𝑋𝐾𝑌) ∈ 𝐵) |
33 | | fvco3 6185 |
. . . . . . . 8
⊢ ((𝐾:((0[,]1) ×
(0[,]1))⟶𝐵 ∧
〈𝑋, 𝑌〉 ∈ ((0[,]1) × (0[,]1)))
→ ((𝐹 ∘ 𝐾)‘〈𝑋, 𝑌〉) = (𝐹‘(𝐾‘〈𝑋, 𝑌〉))) |
34 | 12, 30, 33 | syl2anc 691 |
. . . . . . 7
⊢ (𝜑 → ((𝐹 ∘ 𝐾)‘〈𝑋, 𝑌〉) = (𝐹‘(𝐾‘〈𝑋, 𝑌〉))) |
35 | 13 | fveq1d 6105 |
. . . . . . 7
⊢ (𝜑 → ((𝐹 ∘ 𝐾)‘〈𝑋, 𝑌〉) = (𝐺‘〈𝑋, 𝑌〉)) |
36 | 34, 35 | eqtr3d 2646 |
. . . . . 6
⊢ (𝜑 → (𝐹‘(𝐾‘〈𝑋, 𝑌〉)) = (𝐺‘〈𝑋, 𝑌〉)) |
37 | | df-ov 6552 |
. . . . . . 7
⊢ (𝑋𝐾𝑌) = (𝐾‘〈𝑋, 𝑌〉) |
38 | 37 | fveq2i 6106 |
. . . . . 6
⊢ (𝐹‘(𝑋𝐾𝑌)) = (𝐹‘(𝐾‘〈𝑋, 𝑌〉)) |
39 | | df-ov 6552 |
. . . . . 6
⊢ (𝑋𝐺𝑌) = (𝐺‘〈𝑋, 𝑌〉) |
40 | 36, 38, 39 | 3eqtr4g 2669 |
. . . . 5
⊢ (𝜑 → (𝐹‘(𝑋𝐾𝑌)) = (𝑋𝐺𝑌)) |
41 | | cvmlift2lem9.1 |
. . . . 5
⊢ (𝜑 → (𝑋𝐺𝑌) ∈ 𝑀) |
42 | 40, 41 | eqeltrd 2688 |
. . . 4
⊢ (𝜑 → (𝐹‘(𝑋𝐾𝑌)) ∈ 𝑀) |
43 | | cvmlift2lem9.w |
. . . . 5
⊢ 𝑊 = (℩𝑏 ∈ 𝑇 (𝑋𝐾𝑌) ∈ 𝑏) |
44 | 5, 1, 43 | cvmsiota 30513 |
. . . 4
⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ (𝑇 ∈ (𝑆‘𝑀) ∧ (𝑋𝐾𝑌) ∈ 𝐵 ∧ (𝐹‘(𝑋𝐾𝑌)) ∈ 𝑀)) → (𝑊 ∈ 𝑇 ∧ (𝑋𝐾𝑌) ∈ 𝑊)) |
45 | 6, 31, 32, 42, 44 | syl13anc 1320 |
. . 3
⊢ (𝜑 → (𝑊 ∈ 𝑇 ∧ (𝑋𝐾𝑌) ∈ 𝑊)) |
46 | 37 | eleq1i 2679 |
. . . 4
⊢ ((𝑋𝐾𝑌) ∈ 𝑊 ↔ (𝐾‘〈𝑋, 𝑌〉) ∈ 𝑊) |
47 | 46 | anbi2i 726 |
. . 3
⊢ ((𝑊 ∈ 𝑇 ∧ (𝑋𝐾𝑌) ∈ 𝑊) ↔ (𝑊 ∈ 𝑇 ∧ (𝐾‘〈𝑋, 𝑌〉) ∈ 𝑊)) |
48 | 45, 47 | sylib 207 |
. 2
⊢ (𝜑 → (𝑊 ∈ 𝑇 ∧ (𝐾‘〈𝑋, 𝑌〉) ∈ 𝑊)) |
49 | | xpss12 5148 |
. . 3
⊢ ((𝑈 ⊆ (0[,]1) ∧ 𝑉 ⊆ (0[,]1)) → (𝑈 × 𝑉) ⊆ ((0[,]1) ×
(0[,]1))) |
50 | 20, 26, 49 | syl2anc 691 |
. 2
⊢ (𝜑 → (𝑈 × 𝑉) ⊆ ((0[,]1) ×
(0[,]1))) |
51 | | snidg 4153 |
. . . . . . 7
⊢ (𝑚 ∈ 𝑈 → 𝑚 ∈ {𝑚}) |
52 | 51 | ad2antrl 760 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → 𝑚 ∈ {𝑚}) |
53 | | simprr 792 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → 𝑛 ∈ 𝑉) |
54 | | ovres 6698 |
. . . . . 6
⊢ ((𝑚 ∈ {𝑚} ∧ 𝑛 ∈ 𝑉) → (𝑚(𝐾 ↾ ({𝑚} × 𝑉))𝑛) = (𝑚𝐾𝑛)) |
55 | 52, 53, 54 | syl2anc 691 |
. . . . 5
⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → (𝑚(𝐾 ↾ ({𝑚} × 𝑉))𝑛) = (𝑚𝐾𝑛)) |
56 | | eqid 2610 |
. . . . . . . 8
⊢ ∪ ((II ×t II) ↾t ({𝑚} × 𝑉)) = ∪ ((II
×t II) ↾t ({𝑚} × 𝑉)) |
57 | 2 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → II ∈ Top) |
58 | | snex 4835 |
. . . . . . . . . . 11
⊢ {𝑚} ∈ V |
59 | 58 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → {𝑚} ∈ V) |
60 | 23 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → 𝑉 ∈ II) |
61 | | txrest 21244 |
. . . . . . . . . 10
⊢ (((II
∈ Top ∧ II ∈ Top) ∧ ({𝑚} ∈ V ∧ 𝑉 ∈ II)) → ((II ×t
II) ↾t ({𝑚} × 𝑉)) = ((II ↾t {𝑚}) ×t (II
↾t 𝑉))) |
62 | 57, 57, 59, 60, 61 | syl22anc 1319 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → ((II ×t II)
↾t ({𝑚}
× 𝑉)) = ((II
↾t {𝑚})
×t (II ↾t 𝑉))) |
63 | | iitopon 22490 |
. . . . . . . . . . . 12
⊢ II ∈
(TopOn‘(0[,]1)) |
64 | 20 | sselda 3568 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑈) → 𝑚 ∈ (0[,]1)) |
65 | 64 | adantrr 749 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → 𝑚 ∈ (0[,]1)) |
66 | | restsn2 20785 |
. . . . . . . . . . . 12
⊢ ((II
∈ (TopOn‘(0[,]1)) ∧ 𝑚 ∈ (0[,]1)) → (II
↾t {𝑚}) =
𝒫 {𝑚}) |
67 | 63, 65, 66 | sylancr 694 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → (II ↾t {𝑚}) = 𝒫 {𝑚}) |
68 | | pwsn 4366 |
. . . . . . . . . . . 12
⊢ 𝒫
{𝑚} = {∅, {𝑚}} |
69 | | indiscon 21031 |
. . . . . . . . . . . 12
⊢ {∅,
{𝑚}} ∈
Con |
70 | 68, 69 | eqeltri 2684 |
. . . . . . . . . . 11
⊢ 𝒫
{𝑚} ∈
Con |
71 | 67, 70 | syl6eqel 2696 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → (II ↾t {𝑚}) ∈ Con) |
72 | | cvmlift2lem9.6 |
. . . . . . . . . . 11
⊢ (𝜑 → (II ↾t
𝑉) ∈
Con) |
73 | 72 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → (II ↾t 𝑉) ∈ Con) |
74 | | txcon 21302 |
. . . . . . . . . 10
⊢ (((II
↾t {𝑚})
∈ Con ∧ (II ↾t 𝑉) ∈ Con) → ((II
↾t {𝑚})
×t (II ↾t 𝑉)) ∈ Con) |
75 | 71, 73, 74 | syl2anc 691 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → ((II ↾t {𝑚}) ×t (II
↾t 𝑉))
∈ Con) |
76 | 62, 75 | eqeltrd 2688 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → ((II ×t II)
↾t ({𝑚}
× 𝑉)) ∈
Con) |
77 | 1, 6, 7, 8, 9, 10,
11 | cvmlift2lem6 30544 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ (0[,]1)) → (𝐾 ↾ ({𝑚} × (0[,]1))) ∈ (((II
×t II) ↾t ({𝑚} × (0[,]1))) Cn 𝐶)) |
78 | 65, 77 | syldan 486 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → (𝐾 ↾ ({𝑚} × (0[,]1))) ∈ (((II
×t II) ↾t ({𝑚} × (0[,]1))) Cn 𝐶)) |
79 | 26 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → 𝑉 ⊆ (0[,]1)) |
80 | | xpss2 5152 |
. . . . . . . . . . . . 13
⊢ (𝑉 ⊆ (0[,]1) → ({𝑚} × 𝑉) ⊆ ({𝑚} × (0[,]1))) |
81 | 79, 80 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → ({𝑚} × 𝑉) ⊆ ({𝑚} × (0[,]1))) |
82 | 65 | snssd 4281 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → {𝑚} ⊆ (0[,]1)) |
83 | | xpss1 5151 |
. . . . . . . . . . . . . 14
⊢ ({𝑚} ⊆ (0[,]1) → ({𝑚} × (0[,]1)) ⊆
((0[,]1) × (0[,]1))) |
84 | 82, 83 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → ({𝑚} × (0[,]1)) ⊆ ((0[,]1) ×
(0[,]1))) |
85 | 4 | restuni 20776 |
. . . . . . . . . . . . 13
⊢ (((II
×t II) ∈ Top ∧ ({𝑚} × (0[,]1)) ⊆ ((0[,]1) ×
(0[,]1))) → ({𝑚}
× (0[,]1)) = ∪ ((II ×t II)
↾t ({𝑚}
× (0[,]1)))) |
86 | 15, 84, 85 | sylancr 694 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → ({𝑚} × (0[,]1)) = ∪ ((II ×t II) ↾t ({𝑚} ×
(0[,]1)))) |
87 | 81, 86 | sseqtrd 3604 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → ({𝑚} × 𝑉) ⊆ ∪ ((II
×t II) ↾t ({𝑚} × (0[,]1)))) |
88 | | eqid 2610 |
. . . . . . . . . . . 12
⊢ ∪ ((II ×t II) ↾t ({𝑚} × (0[,]1))) = ∪ ((II ×t II) ↾t ({𝑚} ×
(0[,]1))) |
89 | 88 | cnrest 20899 |
. . . . . . . . . . 11
⊢ (((𝐾 ↾ ({𝑚} × (0[,]1))) ∈ (((II
×t II) ↾t ({𝑚} × (0[,]1))) Cn 𝐶) ∧ ({𝑚} × 𝑉) ⊆ ∪ ((II
×t II) ↾t ({𝑚} × (0[,]1)))) → ((𝐾 ↾ ({𝑚} × (0[,]1))) ↾ ({𝑚} × 𝑉)) ∈ ((((II ×t II)
↾t ({𝑚}
× (0[,]1))) ↾t ({𝑚} × 𝑉)) Cn 𝐶)) |
90 | 78, 87, 89 | syl2anc 691 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → ((𝐾 ↾ ({𝑚} × (0[,]1))) ↾ ({𝑚} × 𝑉)) ∈ ((((II ×t II)
↾t ({𝑚}
× (0[,]1))) ↾t ({𝑚} × 𝑉)) Cn 𝐶)) |
91 | 81 | resabs1d 5348 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → ((𝐾 ↾ ({𝑚} × (0[,]1))) ↾ ({𝑚} × 𝑉)) = (𝐾 ↾ ({𝑚} × 𝑉))) |
92 | 15 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → (II ×t II) ∈
Top) |
93 | | ovex 6577 |
. . . . . . . . . . . . . 14
⊢ (0[,]1)
∈ V |
94 | 58, 93 | xpex 6860 |
. . . . . . . . . . . . 13
⊢ ({𝑚} × (0[,]1)) ∈
V |
95 | 94 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → ({𝑚} × (0[,]1)) ∈ V) |
96 | | restabs 20779 |
. . . . . . . . . . . 12
⊢ (((II
×t II) ∈ Top ∧ ({𝑚} × 𝑉) ⊆ ({𝑚} × (0[,]1)) ∧ ({𝑚} × (0[,]1)) ∈ V) → (((II
×t II) ↾t ({𝑚} × (0[,]1))) ↾t
({𝑚} × 𝑉)) = ((II ×t
II) ↾t ({𝑚} × 𝑉))) |
97 | 92, 81, 95, 96 | syl3anc 1318 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → (((II ×t II)
↾t ({𝑚}
× (0[,]1))) ↾t ({𝑚} × 𝑉)) = ((II ×t II)
↾t ({𝑚}
× 𝑉))) |
98 | 97 | oveq1d 6564 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → ((((II ×t II)
↾t ({𝑚}
× (0[,]1))) ↾t ({𝑚} × 𝑉)) Cn 𝐶) = (((II ×t II)
↾t ({𝑚}
× 𝑉)) Cn 𝐶)) |
99 | 90, 91, 98 | 3eltr3d 2702 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → (𝐾 ↾ ({𝑚} × 𝑉)) ∈ (((II ×t II)
↾t ({𝑚}
× 𝑉)) Cn 𝐶)) |
100 | | cvmtop1 30496 |
. . . . . . . . . . . . 13
⊢ (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐶 ∈ Top) |
101 | 6, 100 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐶 ∈ Top) |
102 | 101 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → 𝐶 ∈ Top) |
103 | 1 | toptopon 20548 |
. . . . . . . . . . 11
⊢ (𝐶 ∈ Top ↔ 𝐶 ∈ (TopOn‘𝐵)) |
104 | 102, 103 | sylib 207 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → 𝐶 ∈ (TopOn‘𝐵)) |
105 | | df-ima 5051 |
. . . . . . . . . . 11
⊢ (𝐾 “ ({𝑚} × 𝑉)) = ran (𝐾 ↾ ({𝑚} × 𝑉)) |
106 | | simprl 790 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → 𝑚 ∈ 𝑈) |
107 | 106 | snssd 4281 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → {𝑚} ⊆ 𝑈) |
108 | | xpss1 5151 |
. . . . . . . . . . . . 13
⊢ ({𝑚} ⊆ 𝑈 → ({𝑚} × 𝑉) ⊆ (𝑈 × 𝑉)) |
109 | | imass2 5420 |
. . . . . . . . . . . . 13
⊢ (({𝑚} × 𝑉) ⊆ (𝑈 × 𝑉) → (𝐾 “ ({𝑚} × 𝑉)) ⊆ (𝐾 “ (𝑈 × 𝑉))) |
110 | 107, 108,
109 | 3syl 18 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → (𝐾 “ ({𝑚} × 𝑉)) ⊆ (𝐾 “ (𝑈 × 𝑉))) |
111 | | cvmlift2lem9.9 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑈 × 𝑉) ⊆ (◡𝐺 “ 𝑀)) |
112 | | imaco 5557 |
. . . . . . . . . . . . . . . 16
⊢ ((◡𝐾 ∘ ◡𝐹) “ 𝑀) = (◡𝐾 “ (◡𝐹 “ 𝑀)) |
113 | | cnvco 5230 |
. . . . . . . . . . . . . . . . . 18
⊢ ◡(𝐹 ∘ 𝐾) = (◡𝐾 ∘ ◡𝐹) |
114 | 13 | cnveqd 5220 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ◡(𝐹 ∘ 𝐾) = ◡𝐺) |
115 | 113, 114 | syl5eqr 2658 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (◡𝐾 ∘ ◡𝐹) = ◡𝐺) |
116 | 115 | imaeq1d 5384 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((◡𝐾 ∘ ◡𝐹) “ 𝑀) = (◡𝐺 “ 𝑀)) |
117 | 112, 116 | syl5eqr 2658 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (◡𝐾 “ (◡𝐹 “ 𝑀)) = (◡𝐺 “ 𝑀)) |
118 | 111, 117 | sseqtr4d 3605 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑈 × 𝑉) ⊆ (◡𝐾 “ (◡𝐹 “ 𝑀))) |
119 | | ffun 5961 |
. . . . . . . . . . . . . . . 16
⊢ (𝐾:((0[,]1) ×
(0[,]1))⟶𝐵 →
Fun 𝐾) |
120 | 12, 119 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → Fun 𝐾) |
121 | | fdm 5964 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐾:((0[,]1) ×
(0[,]1))⟶𝐵 →
dom 𝐾 = ((0[,]1) ×
(0[,]1))) |
122 | 12, 121 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → dom 𝐾 = ((0[,]1) ×
(0[,]1))) |
123 | 50, 122 | sseqtr4d 3605 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑈 × 𝑉) ⊆ dom 𝐾) |
124 | | funimass3 6241 |
. . . . . . . . . . . . . . 15
⊢ ((Fun
𝐾 ∧ (𝑈 × 𝑉) ⊆ dom 𝐾) → ((𝐾 “ (𝑈 × 𝑉)) ⊆ (◡𝐹 “ 𝑀) ↔ (𝑈 × 𝑉) ⊆ (◡𝐾 “ (◡𝐹 “ 𝑀)))) |
125 | 120, 123,
124 | syl2anc 691 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝐾 “ (𝑈 × 𝑉)) ⊆ (◡𝐹 “ 𝑀) ↔ (𝑈 × 𝑉) ⊆ (◡𝐾 “ (◡𝐹 “ 𝑀)))) |
126 | 118, 125 | mpbird 246 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐾 “ (𝑈 × 𝑉)) ⊆ (◡𝐹 “ 𝑀)) |
127 | 126 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → (𝐾 “ (𝑈 × 𝑉)) ⊆ (◡𝐹 “ 𝑀)) |
128 | 110, 127 | sstrd 3578 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → (𝐾 “ ({𝑚} × 𝑉)) ⊆ (◡𝐹 “ 𝑀)) |
129 | 105, 128 | syl5eqssr 3613 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → ran (𝐾 ↾ ({𝑚} × 𝑉)) ⊆ (◡𝐹 “ 𝑀)) |
130 | | cnvimass 5404 |
. . . . . . . . . . . 12
⊢ (◡𝐹 “ 𝑀) ⊆ dom 𝐹 |
131 | | cvmcn 30498 |
. . . . . . . . . . . . . 14
⊢ (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐹 ∈ (𝐶 Cn 𝐽)) |
132 | 6, 131 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐹 ∈ (𝐶 Cn 𝐽)) |
133 | | eqid 2610 |
. . . . . . . . . . . . . 14
⊢ ∪ 𝐽 =
∪ 𝐽 |
134 | 1, 133 | cnf 20860 |
. . . . . . . . . . . . 13
⊢ (𝐹 ∈ (𝐶 Cn 𝐽) → 𝐹:𝐵⟶∪ 𝐽) |
135 | | fdm 5964 |
. . . . . . . . . . . . 13
⊢ (𝐹:𝐵⟶∪ 𝐽 → dom 𝐹 = 𝐵) |
136 | 132, 134,
135 | 3syl 18 |
. . . . . . . . . . . 12
⊢ (𝜑 → dom 𝐹 = 𝐵) |
137 | 130, 136 | syl5sseq 3616 |
. . . . . . . . . . 11
⊢ (𝜑 → (◡𝐹 “ 𝑀) ⊆ 𝐵) |
138 | 137 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → (◡𝐹 “ 𝑀) ⊆ 𝐵) |
139 | | cnrest2 20900 |
. . . . . . . . . 10
⊢ ((𝐶 ∈ (TopOn‘𝐵) ∧ ran (𝐾 ↾ ({𝑚} × 𝑉)) ⊆ (◡𝐹 “ 𝑀) ∧ (◡𝐹 “ 𝑀) ⊆ 𝐵) → ((𝐾 ↾ ({𝑚} × 𝑉)) ∈ (((II ×t II)
↾t ({𝑚}
× 𝑉)) Cn 𝐶) ↔ (𝐾 ↾ ({𝑚} × 𝑉)) ∈ (((II ×t II)
↾t ({𝑚}
× 𝑉)) Cn (𝐶 ↾t (◡𝐹 “ 𝑀))))) |
140 | 104, 129,
138, 139 | syl3anc 1318 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → ((𝐾 ↾ ({𝑚} × 𝑉)) ∈ (((II ×t II)
↾t ({𝑚}
× 𝑉)) Cn 𝐶) ↔ (𝐾 ↾ ({𝑚} × 𝑉)) ∈ (((II ×t II)
↾t ({𝑚}
× 𝑉)) Cn (𝐶 ↾t (◡𝐹 “ 𝑀))))) |
141 | 99, 140 | mpbid 221 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → (𝐾 ↾ ({𝑚} × 𝑉)) ∈ (((II ×t II)
↾t ({𝑚}
× 𝑉)) Cn (𝐶 ↾t (◡𝐹 “ 𝑀)))) |
142 | 5 | cvmsss 30503 |
. . . . . . . . . . . 12
⊢ (𝑇 ∈ (𝑆‘𝑀) → 𝑇 ⊆ 𝐶) |
143 | 31, 142 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑇 ⊆ 𝐶) |
144 | 45 | simpld 474 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑊 ∈ 𝑇) |
145 | 143, 144 | sseldd 3569 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑊 ∈ 𝐶) |
146 | | elssuni 4403 |
. . . . . . . . . . . 12
⊢ (𝑊 ∈ 𝑇 → 𝑊 ⊆ ∪ 𝑇) |
147 | 144, 146 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑊 ⊆ ∪ 𝑇) |
148 | 5 | cvmsuni 30505 |
. . . . . . . . . . . 12
⊢ (𝑇 ∈ (𝑆‘𝑀) → ∪ 𝑇 = (◡𝐹 “ 𝑀)) |
149 | 31, 148 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → ∪ 𝑇 =
(◡𝐹 “ 𝑀)) |
150 | 147, 149 | sseqtrd 3604 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑊 ⊆ (◡𝐹 “ 𝑀)) |
151 | 5 | cvmsrcl 30500 |
. . . . . . . . . . . . 13
⊢ (𝑇 ∈ (𝑆‘𝑀) → 𝑀 ∈ 𝐽) |
152 | 31, 151 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑀 ∈ 𝐽) |
153 | | cnima 20879 |
. . . . . . . . . . . 12
⊢ ((𝐹 ∈ (𝐶 Cn 𝐽) ∧ 𝑀 ∈ 𝐽) → (◡𝐹 “ 𝑀) ∈ 𝐶) |
154 | 132, 152,
153 | syl2anc 691 |
. . . . . . . . . . 11
⊢ (𝜑 → (◡𝐹 “ 𝑀) ∈ 𝐶) |
155 | | restopn2 20791 |
. . . . . . . . . . 11
⊢ ((𝐶 ∈ Top ∧ (◡𝐹 “ 𝑀) ∈ 𝐶) → (𝑊 ∈ (𝐶 ↾t (◡𝐹 “ 𝑀)) ↔ (𝑊 ∈ 𝐶 ∧ 𝑊 ⊆ (◡𝐹 “ 𝑀)))) |
156 | 101, 154,
155 | syl2anc 691 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑊 ∈ (𝐶 ↾t (◡𝐹 “ 𝑀)) ↔ (𝑊 ∈ 𝐶 ∧ 𝑊 ⊆ (◡𝐹 “ 𝑀)))) |
157 | 145, 150,
156 | mpbir2and 959 |
. . . . . . . . 9
⊢ (𝜑 → 𝑊 ∈ (𝐶 ↾t (◡𝐹 “ 𝑀))) |
158 | 157 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → 𝑊 ∈ (𝐶 ↾t (◡𝐹 “ 𝑀))) |
159 | 5 | cvmscld 30509 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑇 ∈ (𝑆‘𝑀) ∧ 𝑊 ∈ 𝑇) → 𝑊 ∈ (Clsd‘(𝐶 ↾t (◡𝐹 “ 𝑀)))) |
160 | 6, 31, 144, 159 | syl3anc 1318 |
. . . . . . . . 9
⊢ (𝜑 → 𝑊 ∈ (Clsd‘(𝐶 ↾t (◡𝐹 “ 𝑀)))) |
161 | 160 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → 𝑊 ∈ (Clsd‘(𝐶 ↾t (◡𝐹 “ 𝑀)))) |
162 | | cvmlift2lem9.10 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑍 ∈ 𝑉) |
163 | 162 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → 𝑍 ∈ 𝑉) |
164 | | opelxpi 5072 |
. . . . . . . . . 10
⊢ ((𝑚 ∈ {𝑚} ∧ 𝑍 ∈ 𝑉) → 〈𝑚, 𝑍〉 ∈ ({𝑚} × 𝑉)) |
165 | 52, 163, 164 | syl2anc 691 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → 〈𝑚, 𝑍〉 ∈ ({𝑚} × 𝑉)) |
166 | 81, 84 | sstrd 3578 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → ({𝑚} × 𝑉) ⊆ ((0[,]1) ×
(0[,]1))) |
167 | 4 | restuni 20776 |
. . . . . . . . . 10
⊢ (((II
×t II) ∈ Top ∧ ({𝑚} × 𝑉) ⊆ ((0[,]1) × (0[,]1))) →
({𝑚} × 𝑉) = ∪
((II ×t II) ↾t ({𝑚} × 𝑉))) |
168 | 15, 166, 167 | sylancr 694 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → ({𝑚} × 𝑉) = ∪ ((II
×t II) ↾t ({𝑚} × 𝑉))) |
169 | 165, 168 | eleqtrd 2690 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → 〈𝑚, 𝑍〉 ∈ ∪
((II ×t II) ↾t ({𝑚} × 𝑉))) |
170 | | df-ov 6552 |
. . . . . . . . . 10
⊢ (𝑚(𝐾 ↾ ({𝑚} × 𝑉))𝑍) = ((𝐾 ↾ ({𝑚} × 𝑉))‘〈𝑚, 𝑍〉) |
171 | | ovres 6698 |
. . . . . . . . . . . 12
⊢ ((𝑚 ∈ {𝑚} ∧ 𝑍 ∈ 𝑉) → (𝑚(𝐾 ↾ ({𝑚} × 𝑉))𝑍) = (𝑚𝐾𝑍)) |
172 | 52, 163, 171 | syl2anc 691 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → (𝑚(𝐾 ↾ ({𝑚} × 𝑉))𝑍) = (𝑚𝐾𝑍)) |
173 | | snidg 4153 |
. . . . . . . . . . . . . 14
⊢ (𝑍 ∈ 𝑉 → 𝑍 ∈ {𝑍}) |
174 | 162, 173 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑍 ∈ {𝑍}) |
175 | 174 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → 𝑍 ∈ {𝑍}) |
176 | | ovres 6698 |
. . . . . . . . . . . 12
⊢ ((𝑚 ∈ 𝑈 ∧ 𝑍 ∈ {𝑍}) → (𝑚(𝐾 ↾ (𝑈 × {𝑍}))𝑍) = (𝑚𝐾𝑍)) |
177 | 106, 175,
176 | syl2anc 691 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → (𝑚(𝐾 ↾ (𝑈 × {𝑍}))𝑍) = (𝑚𝐾𝑍)) |
178 | 172, 177 | eqtr4d 2647 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → (𝑚(𝐾 ↾ ({𝑚} × 𝑉))𝑍) = (𝑚(𝐾 ↾ (𝑈 × {𝑍}))𝑍)) |
179 | 170, 178 | syl5eqr 2658 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → ((𝐾 ↾ ({𝑚} × 𝑉))‘〈𝑚, 𝑍〉) = (𝑚(𝐾 ↾ (𝑈 × {𝑍}))𝑍)) |
180 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢ ∪ ((II ×t II) ↾t (𝑈 × {𝑍})) = ∪ ((II
×t II) ↾t (𝑈 × {𝑍})) |
181 | 2 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → II ∈
Top) |
182 | | snex 4835 |
. . . . . . . . . . . . . . . 16
⊢ {𝑍} ∈ V |
183 | 182 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → {𝑍} ∈ V) |
184 | | txrest 21244 |
. . . . . . . . . . . . . . 15
⊢ (((II
∈ Top ∧ II ∈ Top) ∧ (𝑈 ∈ II ∧ {𝑍} ∈ V)) → ((II ×t
II) ↾t (𝑈
× {𝑍})) = ((II
↾t 𝑈)
×t (II ↾t {𝑍}))) |
185 | 181, 181,
17, 183, 184 | syl22anc 1319 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((II ×t
II) ↾t (𝑈
× {𝑍})) = ((II
↾t 𝑈)
×t (II ↾t {𝑍}))) |
186 | | cvmlift2lem9.5 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (II ↾t
𝑈) ∈
Con) |
187 | 26, 162 | sseldd 3569 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑍 ∈ (0[,]1)) |
188 | | restsn2 20785 |
. . . . . . . . . . . . . . . . 17
⊢ ((II
∈ (TopOn‘(0[,]1)) ∧ 𝑍 ∈ (0[,]1)) → (II
↾t {𝑍}) =
𝒫 {𝑍}) |
189 | 63, 187, 188 | sylancr 694 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (II ↾t
{𝑍}) = 𝒫 {𝑍}) |
190 | | pwsn 4366 |
. . . . . . . . . . . . . . . . 17
⊢ 𝒫
{𝑍} = {∅, {𝑍}} |
191 | | indiscon 21031 |
. . . . . . . . . . . . . . . . 17
⊢ {∅,
{𝑍}} ∈
Con |
192 | 190, 191 | eqeltri 2684 |
. . . . . . . . . . . . . . . 16
⊢ 𝒫
{𝑍} ∈
Con |
193 | 189, 192 | syl6eqel 2696 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (II ↾t
{𝑍}) ∈
Con) |
194 | | txcon 21302 |
. . . . . . . . . . . . . . 15
⊢ (((II
↾t 𝑈)
∈ Con ∧ (II ↾t {𝑍}) ∈ Con) → ((II
↾t 𝑈)
×t (II ↾t {𝑍})) ∈ Con) |
195 | 186, 193,
194 | syl2anc 691 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((II ↾t
𝑈) ×t (II
↾t {𝑍}))
∈ Con) |
196 | 185, 195 | eqeltrd 2688 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((II ×t
II) ↾t (𝑈
× {𝑍})) ∈
Con) |
197 | | cvmlift2lem9.11 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐾 ↾ (𝑈 × {𝑍})) ∈ (((II ×t II)
↾t (𝑈
× {𝑍})) Cn 𝐶)) |
198 | 101, 103 | sylib 207 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐶 ∈ (TopOn‘𝐵)) |
199 | | df-ima 5051 |
. . . . . . . . . . . . . . . 16
⊢ (𝐾 “ (𝑈 × {𝑍})) = ran (𝐾 ↾ (𝑈 × {𝑍})) |
200 | 162 | snssd 4281 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → {𝑍} ⊆ 𝑉) |
201 | | xpss2 5152 |
. . . . . . . . . . . . . . . . . 18
⊢ ({𝑍} ⊆ 𝑉 → (𝑈 × {𝑍}) ⊆ (𝑈 × 𝑉)) |
202 | | imass2 5420 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑈 × {𝑍}) ⊆ (𝑈 × 𝑉) → (𝐾 “ (𝑈 × {𝑍})) ⊆ (𝐾 “ (𝑈 × 𝑉))) |
203 | 200, 201,
202 | 3syl 18 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝐾 “ (𝑈 × {𝑍})) ⊆ (𝐾 “ (𝑈 × 𝑉))) |
204 | 203, 126 | sstrd 3578 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐾 “ (𝑈 × {𝑍})) ⊆ (◡𝐹 “ 𝑀)) |
205 | 199, 204 | syl5eqssr 3613 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ran (𝐾 ↾ (𝑈 × {𝑍})) ⊆ (◡𝐹 “ 𝑀)) |
206 | | cnrest2 20900 |
. . . . . . . . . . . . . . 15
⊢ ((𝐶 ∈ (TopOn‘𝐵) ∧ ran (𝐾 ↾ (𝑈 × {𝑍})) ⊆ (◡𝐹 “ 𝑀) ∧ (◡𝐹 “ 𝑀) ⊆ 𝐵) → ((𝐾 ↾ (𝑈 × {𝑍})) ∈ (((II ×t II)
↾t (𝑈
× {𝑍})) Cn 𝐶) ↔ (𝐾 ↾ (𝑈 × {𝑍})) ∈ (((II ×t II)
↾t (𝑈
× {𝑍})) Cn (𝐶 ↾t (◡𝐹 “ 𝑀))))) |
207 | 198, 205,
137, 206 | syl3anc 1318 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝐾 ↾ (𝑈 × {𝑍})) ∈ (((II ×t II)
↾t (𝑈
× {𝑍})) Cn 𝐶) ↔ (𝐾 ↾ (𝑈 × {𝑍})) ∈ (((II ×t II)
↾t (𝑈
× {𝑍})) Cn (𝐶 ↾t (◡𝐹 “ 𝑀))))) |
208 | 197, 207 | mpbid 221 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐾 ↾ (𝑈 × {𝑍})) ∈ (((II ×t II)
↾t (𝑈
× {𝑍})) Cn (𝐶 ↾t (◡𝐹 “ 𝑀)))) |
209 | | opelxpi 5072 |
. . . . . . . . . . . . . . 15
⊢ ((𝑋 ∈ 𝑈 ∧ 𝑍 ∈ {𝑍}) → 〈𝑋, 𝑍〉 ∈ (𝑈 × {𝑍})) |
210 | 21, 174, 209 | syl2anc 691 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 〈𝑋, 𝑍〉 ∈ (𝑈 × {𝑍})) |
211 | 187 | snssd 4281 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → {𝑍} ⊆ (0[,]1)) |
212 | | xpss12 5148 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑈 ⊆ (0[,]1) ∧ {𝑍} ⊆ (0[,]1)) → (𝑈 × {𝑍}) ⊆ ((0[,]1) ×
(0[,]1))) |
213 | 20, 211, 212 | syl2anc 691 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑈 × {𝑍}) ⊆ ((0[,]1) ×
(0[,]1))) |
214 | 4 | restuni 20776 |
. . . . . . . . . . . . . . 15
⊢ (((II
×t II) ∈ Top ∧ (𝑈 × {𝑍}) ⊆ ((0[,]1) × (0[,]1))) →
(𝑈 × {𝑍}) = ∪ ((II ×t II) ↾t (𝑈 × {𝑍}))) |
215 | 15, 213, 214 | sylancr 694 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑈 × {𝑍}) = ∪ ((II
×t II) ↾t (𝑈 × {𝑍}))) |
216 | 210, 215 | eleqtrd 2690 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 〈𝑋, 𝑍〉 ∈ ∪
((II ×t II) ↾t (𝑈 × {𝑍}))) |
217 | | df-ov 6552 |
. . . . . . . . . . . . . . 15
⊢ (𝑋(𝐾 ↾ (𝑈 × {𝑍}))𝑍) = ((𝐾 ↾ (𝑈 × {𝑍}))‘〈𝑋, 𝑍〉) |
218 | | ovres 6698 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑋 ∈ 𝑈 ∧ 𝑍 ∈ {𝑍}) → (𝑋(𝐾 ↾ (𝑈 × {𝑍}))𝑍) = (𝑋𝐾𝑍)) |
219 | 21, 174, 218 | syl2anc 691 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑋(𝐾 ↾ (𝑈 × {𝑍}))𝑍) = (𝑋𝐾𝑍)) |
220 | | snidg 4153 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑋 ∈ 𝑈 → 𝑋 ∈ {𝑋}) |
221 | 21, 220 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑋 ∈ {𝑋}) |
222 | | ovres 6698 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑋 ∈ {𝑋} ∧ 𝑍 ∈ 𝑉) → (𝑋(𝐾 ↾ ({𝑋} × 𝑉))𝑍) = (𝑋𝐾𝑍)) |
223 | 221, 162,
222 | syl2anc 691 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑋(𝐾 ↾ ({𝑋} × 𝑉))𝑍) = (𝑋𝐾𝑍)) |
224 | 219, 223 | eqtr4d 2647 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑋(𝐾 ↾ (𝑈 × {𝑍}))𝑍) = (𝑋(𝐾 ↾ ({𝑋} × 𝑉))𝑍)) |
225 | 217, 224 | syl5eqr 2658 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝐾 ↾ (𝑈 × {𝑍}))‘〈𝑋, 𝑍〉) = (𝑋(𝐾 ↾ ({𝑋} × 𝑉))𝑍)) |
226 | | eqid 2610 |
. . . . . . . . . . . . . . . . 17
⊢ ∪ ((II ×t II) ↾t ({𝑋} × 𝑉)) = ∪ ((II
×t II) ↾t ({𝑋} × 𝑉)) |
227 | | snex 4835 |
. . . . . . . . . . . . . . . . . . . 20
⊢ {𝑋} ∈ V |
228 | 227 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → {𝑋} ∈ V) |
229 | | txrest 21244 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((II
∈ Top ∧ II ∈ Top) ∧ ({𝑋} ∈ V ∧ 𝑉 ∈ II)) → ((II ×t
II) ↾t ({𝑋} × 𝑉)) = ((II ↾t {𝑋}) ×t (II
↾t 𝑉))) |
230 | 181, 181,
228, 23, 229 | syl22anc 1319 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((II ×t
II) ↾t ({𝑋} × 𝑉)) = ((II ↾t {𝑋}) ×t (II
↾t 𝑉))) |
231 | | restsn2 20785 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((II
∈ (TopOn‘(0[,]1)) ∧ 𝑋 ∈ (0[,]1)) → (II
↾t {𝑋}) =
𝒫 {𝑋}) |
232 | 63, 22, 231 | sylancr 694 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (II ↾t
{𝑋}) = 𝒫 {𝑋}) |
233 | | pwsn 4366 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 𝒫
{𝑋} = {∅, {𝑋}} |
234 | | indiscon 21031 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ {∅,
{𝑋}} ∈
Con |
235 | 233, 234 | eqeltri 2684 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 𝒫
{𝑋} ∈
Con |
236 | 232, 235 | syl6eqel 2696 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (II ↾t
{𝑋}) ∈
Con) |
237 | | txcon 21302 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((II
↾t {𝑋})
∈ Con ∧ (II ↾t 𝑉) ∈ Con) → ((II
↾t {𝑋})
×t (II ↾t 𝑉)) ∈ Con) |
238 | 236, 72, 237 | syl2anc 691 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((II ↾t
{𝑋}) ×t
(II ↾t 𝑉))
∈ Con) |
239 | 230, 238 | eqeltrd 2688 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((II ×t
II) ↾t ({𝑋} × 𝑉)) ∈ Con) |
240 | 1, 6, 7, 8, 9, 10,
11 | cvmlift2lem6 30544 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑋 ∈ (0[,]1)) → (𝐾 ↾ ({𝑋} × (0[,]1))) ∈ (((II
×t II) ↾t ({𝑋} × (0[,]1))) Cn 𝐶)) |
241 | 22, 240 | mpdan 699 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝐾 ↾ ({𝑋} × (0[,]1))) ∈ (((II
×t II) ↾t ({𝑋} × (0[,]1))) Cn 𝐶)) |
242 | | xpss2 5152 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑉 ⊆ (0[,]1) → ({𝑋} × 𝑉) ⊆ ({𝑋} × (0[,]1))) |
243 | 23, 25, 242 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → ({𝑋} × 𝑉) ⊆ ({𝑋} × (0[,]1))) |
244 | 22 | snssd 4281 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → {𝑋} ⊆ (0[,]1)) |
245 | | xpss1 5151 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ({𝑋} ⊆ (0[,]1) → ({𝑋} × (0[,]1)) ⊆
((0[,]1) × (0[,]1))) |
246 | 244, 245 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → ({𝑋} × (0[,]1)) ⊆ ((0[,]1) ×
(0[,]1))) |
247 | 4 | restuni 20776 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((II
×t II) ∈ Top ∧ ({𝑋} × (0[,]1)) ⊆ ((0[,]1) ×
(0[,]1))) → ({𝑋}
× (0[,]1)) = ∪ ((II ×t II)
↾t ({𝑋}
× (0[,]1)))) |
248 | 15, 246, 247 | sylancr 694 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → ({𝑋} × (0[,]1)) = ∪ ((II ×t II) ↾t ({𝑋} ×
(0[,]1)))) |
249 | 243, 248 | sseqtrd 3604 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ({𝑋} × 𝑉) ⊆ ∪ ((II
×t II) ↾t ({𝑋} × (0[,]1)))) |
250 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ∪ ((II ×t II) ↾t ({𝑋} × (0[,]1))) = ∪ ((II ×t II) ↾t ({𝑋} ×
(0[,]1))) |
251 | 250 | cnrest 20899 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐾 ↾ ({𝑋} × (0[,]1))) ∈ (((II
×t II) ↾t ({𝑋} × (0[,]1))) Cn 𝐶) ∧ ({𝑋} × 𝑉) ⊆ ∪ ((II
×t II) ↾t ({𝑋} × (0[,]1)))) → ((𝐾 ↾ ({𝑋} × (0[,]1))) ↾ ({𝑋} × 𝑉)) ∈ ((((II ×t II)
↾t ({𝑋}
× (0[,]1))) ↾t ({𝑋} × 𝑉)) Cn 𝐶)) |
252 | 241, 249,
251 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((𝐾 ↾ ({𝑋} × (0[,]1))) ↾ ({𝑋} × 𝑉)) ∈ ((((II ×t II)
↾t ({𝑋}
× (0[,]1))) ↾t ({𝑋} × 𝑉)) Cn 𝐶)) |
253 | 243 | resabs1d 5348 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((𝐾 ↾ ({𝑋} × (0[,]1))) ↾ ({𝑋} × 𝑉)) = (𝐾 ↾ ({𝑋} × 𝑉))) |
254 | 227, 93 | xpex 6860 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ({𝑋} × (0[,]1)) ∈
V |
255 | 254 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → ({𝑋} × (0[,]1)) ∈
V) |
256 | | restabs 20779 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((II
×t II) ∈ Top ∧ ({𝑋} × 𝑉) ⊆ ({𝑋} × (0[,]1)) ∧ ({𝑋} × (0[,]1)) ∈ V) → (((II
×t II) ↾t ({𝑋} × (0[,]1))) ↾t
({𝑋} × 𝑉)) = ((II ×t
II) ↾t ({𝑋} × 𝑉))) |
257 | 16, 243, 255, 256 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (((II ×t
II) ↾t ({𝑋} × (0[,]1))) ↾t
({𝑋} × 𝑉)) = ((II ×t
II) ↾t ({𝑋} × 𝑉))) |
258 | 257 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((((II ×t
II) ↾t ({𝑋} × (0[,]1))) ↾t
({𝑋} × 𝑉)) Cn 𝐶) = (((II ×t II)
↾t ({𝑋}
× 𝑉)) Cn 𝐶)) |
259 | 252, 253,
258 | 3eltr3d 2702 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝐾 ↾ ({𝑋} × 𝑉)) ∈ (((II ×t II)
↾t ({𝑋}
× 𝑉)) Cn 𝐶)) |
260 | | df-ima 5051 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐾 “ ({𝑋} × 𝑉)) = ran (𝐾 ↾ ({𝑋} × 𝑉)) |
261 | 21 | snssd 4281 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → {𝑋} ⊆ 𝑈) |
262 | | xpss1 5151 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ({𝑋} ⊆ 𝑈 → ({𝑋} × 𝑉) ⊆ (𝑈 × 𝑉)) |
263 | | imass2 5420 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (({𝑋} × 𝑉) ⊆ (𝑈 × 𝑉) → (𝐾 “ ({𝑋} × 𝑉)) ⊆ (𝐾 “ (𝑈 × 𝑉))) |
264 | 261, 262,
263 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝐾 “ ({𝑋} × 𝑉)) ⊆ (𝐾 “ (𝑈 × 𝑉))) |
265 | 264, 126 | sstrd 3578 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝐾 “ ({𝑋} × 𝑉)) ⊆ (◡𝐹 “ 𝑀)) |
266 | 260, 265 | syl5eqssr 3613 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ran (𝐾 ↾ ({𝑋} × 𝑉)) ⊆ (◡𝐹 “ 𝑀)) |
267 | | cnrest2 20900 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐶 ∈ (TopOn‘𝐵) ∧ ran (𝐾 ↾ ({𝑋} × 𝑉)) ⊆ (◡𝐹 “ 𝑀) ∧ (◡𝐹 “ 𝑀) ⊆ 𝐵) → ((𝐾 ↾ ({𝑋} × 𝑉)) ∈ (((II ×t II)
↾t ({𝑋}
× 𝑉)) Cn 𝐶) ↔ (𝐾 ↾ ({𝑋} × 𝑉)) ∈ (((II ×t II)
↾t ({𝑋}
× 𝑉)) Cn (𝐶 ↾t (◡𝐹 “ 𝑀))))) |
268 | 198, 266,
137, 267 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((𝐾 ↾ ({𝑋} × 𝑉)) ∈ (((II ×t II)
↾t ({𝑋}
× 𝑉)) Cn 𝐶) ↔ (𝐾 ↾ ({𝑋} × 𝑉)) ∈ (((II ×t II)
↾t ({𝑋}
× 𝑉)) Cn (𝐶 ↾t (◡𝐹 “ 𝑀))))) |
269 | 259, 268 | mpbid 221 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝐾 ↾ ({𝑋} × 𝑉)) ∈ (((II ×t II)
↾t ({𝑋}
× 𝑉)) Cn (𝐶 ↾t (◡𝐹 “ 𝑀)))) |
270 | | opelxpi 5072 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑋 ∈ {𝑋} ∧ 𝑌 ∈ 𝑉) → 〈𝑋, 𝑌〉 ∈ ({𝑋} × 𝑉)) |
271 | 221, 27, 270 | syl2anc 691 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 〈𝑋, 𝑌〉 ∈ ({𝑋} × 𝑉)) |
272 | 261, 262 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ({𝑋} × 𝑉) ⊆ (𝑈 × 𝑉)) |
273 | 272, 50 | sstrd 3578 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ({𝑋} × 𝑉) ⊆ ((0[,]1) ×
(0[,]1))) |
274 | 4 | restuni 20776 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((II
×t II) ∈ Top ∧ ({𝑋} × 𝑉) ⊆ ((0[,]1) × (0[,]1))) →
({𝑋} × 𝑉) = ∪
((II ×t II) ↾t ({𝑋} × 𝑉))) |
275 | 15, 273, 274 | sylancr 694 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ({𝑋} × 𝑉) = ∪ ((II
×t II) ↾t ({𝑋} × 𝑉))) |
276 | 271, 275 | eleqtrd 2690 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 〈𝑋, 𝑌〉 ∈ ∪
((II ×t II) ↾t ({𝑋} × 𝑉))) |
277 | | df-ov 6552 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑋(𝐾 ↾ ({𝑋} × 𝑉))𝑌) = ((𝐾 ↾ ({𝑋} × 𝑉))‘〈𝑋, 𝑌〉) |
278 | | ovres 6698 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑋 ∈ {𝑋} ∧ 𝑌 ∈ 𝑉) → (𝑋(𝐾 ↾ ({𝑋} × 𝑉))𝑌) = (𝑋𝐾𝑌)) |
279 | 221, 27, 278 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑋(𝐾 ↾ ({𝑋} × 𝑉))𝑌) = (𝑋𝐾𝑌)) |
280 | 277, 279 | syl5eqr 2658 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((𝐾 ↾ ({𝑋} × 𝑉))‘〈𝑋, 𝑌〉) = (𝑋𝐾𝑌)) |
281 | 45 | simprd 478 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑋𝐾𝑌) ∈ 𝑊) |
282 | 280, 281 | eqeltrd 2688 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝐾 ↾ ({𝑋} × 𝑉))‘〈𝑋, 𝑌〉) ∈ 𝑊) |
283 | 226, 239,
269, 157, 160, 276, 282 | concn 21039 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐾 ↾ ({𝑋} × 𝑉)):∪ ((II
×t II) ↾t ({𝑋} × 𝑉))⟶𝑊) |
284 | 275 | feq2d 5944 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝐾 ↾ ({𝑋} × 𝑉)):({𝑋} × 𝑉)⟶𝑊 ↔ (𝐾 ↾ ({𝑋} × 𝑉)):∪ ((II
×t II) ↾t ({𝑋} × 𝑉))⟶𝑊)) |
285 | 283, 284 | mpbird 246 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐾 ↾ ({𝑋} × 𝑉)):({𝑋} × 𝑉)⟶𝑊) |
286 | 285, 221,
162 | fovrnd 6704 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑋(𝐾 ↾ ({𝑋} × 𝑉))𝑍) ∈ 𝑊) |
287 | 225, 286 | eqeltrd 2688 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐾 ↾ (𝑈 × {𝑍}))‘〈𝑋, 𝑍〉) ∈ 𝑊) |
288 | 180, 196,
208, 157, 160, 216, 287 | concn 21039 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐾 ↾ (𝑈 × {𝑍})):∪ ((II
×t II) ↾t (𝑈 × {𝑍}))⟶𝑊) |
289 | 215 | feq2d 5944 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐾 ↾ (𝑈 × {𝑍})):(𝑈 × {𝑍})⟶𝑊 ↔ (𝐾 ↾ (𝑈 × {𝑍})):∪ ((II
×t II) ↾t (𝑈 × {𝑍}))⟶𝑊)) |
290 | 288, 289 | mpbird 246 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐾 ↾ (𝑈 × {𝑍})):(𝑈 × {𝑍})⟶𝑊) |
291 | 290 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → (𝐾 ↾ (𝑈 × {𝑍})):(𝑈 × {𝑍})⟶𝑊) |
292 | 291, 106,
175 | fovrnd 6704 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → (𝑚(𝐾 ↾ (𝑈 × {𝑍}))𝑍) ∈ 𝑊) |
293 | 179, 292 | eqeltrd 2688 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → ((𝐾 ↾ ({𝑚} × 𝑉))‘〈𝑚, 𝑍〉) ∈ 𝑊) |
294 | 56, 76, 141, 158, 161, 169, 293 | concn 21039 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → (𝐾 ↾ ({𝑚} × 𝑉)):∪ ((II
×t II) ↾t ({𝑚} × 𝑉))⟶𝑊) |
295 | 168 | feq2d 5944 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → ((𝐾 ↾ ({𝑚} × 𝑉)):({𝑚} × 𝑉)⟶𝑊 ↔ (𝐾 ↾ ({𝑚} × 𝑉)):∪ ((II
×t II) ↾t ({𝑚} × 𝑉))⟶𝑊)) |
296 | 294, 295 | mpbird 246 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → (𝐾 ↾ ({𝑚} × 𝑉)):({𝑚} × 𝑉)⟶𝑊) |
297 | 296, 52, 53 | fovrnd 6704 |
. . . . 5
⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → (𝑚(𝐾 ↾ ({𝑚} × 𝑉))𝑛) ∈ 𝑊) |
298 | 55, 297 | eqeltrrd 2689 |
. . . 4
⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → (𝑚𝐾𝑛) ∈ 𝑊) |
299 | 298 | ralrimivva 2954 |
. . 3
⊢ (𝜑 → ∀𝑚 ∈ 𝑈 ∀𝑛 ∈ 𝑉 (𝑚𝐾𝑛) ∈ 𝑊) |
300 | | funimassov 6709 |
. . . 4
⊢ ((Fun
𝐾 ∧ (𝑈 × 𝑉) ⊆ dom 𝐾) → ((𝐾 “ (𝑈 × 𝑉)) ⊆ 𝑊 ↔ ∀𝑚 ∈ 𝑈 ∀𝑛 ∈ 𝑉 (𝑚𝐾𝑛) ∈ 𝑊)) |
301 | 120, 123,
300 | syl2anc 691 |
. . 3
⊢ (𝜑 → ((𝐾 “ (𝑈 × 𝑉)) ⊆ 𝑊 ↔ ∀𝑚 ∈ 𝑈 ∀𝑛 ∈ 𝑉 (𝑚𝐾𝑛) ∈ 𝑊)) |
302 | 299, 301 | mpbird 246 |
. 2
⊢ (𝜑 → (𝐾 “ (𝑈 × 𝑉)) ⊆ 𝑊) |
303 | 1, 4, 5, 6, 12, 14, 16, 30, 31, 48, 50, 302 | cvmlift2lem9a 30539 |
1
⊢ (𝜑 → (𝐾 ↾ (𝑈 × 𝑉)) ∈ (((II ×t II)
↾t (𝑈
× 𝑉)) Cn 𝐶)) |