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