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 34926
Description: Lemma for cvmlift2 34931. (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 24818 . . 3 II ∈ Top
3 iiuni 24819 . . 3 (0[,]1) = II
42, 2, 3, 3txunii 23515 . 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 34922 . 2 (𝜑𝐾:((0[,]1) × (0[,]1))⟶𝐵)
131, 6, 7, 8, 9, 10, 11cvmlift2lem7 34924 . . 3 (𝜑 → (𝐹𝐾) = 𝐺)
1413, 7eqeltrd 2828 . 2 (𝜑 → (𝐹𝐾) ∈ ((II ×t II) Cn 𝐽))
152, 2txtopi 23512 . . 3 (II ×t II) ∈ Top
1615a1i 11 . 2 (𝜑 → (II ×t II) ∈ Top)
17 cvmlift2lem9.3 . . . . 5 (𝜑𝑈 ∈ II)
18 elssuni 4942 . . . . . 6 (𝑈 ∈ II → 𝑈 II)
1918, 3sseqtrrdi 4031 . . . . 5 (𝑈 ∈ II → 𝑈 ⊆ (0[,]1))
2017, 19syl 17 . . . 4 (𝜑𝑈 ⊆ (0[,]1))
21 cvmlift2lem9.7 . . . 4 (𝜑𝑋𝑈)
2220, 21sseldd 3981 . . 3 (𝜑𝑋 ∈ (0[,]1))
23 cvmlift2lem9.4 . . . . 5 (𝜑𝑉 ∈ II)
24 elssuni 4942 . . . . . 6 (𝑉 ∈ II → 𝑉 II)
2524, 3sseqtrrdi 4031 . . . . 5 (𝑉 ∈ II → 𝑉 ⊆ (0[,]1))
2623, 25syl 17 . . . 4 (𝜑𝑉 ⊆ (0[,]1))
27 cvmlift2lem9.8 . . . 4 (𝜑𝑌𝑉)
2826, 27sseldd 3981 . . 3 (𝜑𝑌 ∈ (0[,]1))
29 opelxpi 5717 . . 3 ((𝑋 ∈ (0[,]1) ∧ 𝑌 ∈ (0[,]1)) → ⟨𝑋, 𝑌⟩ ∈ ((0[,]1) × (0[,]1)))
3022, 28, 29syl2anc 582 . 2 (𝜑 → ⟨𝑋, 𝑌⟩ ∈ ((0[,]1) × (0[,]1)))
31 cvmlift2lem9.2 . 2 (𝜑𝑇 ∈ (𝑆𝑀))
3212, 22, 28fovcdmd 7597 . . . 4 (𝜑 → (𝑋𝐾𝑌) ∈ 𝐵)
33 fvco3 7000 . . . . . . . 8 ((𝐾:((0[,]1) × (0[,]1))⟶𝐵 ∧ ⟨𝑋, 𝑌⟩ ∈ ((0[,]1) × (0[,]1))) → ((𝐹𝐾)‘⟨𝑋, 𝑌⟩) = (𝐹‘(𝐾‘⟨𝑋, 𝑌⟩)))
3412, 30, 33syl2anc 582 . . . . . . 7 (𝜑 → ((𝐹𝐾)‘⟨𝑋, 𝑌⟩) = (𝐹‘(𝐾‘⟨𝑋, 𝑌⟩)))
3513fveq1d 6902 . . . . . . 7 (𝜑 → ((𝐹𝐾)‘⟨𝑋, 𝑌⟩) = (𝐺‘⟨𝑋, 𝑌⟩))
3634, 35eqtr3d 2769 . . . . . 6 (𝜑 → (𝐹‘(𝐾‘⟨𝑋, 𝑌⟩)) = (𝐺‘⟨𝑋, 𝑌⟩))
37 df-ov 7427 . . . . . . 7 (𝑋𝐾𝑌) = (𝐾‘⟨𝑋, 𝑌⟩)
3837fveq2i 6903 . . . . . 6 (𝐹‘(𝑋𝐾𝑌)) = (𝐹‘(𝐾‘⟨𝑋, 𝑌⟩))
39 df-ov 7427 . . . . . 6 (𝑋𝐺𝑌) = (𝐺‘⟨𝑋, 𝑌⟩)
4036, 38, 393eqtr4g 2792 . . . . 5 (𝜑 → (𝐹‘(𝑋𝐾𝑌)) = (𝑋𝐺𝑌))
41 cvmlift2lem9.1 . . . . 5 (𝜑 → (𝑋𝐺𝑌) ∈ 𝑀)
4240, 41eqeltrd 2828 . . . 4 (𝜑 → (𝐹‘(𝑋𝐾𝑌)) ∈ 𝑀)
43 cvmlift2lem9.w . . . . 5 𝑊 = (𝑏𝑇 (𝑋𝐾𝑌) ∈ 𝑏)
445, 1, 43cvmsiota 34892 . . . 4 ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ (𝑇 ∈ (𝑆𝑀) ∧ (𝑋𝐾𝑌) ∈ 𝐵 ∧ (𝐹‘(𝑋𝐾𝑌)) ∈ 𝑀)) → (𝑊𝑇 ∧ (𝑋𝐾𝑌) ∈ 𝑊))
456, 31, 32, 42, 44syl13anc 1369 . . 3 (𝜑 → (𝑊𝑇 ∧ (𝑋𝐾𝑌) ∈ 𝑊))
4637eleq1i 2819 . . . 4 ((𝑋𝐾𝑌) ∈ 𝑊 ↔ (𝐾‘⟨𝑋, 𝑌⟩) ∈ 𝑊)
4746anbi2i 621 . . 3 ((𝑊𝑇 ∧ (𝑋𝐾𝑌) ∈ 𝑊) ↔ (𝑊𝑇 ∧ (𝐾‘⟨𝑋, 𝑌⟩) ∈ 𝑊))
4845, 47sylib 217 . 2 (𝜑 → (𝑊𝑇 ∧ (𝐾‘⟨𝑋, 𝑌⟩) ∈ 𝑊))
49 xpss12 5695 . . 3 ((𝑈 ⊆ (0[,]1) ∧ 𝑉 ⊆ (0[,]1)) → (𝑈 × 𝑉) ⊆ ((0[,]1) × (0[,]1)))
5020, 26, 49syl2anc 582 . 2 (𝜑 → (𝑈 × 𝑉) ⊆ ((0[,]1) × (0[,]1)))
51 snidg 4665 . . . . . . 7 (𝑚𝑈𝑚 ∈ {𝑚})
5251ad2antrl 726 . . . . . 6 ((𝜑 ∧ (𝑚𝑈𝑛𝑉)) → 𝑚 ∈ {𝑚})
53 simprr 771 . . . . . 6 ((𝜑 ∧ (𝑚𝑈𝑛𝑉)) → 𝑛𝑉)
54 ovres 7591 . . . . . 6 ((𝑚 ∈ {𝑚} ∧ 𝑛𝑉) → (𝑚(𝐾 ↾ ({𝑚} × 𝑉))𝑛) = (𝑚𝐾𝑛))
5552, 53, 54syl2anc 582 . . . . 5 ((𝜑 ∧ (𝑚𝑈𝑛𝑉)) → (𝑚(𝐾 ↾ ({𝑚} × 𝑉))𝑛) = (𝑚𝐾𝑛))
56 eqid 2727 . . . . . . . 8 ((II ×t II) ↾t ({𝑚} × 𝑉)) = ((II ×t II) ↾t ({𝑚} × 𝑉))
572a1i 11 . . . . . . . . . 10 ((𝜑 ∧ (𝑚𝑈𝑛𝑉)) → II ∈ Top)
58 snex 5435 . . . . . . . . . . 11 {𝑚} ∈ V
5958a1i 11 . . . . . . . . . 10 ((𝜑 ∧ (𝑚𝑈𝑛𝑉)) → {𝑚} ∈ V)
6023adantr 479 . . . . . . . . . 10 ((𝜑 ∧ (𝑚𝑈𝑛𝑉)) → 𝑉 ∈ II)
61 txrest 23553 . . . . . . . . . 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 24817 . . . . . . . . . . . 12 II ∈ (TopOn‘(0[,]1))
6420sselda 3980 . . . . . . . . . . . . 13 ((𝜑𝑚𝑈) → 𝑚 ∈ (0[,]1))
6564adantrr 715 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑚𝑈𝑛𝑉)) → 𝑚 ∈ (0[,]1))
66 restsn2 23093 . . . . . . . . . . . 12 ((II ∈ (TopOn‘(0[,]1)) ∧ 𝑚 ∈ (0[,]1)) → (II ↾t {𝑚}) = 𝒫 {𝑚})
6763, 65, 66sylancr 585 . . . . . . . . . . 11 ((𝜑 ∧ (𝑚𝑈𝑛𝑉)) → (II ↾t {𝑚}) = 𝒫 {𝑚})
68 pwsn 4903 . . . . . . . . . . . 12 𝒫 {𝑚} = {∅, {𝑚}}
69 indisconn 23340 . . . . . . . . . . . 12 {∅, {𝑚}} ∈ Conn
7068, 69eqeltri 2824 . . . . . . . . . . 11 𝒫 {𝑚} ∈ Conn
7167, 70eqeltrdi 2836 . . . . . . . . . 10 ((𝜑 ∧ (𝑚𝑈𝑛𝑉)) → (II ↾t {𝑚}) ∈ Conn)
72 cvmlift2lem9.6 . . . . . . . . . . 11 (𝜑 → (II ↾t 𝑉) ∈ Conn)
7372adantr 479 . . . . . . . . . 10 ((𝜑 ∧ (𝑚𝑈𝑛𝑉)) → (II ↾t 𝑉) ∈ Conn)
74 txconn 23611 . . . . . . . . . 10 (((II ↾t {𝑚}) ∈ Conn ∧ (II ↾t 𝑉) ∈ Conn) → ((II ↾t {𝑚}) ×t (II ↾t 𝑉)) ∈ Conn)
7571, 73, 74syl2anc 582 . . . . . . . . 9 ((𝜑 ∧ (𝑚𝑈𝑛𝑉)) → ((II ↾t {𝑚}) ×t (II ↾t 𝑉)) ∈ Conn)
7662, 75eqeltrd 2828 . . . . . . . 8 ((𝜑 ∧ (𝑚𝑈𝑛𝑉)) → ((II ×t II) ↾t ({𝑚} × 𝑉)) ∈ Conn)
771, 6, 7, 8, 9, 10, 11cvmlift2lem6 34923 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ (0[,]1)) → (𝐾 ↾ ({𝑚} × (0[,]1))) ∈ (((II ×t II) ↾t ({𝑚} × (0[,]1))) Cn 𝐶))
7865, 77syldan 589 . . . . . . . . . . 11 ((𝜑 ∧ (𝑚𝑈𝑛𝑉)) → (𝐾 ↾ ({𝑚} × (0[,]1))) ∈ (((II ×t II) ↾t ({𝑚} × (0[,]1))) Cn 𝐶))
7926adantr 479 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑚𝑈𝑛𝑉)) → 𝑉 ⊆ (0[,]1))
80 xpss2 5700 . . . . . . . . . . . . 13 (𝑉 ⊆ (0[,]1) → ({𝑚} × 𝑉) ⊆ ({𝑚} × (0[,]1)))
8179, 80syl 17 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑚𝑈𝑛𝑉)) → ({𝑚} × 𝑉) ⊆ ({𝑚} × (0[,]1)))
8265snssd 4815 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑚𝑈𝑛𝑉)) → {𝑚} ⊆ (0[,]1))
83 xpss1 5699 . . . . . . . . . . . . . 14 ({𝑚} ⊆ (0[,]1) → ({𝑚} × (0[,]1)) ⊆ ((0[,]1) × (0[,]1)))
8482, 83syl 17 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑚𝑈𝑛𝑉)) → ({𝑚} × (0[,]1)) ⊆ ((0[,]1) × (0[,]1)))
854restuni 23084 . . . . . . . . . . . . 13 (((II ×t II) ∈ Top ∧ ({𝑚} × (0[,]1)) ⊆ ((0[,]1) × (0[,]1))) → ({𝑚} × (0[,]1)) = ((II ×t II) ↾t ({𝑚} × (0[,]1))))
8615, 84, 85sylancr 585 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑚𝑈𝑛𝑉)) → ({𝑚} × (0[,]1)) = ((II ×t II) ↾t ({𝑚} × (0[,]1))))
8781, 86sseqtrd 4020 . . . . . . . . . . 11 ((𝜑 ∧ (𝑚𝑈𝑛𝑉)) → ({𝑚} × 𝑉) ⊆ ((II ×t II) ↾t ({𝑚} × (0[,]1))))
88 eqid 2727 . . . . . . . . . . . 12 ((II ×t II) ↾t ({𝑚} × (0[,]1))) = ((II ×t II) ↾t ({𝑚} × (0[,]1)))
8988cnrest 23207 . . . . . . . . . . 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 582 . . . . . . . . . 10 ((𝜑 ∧ (𝑚𝑈𝑛𝑉)) → ((𝐾 ↾ ({𝑚} × (0[,]1))) ↾ ({𝑚} × 𝑉)) ∈ ((((II ×t II) ↾t ({𝑚} × (0[,]1))) ↾t ({𝑚} × 𝑉)) Cn 𝐶))
9181resabs1d 6015 . . . . . . . . . 10 ((𝜑 ∧ (𝑚𝑈𝑛𝑉)) → ((𝐾 ↾ ({𝑚} × (0[,]1))) ↾ ({𝑚} × 𝑉)) = (𝐾 ↾ ({𝑚} × 𝑉)))
9215a1i 11 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑚𝑈𝑛𝑉)) → (II ×t II) ∈ Top)
93 ovex 7457 . . . . . . . . . . . . . 14 (0[,]1) ∈ V
9458, 93xpex 7759 . . . . . . . . . . . . 13 ({𝑚} × (0[,]1)) ∈ V
9594a1i 11 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑚𝑈𝑛𝑉)) → ({𝑚} × (0[,]1)) ∈ V)
96 restabs 23087 . . . . . . . . . . . 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 7439 . . . . . . . . . 10 ((𝜑 ∧ (𝑚𝑈𝑛𝑉)) → ((((II ×t II) ↾t ({𝑚} × (0[,]1))) ↾t ({𝑚} × 𝑉)) Cn 𝐶) = (((II ×t II) ↾t ({𝑚} × 𝑉)) Cn 𝐶))
9990, 91, 983eltr3d 2842 . . . . . . . . 9 ((𝜑 ∧ (𝑚𝑈𝑛𝑉)) → (𝐾 ↾ ({𝑚} × 𝑉)) ∈ (((II ×t II) ↾t ({𝑚} × 𝑉)) Cn 𝐶))
100 cvmtop1 34875 . . . . . . . . . . . . 13 (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐶 ∈ Top)
1016, 100syl 17 . . . . . . . . . . . 12 (𝜑𝐶 ∈ Top)
102101adantr 479 . . . . . . . . . . 11 ((𝜑 ∧ (𝑚𝑈𝑛𝑉)) → 𝐶 ∈ Top)
1031toptopon 22837 . . . . . . . . . . 11 (𝐶 ∈ Top ↔ 𝐶 ∈ (TopOn‘𝐵))
104102, 103sylib 217 . . . . . . . . . 10 ((𝜑 ∧ (𝑚𝑈𝑛𝑉)) → 𝐶 ∈ (TopOn‘𝐵))
105 df-ima 5693 . . . . . . . . . . 11 (𝐾 “ ({𝑚} × 𝑉)) = ran (𝐾 ↾ ({𝑚} × 𝑉))
106 simprl 769 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑚𝑈𝑛𝑉)) → 𝑚𝑈)
107106snssd 4815 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑚𝑈𝑛𝑉)) → {𝑚} ⊆ 𝑈)
108 xpss1 5699 . . . . . . . . . . . . 13 ({𝑚} ⊆ 𝑈 → ({𝑚} × 𝑉) ⊆ (𝑈 × 𝑉))
109 imass2 6109 . . . . . . . . . . . . 13 (({𝑚} × 𝑉) ⊆ (𝑈 × 𝑉) → (𝐾 “ ({𝑚} × 𝑉)) ⊆ (𝐾 “ (𝑈 × 𝑉)))
110107, 108, 1093syl 18 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑚𝑈𝑛𝑉)) → (𝐾 “ ({𝑚} × 𝑉)) ⊆ (𝐾 “ (𝑈 × 𝑉)))
111 cvmlift2lem9.9 . . . . . . . . . . . . . . 15 (𝜑 → (𝑈 × 𝑉) ⊆ (𝐺𝑀))
112 imaco 6258 . . . . . . . . . . . . . . . 16 ((𝐾𝐹) “ 𝑀) = (𝐾 “ (𝐹𝑀))
113 cnvco 5890 . . . . . . . . . . . . . . . . . 18 (𝐹𝐾) = (𝐾𝐹)
11413cnveqd 5880 . . . . . . . . . . . . . . . . . 18 (𝜑(𝐹𝐾) = 𝐺)
115113, 114eqtr3id 2781 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐾𝐹) = 𝐺)
116115imaeq1d 6065 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐾𝐹) “ 𝑀) = (𝐺𝑀))
117112, 116eqtr3id 2781 . . . . . . . . . . . . . . 15 (𝜑 → (𝐾 “ (𝐹𝑀)) = (𝐺𝑀))
118111, 117sseqtrrd 4021 . . . . . . . . . . . . . 14 (𝜑 → (𝑈 × 𝑉) ⊆ (𝐾 “ (𝐹𝑀)))
11912ffund 6729 . . . . . . . . . . . . . . 15 (𝜑 → Fun 𝐾)
12012fdmd 6736 . . . . . . . . . . . . . . . 16 (𝜑 → dom 𝐾 = ((0[,]1) × (0[,]1)))
12150, 120sseqtrrd 4021 . . . . . . . . . . . . . . 15 (𝜑 → (𝑈 × 𝑉) ⊆ dom 𝐾)
122 funimass3 7066 . . . . . . . . . . . . . . 15 ((Fun 𝐾 ∧ (𝑈 × 𝑉) ⊆ dom 𝐾) → ((𝐾 “ (𝑈 × 𝑉)) ⊆ (𝐹𝑀) ↔ (𝑈 × 𝑉) ⊆ (𝐾 “ (𝐹𝑀))))
123119, 121, 122syl2anc 582 . . . . . . . . . . . . . 14 (𝜑 → ((𝐾 “ (𝑈 × 𝑉)) ⊆ (𝐹𝑀) ↔ (𝑈 × 𝑉) ⊆ (𝐾 “ (𝐹𝑀))))
124118, 123mpbird 256 . . . . . . . . . . . . 13 (𝜑 → (𝐾 “ (𝑈 × 𝑉)) ⊆ (𝐹𝑀))
125124adantr 479 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑚𝑈𝑛𝑉)) → (𝐾 “ (𝑈 × 𝑉)) ⊆ (𝐹𝑀))
126110, 125sstrd 3990 . . . . . . . . . . 11 ((𝜑 ∧ (𝑚𝑈𝑛𝑉)) → (𝐾 “ ({𝑚} × 𝑉)) ⊆ (𝐹𝑀))
127105, 126eqsstrrid 4029 . . . . . . . . . 10 ((𝜑 ∧ (𝑚𝑈𝑛𝑉)) → ran (𝐾 ↾ ({𝑚} × 𝑉)) ⊆ (𝐹𝑀))
128 cnvimass 6088 . . . . . . . . . . . 12 (𝐹𝑀) ⊆ dom 𝐹
129 cvmcn 34877 . . . . . . . . . . . . . 14 (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐹 ∈ (𝐶 Cn 𝐽))
1306, 129syl 17 . . . . . . . . . . . . 13 (𝜑𝐹 ∈ (𝐶 Cn 𝐽))
131 eqid 2727 . . . . . . . . . . . . . 14 𝐽 = 𝐽
1321, 131cnf 23168 . . . . . . . . . . . . 13 (𝐹 ∈ (𝐶 Cn 𝐽) → 𝐹:𝐵 𝐽)
133 fdm 6734 . . . . . . . . . . . . 13 (𝐹:𝐵 𝐽 → dom 𝐹 = 𝐵)
134130, 132, 1333syl 18 . . . . . . . . . . . 12 (𝜑 → dom 𝐹 = 𝐵)
135128, 134sseqtrid 4032 . . . . . . . . . . 11 (𝜑 → (𝐹𝑀) ⊆ 𝐵)
136135adantr 479 . . . . . . . . . 10 ((𝜑 ∧ (𝑚𝑈𝑛𝑉)) → (𝐹𝑀) ⊆ 𝐵)
137 cnrest2 23208 . . . . . . . . . 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 231 . . . . . . . 8 ((𝜑 ∧ (𝑚𝑈𝑛𝑉)) → (𝐾 ↾ ({𝑚} × 𝑉)) ∈ (((II ×t II) ↾t ({𝑚} × 𝑉)) Cn (𝐶t (𝐹𝑀))))
1405cvmsss 34882 . . . . . . . . . . . 12 (𝑇 ∈ (𝑆𝑀) → 𝑇𝐶)
14131, 140syl 17 . . . . . . . . . . 11 (𝜑𝑇𝐶)
14245simpld 493 . . . . . . . . . . 11 (𝜑𝑊𝑇)
143141, 142sseldd 3981 . . . . . . . . . 10 (𝜑𝑊𝐶)
144 elssuni 4942 . . . . . . . . . . . 12 (𝑊𝑇𝑊 𝑇)
145142, 144syl 17 . . . . . . . . . . 11 (𝜑𝑊 𝑇)
1465cvmsuni 34884 . . . . . . . . . . . 12 (𝑇 ∈ (𝑆𝑀) → 𝑇 = (𝐹𝑀))
14731, 146syl 17 . . . . . . . . . . 11 (𝜑 𝑇 = (𝐹𝑀))
148145, 147sseqtrd 4020 . . . . . . . . . 10 (𝜑𝑊 ⊆ (𝐹𝑀))
1495cvmsrcl 34879 . . . . . . . . . . . . 13 (𝑇 ∈ (𝑆𝑀) → 𝑀𝐽)
15031, 149syl 17 . . . . . . . . . . . 12 (𝜑𝑀𝐽)
151 cnima 23187 . . . . . . . . . . . 12 ((𝐹 ∈ (𝐶 Cn 𝐽) ∧ 𝑀𝐽) → (𝐹𝑀) ∈ 𝐶)
152130, 150, 151syl2anc 582 . . . . . . . . . . 11 (𝜑 → (𝐹𝑀) ∈ 𝐶)
153 restopn2 23099 . . . . . . . . . . 11 ((𝐶 ∈ Top ∧ (𝐹𝑀) ∈ 𝐶) → (𝑊 ∈ (𝐶t (𝐹𝑀)) ↔ (𝑊𝐶𝑊 ⊆ (𝐹𝑀))))
154101, 152, 153syl2anc 582 . . . . . . . . . 10 (𝜑 → (𝑊 ∈ (𝐶t (𝐹𝑀)) ↔ (𝑊𝐶𝑊 ⊆ (𝐹𝑀))))
155143, 148, 154mpbir2and 711 . . . . . . . . 9 (𝜑𝑊 ∈ (𝐶t (𝐹𝑀)))
156155adantr 479 . . . . . . . 8 ((𝜑 ∧ (𝑚𝑈𝑛𝑉)) → 𝑊 ∈ (𝐶t (𝐹𝑀)))
1575cvmscld 34888 . . . . . . . . . 10 ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑇 ∈ (𝑆𝑀) ∧ 𝑊𝑇) → 𝑊 ∈ (Clsd‘(𝐶t (𝐹𝑀))))
1586, 31, 142, 157syl3anc 1368 . . . . . . . . 9 (𝜑𝑊 ∈ (Clsd‘(𝐶t (𝐹𝑀))))
159158adantr 479 . . . . . . . 8 ((𝜑 ∧ (𝑚𝑈𝑛𝑉)) → 𝑊 ∈ (Clsd‘(𝐶t (𝐹𝑀))))
160 cvmlift2lem9.10 . . . . . . . . . . 11 (𝜑𝑍𝑉)
161160adantr 479 . . . . . . . . . 10 ((𝜑 ∧ (𝑚𝑈𝑛𝑉)) → 𝑍𝑉)
162 opelxpi 5717 . . . . . . . . . 10 ((𝑚 ∈ {𝑚} ∧ 𝑍𝑉) → ⟨𝑚, 𝑍⟩ ∈ ({𝑚} × 𝑉))
16352, 161, 162syl2anc 582 . . . . . . . . 9 ((𝜑 ∧ (𝑚𝑈𝑛𝑉)) → ⟨𝑚, 𝑍⟩ ∈ ({𝑚} × 𝑉))
16481, 84sstrd 3990 . . . . . . . . . 10 ((𝜑 ∧ (𝑚𝑈𝑛𝑉)) → ({𝑚} × 𝑉) ⊆ ((0[,]1) × (0[,]1)))
1654restuni 23084 . . . . . . . . . 10 (((II ×t II) ∈ Top ∧ ({𝑚} × 𝑉) ⊆ ((0[,]1) × (0[,]1))) → ({𝑚} × 𝑉) = ((II ×t II) ↾t ({𝑚} × 𝑉)))
16615, 164, 165sylancr 585 . . . . . . . . 9 ((𝜑 ∧ (𝑚𝑈𝑛𝑉)) → ({𝑚} × 𝑉) = ((II ×t II) ↾t ({𝑚} × 𝑉)))
167163, 166eleqtrd 2830 . . . . . . . 8 ((𝜑 ∧ (𝑚𝑈𝑛𝑉)) → ⟨𝑚, 𝑍⟩ ∈ ((II ×t II) ↾t ({𝑚} × 𝑉)))
168 df-ov 7427 . . . . . . . . . 10 (𝑚(𝐾 ↾ ({𝑚} × 𝑉))𝑍) = ((𝐾 ↾ ({𝑚} × 𝑉))‘⟨𝑚, 𝑍⟩)
169 ovres 7591 . . . . . . . . . . . 12 ((𝑚 ∈ {𝑚} ∧ 𝑍𝑉) → (𝑚(𝐾 ↾ ({𝑚} × 𝑉))𝑍) = (𝑚𝐾𝑍))
17052, 161, 169syl2anc 582 . . . . . . . . . . 11 ((𝜑 ∧ (𝑚𝑈𝑛𝑉)) → (𝑚(𝐾 ↾ ({𝑚} × 𝑉))𝑍) = (𝑚𝐾𝑍))
171 snidg 4665 . . . . . . . . . . . . . 14 (𝑍𝑉𝑍 ∈ {𝑍})
172160, 171syl 17 . . . . . . . . . . . . 13 (𝜑𝑍 ∈ {𝑍})
173172adantr 479 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑚𝑈𝑛𝑉)) → 𝑍 ∈ {𝑍})
174 ovres 7591 . . . . . . . . . . . 12 ((𝑚𝑈𝑍 ∈ {𝑍}) → (𝑚(𝐾 ↾ (𝑈 × {𝑍}))𝑍) = (𝑚𝐾𝑍))
175106, 173, 174syl2anc 582 . . . . . . . . . . 11 ((𝜑 ∧ (𝑚𝑈𝑛𝑉)) → (𝑚(𝐾 ↾ (𝑈 × {𝑍}))𝑍) = (𝑚𝐾𝑍))
176170, 175eqtr4d 2770 . . . . . . . . . 10 ((𝜑 ∧ (𝑚𝑈𝑛𝑉)) → (𝑚(𝐾 ↾ ({𝑚} × 𝑉))𝑍) = (𝑚(𝐾 ↾ (𝑈 × {𝑍}))𝑍))
177168, 176eqtr3id 2781 . . . . . . . . 9 ((𝜑 ∧ (𝑚𝑈𝑛𝑉)) → ((𝐾 ↾ ({𝑚} × 𝑉))‘⟨𝑚, 𝑍⟩) = (𝑚(𝐾 ↾ (𝑈 × {𝑍}))𝑍))
178 eqid 2727 . . . . . . . . . . . . 13 ((II ×t II) ↾t (𝑈 × {𝑍})) = ((II ×t II) ↾t (𝑈 × {𝑍}))
1792a1i 11 . . . . . . . . . . . . . . 15 (𝜑 → II ∈ Top)
180 snex 5435 . . . . . . . . . . . . . . . 16 {𝑍} ∈ V
181180a1i 11 . . . . . . . . . . . . . . 15 (𝜑 → {𝑍} ∈ V)
182 txrest 23553 . . . . . . . . . . . . . . 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 3981 . . . . . . . . . . . . . . . . 17 (𝜑𝑍 ∈ (0[,]1))
186 restsn2 23093 . . . . . . . . . . . . . . . . 17 ((II ∈ (TopOn‘(0[,]1)) ∧ 𝑍 ∈ (0[,]1)) → (II ↾t {𝑍}) = 𝒫 {𝑍})
18763, 185, 186sylancr 585 . . . . . . . . . . . . . . . 16 (𝜑 → (II ↾t {𝑍}) = 𝒫 {𝑍})
188 pwsn 4903 . . . . . . . . . . . . . . . . 17 𝒫 {𝑍} = {∅, {𝑍}}
189 indisconn 23340 . . . . . . . . . . . . . . . . 17 {∅, {𝑍}} ∈ Conn
190188, 189eqeltri 2824 . . . . . . . . . . . . . . . 16 𝒫 {𝑍} ∈ Conn
191187, 190eqeltrdi 2836 . . . . . . . . . . . . . . 15 (𝜑 → (II ↾t {𝑍}) ∈ Conn)
192 txconn 23611 . . . . . . . . . . . . . . 15 (((II ↾t 𝑈) ∈ Conn ∧ (II ↾t {𝑍}) ∈ Conn) → ((II ↾t 𝑈) ×t (II ↾t {𝑍})) ∈ Conn)
193184, 191, 192syl2anc 582 . . . . . . . . . . . . . 14 (𝜑 → ((II ↾t 𝑈) ×t (II ↾t {𝑍})) ∈ Conn)
194183, 193eqeltrd 2828 . . . . . . . . . . . . 13 (𝜑 → ((II ×t II) ↾t (𝑈 × {𝑍})) ∈ Conn)
195 cvmlift2lem9.11 . . . . . . . . . . . . . 14 (𝜑 → (𝐾 ↾ (𝑈 × {𝑍})) ∈ (((II ×t II) ↾t (𝑈 × {𝑍})) Cn 𝐶))
196101, 103sylib 217 . . . . . . . . . . . . . . 15 (𝜑𝐶 ∈ (TopOn‘𝐵))
197 df-ima 5693 . . . . . . . . . . . . . . . 16 (𝐾 “ (𝑈 × {𝑍})) = ran (𝐾 ↾ (𝑈 × {𝑍}))
198160snssd 4815 . . . . . . . . . . . . . . . . . 18 (𝜑 → {𝑍} ⊆ 𝑉)
199 xpss2 5700 . . . . . . . . . . . . . . . . . 18 ({𝑍} ⊆ 𝑉 → (𝑈 × {𝑍}) ⊆ (𝑈 × 𝑉))
200 imass2 6109 . . . . . . . . . . . . . . . . . 18 ((𝑈 × {𝑍}) ⊆ (𝑈 × 𝑉) → (𝐾 “ (𝑈 × {𝑍})) ⊆ (𝐾 “ (𝑈 × 𝑉)))
201198, 199, 2003syl 18 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐾 “ (𝑈 × {𝑍})) ⊆ (𝐾 “ (𝑈 × 𝑉)))
202201, 124sstrd 3990 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐾 “ (𝑈 × {𝑍})) ⊆ (𝐹𝑀))
203197, 202eqsstrrid 4029 . . . . . . . . . . . . . . 15 (𝜑 → ran (𝐾 ↾ (𝑈 × {𝑍})) ⊆ (𝐹𝑀))
204 cnrest2 23208 . . . . . . . . . . . . . . 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 231 . . . . . . . . . . . . 13 (𝜑 → (𝐾 ↾ (𝑈 × {𝑍})) ∈ (((II ×t II) ↾t (𝑈 × {𝑍})) Cn (𝐶t (𝐹𝑀))))
207 opelxpi 5717 . . . . . . . . . . . . . . 15 ((𝑋𝑈𝑍 ∈ {𝑍}) → ⟨𝑋, 𝑍⟩ ∈ (𝑈 × {𝑍}))
20821, 172, 207syl2anc 582 . . . . . . . . . . . . . 14 (𝜑 → ⟨𝑋, 𝑍⟩ ∈ (𝑈 × {𝑍}))
209185snssd 4815 . . . . . . . . . . . . . . . 16 (𝜑 → {𝑍} ⊆ (0[,]1))
210 xpss12 5695 . . . . . . . . . . . . . . . 16 ((𝑈 ⊆ (0[,]1) ∧ {𝑍} ⊆ (0[,]1)) → (𝑈 × {𝑍}) ⊆ ((0[,]1) × (0[,]1)))
21120, 209, 210syl2anc 582 . . . . . . . . . . . . . . 15 (𝜑 → (𝑈 × {𝑍}) ⊆ ((0[,]1) × (0[,]1)))
2124restuni 23084 . . . . . . . . . . . . . . 15 (((II ×t II) ∈ Top ∧ (𝑈 × {𝑍}) ⊆ ((0[,]1) × (0[,]1))) → (𝑈 × {𝑍}) = ((II ×t II) ↾t (𝑈 × {𝑍})))
21315, 211, 212sylancr 585 . . . . . . . . . . . . . 14 (𝜑 → (𝑈 × {𝑍}) = ((II ×t II) ↾t (𝑈 × {𝑍})))
214208, 213eleqtrd 2830 . . . . . . . . . . . . 13 (𝜑 → ⟨𝑋, 𝑍⟩ ∈ ((II ×t II) ↾t (𝑈 × {𝑍})))
215 df-ov 7427 . . . . . . . . . . . . . . 15 (𝑋(𝐾 ↾ (𝑈 × {𝑍}))𝑍) = ((𝐾 ↾ (𝑈 × {𝑍}))‘⟨𝑋, 𝑍⟩)
216 ovres 7591 . . . . . . . . . . . . . . . . 17 ((𝑋𝑈𝑍 ∈ {𝑍}) → (𝑋(𝐾 ↾ (𝑈 × {𝑍}))𝑍) = (𝑋𝐾𝑍))
21721, 172, 216syl2anc 582 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑋(𝐾 ↾ (𝑈 × {𝑍}))𝑍) = (𝑋𝐾𝑍))
218 snidg 4665 . . . . . . . . . . . . . . . . . 18 (𝑋𝑈𝑋 ∈ {𝑋})
21921, 218syl 17 . . . . . . . . . . . . . . . . 17 (𝜑𝑋 ∈ {𝑋})
220 ovres 7591 . . . . . . . . . . . . . . . . 17 ((𝑋 ∈ {𝑋} ∧ 𝑍𝑉) → (𝑋(𝐾 ↾ ({𝑋} × 𝑉))𝑍) = (𝑋𝐾𝑍))
221219, 160, 220syl2anc 582 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑋(𝐾 ↾ ({𝑋} × 𝑉))𝑍) = (𝑋𝐾𝑍))
222217, 221eqtr4d 2770 . . . . . . . . . . . . . . 15 (𝜑 → (𝑋(𝐾 ↾ (𝑈 × {𝑍}))𝑍) = (𝑋(𝐾 ↾ ({𝑋} × 𝑉))𝑍))
223215, 222eqtr3id 2781 . . . . . . . . . . . . . 14 (𝜑 → ((𝐾 ↾ (𝑈 × {𝑍}))‘⟨𝑋, 𝑍⟩) = (𝑋(𝐾 ↾ ({𝑋} × 𝑉))𝑍))
224 eqid 2727 . . . . . . . . . . . . . . . . 17 ((II ×t II) ↾t ({𝑋} × 𝑉)) = ((II ×t II) ↾t ({𝑋} × 𝑉))
225 snex 5435 . . . . . . . . . . . . . . . . . . . 20 {𝑋} ∈ V
226225a1i 11 . . . . . . . . . . . . . . . . . . 19 (𝜑 → {𝑋} ∈ V)
227 txrest 23553 . . . . . . . . . . . . . . . . . . 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 23093 . . . . . . . . . . . . . . . . . . . . 21 ((II ∈ (TopOn‘(0[,]1)) ∧ 𝑋 ∈ (0[,]1)) → (II ↾t {𝑋}) = 𝒫 {𝑋})
23063, 22, 229sylancr 585 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (II ↾t {𝑋}) = 𝒫 {𝑋})
231 pwsn 4903 . . . . . . . . . . . . . . . . . . . . 21 𝒫 {𝑋} = {∅, {𝑋}}
232 indisconn 23340 . . . . . . . . . . . . . . . . . . . . 21 {∅, {𝑋}} ∈ Conn
233231, 232eqeltri 2824 . . . . . . . . . . . . . . . . . . . 20 𝒫 {𝑋} ∈ Conn
234230, 233eqeltrdi 2836 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (II ↾t {𝑋}) ∈ Conn)
235 txconn 23611 . . . . . . . . . . . . . . . . . . 19 (((II ↾t {𝑋}) ∈ Conn ∧ (II ↾t 𝑉) ∈ Conn) → ((II ↾t {𝑋}) ×t (II ↾t 𝑉)) ∈ Conn)
236234, 72, 235syl2anc 582 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((II ↾t {𝑋}) ×t (II ↾t 𝑉)) ∈ Conn)
237228, 236eqeltrd 2828 . . . . . . . . . . . . . . . . 17 (𝜑 → ((II ×t II) ↾t ({𝑋} × 𝑉)) ∈ Conn)
2381, 6, 7, 8, 9, 10, 11cvmlift2lem6 34923 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑋 ∈ (0[,]1)) → (𝐾 ↾ ({𝑋} × (0[,]1))) ∈ (((II ×t II) ↾t ({𝑋} × (0[,]1))) Cn 𝐶))
23922, 238mpdan 685 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝐾 ↾ ({𝑋} × (0[,]1))) ∈ (((II ×t II) ↾t ({𝑋} × (0[,]1))) Cn 𝐶))
240 xpss2 5700 . . . . . . . . . . . . . . . . . . . . . 22 (𝑉 ⊆ (0[,]1) → ({𝑋} × 𝑉) ⊆ ({𝑋} × (0[,]1)))
24123, 25, 2403syl 18 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ({𝑋} × 𝑉) ⊆ ({𝑋} × (0[,]1)))
24222snssd 4815 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → {𝑋} ⊆ (0[,]1))
243 xpss1 5699 . . . . . . . . . . . . . . . . . . . . . . 23 ({𝑋} ⊆ (0[,]1) → ({𝑋} × (0[,]1)) ⊆ ((0[,]1) × (0[,]1)))
244242, 243syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ({𝑋} × (0[,]1)) ⊆ ((0[,]1) × (0[,]1)))
2454restuni 23084 . . . . . . . . . . . . . . . . . . . . . 22 (((II ×t II) ∈ Top ∧ ({𝑋} × (0[,]1)) ⊆ ((0[,]1) × (0[,]1))) → ({𝑋} × (0[,]1)) = ((II ×t II) ↾t ({𝑋} × (0[,]1))))
24615, 244, 245sylancr 585 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ({𝑋} × (0[,]1)) = ((II ×t II) ↾t ({𝑋} × (0[,]1))))
247241, 246sseqtrd 4020 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ({𝑋} × 𝑉) ⊆ ((II ×t II) ↾t ({𝑋} × (0[,]1))))
248 eqid 2727 . . . . . . . . . . . . . . . . . . . . 21 ((II ×t II) ↾t ({𝑋} × (0[,]1))) = ((II ×t II) ↾t ({𝑋} × (0[,]1)))
249248cnrest 23207 . . . . . . . . . . . . . . . . . . . 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 582 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝐾 ↾ ({𝑋} × (0[,]1))) ↾ ({𝑋} × 𝑉)) ∈ ((((II ×t II) ↾t ({𝑋} × (0[,]1))) ↾t ({𝑋} × 𝑉)) Cn 𝐶))
251241resabs1d 6015 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝐾 ↾ ({𝑋} × (0[,]1))) ↾ ({𝑋} × 𝑉)) = (𝐾 ↾ ({𝑋} × 𝑉)))
252225, 93xpex 7759 . . . . . . . . . . . . . . . . . . . . . 22 ({𝑋} × (0[,]1)) ∈ V
253252a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ({𝑋} × (0[,]1)) ∈ V)
254 restabs 23087 . . . . . . . . . . . . . . . . . . . . 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 7439 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((((II ×t II) ↾t ({𝑋} × (0[,]1))) ↾t ({𝑋} × 𝑉)) Cn 𝐶) = (((II ×t II) ↾t ({𝑋} × 𝑉)) Cn 𝐶))
257250, 251, 2563eltr3d 2842 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐾 ↾ ({𝑋} × 𝑉)) ∈ (((II ×t II) ↾t ({𝑋} × 𝑉)) Cn 𝐶))
258 df-ima 5693 . . . . . . . . . . . . . . . . . . . 20 (𝐾 “ ({𝑋} × 𝑉)) = ran (𝐾 ↾ ({𝑋} × 𝑉))
25921snssd 4815 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → {𝑋} ⊆ 𝑈)
260 xpss1 5699 . . . . . . . . . . . . . . . . . . . . . 22 ({𝑋} ⊆ 𝑈 → ({𝑋} × 𝑉) ⊆ (𝑈 × 𝑉))
261 imass2 6109 . . . . . . . . . . . . . . . . . . . . . 22 (({𝑋} × 𝑉) ⊆ (𝑈 × 𝑉) → (𝐾 “ ({𝑋} × 𝑉)) ⊆ (𝐾 “ (𝑈 × 𝑉)))
262259, 260, 2613syl 18 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝐾 “ ({𝑋} × 𝑉)) ⊆ (𝐾 “ (𝑈 × 𝑉)))
263262, 124sstrd 3990 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝐾 “ ({𝑋} × 𝑉)) ⊆ (𝐹𝑀))
264258, 263eqsstrrid 4029 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ran (𝐾 ↾ ({𝑋} × 𝑉)) ⊆ (𝐹𝑀))
265 cnrest2 23208 . . . . . . . . . . . . . . . . . . 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 231 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐾 ↾ ({𝑋} × 𝑉)) ∈ (((II ×t II) ↾t ({𝑋} × 𝑉)) Cn (𝐶t (𝐹𝑀))))
268 opelxpi 5717 . . . . . . . . . . . . . . . . . . 19 ((𝑋 ∈ {𝑋} ∧ 𝑌𝑉) → ⟨𝑋, 𝑌⟩ ∈ ({𝑋} × 𝑉))
269219, 27, 268syl2anc 582 . . . . . . . . . . . . . . . . . 18 (𝜑 → ⟨𝑋, 𝑌⟩ ∈ ({𝑋} × 𝑉))
270259, 260syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ({𝑋} × 𝑉) ⊆ (𝑈 × 𝑉))
271270, 50sstrd 3990 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ({𝑋} × 𝑉) ⊆ ((0[,]1) × (0[,]1)))
2724restuni 23084 . . . . . . . . . . . . . . . . . . 19 (((II ×t II) ∈ Top ∧ ({𝑋} × 𝑉) ⊆ ((0[,]1) × (0[,]1))) → ({𝑋} × 𝑉) = ((II ×t II) ↾t ({𝑋} × 𝑉)))
27315, 271, 272sylancr 585 . . . . . . . . . . . . . . . . . 18 (𝜑 → ({𝑋} × 𝑉) = ((II ×t II) ↾t ({𝑋} × 𝑉)))
274269, 273eleqtrd 2830 . . . . . . . . . . . . . . . . 17 (𝜑 → ⟨𝑋, 𝑌⟩ ∈ ((II ×t II) ↾t ({𝑋} × 𝑉)))
275 df-ov 7427 . . . . . . . . . . . . . . . . . . 19 (𝑋(𝐾 ↾ ({𝑋} × 𝑉))𝑌) = ((𝐾 ↾ ({𝑋} × 𝑉))‘⟨𝑋, 𝑌⟩)
276 ovres 7591 . . . . . . . . . . . . . . . . . . . 20 ((𝑋 ∈ {𝑋} ∧ 𝑌𝑉) → (𝑋(𝐾 ↾ ({𝑋} × 𝑉))𝑌) = (𝑋𝐾𝑌))
277219, 27, 276syl2anc 582 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑋(𝐾 ↾ ({𝑋} × 𝑉))𝑌) = (𝑋𝐾𝑌))
278275, 277eqtr3id 2781 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝐾 ↾ ({𝑋} × 𝑉))‘⟨𝑋, 𝑌⟩) = (𝑋𝐾𝑌))
27945simprd 494 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑋𝐾𝑌) ∈ 𝑊)
280278, 279eqeltrd 2828 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝐾 ↾ ({𝑋} × 𝑉))‘⟨𝑋, 𝑌⟩) ∈ 𝑊)
281224, 237, 267, 155, 158, 274, 280conncn 23348 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐾 ↾ ({𝑋} × 𝑉)): ((II ×t II) ↾t ({𝑋} × 𝑉))⟶𝑊)
282273feq2d 6711 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐾 ↾ ({𝑋} × 𝑉)):({𝑋} × 𝑉)⟶𝑊 ↔ (𝐾 ↾ ({𝑋} × 𝑉)): ((II ×t II) ↾t ({𝑋} × 𝑉))⟶𝑊))
283281, 282mpbird 256 . . . . . . . . . . . . . . 15 (𝜑 → (𝐾 ↾ ({𝑋} × 𝑉)):({𝑋} × 𝑉)⟶𝑊)
284283, 219, 160fovcdmd 7597 . . . . . . . . . . . . . 14 (𝜑 → (𝑋(𝐾 ↾ ({𝑋} × 𝑉))𝑍) ∈ 𝑊)
285223, 284eqeltrd 2828 . . . . . . . . . . . . 13 (𝜑 → ((𝐾 ↾ (𝑈 × {𝑍}))‘⟨𝑋, 𝑍⟩) ∈ 𝑊)
286178, 194, 206, 155, 158, 214, 285conncn 23348 . . . . . . . . . . . 12 (𝜑 → (𝐾 ↾ (𝑈 × {𝑍})): ((II ×t II) ↾t (𝑈 × {𝑍}))⟶𝑊)
287213feq2d 6711 . . . . . . . . . . . 12 (𝜑 → ((𝐾 ↾ (𝑈 × {𝑍})):(𝑈 × {𝑍})⟶𝑊 ↔ (𝐾 ↾ (𝑈 × {𝑍})): ((II ×t II) ↾t (𝑈 × {𝑍}))⟶𝑊))
288286, 287mpbird 256 . . . . . . . . . . 11 (𝜑 → (𝐾 ↾ (𝑈 × {𝑍})):(𝑈 × {𝑍})⟶𝑊)
289288adantr 479 . . . . . . . . . 10 ((𝜑 ∧ (𝑚𝑈𝑛𝑉)) → (𝐾 ↾ (𝑈 × {𝑍})):(𝑈 × {𝑍})⟶𝑊)
290289, 106, 173fovcdmd 7597 . . . . . . . . 9 ((𝜑 ∧ (𝑚𝑈𝑛𝑉)) → (𝑚(𝐾 ↾ (𝑈 × {𝑍}))𝑍) ∈ 𝑊)
291177, 290eqeltrd 2828 . . . . . . . 8 ((𝜑 ∧ (𝑚𝑈𝑛𝑉)) → ((𝐾 ↾ ({𝑚} × 𝑉))‘⟨𝑚, 𝑍⟩) ∈ 𝑊)
29256, 76, 139, 156, 159, 167, 291conncn 23348 . . . . . . 7 ((𝜑 ∧ (𝑚𝑈𝑛𝑉)) → (𝐾 ↾ ({𝑚} × 𝑉)): ((II ×t II) ↾t ({𝑚} × 𝑉))⟶𝑊)
293166feq2d 6711 . . . . . . 7 ((𝜑 ∧ (𝑚𝑈𝑛𝑉)) → ((𝐾 ↾ ({𝑚} × 𝑉)):({𝑚} × 𝑉)⟶𝑊 ↔ (𝐾 ↾ ({𝑚} × 𝑉)): ((II ×t II) ↾t ({𝑚} × 𝑉))⟶𝑊))
294292, 293mpbird 256 . . . . . 6 ((𝜑 ∧ (𝑚𝑈𝑛𝑉)) → (𝐾 ↾ ({𝑚} × 𝑉)):({𝑚} × 𝑉)⟶𝑊)
295294, 52, 53fovcdmd 7597 . . . . 5 ((𝜑 ∧ (𝑚𝑈𝑛𝑉)) → (𝑚(𝐾 ↾ ({𝑚} × 𝑉))𝑛) ∈ 𝑊)
29655, 295eqeltrrd 2829 . . . 4 ((𝜑 ∧ (𝑚𝑈𝑛𝑉)) → (𝑚𝐾𝑛) ∈ 𝑊)
297296ralrimivva 3196 . . 3 (𝜑 → ∀𝑚𝑈𝑛𝑉 (𝑚𝐾𝑛) ∈ 𝑊)
298 funimassov 7602 . . . 4 ((Fun 𝐾 ∧ (𝑈 × 𝑉) ⊆ dom 𝐾) → ((𝐾 “ (𝑈 × 𝑉)) ⊆ 𝑊 ↔ ∀𝑚𝑈𝑛𝑉 (𝑚𝐾𝑛) ∈ 𝑊))
299119, 121, 298syl2anc 582 . . 3 (𝜑 → ((𝐾 “ (𝑈 × 𝑉)) ⊆ 𝑊 ↔ ∀𝑚𝑈𝑛𝑉 (𝑚𝐾𝑛) ∈ 𝑊))
300297, 299mpbird 256 . 2 (𝜑 → (𝐾 “ (𝑈 × 𝑉)) ⊆ 𝑊)
3011, 4, 5, 6, 12, 14, 16, 30, 31, 48, 50, 300cvmlift2lem9a 34918 1 (𝜑 → (𝐾 ↾ (𝑈 × 𝑉)) ∈ (((II ×t II) ↾t (𝑈 × 𝑉)) Cn 𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 394   = wceq 1533  wcel 2098  wral 3057  {crab 3428  Vcvv 3471  cdif 3944  cin 3946  wss 3947  c0 4324  𝒫 cpw 4604  {csn 4630  {cpr 4632  cop 4636   cuni 4910  cmpt 5233   × cxp 5678  ccnv 5679  dom cdm 5680  ran crn 5681  cres 5682  cima 5683  ccom 5684  Fun wfun 6545  wf 6547  cfv 6551  crio 7379  (class class class)co 7424  cmpo 7426  0cc0 11144  1c1 11145  [,]cicc 13365  t crest 17407  Topctop 22813  TopOnctopon 22830  Clsdccld 22938   Cn ccn 23146  Conncconn 23333   ×t ctx 23482  Homeochmeo 23675  IIcii 24813   CovMap ccvm 34870
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2698  ax-rep 5287  ax-sep 5301  ax-nul 5308  ax-pow 5367  ax-pr 5431  ax-un 7744  ax-inf2 9670  ax-cnex 11200  ax-resscn 11201  ax-1cn 11202  ax-icn 11203  ax-addcl 11204  ax-addrcl 11205  ax-mulcl 11206  ax-mulrcl 11207  ax-mulcom 11208  ax-addass 11209  ax-mulass 11210  ax-distr 11211  ax-i2m1 11212  ax-1ne0 11213  ax-1rid 11214  ax-rnegex 11215  ax-rrecex 11216  ax-cnre 11217  ax-pre-lttri 11218  ax-pre-lttrn 11219  ax-pre-ltadd 11220  ax-pre-mulgt0 11221  ax-pre-sup 11222  ax-addf 11223
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2529  df-eu 2558  df-clab 2705  df-cleq 2719  df-clel 2805  df-nfc 2880  df-ne 2937  df-nel 3043  df-ral 3058  df-rex 3067  df-rmo 3372  df-reu 3373  df-rab 3429  df-v 3473  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4325  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-tp 4635  df-op 4637  df-uni 4911  df-int 4952  df-iun 5000  df-iin 5001  df-br 5151  df-opab 5213  df-mpt 5234  df-tr 5268  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5635  df-se 5636  df-we 5637  df-xp 5686  df-rel 5687  df-cnv 5688  df-co 5689  df-dm 5690  df-rn 5691  df-res 5692  df-ima 5693  df-pred 6308  df-ord 6375  df-on 6376  df-lim 6377  df-suc 6378  df-iota 6503  df-fun 6553  df-fn 6554  df-f 6555  df-f1 6556  df-fo 6557  df-f1o 6558  df-fv 6559  df-isom 6560  df-riota 7380  df-ov 7427  df-oprab 7428  df-mpo 7429  df-of 7689  df-om 7875  df-1st 7997  df-2nd 7998  df-supp 8170  df-frecs 8291  df-wrecs 8322  df-recs 8396  df-rdg 8435  df-1o 8491  df-2o 8492  df-er 8729  df-ec 8731  df-map 8851  df-ixp 8921  df-en 8969  df-dom 8970  df-sdom 8971  df-fin 8972  df-fsupp 9392  df-fi 9440  df-sup 9471  df-inf 9472  df-oi 9539  df-card 9968  df-pnf 11286  df-mnf 11287  df-xr 11288  df-ltxr 11289  df-le 11290  df-sub 11482  df-neg 11483  df-div 11908  df-nn 12249  df-2 12311  df-3 12312  df-4 12313  df-5 12314  df-6 12315  df-7 12316  df-8 12317  df-9 12318  df-n0 12509  df-z 12595  df-dec 12714  df-uz 12859  df-q 12969  df-rp 13013  df-xneg 13130  df-xadd 13131  df-xmul 13132  df-ioo 13366  df-ico 13368  df-icc 13369  df-fz 13523  df-fzo 13666  df-fl 13795  df-seq 14005  df-exp 14065  df-hash 14328  df-cj 15084  df-re 15085  df-im 15086  df-sqrt 15220  df-abs 15221  df-clim 15470  df-sum 15671  df-struct 17121  df-sets 17138  df-slot 17156  df-ndx 17168  df-base 17186  df-ress 17215  df-plusg 17251  df-mulr 17252  df-starv 17253  df-sca 17254  df-vsca 17255  df-ip 17256  df-tset 17257  df-ple 17258  df-ds 17260  df-unif 17261  df-hom 17262  df-cco 17263  df-rest 17409  df-topn 17410  df-0g 17428  df-gsum 17429  df-topgen 17430  df-pt 17431  df-prds 17434  df-xrs 17489  df-qtop 17494  df-imas 17495  df-xps 17497  df-mre 17571  df-mrc 17572  df-acs 17574  df-mgm 18605  df-sgrp 18684  df-mnd 18700  df-submnd 18746  df-mulg 19029  df-cntz 19273  df-cmn 19742  df-psmet 21276  df-xmet 21277  df-met 21278  df-bl 21279  df-mopn 21280  df-cnfld 21285  df-top 22814  df-topon 22831  df-topsp 22853  df-bases 22867  df-cld 22941  df-ntr 22942  df-cls 22943  df-nei 23020  df-cn 23149  df-cnp 23150  df-cmp 23309  df-conn 23334  df-lly 23388  df-nlly 23389  df-tx 23484  df-hmeo 23677  df-xms 24244  df-ms 24245  df-tms 24246  df-ii 24815  df-cncf 24816  df-htpy 24914  df-phtpy 24915  df-phtpc 24936  df-pconn 34836  df-sconn 34837  df-cvm 34871
This theorem is referenced by:  cvmlift2lem10  34927
  Copyright terms: Public domain W3C validator