Users' Mathboxes Mathbox for Mario Carneiro < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  cvmlift2lem9 Structured version   Visualization version   GIF version

Theorem cvmlift2lem9 32632
Description: Lemma for cvmlift2 32637. (Contributed by Mario Carneiro, 1-Jun-2015.)
Hypotheses
Ref Expression
cvmlift2.b 𝐵 = 𝐶
cvmlift2.f (𝜑𝐹 ∈ (𝐶 CovMap 𝐽))
cvmlift2.g (𝜑𝐺 ∈ ((II ×t II) Cn 𝐽))
cvmlift2.p (𝜑𝑃𝐵)
cvmlift2.i (𝜑 → (𝐹𝑃) = (0𝐺0))
cvmlift2.h 𝐻 = (𝑓 ∈ (II Cn 𝐶)((𝐹𝑓) = (𝑧 ∈ (0[,]1) ↦ (𝑧𝐺0)) ∧ (𝑓‘0) = 𝑃))
cvmlift2.k 𝐾 = (𝑥 ∈ (0[,]1), 𝑦 ∈ (0[,]1) ↦ ((𝑓 ∈ (II Cn 𝐶)((𝐹𝑓) = (𝑧 ∈ (0[,]1) ↦ (𝑥𝐺𝑧)) ∧ (𝑓‘0) = (𝐻𝑥)))‘𝑦))
cvmlift2lem10.s 𝑆 = (𝑘𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ ( 𝑠 = (𝐹𝑘) ∧ ∀𝑐𝑠 (∀𝑑 ∈ (𝑠 ∖ {𝑐})(𝑐𝑑) = ∅ ∧ (𝐹𝑐) ∈ ((𝐶t 𝑐)Homeo(𝐽t 𝑘))))})
cvmlift2lem9.1 (𝜑 → (𝑋𝐺𝑌) ∈ 𝑀)
cvmlift2lem9.2 (𝜑𝑇 ∈ (𝑆𝑀))
cvmlift2lem9.3 (𝜑𝑈 ∈ II)
cvmlift2lem9.4 (𝜑𝑉 ∈ II)
cvmlift2lem9.5 (𝜑 → (II ↾t 𝑈) ∈ Conn)
cvmlift2lem9.6 (𝜑 → (II ↾t 𝑉) ∈ Conn)
cvmlift2lem9.7 (𝜑𝑋𝑈)
cvmlift2lem9.8 (𝜑𝑌𝑉)
cvmlift2lem9.9 (𝜑 → (𝑈 × 𝑉) ⊆ (𝐺𝑀))
cvmlift2lem9.10 (𝜑𝑍𝑉)
cvmlift2lem9.11 (𝜑 → (𝐾 ↾ (𝑈 × {𝑍})) ∈ (((II ×t II) ↾t (𝑈 × {𝑍})) Cn 𝐶))
cvmlift2lem9.w 𝑊 = (𝑏𝑇 (𝑋𝐾𝑌) ∈ 𝑏)
Assertion
Ref Expression
cvmlift2lem9 (𝜑 → (𝐾 ↾ (𝑈 × 𝑉)) ∈ (((II ×t II) ↾t (𝑈 × 𝑉)) Cn 𝐶))
Distinct variable groups:   𝑏,𝑐,𝑑,𝑓,𝑘,𝑠,𝑥,𝑦,𝑧,𝐹   𝜑,𝑏,𝑓,𝑥,𝑦,𝑧   𝑀,𝑏,𝑐,𝑑,𝑘,𝑠,𝑥,𝑦,𝑧   𝑆,𝑏,𝑓,𝑥,𝑦,𝑧   𝐽,𝑏,𝑐,𝑑,𝑓,𝑘,𝑠,𝑥,𝑦,𝑧   𝑇,𝑏,𝑐,𝑑,𝑠   𝑧,𝑈   𝐺,𝑏,𝑐,𝑓,𝑘,𝑥,𝑦,𝑧   𝑊,𝑐,𝑑   𝐻,𝑏,𝑐,𝑓,𝑥,𝑦,𝑧   𝑋,𝑏,𝑐,𝑑,𝑓,𝑘,𝑥,𝑦,𝑧   𝑧,𝑍   𝐶,𝑏,𝑐,𝑑,𝑓,𝑘,𝑠,𝑥,𝑦,𝑧   𝑃,𝑓,𝑘,𝑥,𝑦,𝑧   𝐵,𝑏,𝑐,𝑑,𝑥,𝑦,𝑧   𝑌,𝑏,𝑐,𝑑,𝑓,𝑘,𝑥,𝑦,𝑧   𝐾,𝑏,𝑐,𝑑,𝑓,𝑥,𝑦,𝑧
Allowed substitution hints:   𝜑(𝑘,𝑠,𝑐,𝑑)   𝐵(𝑓,𝑘,𝑠)   𝑃(𝑠,𝑏,𝑐,𝑑)   𝑆(𝑘,𝑠,𝑐,𝑑)   𝑇(𝑥,𝑦,𝑧,𝑓,𝑘)   𝑈(𝑥,𝑦,𝑓,𝑘,𝑠,𝑏,𝑐,𝑑)   𝐺(𝑠,𝑑)   𝐻(𝑘,𝑠,𝑑)   𝐾(𝑘,𝑠)   𝑀(𝑓)   𝑉(𝑥,𝑦,𝑧,𝑓,𝑘,𝑠,𝑏,𝑐,𝑑)   𝑊(𝑥,𝑦,𝑧,𝑓,𝑘,𝑠,𝑏)   𝑋(𝑠)   𝑌(𝑠)   𝑍(𝑥,𝑦,𝑓,𝑘,𝑠,𝑏,𝑐,𝑑)

Proof of Theorem cvmlift2lem9
Dummy variables 𝑚 𝑛 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 cvmlift2.b . 2 𝐵 = 𝐶
2 iitop 23483 . . 3 II ∈ Top
3 iiuni 23484 . . 3 (0[,]1) = II
42, 2, 3, 3txunii 22196 . 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) = (𝐻𝑥)))‘𝑦))
121, 6, 7, 8, 9, 10, 11cvmlift2lem5 32628 . 2 (𝜑𝐾:((0[,]1) × (0[,]1))⟶𝐵)
131, 6, 7, 8, 9, 10, 11cvmlift2lem7 32630 . . 3 (𝜑 → (𝐹𝐾) = 𝐺)
1413, 7eqeltrd 2914 . 2 (𝜑 → (𝐹𝐾) ∈ ((II ×t II) Cn 𝐽))
152, 2txtopi 22193 . . 3 (II ×t II) ∈ Top
1615a1i 11 . 2 (𝜑 → (II ×t II) ∈ Top)
17 cvmlift2lem9.3 . . . . 5 (𝜑𝑈 ∈ II)
18 elssuni 4843 . . . . . 6 (𝑈 ∈ II → 𝑈 II)
1918, 3sseqtrrdi 3993 . . . . 5 (𝑈 ∈ II → 𝑈 ⊆ (0[,]1))
2017, 19syl 17 . . . 4 (𝜑𝑈 ⊆ (0[,]1))
21 cvmlift2lem9.7 . . . 4 (𝜑𝑋𝑈)
2220, 21sseldd 3943 . . 3 (𝜑𝑋 ∈ (0[,]1))
23 cvmlift2lem9.4 . . . . 5 (𝜑𝑉 ∈ II)
24 elssuni 4843 . . . . . 6 (𝑉 ∈ II → 𝑉 II)
2524, 3sseqtrrdi 3993 . . . . 5 (𝑉 ∈ II → 𝑉 ⊆ (0[,]1))
2623, 25syl 17 . . . 4 (𝜑𝑉 ⊆ (0[,]1))
27 cvmlift2lem9.8 . . . 4 (𝜑𝑌𝑉)
2826, 27sseldd 3943 . . 3 (𝜑𝑌 ∈ (0[,]1))
29 opelxpi 5569 . . 3 ((𝑋 ∈ (0[,]1) ∧ 𝑌 ∈ (0[,]1)) → ⟨𝑋, 𝑌⟩ ∈ ((0[,]1) × (0[,]1)))
3022, 28, 29syl2anc 587 . 2 (𝜑 → ⟨𝑋, 𝑌⟩ ∈ ((0[,]1) × (0[,]1)))
31 cvmlift2lem9.2 . 2 (𝜑𝑇 ∈ (𝑆𝑀))
3212, 22, 28fovrnd 7305 . . . 4 (𝜑 → (𝑋𝐾𝑌) ∈ 𝐵)
33 fvco3 6742 . . . . . . . 8 ((𝐾:((0[,]1) × (0[,]1))⟶𝐵 ∧ ⟨𝑋, 𝑌⟩ ∈ ((0[,]1) × (0[,]1))) → ((𝐹𝐾)‘⟨𝑋, 𝑌⟩) = (𝐹‘(𝐾‘⟨𝑋, 𝑌⟩)))
3412, 30, 33syl2anc 587 . . . . . . 7 (𝜑 → ((𝐹𝐾)‘⟨𝑋, 𝑌⟩) = (𝐹‘(𝐾‘⟨𝑋, 𝑌⟩)))
3513fveq1d 6654 . . . . . . 7 (𝜑 → ((𝐹𝐾)‘⟨𝑋, 𝑌⟩) = (𝐺‘⟨𝑋, 𝑌⟩))
3634, 35eqtr3d 2859 . . . . . 6 (𝜑 → (𝐹‘(𝐾‘⟨𝑋, 𝑌⟩)) = (𝐺‘⟨𝑋, 𝑌⟩))
37 df-ov 7143 . . . . . . 7 (𝑋𝐾𝑌) = (𝐾‘⟨𝑋, 𝑌⟩)
3837fveq2i 6655 . . . . . 6 (𝐹‘(𝑋𝐾𝑌)) = (𝐹‘(𝐾‘⟨𝑋, 𝑌⟩))
39 df-ov 7143 . . . . . 6 (𝑋𝐺𝑌) = (𝐺‘⟨𝑋, 𝑌⟩)
4036, 38, 393eqtr4g 2882 . . . . 5 (𝜑 → (𝐹‘(𝑋𝐾𝑌)) = (𝑋𝐺𝑌))
41 cvmlift2lem9.1 . . . . 5 (𝜑 → (𝑋𝐺𝑌) ∈ 𝑀)
4240, 41eqeltrd 2914 . . . 4 (𝜑 → (𝐹‘(𝑋𝐾𝑌)) ∈ 𝑀)
43 cvmlift2lem9.w . . . . 5 𝑊 = (𝑏𝑇 (𝑋𝐾𝑌) ∈ 𝑏)
445, 1, 43cvmsiota 32598 . . . 4 ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ (𝑇 ∈ (𝑆𝑀) ∧ (𝑋𝐾𝑌) ∈ 𝐵 ∧ (𝐹‘(𝑋𝐾𝑌)) ∈ 𝑀)) → (𝑊𝑇 ∧ (𝑋𝐾𝑌) ∈ 𝑊))
456, 31, 32, 42, 44syl13anc 1369 . . 3 (𝜑 → (𝑊𝑇 ∧ (𝑋𝐾𝑌) ∈ 𝑊))
4637eleq1i 2904 . . . 4 ((𝑋𝐾𝑌) ∈ 𝑊 ↔ (𝐾‘⟨𝑋, 𝑌⟩) ∈ 𝑊)
4746anbi2i 625 . . 3 ((𝑊𝑇 ∧ (𝑋𝐾𝑌) ∈ 𝑊) ↔ (𝑊𝑇 ∧ (𝐾‘⟨𝑋, 𝑌⟩) ∈ 𝑊))
4845, 47sylib 221 . 2 (𝜑 → (𝑊𝑇 ∧ (𝐾‘⟨𝑋, 𝑌⟩) ∈ 𝑊))
49 xpss12 5547 . . 3 ((𝑈 ⊆ (0[,]1) ∧ 𝑉 ⊆ (0[,]1)) → (𝑈 × 𝑉) ⊆ ((0[,]1) × (0[,]1)))
5020, 26, 49syl2anc 587 . 2 (𝜑 → (𝑈 × 𝑉) ⊆ ((0[,]1) × (0[,]1)))
51 snidg 4573 . . . . . . 7 (𝑚𝑈𝑚 ∈ {𝑚})
5251ad2antrl 727 . . . . . 6 ((𝜑 ∧ (𝑚𝑈𝑛𝑉)) → 𝑚 ∈ {𝑚})
53 simprr 772 . . . . . 6 ((𝜑 ∧ (𝑚𝑈𝑛𝑉)) → 𝑛𝑉)
54 ovres 7299 . . . . . 6 ((𝑚 ∈ {𝑚} ∧ 𝑛𝑉) → (𝑚(𝐾 ↾ ({𝑚} × 𝑉))𝑛) = (𝑚𝐾𝑛))
5552, 53, 54syl2anc 587 . . . . 5 ((𝜑 ∧ (𝑚𝑈𝑛𝑉)) → (𝑚(𝐾 ↾ ({𝑚} × 𝑉))𝑛) = (𝑚𝐾𝑛))
56 eqid 2822 . . . . . . . 8 ((II ×t II) ↾t ({𝑚} × 𝑉)) = ((II ×t II) ↾t ({𝑚} × 𝑉))
572a1i 11 . . . . . . . . . 10 ((𝜑 ∧ (𝑚𝑈𝑛𝑉)) → II ∈ Top)
58 snex 5309 . . . . . . . . . . 11 {𝑚} ∈ V
5958a1i 11 . . . . . . . . . 10 ((𝜑 ∧ (𝑚𝑈𝑛𝑉)) → {𝑚} ∈ V)
6023adantr 484 . . . . . . . . . 10 ((𝜑 ∧ (𝑚𝑈𝑛𝑉)) → 𝑉 ∈ II)
61 txrest 22234 . . . . . . . . . 10 (((II ∈ Top ∧ II ∈ Top) ∧ ({𝑚} ∈ V ∧ 𝑉 ∈ II)) → ((II ×t II) ↾t ({𝑚} × 𝑉)) = ((II ↾t {𝑚}) ×t (II ↾t 𝑉)))
6257, 57, 59, 60, 61syl22anc 837 . . . . . . . . 9 ((𝜑 ∧ (𝑚𝑈𝑛𝑉)) → ((II ×t II) ↾t ({𝑚} × 𝑉)) = ((II ↾t {𝑚}) ×t (II ↾t 𝑉)))
63 iitopon 23482 . . . . . . . . . . . 12 II ∈ (TopOn‘(0[,]1))
6420sselda 3942 . . . . . . . . . . . . 13 ((𝜑𝑚𝑈) → 𝑚 ∈ (0[,]1))
6564adantrr 716 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑚𝑈𝑛𝑉)) → 𝑚 ∈ (0[,]1))
66 restsn2 21774 . . . . . . . . . . . 12 ((II ∈ (TopOn‘(0[,]1)) ∧ 𝑚 ∈ (0[,]1)) → (II ↾t {𝑚}) = 𝒫 {𝑚})
6763, 65, 66sylancr 590 . . . . . . . . . . 11 ((𝜑 ∧ (𝑚𝑈𝑛𝑉)) → (II ↾t {𝑚}) = 𝒫 {𝑚})
68 pwsn 4805 . . . . . . . . . . . 12 𝒫 {𝑚} = {∅, {𝑚}}
69 indisconn 22021 . . . . . . . . . . . 12 {∅, {𝑚}} ∈ Conn
7068, 69eqeltri 2910 . . . . . . . . . . 11 𝒫 {𝑚} ∈ Conn
7167, 70eqeltrdi 2922 . . . . . . . . . 10 ((𝜑 ∧ (𝑚𝑈𝑛𝑉)) → (II ↾t {𝑚}) ∈ Conn)
72 cvmlift2lem9.6 . . . . . . . . . . 11 (𝜑 → (II ↾t 𝑉) ∈ Conn)
7372adantr 484 . . . . . . . . . 10 ((𝜑 ∧ (𝑚𝑈𝑛𝑉)) → (II ↾t 𝑉) ∈ Conn)
74 txconn 22292 . . . . . . . . . 10 (((II ↾t {𝑚}) ∈ Conn ∧ (II ↾t 𝑉) ∈ Conn) → ((II ↾t {𝑚}) ×t (II ↾t 𝑉)) ∈ Conn)
7571, 73, 74syl2anc 587 . . . . . . . . 9 ((𝜑 ∧ (𝑚𝑈𝑛𝑉)) → ((II ↾t {𝑚}) ×t (II ↾t 𝑉)) ∈ Conn)
7662, 75eqeltrd 2914 . . . . . . . 8 ((𝜑 ∧ (𝑚𝑈𝑛𝑉)) → ((II ×t II) ↾t ({𝑚} × 𝑉)) ∈ Conn)
771, 6, 7, 8, 9, 10, 11cvmlift2lem6 32629 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ (0[,]1)) → (𝐾 ↾ ({𝑚} × (0[,]1))) ∈ (((II ×t II) ↾t ({𝑚} × (0[,]1))) Cn 𝐶))
7865, 77syldan 594 . . . . . . . . . . 11 ((𝜑 ∧ (𝑚𝑈𝑛𝑉)) → (𝐾 ↾ ({𝑚} × (0[,]1))) ∈ (((II ×t II) ↾t ({𝑚} × (0[,]1))) Cn 𝐶))
7926adantr 484 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑚𝑈𝑛𝑉)) → 𝑉 ⊆ (0[,]1))
80 xpss2 5552 . . . . . . . . . . . . 13 (𝑉 ⊆ (0[,]1) → ({𝑚} × 𝑉) ⊆ ({𝑚} × (0[,]1)))
8179, 80syl 17 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑚𝑈𝑛𝑉)) → ({𝑚} × 𝑉) ⊆ ({𝑚} × (0[,]1)))
8265snssd 4715 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑚𝑈𝑛𝑉)) → {𝑚} ⊆ (0[,]1))
83 xpss1 5551 . . . . . . . . . . . . . 14 ({𝑚} ⊆ (0[,]1) → ({𝑚} × (0[,]1)) ⊆ ((0[,]1) × (0[,]1)))
8482, 83syl 17 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑚𝑈𝑛𝑉)) → ({𝑚} × (0[,]1)) ⊆ ((0[,]1) × (0[,]1)))
854restuni 21765 . . . . . . . . . . . . 13 (((II ×t II) ∈ Top ∧ ({𝑚} × (0[,]1)) ⊆ ((0[,]1) × (0[,]1))) → ({𝑚} × (0[,]1)) = ((II ×t II) ↾t ({𝑚} × (0[,]1))))
8615, 84, 85sylancr 590 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑚𝑈𝑛𝑉)) → ({𝑚} × (0[,]1)) = ((II ×t II) ↾t ({𝑚} × (0[,]1))))
8781, 86sseqtrd 3982 . . . . . . . . . . 11 ((𝜑 ∧ (𝑚𝑈𝑛𝑉)) → ({𝑚} × 𝑉) ⊆ ((II ×t II) ↾t ({𝑚} × (0[,]1))))
88 eqid 2822 . . . . . . . . . . . 12 ((II ×t II) ↾t ({𝑚} × (0[,]1))) = ((II ×t II) ↾t ({𝑚} × (0[,]1)))
8988cnrest 21888 . . . . . . . . . . 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 𝐶))
9078, 87, 89syl2anc 587 . . . . . . . . . 10 ((𝜑 ∧ (𝑚𝑈𝑛𝑉)) → ((𝐾 ↾ ({𝑚} × (0[,]1))) ↾ ({𝑚} × 𝑉)) ∈ ((((II ×t II) ↾t ({𝑚} × (0[,]1))) ↾t ({𝑚} × 𝑉)) Cn 𝐶))
9181resabs1d 5862 . . . . . . . . . 10 ((𝜑 ∧ (𝑚𝑈𝑛𝑉)) → ((𝐾 ↾ ({𝑚} × (0[,]1))) ↾ ({𝑚} × 𝑉)) = (𝐾 ↾ ({𝑚} × 𝑉)))
9215a1i 11 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑚𝑈𝑛𝑉)) → (II ×t II) ∈ Top)
93 ovex 7173 . . . . . . . . . . . . . 14 (0[,]1) ∈ V
9458, 93xpex 7461 . . . . . . . . . . . . 13 ({𝑚} × (0[,]1)) ∈ V
9594a1i 11 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑚𝑈𝑛𝑉)) → ({𝑚} × (0[,]1)) ∈ V)
96 restabs 21768 . . . . . . . . . . . 12 (((II ×t II) ∈ Top ∧ ({𝑚} × 𝑉) ⊆ ({𝑚} × (0[,]1)) ∧ ({𝑚} × (0[,]1)) ∈ V) → (((II ×t II) ↾t ({𝑚} × (0[,]1))) ↾t ({𝑚} × 𝑉)) = ((II ×t II) ↾t ({𝑚} × 𝑉)))
9792, 81, 95, 96syl3anc 1368 . . . . . . . . . . 11 ((𝜑 ∧ (𝑚𝑈𝑛𝑉)) → (((II ×t II) ↾t ({𝑚} × (0[,]1))) ↾t ({𝑚} × 𝑉)) = ((II ×t II) ↾t ({𝑚} × 𝑉)))
9897oveq1d 7155 . . . . . . . . . 10 ((𝜑 ∧ (𝑚𝑈𝑛𝑉)) → ((((II ×t II) ↾t ({𝑚} × (0[,]1))) ↾t ({𝑚} × 𝑉)) Cn 𝐶) = (((II ×t II) ↾t ({𝑚} × 𝑉)) Cn 𝐶))
9990, 91, 983eltr3d 2928 . . . . . . . . 9 ((𝜑 ∧ (𝑚𝑈𝑛𝑉)) → (𝐾 ↾ ({𝑚} × 𝑉)) ∈ (((II ×t II) ↾t ({𝑚} × 𝑉)) Cn 𝐶))
100 cvmtop1 32581 . . . . . . . . . . . . 13 (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐶 ∈ Top)
1016, 100syl 17 . . . . . . . . . . . 12 (𝜑𝐶 ∈ Top)
102101adantr 484 . . . . . . . . . . 11 ((𝜑 ∧ (𝑚𝑈𝑛𝑉)) → 𝐶 ∈ Top)
1031toptopon 21520 . . . . . . . . . . 11 (𝐶 ∈ Top ↔ 𝐶 ∈ (TopOn‘𝐵))
104102, 103sylib 221 . . . . . . . . . 10 ((𝜑 ∧ (𝑚𝑈𝑛𝑉)) → 𝐶 ∈ (TopOn‘𝐵))
105 df-ima 5545 . . . . . . . . . . 11 (𝐾 “ ({𝑚} × 𝑉)) = ran (𝐾 ↾ ({𝑚} × 𝑉))
106 simprl 770 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑚𝑈𝑛𝑉)) → 𝑚𝑈)
107106snssd 4715 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑚𝑈𝑛𝑉)) → {𝑚} ⊆ 𝑈)
108 xpss1 5551 . . . . . . . . . . . . 13 ({𝑚} ⊆ 𝑈 → ({𝑚} × 𝑉) ⊆ (𝑈 × 𝑉))
109 imass2 5943 . . . . . . . . . . . . 13 (({𝑚} × 𝑉) ⊆ (𝑈 × 𝑉) → (𝐾 “ ({𝑚} × 𝑉)) ⊆ (𝐾 “ (𝑈 × 𝑉)))
110107, 108, 1093syl 18 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑚𝑈𝑛𝑉)) → (𝐾 “ ({𝑚} × 𝑉)) ⊆ (𝐾 “ (𝑈 × 𝑉)))
111 cvmlift2lem9.9 . . . . . . . . . . . . . . 15 (𝜑 → (𝑈 × 𝑉) ⊆ (𝐺𝑀))
112 imaco 6082 . . . . . . . . . . . . . . . 16 ((𝐾𝐹) “ 𝑀) = (𝐾 “ (𝐹𝑀))
113 cnvco 5733 . . . . . . . . . . . . . . . . . 18 (𝐹𝐾) = (𝐾𝐹)
11413cnveqd 5723 . . . . . . . . . . . . . . . . . 18 (𝜑(𝐹𝐾) = 𝐺)
115113, 114syl5eqr 2871 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐾𝐹) = 𝐺)
116115imaeq1d 5906 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐾𝐹) “ 𝑀) = (𝐺𝑀))
117112, 116syl5eqr 2871 . . . . . . . . . . . . . . 15 (𝜑 → (𝐾 “ (𝐹𝑀)) = (𝐺𝑀))
118111, 117sseqtrrd 3983 . . . . . . . . . . . . . 14 (𝜑 → (𝑈 × 𝑉) ⊆ (𝐾 “ (𝐹𝑀)))
11912ffund 6498 . . . . . . . . . . . . . . 15 (𝜑 → Fun 𝐾)
12012fdmd 6504 . . . . . . . . . . . . . . . 16 (𝜑 → dom 𝐾 = ((0[,]1) × (0[,]1)))
12150, 120sseqtrrd 3983 . . . . . . . . . . . . . . 15 (𝜑 → (𝑈 × 𝑉) ⊆ dom 𝐾)
122 funimass3 6806 . . . . . . . . . . . . . . 15 ((Fun 𝐾 ∧ (𝑈 × 𝑉) ⊆ dom 𝐾) → ((𝐾 “ (𝑈 × 𝑉)) ⊆ (𝐹𝑀) ↔ (𝑈 × 𝑉) ⊆ (𝐾 “ (𝐹𝑀))))
123119, 121, 122syl2anc 587 . . . . . . . . . . . . . 14 (𝜑 → ((𝐾 “ (𝑈 × 𝑉)) ⊆ (𝐹𝑀) ↔ (𝑈 × 𝑉) ⊆ (𝐾 “ (𝐹𝑀))))
124118, 123mpbird 260 . . . . . . . . . . . . 13 (𝜑 → (𝐾 “ (𝑈 × 𝑉)) ⊆ (𝐹𝑀))
125124adantr 484 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑚𝑈𝑛𝑉)) → (𝐾 “ (𝑈 × 𝑉)) ⊆ (𝐹𝑀))
126110, 125sstrd 3952 . . . . . . . . . . 11 ((𝜑 ∧ (𝑚𝑈𝑛𝑉)) → (𝐾 “ ({𝑚} × 𝑉)) ⊆ (𝐹𝑀))
127105, 126eqsstrrid 3991 . . . . . . . . . 10 ((𝜑 ∧ (𝑚𝑈𝑛𝑉)) → ran (𝐾 ↾ ({𝑚} × 𝑉)) ⊆ (𝐹𝑀))
128 cnvimass 5927 . . . . . . . . . . . 12 (𝐹𝑀) ⊆ dom 𝐹
129 cvmcn 32583 . . . . . . . . . . . . . 14 (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐹 ∈ (𝐶 Cn 𝐽))
1306, 129syl 17 . . . . . . . . . . . . 13 (𝜑𝐹 ∈ (𝐶 Cn 𝐽))
131 eqid 2822 . . . . . . . . . . . . . 14 𝐽 = 𝐽
1321, 131cnf 21849 . . . . . . . . . . . . 13 (𝐹 ∈ (𝐶 Cn 𝐽) → 𝐹:𝐵 𝐽)
133 fdm 6502 . . . . . . . . . . . . 13 (𝐹:𝐵 𝐽 → dom 𝐹 = 𝐵)
134130, 132, 1333syl 18 . . . . . . . . . . . 12 (𝜑 → dom 𝐹 = 𝐵)
135128, 134sseqtrid 3994 . . . . . . . . . . 11 (𝜑 → (𝐹𝑀) ⊆ 𝐵)
136135adantr 484 . . . . . . . . . 10 ((𝜑 ∧ (𝑚𝑈𝑛𝑉)) → (𝐹𝑀) ⊆ 𝐵)
137 cnrest2 21889 . . . . . . . . . 10 ((𝐶 ∈ (TopOn‘𝐵) ∧ ran (𝐾 ↾ ({𝑚} × 𝑉)) ⊆ (𝐹𝑀) ∧ (𝐹𝑀) ⊆ 𝐵) → ((𝐾 ↾ ({𝑚} × 𝑉)) ∈ (((II ×t II) ↾t ({𝑚} × 𝑉)) Cn 𝐶) ↔ (𝐾 ↾ ({𝑚} × 𝑉)) ∈ (((II ×t II) ↾t ({𝑚} × 𝑉)) Cn (𝐶t (𝐹𝑀)))))
138104, 127, 136, 137syl3anc 1368 . . . . . . . . 9 ((𝜑 ∧ (𝑚𝑈𝑛𝑉)) → ((𝐾 ↾ ({𝑚} × 𝑉)) ∈ (((II ×t II) ↾t ({𝑚} × 𝑉)) Cn 𝐶) ↔ (𝐾 ↾ ({𝑚} × 𝑉)) ∈ (((II ×t II) ↾t ({𝑚} × 𝑉)) Cn (𝐶t (𝐹𝑀)))))
13999, 138mpbid 235 . . . . . . . 8 ((𝜑 ∧ (𝑚𝑈𝑛𝑉)) → (𝐾 ↾ ({𝑚} × 𝑉)) ∈ (((II ×t II) ↾t ({𝑚} × 𝑉)) Cn (𝐶t (𝐹𝑀))))
1405cvmsss 32588 . . . . . . . . . . . 12 (𝑇 ∈ (𝑆𝑀) → 𝑇𝐶)
14131, 140syl 17 . . . . . . . . . . 11 (𝜑𝑇𝐶)
14245simpld 498 . . . . . . . . . . 11 (𝜑𝑊𝑇)
143141, 142sseldd 3943 . . . . . . . . . 10 (𝜑𝑊𝐶)
144 elssuni 4843 . . . . . . . . . . . 12 (𝑊𝑇𝑊 𝑇)
145142, 144syl 17 . . . . . . . . . . 11 (𝜑𝑊 𝑇)
1465cvmsuni 32590 . . . . . . . . . . . 12 (𝑇 ∈ (𝑆𝑀) → 𝑇 = (𝐹𝑀))
14731, 146syl 17 . . . . . . . . . . 11 (𝜑 𝑇 = (𝐹𝑀))
148145, 147sseqtrd 3982 . . . . . . . . . 10 (𝜑𝑊 ⊆ (𝐹𝑀))
1495cvmsrcl 32585 . . . . . . . . . . . . 13 (𝑇 ∈ (𝑆𝑀) → 𝑀𝐽)
15031, 149syl 17 . . . . . . . . . . . 12 (𝜑𝑀𝐽)
151 cnima 21868 . . . . . . . . . . . 12 ((𝐹 ∈ (𝐶 Cn 𝐽) ∧ 𝑀𝐽) → (𝐹𝑀) ∈ 𝐶)
152130, 150, 151syl2anc 587 . . . . . . . . . . 11 (𝜑 → (𝐹𝑀) ∈ 𝐶)
153 restopn2 21780 . . . . . . . . . . 11 ((𝐶 ∈ Top ∧ (𝐹𝑀) ∈ 𝐶) → (𝑊 ∈ (𝐶t (𝐹𝑀)) ↔ (𝑊𝐶𝑊 ⊆ (𝐹𝑀))))
154101, 152, 153syl2anc 587 . . . . . . . . . 10 (𝜑 → (𝑊 ∈ (𝐶t (𝐹𝑀)) ↔ (𝑊𝐶𝑊 ⊆ (𝐹𝑀))))
155143, 148, 154mpbir2and 712 . . . . . . . . 9 (𝜑𝑊 ∈ (𝐶t (𝐹𝑀)))
156155adantr 484 . . . . . . . 8 ((𝜑 ∧ (𝑚𝑈𝑛𝑉)) → 𝑊 ∈ (𝐶t (𝐹𝑀)))
1575cvmscld 32594 . . . . . . . . . 10 ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑇 ∈ (𝑆𝑀) ∧ 𝑊𝑇) → 𝑊 ∈ (Clsd‘(𝐶t (𝐹𝑀))))
1586, 31, 142, 157syl3anc 1368 . . . . . . . . 9 (𝜑𝑊 ∈ (Clsd‘(𝐶t (𝐹𝑀))))
159158adantr 484 . . . . . . . 8 ((𝜑 ∧ (𝑚𝑈𝑛𝑉)) → 𝑊 ∈ (Clsd‘(𝐶t (𝐹𝑀))))
160 cvmlift2lem9.10 . . . . . . . . . . 11 (𝜑𝑍𝑉)
161160adantr 484 . . . . . . . . . 10 ((𝜑 ∧ (𝑚𝑈𝑛𝑉)) → 𝑍𝑉)
162 opelxpi 5569 . . . . . . . . . 10 ((𝑚 ∈ {𝑚} ∧ 𝑍𝑉) → ⟨𝑚, 𝑍⟩ ∈ ({𝑚} × 𝑉))
16352, 161, 162syl2anc 587 . . . . . . . . 9 ((𝜑 ∧ (𝑚𝑈𝑛𝑉)) → ⟨𝑚, 𝑍⟩ ∈ ({𝑚} × 𝑉))
16481, 84sstrd 3952 . . . . . . . . . 10 ((𝜑 ∧ (𝑚𝑈𝑛𝑉)) → ({𝑚} × 𝑉) ⊆ ((0[,]1) × (0[,]1)))
1654restuni 21765 . . . . . . . . . 10 (((II ×t II) ∈ Top ∧ ({𝑚} × 𝑉) ⊆ ((0[,]1) × (0[,]1))) → ({𝑚} × 𝑉) = ((II ×t II) ↾t ({𝑚} × 𝑉)))
16615, 164, 165sylancr 590 . . . . . . . . 9 ((𝜑 ∧ (𝑚𝑈𝑛𝑉)) → ({𝑚} × 𝑉) = ((II ×t II) ↾t ({𝑚} × 𝑉)))
167163, 166eleqtrd 2916 . . . . . . . 8 ((𝜑 ∧ (𝑚𝑈𝑛𝑉)) → ⟨𝑚, 𝑍⟩ ∈ ((II ×t II) ↾t ({𝑚} × 𝑉)))
168 df-ov 7143 . . . . . . . . . 10 (𝑚(𝐾 ↾ ({𝑚} × 𝑉))𝑍) = ((𝐾 ↾ ({𝑚} × 𝑉))‘⟨𝑚, 𝑍⟩)
169 ovres 7299 . . . . . . . . . . . 12 ((𝑚 ∈ {𝑚} ∧ 𝑍𝑉) → (𝑚(𝐾 ↾ ({𝑚} × 𝑉))𝑍) = (𝑚𝐾𝑍))
17052, 161, 169syl2anc 587 . . . . . . . . . . 11 ((𝜑 ∧ (𝑚𝑈𝑛𝑉)) → (𝑚(𝐾 ↾ ({𝑚} × 𝑉))𝑍) = (𝑚𝐾𝑍))
171 snidg 4573 . . . . . . . . . . . . . 14 (𝑍𝑉𝑍 ∈ {𝑍})
172160, 171syl 17 . . . . . . . . . . . . 13 (𝜑𝑍 ∈ {𝑍})
173172adantr 484 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑚𝑈𝑛𝑉)) → 𝑍 ∈ {𝑍})
174 ovres 7299 . . . . . . . . . . . 12 ((𝑚𝑈𝑍 ∈ {𝑍}) → (𝑚(𝐾 ↾ (𝑈 × {𝑍}))𝑍) = (𝑚𝐾𝑍))
175106, 173, 174syl2anc 587 . . . . . . . . . . 11 ((𝜑 ∧ (𝑚𝑈𝑛𝑉)) → (𝑚(𝐾 ↾ (𝑈 × {𝑍}))𝑍) = (𝑚𝐾𝑍))
176170, 175eqtr4d 2860 . . . . . . . . . 10 ((𝜑 ∧ (𝑚𝑈𝑛𝑉)) → (𝑚(𝐾 ↾ ({𝑚} × 𝑉))𝑍) = (𝑚(𝐾 ↾ (𝑈 × {𝑍}))𝑍))
177168, 176syl5eqr 2871 . . . . . . . . 9 ((𝜑 ∧ (𝑚𝑈𝑛𝑉)) → ((𝐾 ↾ ({𝑚} × 𝑉))‘⟨𝑚, 𝑍⟩) = (𝑚(𝐾 ↾ (𝑈 × {𝑍}))𝑍))
178 eqid 2822 . . . . . . . . . . . . 13 ((II ×t II) ↾t (𝑈 × {𝑍})) = ((II ×t II) ↾t (𝑈 × {𝑍}))
1792a1i 11 . . . . . . . . . . . . . . 15 (𝜑 → II ∈ Top)
180 snex 5309 . . . . . . . . . . . . . . . 16 {𝑍} ∈ V
181180a1i 11 . . . . . . . . . . . . . . 15 (𝜑 → {𝑍} ∈ V)
182 txrest 22234 . . . . . . . . . . . . . . 15 (((II ∈ Top ∧ II ∈ Top) ∧ (𝑈 ∈ II ∧ {𝑍} ∈ V)) → ((II ×t II) ↾t (𝑈 × {𝑍})) = ((II ↾t 𝑈) ×t (II ↾t {𝑍})))
183179, 179, 17, 181, 182syl22anc 837 . . . . . . . . . . . . . 14 (𝜑 → ((II ×t II) ↾t (𝑈 × {𝑍})) = ((II ↾t 𝑈) ×t (II ↾t {𝑍})))
184 cvmlift2lem9.5 . . . . . . . . . . . . . . 15 (𝜑 → (II ↾t 𝑈) ∈ Conn)
18526, 160sseldd 3943 . . . . . . . . . . . . . . . . 17 (𝜑𝑍 ∈ (0[,]1))
186 restsn2 21774 . . . . . . . . . . . . . . . . 17 ((II ∈ (TopOn‘(0[,]1)) ∧ 𝑍 ∈ (0[,]1)) → (II ↾t {𝑍}) = 𝒫 {𝑍})
18763, 185, 186sylancr 590 . . . . . . . . . . . . . . . 16 (𝜑 → (II ↾t {𝑍}) = 𝒫 {𝑍})
188 pwsn 4805 . . . . . . . . . . . . . . . . 17 𝒫 {𝑍} = {∅, {𝑍}}
189 indisconn 22021 . . . . . . . . . . . . . . . . 17 {∅, {𝑍}} ∈ Conn
190188, 189eqeltri 2910 . . . . . . . . . . . . . . . 16 𝒫 {𝑍} ∈ Conn
191187, 190eqeltrdi 2922 . . . . . . . . . . . . . . 15 (𝜑 → (II ↾t {𝑍}) ∈ Conn)
192 txconn 22292 . . . . . . . . . . . . . . 15 (((II ↾t 𝑈) ∈ Conn ∧ (II ↾t {𝑍}) ∈ Conn) → ((II ↾t 𝑈) ×t (II ↾t {𝑍})) ∈ Conn)
193184, 191, 192syl2anc 587 . . . . . . . . . . . . . 14 (𝜑 → ((II ↾t 𝑈) ×t (II ↾t {𝑍})) ∈ Conn)
194183, 193eqeltrd 2914 . . . . . . . . . . . . 13 (𝜑 → ((II ×t II) ↾t (𝑈 × {𝑍})) ∈ Conn)
195 cvmlift2lem9.11 . . . . . . . . . . . . . 14 (𝜑 → (𝐾 ↾ (𝑈 × {𝑍})) ∈ (((II ×t II) ↾t (𝑈 × {𝑍})) Cn 𝐶))
196101, 103sylib 221 . . . . . . . . . . . . . . 15 (𝜑𝐶 ∈ (TopOn‘𝐵))
197 df-ima 5545 . . . . . . . . . . . . . . . 16 (𝐾 “ (𝑈 × {𝑍})) = ran (𝐾 ↾ (𝑈 × {𝑍}))
198160snssd 4715 . . . . . . . . . . . . . . . . . 18 (𝜑 → {𝑍} ⊆ 𝑉)
199 xpss2 5552 . . . . . . . . . . . . . . . . . 18 ({𝑍} ⊆ 𝑉 → (𝑈 × {𝑍}) ⊆ (𝑈 × 𝑉))
200 imass2 5943 . . . . . . . . . . . . . . . . . 18 ((𝑈 × {𝑍}) ⊆ (𝑈 × 𝑉) → (𝐾 “ (𝑈 × {𝑍})) ⊆ (𝐾 “ (𝑈 × 𝑉)))
201198, 199, 2003syl 18 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐾 “ (𝑈 × {𝑍})) ⊆ (𝐾 “ (𝑈 × 𝑉)))
202201, 124sstrd 3952 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐾 “ (𝑈 × {𝑍})) ⊆ (𝐹𝑀))
203197, 202eqsstrrid 3991 . . . . . . . . . . . . . . 15 (𝜑 → ran (𝐾 ↾ (𝑈 × {𝑍})) ⊆ (𝐹𝑀))
204 cnrest2 21889 . . . . . . . . . . . . . . 15 ((𝐶 ∈ (TopOn‘𝐵) ∧ ran (𝐾 ↾ (𝑈 × {𝑍})) ⊆ (𝐹𝑀) ∧ (𝐹𝑀) ⊆ 𝐵) → ((𝐾 ↾ (𝑈 × {𝑍})) ∈ (((II ×t II) ↾t (𝑈 × {𝑍})) Cn 𝐶) ↔ (𝐾 ↾ (𝑈 × {𝑍})) ∈ (((II ×t II) ↾t (𝑈 × {𝑍})) Cn (𝐶t (𝐹𝑀)))))
205196, 203, 135, 204syl3anc 1368 . . . . . . . . . . . . . 14 (𝜑 → ((𝐾 ↾ (𝑈 × {𝑍})) ∈ (((II ×t II) ↾t (𝑈 × {𝑍})) Cn 𝐶) ↔ (𝐾 ↾ (𝑈 × {𝑍})) ∈ (((II ×t II) ↾t (𝑈 × {𝑍})) Cn (𝐶t (𝐹𝑀)))))
206195, 205mpbid 235 . . . . . . . . . . . . 13 (𝜑 → (𝐾 ↾ (𝑈 × {𝑍})) ∈ (((II ×t II) ↾t (𝑈 × {𝑍})) Cn (𝐶t (𝐹𝑀))))
207 opelxpi 5569 . . . . . . . . . . . . . . 15 ((𝑋𝑈𝑍 ∈ {𝑍}) → ⟨𝑋, 𝑍⟩ ∈ (𝑈 × {𝑍}))
20821, 172, 207syl2anc 587 . . . . . . . . . . . . . 14 (𝜑 → ⟨𝑋, 𝑍⟩ ∈ (𝑈 × {𝑍}))
209185snssd 4715 . . . . . . . . . . . . . . . 16 (𝜑 → {𝑍} ⊆ (0[,]1))
210 xpss12 5547 . . . . . . . . . . . . . . . 16 ((𝑈 ⊆ (0[,]1) ∧ {𝑍} ⊆ (0[,]1)) → (𝑈 × {𝑍}) ⊆ ((0[,]1) × (0[,]1)))
21120, 209, 210syl2anc 587 . . . . . . . . . . . . . . 15 (𝜑 → (𝑈 × {𝑍}) ⊆ ((0[,]1) × (0[,]1)))
2124restuni 21765 . . . . . . . . . . . . . . 15 (((II ×t II) ∈ Top ∧ (𝑈 × {𝑍}) ⊆ ((0[,]1) × (0[,]1))) → (𝑈 × {𝑍}) = ((II ×t II) ↾t (𝑈 × {𝑍})))
21315, 211, 212sylancr 590 . . . . . . . . . . . . . 14 (𝜑 → (𝑈 × {𝑍}) = ((II ×t II) ↾t (𝑈 × {𝑍})))
214208, 213eleqtrd 2916 . . . . . . . . . . . . 13 (𝜑 → ⟨𝑋, 𝑍⟩ ∈ ((II ×t II) ↾t (𝑈 × {𝑍})))
215 df-ov 7143 . . . . . . . . . . . . . . 15 (𝑋(𝐾 ↾ (𝑈 × {𝑍}))𝑍) = ((𝐾 ↾ (𝑈 × {𝑍}))‘⟨𝑋, 𝑍⟩)
216 ovres 7299 . . . . . . . . . . . . . . . . 17 ((𝑋𝑈𝑍 ∈ {𝑍}) → (𝑋(𝐾 ↾ (𝑈 × {𝑍}))𝑍) = (𝑋𝐾𝑍))
21721, 172, 216syl2anc 587 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑋(𝐾 ↾ (𝑈 × {𝑍}))𝑍) = (𝑋𝐾𝑍))
218 snidg 4573 . . . . . . . . . . . . . . . . . 18 (𝑋𝑈𝑋 ∈ {𝑋})
21921, 218syl 17 . . . . . . . . . . . . . . . . 17 (𝜑𝑋 ∈ {𝑋})
220 ovres 7299 . . . . . . . . . . . . . . . . 17 ((𝑋 ∈ {𝑋} ∧ 𝑍𝑉) → (𝑋(𝐾 ↾ ({𝑋} × 𝑉))𝑍) = (𝑋𝐾𝑍))
221219, 160, 220syl2anc 587 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑋(𝐾 ↾ ({𝑋} × 𝑉))𝑍) = (𝑋𝐾𝑍))
222217, 221eqtr4d 2860 . . . . . . . . . . . . . . 15 (𝜑 → (𝑋(𝐾 ↾ (𝑈 × {𝑍}))𝑍) = (𝑋(𝐾 ↾ ({𝑋} × 𝑉))𝑍))
223215, 222syl5eqr 2871 . . . . . . . . . . . . . 14 (𝜑 → ((𝐾 ↾ (𝑈 × {𝑍}))‘⟨𝑋, 𝑍⟩) = (𝑋(𝐾 ↾ ({𝑋} × 𝑉))𝑍))
224 eqid 2822 . . . . . . . . . . . . . . . . 17 ((II ×t II) ↾t ({𝑋} × 𝑉)) = ((II ×t II) ↾t ({𝑋} × 𝑉))
225 snex 5309 . . . . . . . . . . . . . . . . . . . 20 {𝑋} ∈ V
226225a1i 11 . . . . . . . . . . . . . . . . . . 19 (𝜑 → {𝑋} ∈ V)
227 txrest 22234 . . . . . . . . . . . . . . . . . . 19 (((II ∈ Top ∧ II ∈ Top) ∧ ({𝑋} ∈ V ∧ 𝑉 ∈ II)) → ((II ×t II) ↾t ({𝑋} × 𝑉)) = ((II ↾t {𝑋}) ×t (II ↾t 𝑉)))
228179, 179, 226, 23, 227syl22anc 837 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((II ×t II) ↾t ({𝑋} × 𝑉)) = ((II ↾t {𝑋}) ×t (II ↾t 𝑉)))
229 restsn2 21774 . . . . . . . . . . . . . . . . . . . . 21 ((II ∈ (TopOn‘(0[,]1)) ∧ 𝑋 ∈ (0[,]1)) → (II ↾t {𝑋}) = 𝒫 {𝑋})
23063, 22, 229sylancr 590 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (II ↾t {𝑋}) = 𝒫 {𝑋})
231 pwsn 4805 . . . . . . . . . . . . . . . . . . . . 21 𝒫 {𝑋} = {∅, {𝑋}}
232 indisconn 22021 . . . . . . . . . . . . . . . . . . . . 21 {∅, {𝑋}} ∈ Conn
233231, 232eqeltri 2910 . . . . . . . . . . . . . . . . . . . 20 𝒫 {𝑋} ∈ Conn
234230, 233eqeltrdi 2922 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (II ↾t {𝑋}) ∈ Conn)
235 txconn 22292 . . . . . . . . . . . . . . . . . . 19 (((II ↾t {𝑋}) ∈ Conn ∧ (II ↾t 𝑉) ∈ Conn) → ((II ↾t {𝑋}) ×t (II ↾t 𝑉)) ∈ Conn)
236234, 72, 235syl2anc 587 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((II ↾t {𝑋}) ×t (II ↾t 𝑉)) ∈ Conn)
237228, 236eqeltrd 2914 . . . . . . . . . . . . . . . . 17 (𝜑 → ((II ×t II) ↾t ({𝑋} × 𝑉)) ∈ Conn)
2381, 6, 7, 8, 9, 10, 11cvmlift2lem6 32629 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑋 ∈ (0[,]1)) → (𝐾 ↾ ({𝑋} × (0[,]1))) ∈ (((II ×t II) ↾t ({𝑋} × (0[,]1))) Cn 𝐶))
23922, 238mpdan 686 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝐾 ↾ ({𝑋} × (0[,]1))) ∈ (((II ×t II) ↾t ({𝑋} × (0[,]1))) Cn 𝐶))
240 xpss2 5552 . . . . . . . . . . . . . . . . . . . . . 22 (𝑉 ⊆ (0[,]1) → ({𝑋} × 𝑉) ⊆ ({𝑋} × (0[,]1)))
24123, 25, 2403syl 18 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ({𝑋} × 𝑉) ⊆ ({𝑋} × (0[,]1)))
24222snssd 4715 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → {𝑋} ⊆ (0[,]1))
243 xpss1 5551 . . . . . . . . . . . . . . . . . . . . . . 23 ({𝑋} ⊆ (0[,]1) → ({𝑋} × (0[,]1)) ⊆ ((0[,]1) × (0[,]1)))
244242, 243syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ({𝑋} × (0[,]1)) ⊆ ((0[,]1) × (0[,]1)))
2454restuni 21765 . . . . . . . . . . . . . . . . . . . . . 22 (((II ×t II) ∈ Top ∧ ({𝑋} × (0[,]1)) ⊆ ((0[,]1) × (0[,]1))) → ({𝑋} × (0[,]1)) = ((II ×t II) ↾t ({𝑋} × (0[,]1))))
24615, 244, 245sylancr 590 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ({𝑋} × (0[,]1)) = ((II ×t II) ↾t ({𝑋} × (0[,]1))))
247241, 246sseqtrd 3982 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ({𝑋} × 𝑉) ⊆ ((II ×t II) ↾t ({𝑋} × (0[,]1))))
248 eqid 2822 . . . . . . . . . . . . . . . . . . . . 21 ((II ×t II) ↾t ({𝑋} × (0[,]1))) = ((II ×t II) ↾t ({𝑋} × (0[,]1)))
249248cnrest 21888 . . . . . . . . . . . . . . . . . . . 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 𝐶))
250239, 247, 249syl2anc 587 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝐾 ↾ ({𝑋} × (0[,]1))) ↾ ({𝑋} × 𝑉)) ∈ ((((II ×t II) ↾t ({𝑋} × (0[,]1))) ↾t ({𝑋} × 𝑉)) Cn 𝐶))
251241resabs1d 5862 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝐾 ↾ ({𝑋} × (0[,]1))) ↾ ({𝑋} × 𝑉)) = (𝐾 ↾ ({𝑋} × 𝑉)))
252225, 93xpex 7461 . . . . . . . . . . . . . . . . . . . . . 22 ({𝑋} × (0[,]1)) ∈ V
253252a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ({𝑋} × (0[,]1)) ∈ V)
254 restabs 21768 . . . . . . . . . . . . . . . . . . . . 21 (((II ×t II) ∈ Top ∧ ({𝑋} × 𝑉) ⊆ ({𝑋} × (0[,]1)) ∧ ({𝑋} × (0[,]1)) ∈ V) → (((II ×t II) ↾t ({𝑋} × (0[,]1))) ↾t ({𝑋} × 𝑉)) = ((II ×t II) ↾t ({𝑋} × 𝑉)))
25516, 241, 253, 254syl3anc 1368 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (((II ×t II) ↾t ({𝑋} × (0[,]1))) ↾t ({𝑋} × 𝑉)) = ((II ×t II) ↾t ({𝑋} × 𝑉)))
256255oveq1d 7155 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((((II ×t II) ↾t ({𝑋} × (0[,]1))) ↾t ({𝑋} × 𝑉)) Cn 𝐶) = (((II ×t II) ↾t ({𝑋} × 𝑉)) Cn 𝐶))
257250, 251, 2563eltr3d 2928 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐾 ↾ ({𝑋} × 𝑉)) ∈ (((II ×t II) ↾t ({𝑋} × 𝑉)) Cn 𝐶))
258 df-ima 5545 . . . . . . . . . . . . . . . . . . . 20 (𝐾 “ ({𝑋} × 𝑉)) = ran (𝐾 ↾ ({𝑋} × 𝑉))
25921snssd 4715 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → {𝑋} ⊆ 𝑈)
260 xpss1 5551 . . . . . . . . . . . . . . . . . . . . . 22 ({𝑋} ⊆ 𝑈 → ({𝑋} × 𝑉) ⊆ (𝑈 × 𝑉))
261 imass2 5943 . . . . . . . . . . . . . . . . . . . . . 22 (({𝑋} × 𝑉) ⊆ (𝑈 × 𝑉) → (𝐾 “ ({𝑋} × 𝑉)) ⊆ (𝐾 “ (𝑈 × 𝑉)))
262259, 260, 2613syl 18 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝐾 “ ({𝑋} × 𝑉)) ⊆ (𝐾 “ (𝑈 × 𝑉)))
263262, 124sstrd 3952 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝐾 “ ({𝑋} × 𝑉)) ⊆ (𝐹𝑀))
264258, 263eqsstrrid 3991 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ran (𝐾 ↾ ({𝑋} × 𝑉)) ⊆ (𝐹𝑀))
265 cnrest2 21889 . . . . . . . . . . . . . . . . . . 19 ((𝐶 ∈ (TopOn‘𝐵) ∧ ran (𝐾 ↾ ({𝑋} × 𝑉)) ⊆ (𝐹𝑀) ∧ (𝐹𝑀) ⊆ 𝐵) → ((𝐾 ↾ ({𝑋} × 𝑉)) ∈ (((II ×t II) ↾t ({𝑋} × 𝑉)) Cn 𝐶) ↔ (𝐾 ↾ ({𝑋} × 𝑉)) ∈ (((II ×t II) ↾t ({𝑋} × 𝑉)) Cn (𝐶t (𝐹𝑀)))))
266196, 264, 135, 265syl3anc 1368 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝐾 ↾ ({𝑋} × 𝑉)) ∈ (((II ×t II) ↾t ({𝑋} × 𝑉)) Cn 𝐶) ↔ (𝐾 ↾ ({𝑋} × 𝑉)) ∈ (((II ×t II) ↾t ({𝑋} × 𝑉)) Cn (𝐶t (𝐹𝑀)))))
267257, 266mpbid 235 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐾 ↾ ({𝑋} × 𝑉)) ∈ (((II ×t II) ↾t ({𝑋} × 𝑉)) Cn (𝐶t (𝐹𝑀))))
268 opelxpi 5569 . . . . . . . . . . . . . . . . . . 19 ((𝑋 ∈ {𝑋} ∧ 𝑌𝑉) → ⟨𝑋, 𝑌⟩ ∈ ({𝑋} × 𝑉))
269219, 27, 268syl2anc 587 . . . . . . . . . . . . . . . . . 18 (𝜑 → ⟨𝑋, 𝑌⟩ ∈ ({𝑋} × 𝑉))
270259, 260syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ({𝑋} × 𝑉) ⊆ (𝑈 × 𝑉))
271270, 50sstrd 3952 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ({𝑋} × 𝑉) ⊆ ((0[,]1) × (0[,]1)))
2724restuni 21765 . . . . . . . . . . . . . . . . . . 19 (((II ×t II) ∈ Top ∧ ({𝑋} × 𝑉) ⊆ ((0[,]1) × (0[,]1))) → ({𝑋} × 𝑉) = ((II ×t II) ↾t ({𝑋} × 𝑉)))
27315, 271, 272sylancr 590 . . . . . . . . . . . . . . . . . 18 (𝜑 → ({𝑋} × 𝑉) = ((II ×t II) ↾t ({𝑋} × 𝑉)))
274269, 273eleqtrd 2916 . . . . . . . . . . . . . . . . 17 (𝜑 → ⟨𝑋, 𝑌⟩ ∈ ((II ×t II) ↾t ({𝑋} × 𝑉)))
275 df-ov 7143 . . . . . . . . . . . . . . . . . . 19 (𝑋(𝐾 ↾ ({𝑋} × 𝑉))𝑌) = ((𝐾 ↾ ({𝑋} × 𝑉))‘⟨𝑋, 𝑌⟩)
276 ovres 7299 . . . . . . . . . . . . . . . . . . . 20 ((𝑋 ∈ {𝑋} ∧ 𝑌𝑉) → (𝑋(𝐾 ↾ ({𝑋} × 𝑉))𝑌) = (𝑋𝐾𝑌))
277219, 27, 276syl2anc 587 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑋(𝐾 ↾ ({𝑋} × 𝑉))𝑌) = (𝑋𝐾𝑌))
278275, 277syl5eqr 2871 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝐾 ↾ ({𝑋} × 𝑉))‘⟨𝑋, 𝑌⟩) = (𝑋𝐾𝑌))
27945simprd 499 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑋𝐾𝑌) ∈ 𝑊)
280278, 279eqeltrd 2914 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝐾 ↾ ({𝑋} × 𝑉))‘⟨𝑋, 𝑌⟩) ∈ 𝑊)
281224, 237, 267, 155, 158, 274, 280conncn 22029 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐾 ↾ ({𝑋} × 𝑉)): ((II ×t II) ↾t ({𝑋} × 𝑉))⟶𝑊)
282273feq2d 6480 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐾 ↾ ({𝑋} × 𝑉)):({𝑋} × 𝑉)⟶𝑊 ↔ (𝐾 ↾ ({𝑋} × 𝑉)): ((II ×t II) ↾t ({𝑋} × 𝑉))⟶𝑊))
283281, 282mpbird 260 . . . . . . . . . . . . . . 15 (𝜑 → (𝐾 ↾ ({𝑋} × 𝑉)):({𝑋} × 𝑉)⟶𝑊)
284283, 219, 160fovrnd 7305 . . . . . . . . . . . . . 14 (𝜑 → (𝑋(𝐾 ↾ ({𝑋} × 𝑉))𝑍) ∈ 𝑊)
285223, 284eqeltrd 2914 . . . . . . . . . . . . 13 (𝜑 → ((𝐾 ↾ (𝑈 × {𝑍}))‘⟨𝑋, 𝑍⟩) ∈ 𝑊)
286178, 194, 206, 155, 158, 214, 285conncn 22029 . . . . . . . . . . . 12 (𝜑 → (𝐾 ↾ (𝑈 × {𝑍})): ((II ×t II) ↾t (𝑈 × {𝑍}))⟶𝑊)
287213feq2d 6480 . . . . . . . . . . . 12 (𝜑 → ((𝐾 ↾ (𝑈 × {𝑍})):(𝑈 × {𝑍})⟶𝑊 ↔ (𝐾 ↾ (𝑈 × {𝑍})): ((II ×t II) ↾t (𝑈 × {𝑍}))⟶𝑊))
288286, 287mpbird 260 . . . . . . . . . . 11 (𝜑 → (𝐾 ↾ (𝑈 × {𝑍})):(𝑈 × {𝑍})⟶𝑊)
289288adantr 484 . . . . . . . . . 10 ((𝜑 ∧ (𝑚𝑈𝑛𝑉)) → (𝐾 ↾ (𝑈 × {𝑍})):(𝑈 × {𝑍})⟶𝑊)
290289, 106, 173fovrnd 7305 . . . . . . . . 9 ((𝜑 ∧ (𝑚𝑈𝑛𝑉)) → (𝑚(𝐾 ↾ (𝑈 × {𝑍}))𝑍) ∈ 𝑊)
291177, 290eqeltrd 2914 . . . . . . . 8 ((𝜑 ∧ (𝑚𝑈𝑛𝑉)) → ((𝐾 ↾ ({𝑚} × 𝑉))‘⟨𝑚, 𝑍⟩) ∈ 𝑊)
29256, 76, 139, 156, 159, 167, 291conncn 22029 . . . . . . 7 ((𝜑 ∧ (𝑚𝑈𝑛𝑉)) → (𝐾 ↾ ({𝑚} × 𝑉)): ((II ×t II) ↾t ({𝑚} × 𝑉))⟶𝑊)
293166feq2d 6480 . . . . . . 7 ((𝜑 ∧ (𝑚𝑈𝑛𝑉)) → ((𝐾 ↾ ({𝑚} × 𝑉)):({𝑚} × 𝑉)⟶𝑊 ↔ (𝐾 ↾ ({𝑚} × 𝑉)): ((II ×t II) ↾t ({𝑚} × 𝑉))⟶𝑊))
294292, 293mpbird 260 . . . . . 6 ((𝜑 ∧ (𝑚𝑈𝑛𝑉)) → (𝐾 ↾ ({𝑚} × 𝑉)):({𝑚} × 𝑉)⟶𝑊)
295294, 52, 53fovrnd 7305 . . . . 5 ((𝜑 ∧ (𝑚𝑈𝑛𝑉)) → (𝑚(𝐾 ↾ ({𝑚} × 𝑉))𝑛) ∈ 𝑊)
29655, 295eqeltrrd 2915 . . . 4 ((𝜑 ∧ (𝑚𝑈𝑛𝑉)) → (𝑚𝐾𝑛) ∈ 𝑊)
297296ralrimivva 3181 . . 3 (𝜑 → ∀𝑚𝑈𝑛𝑉 (𝑚𝐾𝑛) ∈ 𝑊)
298 funimassov 7310 . . . 4 ((Fun 𝐾 ∧ (𝑈 × 𝑉) ⊆ dom 𝐾) → ((𝐾 “ (𝑈 × 𝑉)) ⊆ 𝑊 ↔ ∀𝑚𝑈𝑛𝑉 (𝑚𝐾𝑛) ∈ 𝑊))
299119, 121, 298syl2anc 587 . . 3 (𝜑 → ((𝐾 “ (𝑈 × 𝑉)) ⊆ 𝑊 ↔ ∀𝑚𝑈𝑛𝑉 (𝑚𝐾𝑛) ∈ 𝑊))
300297, 299mpbird 260 . 2 (𝜑 → (𝐾 “ (𝑈 × 𝑉)) ⊆ 𝑊)
3011, 4, 5, 6, 12, 14, 16, 30, 31, 48, 50, 300cvmlift2lem9a 32624 1 (𝜑 → (𝐾 ↾ (𝑈 × 𝑉)) ∈ (((II ×t II) ↾t (𝑈 × 𝑉)) Cn 𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399   = wceq 1538  wcel 2114  wral 3130  {crab 3134  Vcvv 3469  cdif 3905  cin 3907  wss 3908  c0 4265  𝒫 cpw 4511  {csn 4539  {cpr 4541  cop 4545   cuni 4813  cmpt 5122   × cxp 5530  ccnv 5531  dom cdm 5532  ran crn 5533  cres 5534  cima 5535  ccom 5536  Fun wfun 6328  wf 6330  cfv 6334  crio 7097  (class class class)co 7140  cmpo 7142  0cc0 10526  1c1 10527  [,]cicc 12729  t crest 16685  Topctop 21496  TopOnctopon 21513  Clsdccld 21619   Cn ccn 21827  Conncconn 22014   ×t ctx 22163  Homeochmeo 22356  IIcii 23478   CovMap ccvm 32576
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2178  ax-ext 2794  ax-rep 5166  ax-sep 5179  ax-nul 5186  ax-pow 5243  ax-pr 5307  ax-un 7446  ax-inf2 9092  ax-cnex 10582  ax-resscn 10583  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-addrcl 10587  ax-mulcl 10588  ax-mulrcl 10589  ax-mulcom 10590  ax-addass 10591  ax-mulass 10592  ax-distr 10593  ax-i2m1 10594  ax-1ne0 10595  ax-1rid 10596  ax-rnegex 10597  ax-rrecex 10598  ax-cnre 10599  ax-pre-lttri 10600  ax-pre-lttrn 10601  ax-pre-ltadd 10602  ax-pre-mulgt0 10603  ax-pre-sup 10604  ax-addf 10605  ax-mulf 10606
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2622  df-eu 2653  df-clab 2801  df-cleq 2815  df-clel 2894  df-nfc 2962  df-ne 3012  df-nel 3116  df-ral 3135  df-rex 3136  df-reu 3137  df-rmo 3138  df-rab 3139  df-v 3471  df-sbc 3748  df-csb 3856  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-pss 3927  df-nul 4266  df-if 4440  df-pw 4513  df-sn 4540  df-pr 4542  df-tp 4544  df-op 4546  df-uni 4814  df-int 4852  df-iun 4896  df-iin 4897  df-br 5043  df-opab 5105  df-mpt 5123  df-tr 5149  df-id 5437  df-eprel 5442  df-po 5451  df-so 5452  df-fr 5491  df-se 5492  df-we 5493  df-xp 5538  df-rel 5539  df-cnv 5540  df-co 5541  df-dm 5542  df-rn 5543  df-res 5544  df-ima 5545  df-pred 6126  df-ord 6172  df-on 6173  df-lim 6174  df-suc 6175  df-iota 6293  df-fun 6336  df-fn 6337  df-f 6338  df-f1 6339  df-fo 6340  df-f1o 6341  df-fv 6342  df-isom 6343  df-riota 7098  df-ov 7143  df-oprab 7144  df-mpo 7145  df-of 7394  df-om 7566  df-1st 7675  df-2nd 7676  df-supp 7818  df-wrecs 7934  df-recs 7995  df-rdg 8033  df-1o 8089  df-2o 8090  df-oadd 8093  df-er 8276  df-ec 8278  df-map 8395  df-ixp 8449  df-en 8497  df-dom 8498  df-sdom 8499  df-fin 8500  df-fsupp 8822  df-fi 8863  df-sup 8894  df-inf 8895  df-oi 8962  df-card 9356  df-pnf 10666  df-mnf 10667  df-xr 10668  df-ltxr 10669  df-le 10670  df-sub 10861  df-neg 10862  df-div 11287  df-nn 11626  df-2 11688  df-3 11689  df-4 11690  df-5 11691  df-6 11692  df-7 11693  df-8 11694  df-9 11695  df-n0 11886  df-z 11970  df-dec 12087  df-uz 12232  df-q 12337  df-rp 12378  df-xneg 12495  df-xadd 12496  df-xmul 12497  df-ioo 12730  df-ico 12732  df-icc 12733  df-fz 12886  df-fzo 13029  df-fl 13157  df-seq 13365  df-exp 13426  df-hash 13687  df-cj 14449  df-re 14450  df-im 14451  df-sqrt 14585  df-abs 14586  df-clim 14836  df-sum 15034  df-struct 16476  df-ndx 16477  df-slot 16478  df-base 16480  df-sets 16481  df-ress 16482  df-plusg 16569  df-mulr 16570  df-starv 16571  df-sca 16572  df-vsca 16573  df-ip 16574  df-tset 16575  df-ple 16576  df-ds 16578  df-unif 16579  df-hom 16580  df-cco 16581  df-rest 16687  df-topn 16688  df-0g 16706  df-gsum 16707  df-topgen 16708  df-pt 16709  df-prds 16712  df-xrs 16766  df-qtop 16771  df-imas 16772  df-xps 16774  df-mre 16848  df-mrc 16849  df-acs 16851  df-mgm 17843  df-sgrp 17892  df-mnd 17903  df-submnd 17948  df-mulg 18216  df-cntz 18438  df-cmn 18899  df-psmet 20081  df-xmet 20082  df-met 20083  df-bl 20084  df-mopn 20085  df-cnfld 20090  df-top 21497  df-topon 21514  df-topsp 21536  df-bases 21549  df-cld 21622  df-ntr 21623  df-cls 21624  df-nei 21701  df-cn 21830  df-cnp 21831  df-cmp 21990  df-conn 22015  df-lly 22069  df-nlly 22070  df-tx 22165  df-hmeo 22358  df-xms 22925  df-ms 22926  df-tms 22927  df-ii 23480  df-htpy 23573  df-phtpy 23574  df-phtpc 23595  df-pconn 32542  df-sconn 32543  df-cvm 32577
This theorem is referenced by:  cvmlift2lem10  32633
  Copyright terms: Public domain W3C validator