| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | cvmlift2.b | . . . 4
⊢ 𝐵 = ∪
𝐶 | 
| 2 |  | cvmlift2.f | . . . 4
⊢ (𝜑 → 𝐹 ∈ (𝐶 CovMap 𝐽)) | 
| 3 |  | cvmlift2.g | . . . 4
⊢ (𝜑 → 𝐺 ∈ ((II ×t II) Cn
𝐽)) | 
| 4 |  | cvmlift2.p | . . . 4
⊢ (𝜑 → 𝑃 ∈ 𝐵) | 
| 5 |  | cvmlift2.i | . . . 4
⊢ (𝜑 → (𝐹‘𝑃) = (0𝐺0)) | 
| 6 |  | cvmlift2.h | . . . 4
⊢ 𝐻 = (℩𝑓 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑓) = (𝑧 ∈ (0[,]1) ↦ (𝑧𝐺0)) ∧ (𝑓‘0) = 𝑃)) | 
| 7 |  | cvmlift2.k | . . . 4
⊢ 𝐾 = (𝑥 ∈ (0[,]1), 𝑦 ∈ (0[,]1) ↦ ((℩𝑓 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑓) = (𝑧 ∈ (0[,]1) ↦ (𝑥𝐺𝑧)) ∧ (𝑓‘0) = (𝐻‘𝑥)))‘𝑦)) | 
| 8 |  | fveq2 6906 | . . . . . 6
⊢ (𝑎 = 𝑧 → (((II ×t II) CnP
𝐶)‘𝑎) = (((II ×t II) CnP 𝐶)‘𝑧)) | 
| 9 | 8 | eleq2d 2827 | . . . . 5
⊢ (𝑎 = 𝑧 → (𝐾 ∈ (((II ×t II) CnP
𝐶)‘𝑎) ↔ 𝐾 ∈ (((II ×t II) CnP
𝐶)‘𝑧))) | 
| 10 | 9 | cbvrabv 3447 | . . . 4
⊢ {𝑎 ∈ ((0[,]1) ×
(0[,]1)) ∣ 𝐾 ∈
(((II ×t II) CnP 𝐶)‘𝑎)} = {𝑧 ∈ ((0[,]1) × (0[,]1)) ∣
𝐾 ∈ (((II
×t II) CnP 𝐶)‘𝑧)} | 
| 11 |  | sneq 4636 | . . . . . . 7
⊢ (𝑧 = 𝑏 → {𝑧} = {𝑏}) | 
| 12 | 11 | xpeq2d 5715 | . . . . . 6
⊢ (𝑧 = 𝑏 → ((0[,]1) × {𝑧}) = ((0[,]1) × {𝑏})) | 
| 13 | 12 | sseq1d 4015 | . . . . 5
⊢ (𝑧 = 𝑏 → (((0[,]1) × {𝑧}) ⊆ {𝑎 ∈ ((0[,]1) × (0[,]1)) ∣
𝐾 ∈ (((II
×t II) CnP 𝐶)‘𝑎)} ↔ ((0[,]1) × {𝑏}) ⊆ {𝑎 ∈ ((0[,]1) × (0[,]1)) ∣
𝐾 ∈ (((II
×t II) CnP 𝐶)‘𝑎)})) | 
| 14 | 13 | cbvrabv 3447 | . . . 4
⊢ {𝑧 ∈ (0[,]1) ∣ ((0[,]1)
× {𝑧}) ⊆ {𝑎 ∈ ((0[,]1) ×
(0[,]1)) ∣ 𝐾 ∈
(((II ×t II) CnP 𝐶)‘𝑎)}} = {𝑏 ∈ (0[,]1) ∣ ((0[,]1) ×
{𝑏}) ⊆ {𝑎 ∈ ((0[,]1) ×
(0[,]1)) ∣ 𝐾 ∈
(((II ×t II) CnP 𝐶)‘𝑎)}} | 
| 15 |  | simpr 484 | . . . . . . 7
⊢ ((𝑐 = 𝑟 ∧ 𝑑 = 𝑡) → 𝑑 = 𝑡) | 
| 16 | 15 | eleq1d 2826 | . . . . . 6
⊢ ((𝑐 = 𝑟 ∧ 𝑑 = 𝑡) → (𝑑 ∈ (0[,]1) ↔ 𝑡 ∈ (0[,]1))) | 
| 17 |  | xpeq1 5699 | . . . . . . . . . 10
⊢ (𝑣 = 𝑢 → (𝑣 × {𝑏}) = (𝑢 × {𝑏})) | 
| 18 | 17 | sseq1d 4015 | . . . . . . . . 9
⊢ (𝑣 = 𝑢 → ((𝑣 × {𝑏}) ⊆ {𝑎 ∈ ((0[,]1) × (0[,]1)) ∣
𝐾 ∈ (((II
×t II) CnP 𝐶)‘𝑎)} ↔ (𝑢 × {𝑏}) ⊆ {𝑎 ∈ ((0[,]1) × (0[,]1)) ∣
𝐾 ∈ (((II
×t II) CnP 𝐶)‘𝑎)})) | 
| 19 |  | xpeq1 5699 | . . . . . . . . . 10
⊢ (𝑣 = 𝑢 → (𝑣 × {𝑑}) = (𝑢 × {𝑑})) | 
| 20 | 19 | sseq1d 4015 | . . . . . . . . 9
⊢ (𝑣 = 𝑢 → ((𝑣 × {𝑑}) ⊆ {𝑎 ∈ ((0[,]1) × (0[,]1)) ∣
𝐾 ∈ (((II
×t II) CnP 𝐶)‘𝑎)} ↔ (𝑢 × {𝑑}) ⊆ {𝑎 ∈ ((0[,]1) × (0[,]1)) ∣
𝐾 ∈ (((II
×t II) CnP 𝐶)‘𝑎)})) | 
| 21 | 18, 20 | bibi12d 345 | . . . . . . . 8
⊢ (𝑣 = 𝑢 → (((𝑣 × {𝑏}) ⊆ {𝑎 ∈ ((0[,]1) × (0[,]1)) ∣
𝐾 ∈ (((II
×t II) CnP 𝐶)‘𝑎)} ↔ (𝑣 × {𝑑}) ⊆ {𝑎 ∈ ((0[,]1) × (0[,]1)) ∣
𝐾 ∈ (((II
×t II) CnP 𝐶)‘𝑎)}) ↔ ((𝑢 × {𝑏}) ⊆ {𝑎 ∈ ((0[,]1) × (0[,]1)) ∣
𝐾 ∈ (((II
×t II) CnP 𝐶)‘𝑎)} ↔ (𝑢 × {𝑑}) ⊆ {𝑎 ∈ ((0[,]1) × (0[,]1)) ∣
𝐾 ∈ (((II
×t II) CnP 𝐶)‘𝑎)}))) | 
| 22 | 21 | cbvrexvw 3238 | . . . . . . 7
⊢
(∃𝑣 ∈
((nei‘II)‘{𝑐})((𝑣 × {𝑏}) ⊆ {𝑎 ∈ ((0[,]1) × (0[,]1)) ∣
𝐾 ∈ (((II
×t II) CnP 𝐶)‘𝑎)} ↔ (𝑣 × {𝑑}) ⊆ {𝑎 ∈ ((0[,]1) × (0[,]1)) ∣
𝐾 ∈ (((II
×t II) CnP 𝐶)‘𝑎)}) ↔ ∃𝑢 ∈ ((nei‘II)‘{𝑐})((𝑢 × {𝑏}) ⊆ {𝑎 ∈ ((0[,]1) × (0[,]1)) ∣
𝐾 ∈ (((II
×t II) CnP 𝐶)‘𝑎)} ↔ (𝑢 × {𝑑}) ⊆ {𝑎 ∈ ((0[,]1) × (0[,]1)) ∣
𝐾 ∈ (((II
×t II) CnP 𝐶)‘𝑎)})) | 
| 23 |  | simpl 482 | . . . . . . . . . 10
⊢ ((𝑐 = 𝑟 ∧ 𝑑 = 𝑡) → 𝑐 = 𝑟) | 
| 24 | 23 | sneqd 4638 | . . . . . . . . 9
⊢ ((𝑐 = 𝑟 ∧ 𝑑 = 𝑡) → {𝑐} = {𝑟}) | 
| 25 | 24 | fveq2d 6910 | . . . . . . . 8
⊢ ((𝑐 = 𝑟 ∧ 𝑑 = 𝑡) → ((nei‘II)‘{𝑐}) =
((nei‘II)‘{𝑟})) | 
| 26 | 15 | sneqd 4638 | . . . . . . . . . . 11
⊢ ((𝑐 = 𝑟 ∧ 𝑑 = 𝑡) → {𝑑} = {𝑡}) | 
| 27 | 26 | xpeq2d 5715 | . . . . . . . . . 10
⊢ ((𝑐 = 𝑟 ∧ 𝑑 = 𝑡) → (𝑢 × {𝑑}) = (𝑢 × {𝑡})) | 
| 28 | 27 | sseq1d 4015 | . . . . . . . . 9
⊢ ((𝑐 = 𝑟 ∧ 𝑑 = 𝑡) → ((𝑢 × {𝑑}) ⊆ {𝑎 ∈ ((0[,]1) × (0[,]1)) ∣
𝐾 ∈ (((II
×t II) CnP 𝐶)‘𝑎)} ↔ (𝑢 × {𝑡}) ⊆ {𝑎 ∈ ((0[,]1) × (0[,]1)) ∣
𝐾 ∈ (((II
×t II) CnP 𝐶)‘𝑎)})) | 
| 29 | 28 | bibi2d 342 | . . . . . . . 8
⊢ ((𝑐 = 𝑟 ∧ 𝑑 = 𝑡) → (((𝑢 × {𝑏}) ⊆ {𝑎 ∈ ((0[,]1) × (0[,]1)) ∣
𝐾 ∈ (((II
×t II) CnP 𝐶)‘𝑎)} ↔ (𝑢 × {𝑑}) ⊆ {𝑎 ∈ ((0[,]1) × (0[,]1)) ∣
𝐾 ∈ (((II
×t II) CnP 𝐶)‘𝑎)}) ↔ ((𝑢 × {𝑏}) ⊆ {𝑎 ∈ ((0[,]1) × (0[,]1)) ∣
𝐾 ∈ (((II
×t II) CnP 𝐶)‘𝑎)} ↔ (𝑢 × {𝑡}) ⊆ {𝑎 ∈ ((0[,]1) × (0[,]1)) ∣
𝐾 ∈ (((II
×t II) CnP 𝐶)‘𝑎)}))) | 
| 30 | 25, 29 | rexeqbidv 3347 | . . . . . . 7
⊢ ((𝑐 = 𝑟 ∧ 𝑑 = 𝑡) → (∃𝑢 ∈ ((nei‘II)‘{𝑐})((𝑢 × {𝑏}) ⊆ {𝑎 ∈ ((0[,]1) × (0[,]1)) ∣
𝐾 ∈ (((II
×t II) CnP 𝐶)‘𝑎)} ↔ (𝑢 × {𝑑}) ⊆ {𝑎 ∈ ((0[,]1) × (0[,]1)) ∣
𝐾 ∈ (((II
×t II) CnP 𝐶)‘𝑎)}) ↔ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑏}) ⊆ {𝑎 ∈ ((0[,]1) × (0[,]1)) ∣
𝐾 ∈ (((II
×t II) CnP 𝐶)‘𝑎)} ↔ (𝑢 × {𝑡}) ⊆ {𝑎 ∈ ((0[,]1) × (0[,]1)) ∣
𝐾 ∈ (((II
×t II) CnP 𝐶)‘𝑎)}))) | 
| 31 | 22, 30 | bitrid 283 | . . . . . 6
⊢ ((𝑐 = 𝑟 ∧ 𝑑 = 𝑡) → (∃𝑣 ∈ ((nei‘II)‘{𝑐})((𝑣 × {𝑏}) ⊆ {𝑎 ∈ ((0[,]1) × (0[,]1)) ∣
𝐾 ∈ (((II
×t II) CnP 𝐶)‘𝑎)} ↔ (𝑣 × {𝑑}) ⊆ {𝑎 ∈ ((0[,]1) × (0[,]1)) ∣
𝐾 ∈ (((II
×t II) CnP 𝐶)‘𝑎)}) ↔ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑏}) ⊆ {𝑎 ∈ ((0[,]1) × (0[,]1)) ∣
𝐾 ∈ (((II
×t II) CnP 𝐶)‘𝑎)} ↔ (𝑢 × {𝑡}) ⊆ {𝑎 ∈ ((0[,]1) × (0[,]1)) ∣
𝐾 ∈ (((II
×t II) CnP 𝐶)‘𝑎)}))) | 
| 32 | 16, 31 | anbi12d 632 | . . . . 5
⊢ ((𝑐 = 𝑟 ∧ 𝑑 = 𝑡) → ((𝑑 ∈ (0[,]1) ∧ ∃𝑣 ∈
((nei‘II)‘{𝑐})((𝑣 × {𝑏}) ⊆ {𝑎 ∈ ((0[,]1) × (0[,]1)) ∣
𝐾 ∈ (((II
×t II) CnP 𝐶)‘𝑎)} ↔ (𝑣 × {𝑑}) ⊆ {𝑎 ∈ ((0[,]1) × (0[,]1)) ∣
𝐾 ∈ (((II
×t II) CnP 𝐶)‘𝑎)})) ↔ (𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈
((nei‘II)‘{𝑟})((𝑢 × {𝑏}) ⊆ {𝑎 ∈ ((0[,]1) × (0[,]1)) ∣
𝐾 ∈ (((II
×t II) CnP 𝐶)‘𝑎)} ↔ (𝑢 × {𝑡}) ⊆ {𝑎 ∈ ((0[,]1) × (0[,]1)) ∣
𝐾 ∈ (((II
×t II) CnP 𝐶)‘𝑎)})))) | 
| 33 | 32 | cbvopabv 5216 | . . . 4
⊢
{〈𝑐, 𝑑〉 ∣ (𝑑 ∈ (0[,]1) ∧
∃𝑣 ∈
((nei‘II)‘{𝑐})((𝑣 × {𝑏}) ⊆ {𝑎 ∈ ((0[,]1) × (0[,]1)) ∣
𝐾 ∈ (((II
×t II) CnP 𝐶)‘𝑎)} ↔ (𝑣 × {𝑑}) ⊆ {𝑎 ∈ ((0[,]1) × (0[,]1)) ∣
𝐾 ∈ (((II
×t II) CnP 𝐶)‘𝑎)}))} = {〈𝑟, 𝑡〉 ∣ (𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈
((nei‘II)‘{𝑟})((𝑢 × {𝑏}) ⊆ {𝑎 ∈ ((0[,]1) × (0[,]1)) ∣
𝐾 ∈ (((II
×t II) CnP 𝐶)‘𝑎)} ↔ (𝑢 × {𝑡}) ⊆ {𝑎 ∈ ((0[,]1) × (0[,]1)) ∣
𝐾 ∈ (((II
×t II) CnP 𝐶)‘𝑎)}))} | 
| 34 | 1, 2, 3, 4, 5, 6, 7, 10, 14, 33 | cvmlift2lem12 35319 | . . 3
⊢ (𝜑 → 𝐾 ∈ ((II ×t II) Cn
𝐶)) | 
| 35 | 1, 2, 3, 4, 5, 6, 7 | cvmlift2lem7 35314 | . . 3
⊢ (𝜑 → (𝐹 ∘ 𝐾) = 𝐺) | 
| 36 |  | 0elunit 13509 | . . . . 5
⊢ 0 ∈
(0[,]1) | 
| 37 | 1, 2, 3, 4, 5, 6, 7 | cvmlift2lem8 35315 | . . . . 5
⊢ ((𝜑 ∧ 0 ∈ (0[,]1)) →
(0𝐾0) = (𝐻‘0)) | 
| 38 | 36, 37 | mpan2 691 | . . . 4
⊢ (𝜑 → (0𝐾0) = (𝐻‘0)) | 
| 39 | 1, 2, 3, 4, 5, 6 | cvmlift2lem2 35309 | . . . . 5
⊢ (𝜑 → (𝐻 ∈ (II Cn 𝐶) ∧ (𝐹 ∘ 𝐻) = (𝑧 ∈ (0[,]1) ↦ (𝑧𝐺0)) ∧ (𝐻‘0) = 𝑃)) | 
| 40 | 39 | simp3d 1145 | . . . 4
⊢ (𝜑 → (𝐻‘0) = 𝑃) | 
| 41 | 38, 40 | eqtrd 2777 | . . 3
⊢ (𝜑 → (0𝐾0) = 𝑃) | 
| 42 |  | coeq2 5869 | . . . . . 6
⊢ (𝑔 = 𝐾 → (𝐹 ∘ 𝑔) = (𝐹 ∘ 𝐾)) | 
| 43 | 42 | eqeq1d 2739 | . . . . 5
⊢ (𝑔 = 𝐾 → ((𝐹 ∘ 𝑔) = 𝐺 ↔ (𝐹 ∘ 𝐾) = 𝐺)) | 
| 44 |  | oveq 7437 | . . . . . 6
⊢ (𝑔 = 𝐾 → (0𝑔0) = (0𝐾0)) | 
| 45 | 44 | eqeq1d 2739 | . . . . 5
⊢ (𝑔 = 𝐾 → ((0𝑔0) = 𝑃 ↔ (0𝐾0) = 𝑃)) | 
| 46 | 43, 45 | anbi12d 632 | . . . 4
⊢ (𝑔 = 𝐾 → (((𝐹 ∘ 𝑔) = 𝐺 ∧ (0𝑔0) = 𝑃) ↔ ((𝐹 ∘ 𝐾) = 𝐺 ∧ (0𝐾0) = 𝑃))) | 
| 47 | 46 | rspcev 3622 | . . 3
⊢ ((𝐾 ∈ ((II ×t
II) Cn 𝐶) ∧ ((𝐹 ∘ 𝐾) = 𝐺 ∧ (0𝐾0) = 𝑃)) → ∃𝑔 ∈ ((II ×t II) Cn 𝐶)((𝐹 ∘ 𝑔) = 𝐺 ∧ (0𝑔0) = 𝑃)) | 
| 48 | 34, 35, 41, 47 | syl12anc 837 | . 2
⊢ (𝜑 → ∃𝑔 ∈ ((II ×t II) Cn 𝐶)((𝐹 ∘ 𝑔) = 𝐺 ∧ (0𝑔0) = 𝑃)) | 
| 49 |  | iitop 24906 | . . . . 5
⊢ II ∈
Top | 
| 50 |  | iiuni 24907 | . . . . 5
⊢ (0[,]1) =
∪ II | 
| 51 | 49, 49, 50, 50 | txunii 23601 | . . . 4
⊢ ((0[,]1)
× (0[,]1)) = ∪ (II ×t
II) | 
| 52 |  | iiconn 24913 | . . . . . 6
⊢ II ∈
Conn | 
| 53 |  | txconn 23697 | . . . . . 6
⊢ ((II
∈ Conn ∧ II ∈ Conn) → (II ×t II) ∈
Conn) | 
| 54 | 52, 52, 53 | mp2an 692 | . . . . 5
⊢ (II
×t II) ∈ Conn | 
| 55 | 54 | a1i 11 | . . . 4
⊢ (𝜑 → (II ×t
II) ∈ Conn) | 
| 56 |  | iinllyconn 35259 | . . . . . 6
⊢ II ∈
𝑛-Locally Conn | 
| 57 |  | txconn 23697 | . . . . . . 7
⊢ ((𝑥 ∈ Conn ∧ 𝑦 ∈ Conn) → (𝑥 ×t 𝑦) ∈ Conn) | 
| 58 | 57 | txnlly 23645 | . . . . . 6
⊢ ((II
∈ 𝑛-Locally Conn ∧ II ∈ 𝑛-Locally Conn) →
(II ×t II) ∈ 𝑛-Locally Conn) | 
| 59 | 56, 56, 58 | mp2an 692 | . . . . 5
⊢ (II
×t II) ∈ 𝑛-Locally Conn | 
| 60 | 59 | a1i 11 | . . . 4
⊢ (𝜑 → (II ×t
II) ∈ 𝑛-Locally Conn) | 
| 61 |  | opelxpi 5722 | . . . . . 6
⊢ ((0
∈ (0[,]1) ∧ 0 ∈ (0[,]1)) → 〈0, 0〉 ∈ ((0[,]1)
× (0[,]1))) | 
| 62 | 36, 36, 61 | mp2an 692 | . . . . 5
⊢ 〈0,
0〉 ∈ ((0[,]1) × (0[,]1)) | 
| 63 | 62 | a1i 11 | . . . 4
⊢ (𝜑 → 〈0, 0〉 ∈
((0[,]1) × (0[,]1))) | 
| 64 |  | df-ov 7434 | . . . . 5
⊢ (0𝐺0) = (𝐺‘〈0, 0〉) | 
| 65 | 5, 64 | eqtrdi 2793 | . . . 4
⊢ (𝜑 → (𝐹‘𝑃) = (𝐺‘〈0, 0〉)) | 
| 66 | 1, 51, 2, 55, 60, 63, 3, 4, 65 | cvmliftmo 35289 | . . 3
⊢ (𝜑 → ∃*𝑔 ∈ ((II ×t II) Cn 𝐶)((𝐹 ∘ 𝑔) = 𝐺 ∧ (𝑔‘〈0, 0〉) = 𝑃)) | 
| 67 |  | df-ov 7434 | . . . . . 6
⊢ (0𝑔0) = (𝑔‘〈0, 0〉) | 
| 68 | 67 | eqeq1i 2742 | . . . . 5
⊢ ((0𝑔0) = 𝑃 ↔ (𝑔‘〈0, 0〉) = 𝑃) | 
| 69 | 68 | anbi2i 623 | . . . 4
⊢ (((𝐹 ∘ 𝑔) = 𝐺 ∧ (0𝑔0) = 𝑃) ↔ ((𝐹 ∘ 𝑔) = 𝐺 ∧ (𝑔‘〈0, 0〉) = 𝑃)) | 
| 70 | 69 | rmobii 3388 | . . 3
⊢
(∃*𝑔 ∈
((II ×t II) Cn 𝐶)((𝐹 ∘ 𝑔) = 𝐺 ∧ (0𝑔0) = 𝑃) ↔ ∃*𝑔 ∈ ((II ×t II) Cn 𝐶)((𝐹 ∘ 𝑔) = 𝐺 ∧ (𝑔‘〈0, 0〉) = 𝑃)) | 
| 71 | 66, 70 | sylibr 234 | . 2
⊢ (𝜑 → ∃*𝑔 ∈ ((II ×t II) Cn 𝐶)((𝐹 ∘ 𝑔) = 𝐺 ∧ (0𝑔0) = 𝑃)) | 
| 72 |  | reu5 3382 | . 2
⊢
(∃!𝑔 ∈
((II ×t II) Cn 𝐶)((𝐹 ∘ 𝑔) = 𝐺 ∧ (0𝑔0) = 𝑃) ↔ (∃𝑔 ∈ ((II ×t II) Cn 𝐶)((𝐹 ∘ 𝑔) = 𝐺 ∧ (0𝑔0) = 𝑃) ∧ ∃*𝑔 ∈ ((II ×t II) Cn 𝐶)((𝐹 ∘ 𝑔) = 𝐺 ∧ (0𝑔0) = 𝑃))) | 
| 73 | 48, 71, 72 | sylanbrc 583 | 1
⊢ (𝜑 → ∃!𝑔 ∈ ((II ×t II) Cn 𝐶)((𝐹 ∘ 𝑔) = 𝐺 ∧ (0𝑔0) = 𝑃)) |