cvmlift2lem9 - Mathbox for Mario Carneiro

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

Theorem cvmlift2lem9 35505

Description: Lemma for cvmlift2 35510. (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.

Step	Hyp	Ref	Expression
1		cvmlift2.b	. 2 ⊢ 𝐵 = ∪ 𝐶
2		iitop 24829	. . 3 ⊢ II ∈ Top
3		iiuni 24830	. . 3 ⊢ (0[,]1) = ∪ II
4	2, 2, 3, 3	txunii 23537	. 2 ⊢ ((0[,]1) × (0[,]1)) = ∪ (II ×_t II)
5		cvmlift2lem10.s	. 2 ⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (^◡𝐹 “ 𝑘) ∧ ∀𝑐 ∈ 𝑠 (∀𝑑 ∈ (𝑠 ∖ {𝑐})(𝑐 ∩ 𝑑) = ∅ ∧ (𝐹 ↾ 𝑐) ∈ ((𝐶 ↾_t 𝑐)Homeo(𝐽 ↾_t 𝑘))))})
6		cvmlift2.f	. 2 ⊢ (𝜑 → 𝐹 ∈ (𝐶 CovMap 𝐽))
7		cvmlift2.g	. . 3 ⊢ (𝜑 → 𝐺 ∈ ((II ×_t II) Cn 𝐽))
8		cvmlift2.p	. . 3 ⊢ (𝜑 → 𝑃 ∈ 𝐵)
9		cvmlift2.i	. . 3 ⊢ (𝜑 → (𝐹‘𝑃) = (0𝐺0))
10		cvmlift2.h	. . 3 ⊢ 𝐻 = (℩𝑓 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑓) = (𝑧 ∈ (0[,]1) ↦ (𝑧𝐺0)) ∧ (𝑓‘0) = 𝑃))
11		cvmlift2.k	. . 3 ⊢ 𝐾 = (𝑥 ∈ (0[,]1), 𝑦 ∈ (0[,]1) ↦ ((℩𝑓 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑓) = (𝑧 ∈ (0[,]1) ↦ (𝑥𝐺𝑧)) ∧ (𝑓‘0) = (𝐻‘𝑥)))‘𝑦))
12	1, 6, 7, 8, 9, 10, 11	cvmlift2lem5 35501	. 2 ⊢ (𝜑 → 𝐾:((0[,]1) × (0[,]1))⟶𝐵)
13	1, 6, 7, 8, 9, 10, 11	cvmlift2lem7 35503	. . 3 ⊢ (𝜑 → (𝐹 ∘ 𝐾) = 𝐺)
14	13, 7	eqeltrd 2836	. 2 ⊢ (𝜑 → (𝐹 ∘ 𝐾) ∈ ((II ×_t II) Cn 𝐽))
15	2, 2	txtopi 23534	. . 3 ⊢ (II ×_t II) ∈ Top
16	15	a1i 11	. 2 ⊢ (𝜑 → (II ×_t II) ∈ Top)
17		cvmlift2lem9.3	. . . . 5 ⊢ (𝜑 → 𝑈 ∈ II)
18		elssuni 4894	. . . . . 6 ⊢ (𝑈 ∈ II → 𝑈 ⊆ ∪ II)
19	18, 3	sseqtrrdi 3975	. . . . 5 ⊢ (𝑈 ∈ II → 𝑈 ⊆ (0[,]1))
20	17, 19	syl 17	. . . 4 ⊢ (𝜑 → 𝑈 ⊆ (0[,]1))
21		cvmlift2lem9.7	. . . 4 ⊢ (𝜑 → 𝑋 ∈ 𝑈)
22	20, 21	sseldd 3934	. . 3 ⊢ (𝜑 → 𝑋 ∈ (0[,]1))
23		cvmlift2lem9.4	. . . . 5 ⊢ (𝜑 → 𝑉 ∈ II)
24		elssuni 4894	. . . . . 6 ⊢ (𝑉 ∈ II → 𝑉 ⊆ ∪ II)
25	24, 3	sseqtrrdi 3975	. . . . 5 ⊢ (𝑉 ∈ II → 𝑉 ⊆ (0[,]1))
26	23, 25	syl 17	. . . 4 ⊢ (𝜑 → 𝑉 ⊆ (0[,]1))
27		cvmlift2lem9.8	. . . 4 ⊢ (𝜑 → 𝑌 ∈ 𝑉)
28	26, 27	sseldd 3934	. . 3 ⊢ (𝜑 → 𝑌 ∈ (0[,]1))
29		opelxpi 5661	. . 3 ⊢ ((𝑋 ∈ (0[,]1) ∧ 𝑌 ∈ (0[,]1)) → ⟨𝑋, 𝑌⟩ ∈ ((0[,]1) × (0[,]1)))
30	22, 28, 29	syl2anc 584	. 2 ⊢ (𝜑 → ⟨𝑋, 𝑌⟩ ∈ ((0[,]1) × (0[,]1)))
31		cvmlift2lem9.2	. 2 ⊢ (𝜑 → 𝑇 ∈ (𝑆‘𝑀))
32	12, 22, 28	fovcdmd 7530	. . . 4 ⊢ (𝜑 → (𝑋𝐾𝑌) ∈ 𝐵)
33		fvco3 6933	. . . . . . . 8 ⊢ ((𝐾:((0[,]1) × (0[,]1))⟶𝐵 ∧ ⟨𝑋, 𝑌⟩ ∈ ((0[,]1) × (0[,]1))) → ((𝐹 ∘ 𝐾)‘⟨𝑋, 𝑌⟩) = (𝐹‘(𝐾‘⟨𝑋, 𝑌⟩)))
34	12, 30, 33	syl2anc 584	. . . . . . 7 ⊢ (𝜑 → ((𝐹 ∘ 𝐾)‘⟨𝑋, 𝑌⟩) = (𝐹‘(𝐾‘⟨𝑋, 𝑌⟩)))
35	13	fveq1d 6836	. . . . . . 7 ⊢ (𝜑 → ((𝐹 ∘ 𝐾)‘⟨𝑋, 𝑌⟩) = (𝐺‘⟨𝑋, 𝑌⟩))
36	34, 35	eqtr3d 2773	. . . . . 6 ⊢ (𝜑 → (𝐹‘(𝐾‘⟨𝑋, 𝑌⟩)) = (𝐺‘⟨𝑋, 𝑌⟩))
37		df-ov 7361	. . . . . . 7 ⊢ (𝑋𝐾𝑌) = (𝐾‘⟨𝑋, 𝑌⟩)
38	37	fveq2i 6837	. . . . . 6 ⊢ (𝐹‘(𝑋𝐾𝑌)) = (𝐹‘(𝐾‘⟨𝑋, 𝑌⟩))
39		df-ov 7361	. . . . . 6 ⊢ (𝑋𝐺𝑌) = (𝐺‘⟨𝑋, 𝑌⟩)
40	36, 38, 39	3eqtr4g 2796	. . . . 5 ⊢ (𝜑 → (𝐹‘(𝑋𝐾𝑌)) = (𝑋𝐺𝑌))
41		cvmlift2lem9.1	. . . . 5 ⊢ (𝜑 → (𝑋𝐺𝑌) ∈ 𝑀)
42	40, 41	eqeltrd 2836	. . . 4 ⊢ (𝜑 → (𝐹‘(𝑋𝐾𝑌)) ∈ 𝑀)
43		cvmlift2lem9.w	. . . . 5 ⊢ 𝑊 = (℩𝑏 ∈ 𝑇 (𝑋𝐾𝑌) ∈ 𝑏)
44	5, 1, 43	cvmsiota 35471	. . . 4 ⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ (𝑇 ∈ (𝑆‘𝑀) ∧ (𝑋𝐾𝑌) ∈ 𝐵 ∧ (𝐹‘(𝑋𝐾𝑌)) ∈ 𝑀)) → (𝑊 ∈ 𝑇 ∧ (𝑋𝐾𝑌) ∈ 𝑊))
45	6, 31, 32, 42, 44	syl13anc 1374	. . 3 ⊢ (𝜑 → (𝑊 ∈ 𝑇 ∧ (𝑋𝐾𝑌) ∈ 𝑊))
46	37	eleq1i 2827	. . . 4 ⊢ ((𝑋𝐾𝑌) ∈ 𝑊 ↔ (𝐾‘⟨𝑋, 𝑌⟩) ∈ 𝑊)
47	46	anbi2i 623	. . 3 ⊢ ((𝑊 ∈ 𝑇 ∧ (𝑋𝐾𝑌) ∈ 𝑊) ↔ (𝑊 ∈ 𝑇 ∧ (𝐾‘⟨𝑋, 𝑌⟩) ∈ 𝑊))
48	45, 47	sylib 218	. 2 ⊢ (𝜑 → (𝑊 ∈ 𝑇 ∧ (𝐾‘⟨𝑋, 𝑌⟩) ∈ 𝑊))
49		xpss12 5639	. . 3 ⊢ ((𝑈 ⊆ (0[,]1) ∧ 𝑉 ⊆ (0[,]1)) → (𝑈 × 𝑉) ⊆ ((0[,]1) × (0[,]1)))
50	20, 26, 49	syl2anc 584	. 2 ⊢ (𝜑 → (𝑈 × 𝑉) ⊆ ((0[,]1) × (0[,]1)))
51		snidg 4617	. . . . . . 7 ⊢ (𝑚 ∈ 𝑈 → 𝑚 ∈ {𝑚})
52	51	ad2antrl 728	. . . . . 6 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → 𝑚 ∈ {𝑚})
53		simprr 772	. . . . . 6 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → 𝑛 ∈ 𝑉)
54		ovres 7524	. . . . . 6 ⊢ ((𝑚 ∈ {𝑚} ∧ 𝑛 ∈ 𝑉) → (𝑚(𝐾 ↾ ({𝑚} × 𝑉))𝑛) = (𝑚𝐾𝑛))
55	52, 53, 54	syl2anc 584	. . . . 5 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → (𝑚(𝐾 ↾ ({𝑚} × 𝑉))𝑛) = (𝑚𝐾𝑛))
56		eqid 2736	. . . . . . . 8 ⊢ ∪ ((II ×_t II) ↾_t ({𝑚} × 𝑉)) = ∪ ((II ×_t II) ↾_t ({𝑚} × 𝑉))
57	2	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → II ∈ Top)
58		snex 5381	. . . . . . . . . . 11 ⊢ {𝑚} ∈ V
59	58	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → {𝑚} ∈ V)
60	23	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → 𝑉 ∈ II)
61		txrest 23575	. . . . . . . . . 10 ⊢ (((II ∈ Top ∧ II ∈ Top) ∧ ({𝑚} ∈ V ∧ 𝑉 ∈ II)) → ((II ×_t II) ↾_t ({𝑚} × 𝑉)) = ((II ↾_t {𝑚}) ×_t (II ↾_t 𝑉)))
62	57, 57, 59, 60, 61	syl22anc 838	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → ((II ×_t II) ↾_t ({𝑚} × 𝑉)) = ((II ↾_t {𝑚}) ×_t (II ↾_t 𝑉)))
63		iitopon 24828	. . . . . . . . . . . 12 ⊢ II ∈ (TopOn‘(0[,]1))
64	20	sselda 3933	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑈) → 𝑚 ∈ (0[,]1))
65	64	adantrr 717	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → 𝑚 ∈ (0[,]1))
66		restsn2 23115	. . . . . . . . . . . 12 ⊢ ((II ∈ (TopOn‘(0[,]1)) ∧ 𝑚 ∈ (0[,]1)) → (II ↾_t {𝑚}) = 𝒫 {𝑚})
67	63, 65, 66	sylancr 587	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → (II ↾_t {𝑚}) = 𝒫 {𝑚})
68		pwsn 4856	. . . . . . . . . . . 12 ⊢ 𝒫 {𝑚} = {∅, {𝑚}}
69		indisconn 23362	. . . . . . . . . . . 12 ⊢ {∅, {𝑚}} ∈ Conn
70	68, 69	eqeltri 2832	. . . . . . . . . . 11 ⊢ 𝒫 {𝑚} ∈ Conn
71	67, 70	eqeltrdi 2844	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → (II ↾_t {𝑚}) ∈ Conn)
72		cvmlift2lem9.6	. . . . . . . . . . 11 ⊢ (𝜑 → (II ↾_t 𝑉) ∈ Conn)
73	72	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → (II ↾_t 𝑉) ∈ Conn)
74		txconn 23633	. . . . . . . . . 10 ⊢ (((II ↾_t {𝑚}) ∈ Conn ∧ (II ↾_t 𝑉) ∈ Conn) → ((II ↾_t {𝑚}) ×_t (II ↾_t 𝑉)) ∈ Conn)
75	71, 73, 74	syl2anc 584	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → ((II ↾_t {𝑚}) ×_t (II ↾_t 𝑉)) ∈ Conn)
76	62, 75	eqeltrd 2836	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → ((II ×_t II) ↾_t ({𝑚} × 𝑉)) ∈ Conn)
77	1, 6, 7, 8, 9, 10, 11	cvmlift2lem6 35502	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑚 ∈ (0[,]1)) → (𝐾 ↾ ({𝑚} × (0[,]1))) ∈ (((II ×_t II) ↾_t ({𝑚} × (0[,]1))) Cn 𝐶))
78	65, 77	syldan 591	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → (𝐾 ↾ ({𝑚} × (0[,]1))) ∈ (((II ×_t II) ↾_t ({𝑚} × (0[,]1))) Cn 𝐶))
79	26	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → 𝑉 ⊆ (0[,]1))
80		xpss2 5644	. . . . . . . . . . . . 13 ⊢ (𝑉 ⊆ (0[,]1) → ({𝑚} × 𝑉) ⊆ ({𝑚} × (0[,]1)))
81	79, 80	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → ({𝑚} × 𝑉) ⊆ ({𝑚} × (0[,]1)))
82	65	snssd 4765	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → {𝑚} ⊆ (0[,]1))
83		xpss1 5643	. . . . . . . . . . . . . 14 ⊢ ({𝑚} ⊆ (0[,]1) → ({𝑚} × (0[,]1)) ⊆ ((0[,]1) × (0[,]1)))
84	82, 83	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → ({𝑚} × (0[,]1)) ⊆ ((0[,]1) × (0[,]1)))
85	4	restuni 23106	. . . . . . . . . . . . 13 ⊢ (((II ×_t II) ∈ Top ∧ ({𝑚} × (0[,]1)) ⊆ ((0[,]1) × (0[,]1))) → ({𝑚} × (0[,]1)) = ∪ ((II ×_t II) ↾_t ({𝑚} × (0[,]1))))
86	15, 84, 85	sylancr 587	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → ({𝑚} × (0[,]1)) = ∪ ((II ×_t II) ↾_t ({𝑚} × (0[,]1))))
87	81, 86	sseqtrd 3970	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → ({𝑚} × 𝑉) ⊆ ∪ ((II ×_t II) ↾_t ({𝑚} × (0[,]1))))
88		eqid 2736	. . . . . . . . . . . 12 ⊢ ∪ ((II ×_t II) ↾_t ({𝑚} × (0[,]1))) = ∪ ((II ×_t II) ↾_t ({𝑚} × (0[,]1)))
89	88	cnrest 23229	. . . . . . . . . . 11 ⊢ (((𝐾 ↾ ({𝑚} × (0[,]1))) ∈ (((II ×_t II) ↾_t ({𝑚} × (0[,]1))) Cn 𝐶) ∧ ({𝑚} × 𝑉) ⊆ ∪ ((II ×_t II) ↾_t ({𝑚} × (0[,]1)))) → ((𝐾 ↾ ({𝑚} × (0[,]1))) ↾ ({𝑚} × 𝑉)) ∈ ((((II ×_t II) ↾_t ({𝑚} × (0[,]1))) ↾_t ({𝑚} × 𝑉)) Cn 𝐶))
90	78, 87, 89	syl2anc 584	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → ((𝐾 ↾ ({𝑚} × (0[,]1))) ↾ ({𝑚} × 𝑉)) ∈ ((((II ×_t II) ↾_t ({𝑚} × (0[,]1))) ↾_t ({𝑚} × 𝑉)) Cn 𝐶))
91	81	resabs1d 5967	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → ((𝐾 ↾ ({𝑚} × (0[,]1))) ↾ ({𝑚} × 𝑉)) = (𝐾 ↾ ({𝑚} × 𝑉)))
92	15	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → (II ×_t II) ∈ Top)
93		ovex 7391	. . . . . . . . . . . . . 14 ⊢ (0[,]1) ∈ V
94	58, 93	xpex 7698	. . . . . . . . . . . . 13 ⊢ ({𝑚} × (0[,]1)) ∈ V
95	94	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → ({𝑚} × (0[,]1)) ∈ V)
96		restabs 23109	. . . . . . . . . . . 12 ⊢ (((II ×_t II) ∈ Top ∧ ({𝑚} × 𝑉) ⊆ ({𝑚} × (0[,]1)) ∧ ({𝑚} × (0[,]1)) ∈ V) → (((II ×_t II) ↾_t ({𝑚} × (0[,]1))) ↾_t ({𝑚} × 𝑉)) = ((II ×_t II) ↾_t ({𝑚} × 𝑉)))
97	92, 81, 95, 96	syl3anc 1373	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → (((II ×_t II) ↾_t ({𝑚} × (0[,]1))) ↾_t ({𝑚} × 𝑉)) = ((II ×_t II) ↾_t ({𝑚} × 𝑉)))
98	97	oveq1d 7373	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → ((((II ×_t II) ↾_t ({𝑚} × (0[,]1))) ↾_t ({𝑚} × 𝑉)) Cn 𝐶) = (((II ×_t II) ↾_t ({𝑚} × 𝑉)) Cn 𝐶))
99	90, 91, 98	3eltr3d 2850	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → (𝐾 ↾ ({𝑚} × 𝑉)) ∈ (((II ×_t II) ↾_t ({𝑚} × 𝑉)) Cn 𝐶))
100		cvmtop1 35454	. . . . . . . . . . . . 13 ⊢ (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐶 ∈ Top)
101	6, 100	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐶 ∈ Top)
102	101	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → 𝐶 ∈ Top)
103	1	toptopon 22861	. . . . . . . . . . 11 ⊢ (𝐶 ∈ Top ↔ 𝐶 ∈ (TopOn‘𝐵))
104	102, 103	sylib 218	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → 𝐶 ∈ (TopOn‘𝐵))
105		df-ima 5637	. . . . . . . . . . 11 ⊢ (𝐾 “ ({𝑚} × 𝑉)) = ran (𝐾 ↾ ({𝑚} × 𝑉))
106		simprl 770	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → 𝑚 ∈ 𝑈)
107	106	snssd 4765	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → {𝑚} ⊆ 𝑈)
108		xpss1 5643	. . . . . . . . . . . . 13 ⊢ ({𝑚} ⊆ 𝑈 → ({𝑚} × 𝑉) ⊆ (𝑈 × 𝑉))
109		imass2 6061	. . . . . . . . . . . . 13 ⊢ (({𝑚} × 𝑉) ⊆ (𝑈 × 𝑉) → (𝐾 “ ({𝑚} × 𝑉)) ⊆ (𝐾 “ (𝑈 × 𝑉)))
110	107, 108, 109	3syl 18	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → (𝐾 “ ({𝑚} × 𝑉)) ⊆ (𝐾 “ (𝑈 × 𝑉)))
111		cvmlift2lem9.9	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑈 × 𝑉) ⊆ (^◡𝐺 “ 𝑀))
112		imaco 6209	. . . . . . . . . . . . . . . 16 ⊢ ((^◡𝐾 ∘ ^◡𝐹) “ 𝑀) = (^◡𝐾 “ (^◡𝐹 “ 𝑀))
113		cnvco 5834	. . . . . . . . . . . . . . . . . 18 ⊢ ^◡(𝐹 ∘ 𝐾) = (^◡𝐾 ∘ ^◡𝐹)
114	13	cnveqd 5824	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ^◡(𝐹 ∘ 𝐾) = ^◡𝐺)
115	113, 114	eqtr3id 2785	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (^◡𝐾 ∘ ^◡𝐹) = ^◡𝐺)
116	115	imaeq1d 6018	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((^◡𝐾 ∘ ^◡𝐹) “ 𝑀) = (^◡𝐺 “ 𝑀))
117	112, 116	eqtr3id 2785	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (^◡𝐾 “ (^◡𝐹 “ 𝑀)) = (^◡𝐺 “ 𝑀))
118	111, 117	sseqtrrd 3971	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑈 × 𝑉) ⊆ (^◡𝐾 “ (^◡𝐹 “ 𝑀)))
119	12	ffund 6666	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → Fun 𝐾)
120	12	fdmd 6672	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → dom 𝐾 = ((0[,]1) × (0[,]1)))
121	50, 120	sseqtrrd 3971	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑈 × 𝑉) ⊆ dom 𝐾)
122		funimass3 6999	. . . . . . . . . . . . . . 15 ⊢ ((Fun 𝐾 ∧ (𝑈 × 𝑉) ⊆ dom 𝐾) → ((𝐾 “ (𝑈 × 𝑉)) ⊆ (^◡𝐹 “ 𝑀) ↔ (𝑈 × 𝑉) ⊆ (^◡𝐾 “ (^◡𝐹 “ 𝑀))))
123	119, 121, 122	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐾 “ (𝑈 × 𝑉)) ⊆ (^◡𝐹 “ 𝑀) ↔ (𝑈 × 𝑉) ⊆ (^◡𝐾 “ (^◡𝐹 “ 𝑀))))
124	118, 123	mpbird 257	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐾 “ (𝑈 × 𝑉)) ⊆ (^◡𝐹 “ 𝑀))
125	124	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → (𝐾 “ (𝑈 × 𝑉)) ⊆ (^◡𝐹 “ 𝑀))
126	110, 125	sstrd 3944	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → (𝐾 “ ({𝑚} × 𝑉)) ⊆ (^◡𝐹 “ 𝑀))
127	105, 126	eqsstrrid 3973	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → ran (𝐾 ↾ ({𝑚} × 𝑉)) ⊆ (^◡𝐹 “ 𝑀))
128		cnvimass 6041	. . . . . . . . . . . 12 ⊢ (^◡𝐹 “ 𝑀) ⊆ dom 𝐹
129		cvmcn 35456	. . . . . . . . . . . . . 14 ⊢ (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐹 ∈ (𝐶 Cn 𝐽))
130	6, 129	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐹 ∈ (𝐶 Cn 𝐽))
131		eqid 2736	. . . . . . . . . . . . . 14 ⊢ ∪ 𝐽 = ∪ 𝐽
132	1, 131	cnf 23190	. . . . . . . . . . . . 13 ⊢ (𝐹 ∈ (𝐶 Cn 𝐽) → 𝐹:𝐵⟶∪ 𝐽)
133		fdm 6671	. . . . . . . . . . . . 13 ⊢ (𝐹:𝐵⟶∪ 𝐽 → dom 𝐹 = 𝐵)
134	130, 132, 133	3syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → dom 𝐹 = 𝐵)
135	128, 134	sseqtrid 3976	. . . . . . . . . . 11 ⊢ (𝜑 → (^◡𝐹 “ 𝑀) ⊆ 𝐵)
136	135	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → (^◡𝐹 “ 𝑀) ⊆ 𝐵)
137		cnrest2 23230	. . . . . . . . . 10 ⊢ ((𝐶 ∈ (TopOn‘𝐵) ∧ ran (𝐾 ↾ ({𝑚} × 𝑉)) ⊆ (^◡𝐹 “ 𝑀) ∧ (^◡𝐹 “ 𝑀) ⊆ 𝐵) → ((𝐾 ↾ ({𝑚} × 𝑉)) ∈ (((II ×_t II) ↾_t ({𝑚} × 𝑉)) Cn 𝐶) ↔ (𝐾 ↾ ({𝑚} × 𝑉)) ∈ (((II ×_t II) ↾_t ({𝑚} × 𝑉)) Cn (𝐶 ↾_t (^◡𝐹 “ 𝑀)))))
138	104, 127, 136, 137	syl3anc 1373	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → ((𝐾 ↾ ({𝑚} × 𝑉)) ∈ (((II ×_t II) ↾_t ({𝑚} × 𝑉)) Cn 𝐶) ↔ (𝐾 ↾ ({𝑚} × 𝑉)) ∈ (((II ×_t II) ↾_t ({𝑚} × 𝑉)) Cn (𝐶 ↾_t (^◡𝐹 “ 𝑀)))))
139	99, 138	mpbid 232	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → (𝐾 ↾ ({𝑚} × 𝑉)) ∈ (((II ×_t II) ↾_t ({𝑚} × 𝑉)) Cn (𝐶 ↾_t (^◡𝐹 “ 𝑀))))
140	5	cvmsss 35461	. . . . . . . . . . . 12 ⊢ (𝑇 ∈ (𝑆‘𝑀) → 𝑇 ⊆ 𝐶)
141	31, 140	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑇 ⊆ 𝐶)
142	45	simpld 494	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑊 ∈ 𝑇)
143	141, 142	sseldd 3934	. . . . . . . . . 10 ⊢ (𝜑 → 𝑊 ∈ 𝐶)
144		elssuni 4894	. . . . . . . . . . . 12 ⊢ (𝑊 ∈ 𝑇 → 𝑊 ⊆ ∪ 𝑇)
145	142, 144	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑊 ⊆ ∪ 𝑇)
146	5	cvmsuni 35463	. . . . . . . . . . . 12 ⊢ (𝑇 ∈ (𝑆‘𝑀) → ∪ 𝑇 = (^◡𝐹 “ 𝑀))
147	31, 146	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → ∪ 𝑇 = (^◡𝐹 “ 𝑀))
148	145, 147	sseqtrd 3970	. . . . . . . . . 10 ⊢ (𝜑 → 𝑊 ⊆ (^◡𝐹 “ 𝑀))
149	5	cvmsrcl 35458	. . . . . . . . . . . . 13 ⊢ (𝑇 ∈ (𝑆‘𝑀) → 𝑀 ∈ 𝐽)
150	31, 149	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑀 ∈ 𝐽)
151		cnima 23209	. . . . . . . . . . . 12 ⊢ ((𝐹 ∈ (𝐶 Cn 𝐽) ∧ 𝑀 ∈ 𝐽) → (^◡𝐹 “ 𝑀) ∈ 𝐶)
152	130, 150, 151	syl2anc 584	. . . . . . . . . . 11 ⊢ (𝜑 → (^◡𝐹 “ 𝑀) ∈ 𝐶)
153		restopn2 23121	. . . . . . . . . . 11 ⊢ ((𝐶 ∈ Top ∧ (^◡𝐹 “ 𝑀) ∈ 𝐶) → (𝑊 ∈ (𝐶 ↾_t (^◡𝐹 “ 𝑀)) ↔ (𝑊 ∈ 𝐶 ∧ 𝑊 ⊆ (^◡𝐹 “ 𝑀))))
154	101, 152, 153	syl2anc 584	. . . . . . . . . 10 ⊢ (𝜑 → (𝑊 ∈ (𝐶 ↾_t (^◡𝐹 “ 𝑀)) ↔ (𝑊 ∈ 𝐶 ∧ 𝑊 ⊆ (^◡𝐹 “ 𝑀))))
155	143, 148, 154	mpbir2and 713	. . . . . . . . 9 ⊢ (𝜑 → 𝑊 ∈ (𝐶 ↾_t (^◡𝐹 “ 𝑀)))
156	155	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → 𝑊 ∈ (𝐶 ↾_t (^◡𝐹 “ 𝑀)))
157	5	cvmscld 35467	. . . . . . . . . 10 ⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑇 ∈ (𝑆‘𝑀) ∧ 𝑊 ∈ 𝑇) → 𝑊 ∈ (Clsd‘(𝐶 ↾_t (^◡𝐹 “ 𝑀))))
158	6, 31, 142, 157	syl3anc 1373	. . . . . . . . 9 ⊢ (𝜑 → 𝑊 ∈ (Clsd‘(𝐶 ↾_t (^◡𝐹 “ 𝑀))))
159	158	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → 𝑊 ∈ (Clsd‘(𝐶 ↾_t (^◡𝐹 “ 𝑀))))
160		cvmlift2lem9.10	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑍 ∈ 𝑉)
161	160	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → 𝑍 ∈ 𝑉)
162		opelxpi 5661	. . . . . . . . . 10 ⊢ ((𝑚 ∈ {𝑚} ∧ 𝑍 ∈ 𝑉) → ⟨𝑚, 𝑍⟩ ∈ ({𝑚} × 𝑉))
163	52, 161, 162	syl2anc 584	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → ⟨𝑚, 𝑍⟩ ∈ ({𝑚} × 𝑉))
164	81, 84	sstrd 3944	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → ({𝑚} × 𝑉) ⊆ ((0[,]1) × (0[,]1)))
165	4	restuni 23106	. . . . . . . . . 10 ⊢ (((II ×_t II) ∈ Top ∧ ({𝑚} × 𝑉) ⊆ ((0[,]1) × (0[,]1))) → ({𝑚} × 𝑉) = ∪ ((II ×_t II) ↾_t ({𝑚} × 𝑉)))
166	15, 164, 165	sylancr 587	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → ({𝑚} × 𝑉) = ∪ ((II ×_t II) ↾_t ({𝑚} × 𝑉)))
167	163, 166	eleqtrd 2838	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → ⟨𝑚, 𝑍⟩ ∈ ∪ ((II ×_t II) ↾_t ({𝑚} × 𝑉)))
168		df-ov 7361	. . . . . . . . . 10 ⊢ (𝑚(𝐾 ↾ ({𝑚} × 𝑉))𝑍) = ((𝐾 ↾ ({𝑚} × 𝑉))‘⟨𝑚, 𝑍⟩)
169		ovres 7524	. . . . . . . . . . . 12 ⊢ ((𝑚 ∈ {𝑚} ∧ 𝑍 ∈ 𝑉) → (𝑚(𝐾 ↾ ({𝑚} × 𝑉))𝑍) = (𝑚𝐾𝑍))
170	52, 161, 169	syl2anc 584	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → (𝑚(𝐾 ↾ ({𝑚} × 𝑉))𝑍) = (𝑚𝐾𝑍))
171		snidg 4617	. . . . . . . . . . . . . 14 ⊢ (𝑍 ∈ 𝑉 → 𝑍 ∈ {𝑍})
172	160, 171	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑍 ∈ {𝑍})
173	172	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → 𝑍 ∈ {𝑍})
174		ovres 7524	. . . . . . . . . . . 12 ⊢ ((𝑚 ∈ 𝑈 ∧ 𝑍 ∈ {𝑍}) → (𝑚(𝐾 ↾ (𝑈 × {𝑍}))𝑍) = (𝑚𝐾𝑍))
175	106, 173, 174	syl2anc 584	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → (𝑚(𝐾 ↾ (𝑈 × {𝑍}))𝑍) = (𝑚𝐾𝑍))
176	170, 175	eqtr4d 2774	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → (𝑚(𝐾 ↾ ({𝑚} × 𝑉))𝑍) = (𝑚(𝐾 ↾ (𝑈 × {𝑍}))𝑍))
177	168, 176	eqtr3id 2785	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → ((𝐾 ↾ ({𝑚} × 𝑉))‘⟨𝑚, 𝑍⟩) = (𝑚(𝐾 ↾ (𝑈 × {𝑍}))𝑍))
178		eqid 2736	. . . . . . . . . . . . 13 ⊢ ∪ ((II ×_t II) ↾_t (𝑈 × {𝑍})) = ∪ ((II ×_t II) ↾_t (𝑈 × {𝑍}))
179	2	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → II ∈ Top)
180		snex 5381	. . . . . . . . . . . . . . . 16 ⊢ {𝑍} ∈ V
181	180	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → {𝑍} ∈ V)
182		txrest 23575	. . . . . . . . . . . . . . 15 ⊢ (((II ∈ Top ∧ II ∈ Top) ∧ (𝑈 ∈ II ∧ {𝑍} ∈ V)) → ((II ×_t II) ↾_t (𝑈 × {𝑍})) = ((II ↾_t 𝑈) ×_t (II ↾_t {𝑍})))
183	179, 179, 17, 181, 182	syl22anc 838	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((II ×_t II) ↾_t (𝑈 × {𝑍})) = ((II ↾_t 𝑈) ×_t (II ↾_t {𝑍})))
184		cvmlift2lem9.5	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (II ↾_t 𝑈) ∈ Conn)
185	26, 160	sseldd 3934	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑍 ∈ (0[,]1))
186		restsn2 23115	. . . . . . . . . . . . . . . . 17 ⊢ ((II ∈ (TopOn‘(0[,]1)) ∧ 𝑍 ∈ (0[,]1)) → (II ↾_t {𝑍}) = 𝒫 {𝑍})
187	63, 185, 186	sylancr 587	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (II ↾_t {𝑍}) = 𝒫 {𝑍})
188		pwsn 4856	. . . . . . . . . . . . . . . . 17 ⊢ 𝒫 {𝑍} = {∅, {𝑍}}
189		indisconn 23362	. . . . . . . . . . . . . . . . 17 ⊢ {∅, {𝑍}} ∈ Conn
190	188, 189	eqeltri 2832	. . . . . . . . . . . . . . . 16 ⊢ 𝒫 {𝑍} ∈ Conn
191	187, 190	eqeltrdi 2844	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (II ↾_t {𝑍}) ∈ Conn)
192		txconn 23633	. . . . . . . . . . . . . . 15 ⊢ (((II ↾_t 𝑈) ∈ Conn ∧ (II ↾_t {𝑍}) ∈ Conn) → ((II ↾_t 𝑈) ×_t (II ↾_t {𝑍})) ∈ Conn)
193	184, 191, 192	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((II ↾_t 𝑈) ×_t (II ↾_t {𝑍})) ∈ Conn)
194	183, 193	eqeltrd 2836	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((II ×_t II) ↾_t (𝑈 × {𝑍})) ∈ Conn)
195		cvmlift2lem9.11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐾 ↾ (𝑈 × {𝑍})) ∈ (((II ×_t II) ↾_t (𝑈 × {𝑍})) Cn 𝐶))
196	101, 103	sylib 218	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐶 ∈ (TopOn‘𝐵))
197		df-ima 5637	. . . . . . . . . . . . . . . 16 ⊢ (𝐾 “ (𝑈 × {𝑍})) = ran (𝐾 ↾ (𝑈 × {𝑍}))
198	160	snssd 4765	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → {𝑍} ⊆ 𝑉)
199		xpss2 5644	. . . . . . . . . . . . . . . . . 18 ⊢ ({𝑍} ⊆ 𝑉 → (𝑈 × {𝑍}) ⊆ (𝑈 × 𝑉))
200		imass2 6061	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑈 × {𝑍}) ⊆ (𝑈 × 𝑉) → (𝐾 “ (𝑈 × {𝑍})) ⊆ (𝐾 “ (𝑈 × 𝑉)))
201	198, 199, 200	3syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐾 “ (𝑈 × {𝑍})) ⊆ (𝐾 “ (𝑈 × 𝑉)))
202	201, 124	sstrd 3944	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐾 “ (𝑈 × {𝑍})) ⊆ (^◡𝐹 “ 𝑀))
203	197, 202	eqsstrrid 3973	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ran (𝐾 ↾ (𝑈 × {𝑍})) ⊆ (^◡𝐹 “ 𝑀))
204		cnrest2 23230	. . . . . . . . . . . . . . 15 ⊢ ((𝐶 ∈ (TopOn‘𝐵) ∧ ran (𝐾 ↾ (𝑈 × {𝑍})) ⊆ (^◡𝐹 “ 𝑀) ∧ (^◡𝐹 “ 𝑀) ⊆ 𝐵) → ((𝐾 ↾ (𝑈 × {𝑍})) ∈ (((II ×_t II) ↾_t (𝑈 × {𝑍})) Cn 𝐶) ↔ (𝐾 ↾ (𝑈 × {𝑍})) ∈ (((II ×_t II) ↾_t (𝑈 × {𝑍})) Cn (𝐶 ↾_t (^◡𝐹 “ 𝑀)))))
205	196, 203, 135, 204	syl3anc 1373	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐾 ↾ (𝑈 × {𝑍})) ∈ (((II ×_t II) ↾_t (𝑈 × {𝑍})) Cn 𝐶) ↔ (𝐾 ↾ (𝑈 × {𝑍})) ∈ (((II ×_t II) ↾_t (𝑈 × {𝑍})) Cn (𝐶 ↾_t (^◡𝐹 “ 𝑀)))))
206	195, 205	mpbid 232	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐾 ↾ (𝑈 × {𝑍})) ∈ (((II ×_t II) ↾_t (𝑈 × {𝑍})) Cn (𝐶 ↾_t (^◡𝐹 “ 𝑀))))
207		opelxpi 5661	. . . . . . . . . . . . . . 15 ⊢ ((𝑋 ∈ 𝑈 ∧ 𝑍 ∈ {𝑍}) → ⟨𝑋, 𝑍⟩ ∈ (𝑈 × {𝑍}))
208	21, 172, 207	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ⟨𝑋, 𝑍⟩ ∈ (𝑈 × {𝑍}))
209	185	snssd 4765	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → {𝑍} ⊆ (0[,]1))
210		xpss12 5639	. . . . . . . . . . . . . . . 16 ⊢ ((𝑈 ⊆ (0[,]1) ∧ {𝑍} ⊆ (0[,]1)) → (𝑈 × {𝑍}) ⊆ ((0[,]1) × (0[,]1)))
211	20, 209, 210	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑈 × {𝑍}) ⊆ ((0[,]1) × (0[,]1)))
212	4	restuni 23106	. . . . . . . . . . . . . . 15 ⊢ (((II ×_t II) ∈ Top ∧ (𝑈 × {𝑍}) ⊆ ((0[,]1) × (0[,]1))) → (𝑈 × {𝑍}) = ∪ ((II ×_t II) ↾_t (𝑈 × {𝑍})))
213	15, 211, 212	sylancr 587	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑈 × {𝑍}) = ∪ ((II ×_t II) ↾_t (𝑈 × {𝑍})))
214	208, 213	eleqtrd 2838	. . . . . . . . . . . . 13 ⊢ (𝜑 → ⟨𝑋, 𝑍⟩ ∈ ∪ ((II ×_t II) ↾_t (𝑈 × {𝑍})))
215		df-ov 7361	. . . . . . . . . . . . . . 15 ⊢ (𝑋(𝐾 ↾ (𝑈 × {𝑍}))𝑍) = ((𝐾 ↾ (𝑈 × {𝑍}))‘⟨𝑋, 𝑍⟩)
216		ovres 7524	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑋 ∈ 𝑈 ∧ 𝑍 ∈ {𝑍}) → (𝑋(𝐾 ↾ (𝑈 × {𝑍}))𝑍) = (𝑋𝐾𝑍))
217	21, 172, 216	syl2anc 584	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑋(𝐾 ↾ (𝑈 × {𝑍}))𝑍) = (𝑋𝐾𝑍))
218		snidg 4617	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑋 ∈ 𝑈 → 𝑋 ∈ {𝑋})
219	21, 218	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑋 ∈ {𝑋})
220		ovres 7524	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑋 ∈ {𝑋} ∧ 𝑍 ∈ 𝑉) → (𝑋(𝐾 ↾ ({𝑋} × 𝑉))𝑍) = (𝑋𝐾𝑍))
221	219, 160, 220	syl2anc 584	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑋(𝐾 ↾ ({𝑋} × 𝑉))𝑍) = (𝑋𝐾𝑍))
222	217, 221	eqtr4d 2774	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑋(𝐾 ↾ (𝑈 × {𝑍}))𝑍) = (𝑋(𝐾 ↾ ({𝑋} × 𝑉))𝑍))
223	215, 222	eqtr3id 2785	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐾 ↾ (𝑈 × {𝑍}))‘⟨𝑋, 𝑍⟩) = (𝑋(𝐾 ↾ ({𝑋} × 𝑉))𝑍))
224		eqid 2736	. . . . . . . . . . . . . . . . 17 ⊢ ∪ ((II ×_t II) ↾_t ({𝑋} × 𝑉)) = ∪ ((II ×_t II) ↾_t ({𝑋} × 𝑉))
225		snex 5381	. . . . . . . . . . . . . . . . . . . 20 ⊢ {𝑋} ∈ V
226	225	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → {𝑋} ∈ V)
227		txrest 23575	. . . . . . . . . . . . . . . . . . 19 ⊢ (((II ∈ Top ∧ II ∈ Top) ∧ ({𝑋} ∈ V ∧ 𝑉 ∈ II)) → ((II ×_t II) ↾_t ({𝑋} × 𝑉)) = ((II ↾_t {𝑋}) ×_t (II ↾_t 𝑉)))
228	179, 179, 226, 23, 227	syl22anc 838	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((II ×_t II) ↾_t ({𝑋} × 𝑉)) = ((II ↾_t {𝑋}) ×_t (II ↾_t 𝑉)))
229		restsn2 23115	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((II ∈ (TopOn‘(0[,]1)) ∧ 𝑋 ∈ (0[,]1)) → (II ↾_t {𝑋}) = 𝒫 {𝑋})
230	63, 22, 229	sylancr 587	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (II ↾_t {𝑋}) = 𝒫 {𝑋})
231		pwsn 4856	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝒫 {𝑋} = {∅, {𝑋}}
232		indisconn 23362	. . . . . . . . . . . . . . . . . . . . 21 ⊢ {∅, {𝑋}} ∈ Conn
233	231, 232	eqeltri 2832	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝒫 {𝑋} ∈ Conn
234	230, 233	eqeltrdi 2844	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (II ↾_t {𝑋}) ∈ Conn)
235		txconn 23633	. . . . . . . . . . . . . . . . . . 19 ⊢ (((II ↾_t {𝑋}) ∈ Conn ∧ (II ↾_t 𝑉) ∈ Conn) → ((II ↾_t {𝑋}) ×_t (II ↾_t 𝑉)) ∈ Conn)
236	234, 72, 235	syl2anc 584	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((II ↾_t {𝑋}) ×_t (II ↾_t 𝑉)) ∈ Conn)
237	228, 236	eqeltrd 2836	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((II ×_t II) ↾_t ({𝑋} × 𝑉)) ∈ Conn)
238	1, 6, 7, 8, 9, 10, 11	cvmlift2lem6 35502	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑋 ∈ (0[,]1)) → (𝐾 ↾ ({𝑋} × (0[,]1))) ∈ (((II ×_t II) ↾_t ({𝑋} × (0[,]1))) Cn 𝐶))
239	22, 238	mpdan 687	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐾 ↾ ({𝑋} × (0[,]1))) ∈ (((II ×_t II) ↾_t ({𝑋} × (0[,]1))) Cn 𝐶))
240		xpss2 5644	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑉 ⊆ (0[,]1) → ({𝑋} × 𝑉) ⊆ ({𝑋} × (0[,]1)))
241	23, 25, 240	3syl 18	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ({𝑋} × 𝑉) ⊆ ({𝑋} × (0[,]1)))
242	22	snssd 4765	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → {𝑋} ⊆ (0[,]1))
243		xpss1 5643	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ({𝑋} ⊆ (0[,]1) → ({𝑋} × (0[,]1)) ⊆ ((0[,]1) × (0[,]1)))
244	242, 243	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ({𝑋} × (0[,]1)) ⊆ ((0[,]1) × (0[,]1)))
245	4	restuni 23106	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((II ×_t II) ∈ Top ∧ ({𝑋} × (0[,]1)) ⊆ ((0[,]1) × (0[,]1))) → ({𝑋} × (0[,]1)) = ∪ ((II ×_t II) ↾_t ({𝑋} × (0[,]1))))
246	15, 244, 245	sylancr 587	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ({𝑋} × (0[,]1)) = ∪ ((II ×_t II) ↾_t ({𝑋} × (0[,]1))))
247	241, 246	sseqtrd 3970	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ({𝑋} × 𝑉) ⊆ ∪ ((II ×_t II) ↾_t ({𝑋} × (0[,]1))))
248		eqid 2736	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ∪ ((II ×_t II) ↾_t ({𝑋} × (0[,]1))) = ∪ ((II ×_t II) ↾_t ({𝑋} × (0[,]1)))
249	248	cnrest 23229	. . . . . . . . . . . . . . . . . . . 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 𝐶))
250	239, 247, 249	syl2anc 584	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝐾 ↾ ({𝑋} × (0[,]1))) ↾ ({𝑋} × 𝑉)) ∈ ((((II ×_t II) ↾_t ({𝑋} × (0[,]1))) ↾_t ({𝑋} × 𝑉)) Cn 𝐶))
251	241	resabs1d 5967	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝐾 ↾ ({𝑋} × (0[,]1))) ↾ ({𝑋} × 𝑉)) = (𝐾 ↾ ({𝑋} × 𝑉)))
252	225, 93	xpex 7698	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ({𝑋} × (0[,]1)) ∈ V
253	252	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ({𝑋} × (0[,]1)) ∈ V)
254		restabs 23109	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((II ×_t II) ∈ Top ∧ ({𝑋} × 𝑉) ⊆ ({𝑋} × (0[,]1)) ∧ ({𝑋} × (0[,]1)) ∈ V) → (((II ×_t II) ↾_t ({𝑋} × (0[,]1))) ↾_t ({𝑋} × 𝑉)) = ((II ×_t II) ↾_t ({𝑋} × 𝑉)))
255	16, 241, 253, 254	syl3anc 1373	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (((II ×_t II) ↾_t ({𝑋} × (0[,]1))) ↾_t ({𝑋} × 𝑉)) = ((II ×_t II) ↾_t ({𝑋} × 𝑉)))
256	255	oveq1d 7373	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((((II ×_t II) ↾_t ({𝑋} × (0[,]1))) ↾_t ({𝑋} × 𝑉)) Cn 𝐶) = (((II ×_t II) ↾_t ({𝑋} × 𝑉)) Cn 𝐶))
257	250, 251, 256	3eltr3d 2850	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐾 ↾ ({𝑋} × 𝑉)) ∈ (((II ×_t II) ↾_t ({𝑋} × 𝑉)) Cn 𝐶))
258		df-ima 5637	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐾 “ ({𝑋} × 𝑉)) = ran (𝐾 ↾ ({𝑋} × 𝑉))
259	21	snssd 4765	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → {𝑋} ⊆ 𝑈)
260		xpss1 5643	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ({𝑋} ⊆ 𝑈 → ({𝑋} × 𝑉) ⊆ (𝑈 × 𝑉))
261		imass2 6061	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (({𝑋} × 𝑉) ⊆ (𝑈 × 𝑉) → (𝐾 “ ({𝑋} × 𝑉)) ⊆ (𝐾 “ (𝑈 × 𝑉)))
262	259, 260, 261	3syl 18	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝐾 “ ({𝑋} × 𝑉)) ⊆ (𝐾 “ (𝑈 × 𝑉)))
263	262, 124	sstrd 3944	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐾 “ ({𝑋} × 𝑉)) ⊆ (^◡𝐹 “ 𝑀))
264	258, 263	eqsstrrid 3973	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ran (𝐾 ↾ ({𝑋} × 𝑉)) ⊆ (^◡𝐹 “ 𝑀))
265		cnrest2 23230	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐶 ∈ (TopOn‘𝐵) ∧ ran (𝐾 ↾ ({𝑋} × 𝑉)) ⊆ (^◡𝐹 “ 𝑀) ∧ (^◡𝐹 “ 𝑀) ⊆ 𝐵) → ((𝐾 ↾ ({𝑋} × 𝑉)) ∈ (((II ×_t II) ↾_t ({𝑋} × 𝑉)) Cn 𝐶) ↔ (𝐾 ↾ ({𝑋} × 𝑉)) ∈ (((II ×_t II) ↾_t ({𝑋} × 𝑉)) Cn (𝐶 ↾_t (^◡𝐹 “ 𝑀)))))
266	196, 264, 135, 265	syl3anc 1373	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝐾 ↾ ({𝑋} × 𝑉)) ∈ (((II ×_t II) ↾_t ({𝑋} × 𝑉)) Cn 𝐶) ↔ (𝐾 ↾ ({𝑋} × 𝑉)) ∈ (((II ×_t II) ↾_t ({𝑋} × 𝑉)) Cn (𝐶 ↾_t (^◡𝐹 “ 𝑀)))))
267	257, 266	mpbid 232	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐾 ↾ ({𝑋} × 𝑉)) ∈ (((II ×_t II) ↾_t ({𝑋} × 𝑉)) Cn (𝐶 ↾_t (^◡𝐹 “ 𝑀))))
268		opelxpi 5661	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑋 ∈ {𝑋} ∧ 𝑌 ∈ 𝑉) → ⟨𝑋, 𝑌⟩ ∈ ({𝑋} × 𝑉))
269	219, 27, 268	syl2anc 584	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ⟨𝑋, 𝑌⟩ ∈ ({𝑋} × 𝑉))
270	259, 260	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ({𝑋} × 𝑉) ⊆ (𝑈 × 𝑉))
271	270, 50	sstrd 3944	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ({𝑋} × 𝑉) ⊆ ((0[,]1) × (0[,]1)))
272	4	restuni 23106	. . . . . . . . . . . . . . . . . . 19 ⊢ (((II ×_t II) ∈ Top ∧ ({𝑋} × 𝑉) ⊆ ((0[,]1) × (0[,]1))) → ({𝑋} × 𝑉) = ∪ ((II ×_t II) ↾_t ({𝑋} × 𝑉)))
273	15, 271, 272	sylancr 587	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ({𝑋} × 𝑉) = ∪ ((II ×_t II) ↾_t ({𝑋} × 𝑉)))
274	269, 273	eleqtrd 2838	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ⟨𝑋, 𝑌⟩ ∈ ∪ ((II ×_t II) ↾_t ({𝑋} × 𝑉)))
275		df-ov 7361	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑋(𝐾 ↾ ({𝑋} × 𝑉))𝑌) = ((𝐾 ↾ ({𝑋} × 𝑉))‘⟨𝑋, 𝑌⟩)
276		ovres 7524	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑋 ∈ {𝑋} ∧ 𝑌 ∈ 𝑉) → (𝑋(𝐾 ↾ ({𝑋} × 𝑉))𝑌) = (𝑋𝐾𝑌))
277	219, 27, 276	syl2anc 584	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑋(𝐾 ↾ ({𝑋} × 𝑉))𝑌) = (𝑋𝐾𝑌))
278	275, 277	eqtr3id 2785	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝐾 ↾ ({𝑋} × 𝑉))‘⟨𝑋, 𝑌⟩) = (𝑋𝐾𝑌))
279	45	simprd 495	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑋𝐾𝑌) ∈ 𝑊)
280	278, 279	eqeltrd 2836	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝐾 ↾ ({𝑋} × 𝑉))‘⟨𝑋, 𝑌⟩) ∈ 𝑊)
281	224, 237, 267, 155, 158, 274, 280	conncn 23370	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐾 ↾ ({𝑋} × 𝑉)):∪ ((II ×_t II) ↾_t ({𝑋} × 𝑉))⟶𝑊)
282	273	feq2d 6646	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐾 ↾ ({𝑋} × 𝑉)):({𝑋} × 𝑉)⟶𝑊 ↔ (𝐾 ↾ ({𝑋} × 𝑉)):∪ ((II ×_t II) ↾_t ({𝑋} × 𝑉))⟶𝑊))
283	281, 282	mpbird 257	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐾 ↾ ({𝑋} × 𝑉)):({𝑋} × 𝑉)⟶𝑊)
284	283, 219, 160	fovcdmd 7530	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑋(𝐾 ↾ ({𝑋} × 𝑉))𝑍) ∈ 𝑊)
285	223, 284	eqeltrd 2836	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐾 ↾ (𝑈 × {𝑍}))‘⟨𝑋, 𝑍⟩) ∈ 𝑊)
286	178, 194, 206, 155, 158, 214, 285	conncn 23370	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐾 ↾ (𝑈 × {𝑍})):∪ ((II ×_t II) ↾_t (𝑈 × {𝑍}))⟶𝑊)
287	213	feq2d 6646	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐾 ↾ (𝑈 × {𝑍})):(𝑈 × {𝑍})⟶𝑊 ↔ (𝐾 ↾ (𝑈 × {𝑍})):∪ ((II ×_t II) ↾_t (𝑈 × {𝑍}))⟶𝑊))
288	286, 287	mpbird 257	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐾 ↾ (𝑈 × {𝑍})):(𝑈 × {𝑍})⟶𝑊)
289	288	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → (𝐾 ↾ (𝑈 × {𝑍})):(𝑈 × {𝑍})⟶𝑊)
290	289, 106, 173	fovcdmd 7530	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → (𝑚(𝐾 ↾ (𝑈 × {𝑍}))𝑍) ∈ 𝑊)
291	177, 290	eqeltrd 2836	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → ((𝐾 ↾ ({𝑚} × 𝑉))‘⟨𝑚, 𝑍⟩) ∈ 𝑊)
292	56, 76, 139, 156, 159, 167, 291	conncn 23370	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → (𝐾 ↾ ({𝑚} × 𝑉)):∪ ((II ×_t II) ↾_t ({𝑚} × 𝑉))⟶𝑊)
293	166	feq2d 6646	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → ((𝐾 ↾ ({𝑚} × 𝑉)):({𝑚} × 𝑉)⟶𝑊 ↔ (𝐾 ↾ ({𝑚} × 𝑉)):∪ ((II ×_t II) ↾_t ({𝑚} × 𝑉))⟶𝑊))
294	292, 293	mpbird 257	. . . . . 6 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → (𝐾 ↾ ({𝑚} × 𝑉)):({𝑚} × 𝑉)⟶𝑊)
295	294, 52, 53	fovcdmd 7530	. . . . 5 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → (𝑚(𝐾 ↾ ({𝑚} × 𝑉))𝑛) ∈ 𝑊)
296	55, 295	eqeltrrd 2837	. . . 4 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → (𝑚𝐾𝑛) ∈ 𝑊)
297	296	ralrimivva 3179	. . 3 ⊢ (𝜑 → ∀𝑚 ∈ 𝑈 ∀𝑛 ∈ 𝑉 (𝑚𝐾𝑛) ∈ 𝑊)
298		funimassov 7535	. . . 4 ⊢ ((Fun 𝐾 ∧ (𝑈 × 𝑉) ⊆ dom 𝐾) → ((𝐾 “ (𝑈 × 𝑉)) ⊆ 𝑊 ↔ ∀𝑚 ∈ 𝑈 ∀𝑛 ∈ 𝑉 (𝑚𝐾𝑛) ∈ 𝑊))
299	119, 121, 298	syl2anc 584	. . 3 ⊢ (𝜑 → ((𝐾 “ (𝑈 × 𝑉)) ⊆ 𝑊 ↔ ∀𝑚 ∈ 𝑈 ∀𝑛 ∈ 𝑉 (𝑚𝐾𝑛) ∈ 𝑊))
300	297, 299	mpbird 257	. 2 ⊢ (𝜑 → (𝐾 “ (𝑈 × 𝑉)) ⊆ 𝑊)
301	1, 4, 5, 6, 12, 14, 16, 30, 31, 48, 50, 300	cvmlift2lem9a 35497	1 ⊢ (𝜑 → (𝐾 ↾ (𝑈 × 𝑉)) ∈ (((II ×_t II) ↾_t (𝑈 × 𝑉)) Cn 𝐶))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1541 ∈ wcel 2113 ∀wral 3051 {crab 3399 Vcvv 3440 ∖ cdif 3898 ∩ cin 3900 ⊆ wss 3901 ∅c0 4285 𝒫 cpw 4554 {csn 4580 {cpr 4582 ⟨cop 4586 ∪ cuni 4863 ↦ cmpt 5179 × cxp 5622 ^◡ccnv 5623 dom cdm 5624 ran crn 5625 ↾ cres 5626 “ cima 5627 ∘ ccom 5628 Fun wfun 6486 ⟶wf 6488 ‘cfv 6492 ℩crio 7314 (class class class)co 7358 ∈ cmpo 7360 0cc0 11026 1c1 11027 [,]cicc 13264 ↾_t crest 17340 Topctop 22837 TopOnctopon 22854 Clsdccld 22960 Cn ccn 23168 Conncconn 23355 ×_t ctx 23504 Homeochmeo 23697 IIcii 24824 CovMap ccvm 35449

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2115 ax-9 2123 ax-10 2146 ax-11 2162 ax-12 2184 ax-ext 2708 ax-rep 5224 ax-sep 5241 ax-nul 5251 ax-pow 5310 ax-pr 5377 ax-un 7680 ax-inf2 9550 ax-cnex 11082 ax-resscn 11083 ax-1cn 11084 ax-icn 11085 ax-addcl 11086 ax-addrcl 11087 ax-mulcl 11088 ax-mulrcl 11089 ax-mulcom 11090 ax-addass 11091 ax-mulass 11092 ax-distr 11093 ax-i2m1 11094 ax-1ne0 11095 ax-1rid 11096 ax-rnegex 11097 ax-rrecex 11098 ax-cnre 11099 ax-pre-lttri 11100 ax-pre-lttrn 11101 ax-pre-ltadd 11102 ax-pre-mulgt0 11103 ax-pre-sup 11104 ax-addf 11105

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2539 df-eu 2569 df-clab 2715 df-cleq 2728 df-clel 2811 df-nfc 2885 df-ne 2933 df-nel 3037 df-ral 3052 df-rex 3061 df-rmo 3350 df-reu 3351 df-rab 3400 df-v 3442 df-sbc 3741 df-csb 3850 df-dif 3904 df-un 3906 df-in 3908 df-ss 3918 df-pss 3921 df-nul 4286 df-if 4480 df-pw 4556 df-sn 4581 df-pr 4583 df-tp 4585 df-op 4587 df-uni 4864 df-int 4903 df-iun 4948 df-iin 4949 df-br 5099 df-opab 5161 df-mpt 5180 df-tr 5206 df-id 5519 df-eprel 5524 df-po 5532 df-so 5533 df-fr 5577 df-se 5578 df-we 5579 df-xp 5630 df-rel 5631 df-cnv 5632 df-co 5633 df-dm 5634 df-rn 5635 df-res 5636 df-ima 5637 df-pred 6259 df-ord 6320 df-on 6321 df-lim 6322 df-suc 6323 df-iota 6448 df-fun 6494 df-fn 6495 df-f 6496 df-f1 6497 df-fo 6498 df-f1o 6499 df-fv 6500 df-isom 6501 df-riota 7315 df-ov 7361 df-oprab 7362 df-mpo 7363 df-of 7622 df-om 7809 df-1st 7933 df-2nd 7934 df-supp 8103 df-frecs 8223 df-wrecs 8254 df-recs 8303 df-rdg 8341 df-1o 8397 df-2o 8398 df-er 8635 df-ec 8637 df-map 8765 df-ixp 8836 df-en 8884 df-dom 8885 df-sdom 8886 df-fin 8887 df-fsupp 9265 df-fi 9314 df-sup 9345 df-inf 9346 df-oi 9415 df-card 9851 df-pnf 11168 df-mnf 11169 df-xr 11170 df-ltxr 11171 df-le 11172 df-sub 11366 df-neg 11367 df-div 11795 df-nn 12146 df-2 12208 df-3 12209 df-4 12210 df-5 12211 df-6 12212 df-7 12213 df-8 12214 df-9 12215 df-n0 12402 df-z 12489 df-dec 12608 df-uz 12752 df-q 12862 df-rp 12906 df-xneg 13026 df-xadd 13027 df-xmul 13028 df-ioo 13265 df-ico 13267 df-icc 13268 df-fz 13424 df-fzo 13571 df-fl 13712 df-seq 13925 df-exp 13985 df-hash 14254 df-cj 15022 df-re 15023 df-im 15024 df-sqrt 15158 df-abs 15159 df-clim 15411 df-sum 15610 df-struct 17074 df-sets 17091 df-slot 17109 df-ndx 17121 df-base 17137 df-ress 17158 df-plusg 17190 df-mulr 17191 df-starv 17192 df-sca 17193 df-vsca 17194 df-ip 17195 df-tset 17196 df-ple 17197 df-ds 17199 df-unif 17200 df-hom 17201 df-cco 17202 df-rest 17342 df-topn 17343 df-0g 17361 df-gsum 17362 df-topgen 17363 df-pt 17364 df-prds 17367 df-xrs 17423 df-qtop 17428 df-imas 17429 df-xps 17431 df-mre 17505 df-mrc 17506 df-acs 17508 df-mgm 18565 df-sgrp 18644 df-mnd 18660 df-submnd 18709 df-mulg 18998 df-cntz 19246 df-cmn 19711 df-psmet 21301 df-xmet 21302 df-met 21303 df-bl 21304 df-mopn 21305 df-cnfld 21310 df-top 22838 df-topon 22855 df-topsp 22877 df-bases 22890 df-cld 22963 df-ntr 22964 df-cls 22965 df-nei 23042 df-cn 23171 df-cnp 23172 df-cmp 23331 df-conn 23356 df-lly 23410 df-nlly 23411 df-tx 23506 df-hmeo 23699 df-xms 24264 df-ms 24265 df-tms 24266 df-ii 24826 df-cncf 24827 df-htpy 24925 df-phtpy 24926 df-phtpc 24947 df-pconn 35415 df-sconn 35416 df-cvm 35450

This theorem is referenced by: cvmlift2lem10 35506

W3C validator