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 35493

Description: Lemma for cvmlift2 35498. (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 24847	. . 3 ⊢ II ∈ Top
3		iiuni 24848	. . 3 ⊢ (0[,]1) = ∪ II
4	2, 2, 3, 3	txunii 23558	. 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 35489	. 2 ⊢ (𝜑 → 𝐾:((0[,]1) × (0[,]1))⟶𝐵)
13	1, 6, 7, 8, 9, 10, 11	cvmlift2lem7 35491	. . 3 ⊢ (𝜑 → (𝐹 ∘ 𝐾) = 𝐺)
14	13, 7	eqeltrd 2836	. 2 ⊢ (𝜑 → (𝐹 ∘ 𝐾) ∈ ((II ×_t II) Cn 𝐽))
15	2, 2	txtopi 23555	. . 3 ⊢ (II ×_t II) ∈ Top
16	15	a1i 11	. 2 ⊢ (𝜑 → (II ×_t II) ∈ Top)
17		cvmlift2lem9.3	. . . . 5 ⊢ (𝜑 → 𝑈 ∈ II)
18		elssuni 4881	. . . . . 6 ⊢ (𝑈 ∈ II → 𝑈 ⊆ ∪ II)
19	18, 3	sseqtrrdi 3963	. . . . 5 ⊢ (𝑈 ∈ II → 𝑈 ⊆ (0[,]1))
20	17, 19	syl 17	. . . 4 ⊢ (𝜑 → 𝑈 ⊆ (0[,]1))
21		cvmlift2lem9.7	. . . 4 ⊢ (𝜑 → 𝑋 ∈ 𝑈)
22	20, 21	sseldd 3922	. . 3 ⊢ (𝜑 → 𝑋 ∈ (0[,]1))
23		cvmlift2lem9.4	. . . . 5 ⊢ (𝜑 → 𝑉 ∈ II)
24		elssuni 4881	. . . . . 6 ⊢ (𝑉 ∈ II → 𝑉 ⊆ ∪ II)
25	24, 3	sseqtrrdi 3963	. . . . 5 ⊢ (𝑉 ∈ II → 𝑉 ⊆ (0[,]1))
26	23, 25	syl 17	. . . 4 ⊢ (𝜑 → 𝑉 ⊆ (0[,]1))
27		cvmlift2lem9.8	. . . 4 ⊢ (𝜑 → 𝑌 ∈ 𝑉)
28	26, 27	sseldd 3922	. . 3 ⊢ (𝜑 → 𝑌 ∈ (0[,]1))
29		opelxpi 5668	. . 3 ⊢ ((𝑋 ∈ (0[,]1) ∧ 𝑌 ∈ (0[,]1)) → ⟨𝑋, 𝑌⟩ ∈ ((0[,]1) × (0[,]1)))
30	22, 28, 29	syl2anc 585	. 2 ⊢ (𝜑 → ⟨𝑋, 𝑌⟩ ∈ ((0[,]1) × (0[,]1)))
31		cvmlift2lem9.2	. 2 ⊢ (𝜑 → 𝑇 ∈ (𝑆‘𝑀))
32	12, 22, 28	fovcdmd 7539	. . . 4 ⊢ (𝜑 → (𝑋𝐾𝑌) ∈ 𝐵)
33		fvco3 6939	. . . . . . . 8 ⊢ ((𝐾:((0[,]1) × (0[,]1))⟶𝐵 ∧ ⟨𝑋, 𝑌⟩ ∈ ((0[,]1) × (0[,]1))) → ((𝐹 ∘ 𝐾)‘⟨𝑋, 𝑌⟩) = (𝐹‘(𝐾‘⟨𝑋, 𝑌⟩)))
34	12, 30, 33	syl2anc 585	. . . . . . 7 ⊢ (𝜑 → ((𝐹 ∘ 𝐾)‘⟨𝑋, 𝑌⟩) = (𝐹‘(𝐾‘⟨𝑋, 𝑌⟩)))
35	13	fveq1d 6842	. . . . . . 7 ⊢ (𝜑 → ((𝐹 ∘ 𝐾)‘⟨𝑋, 𝑌⟩) = (𝐺‘⟨𝑋, 𝑌⟩))
36	34, 35	eqtr3d 2773	. . . . . 6 ⊢ (𝜑 → (𝐹‘(𝐾‘⟨𝑋, 𝑌⟩)) = (𝐺‘⟨𝑋, 𝑌⟩))
37		df-ov 7370	. . . . . . 7 ⊢ (𝑋𝐾𝑌) = (𝐾‘⟨𝑋, 𝑌⟩)
38	37	fveq2i 6843	. . . . . 6 ⊢ (𝐹‘(𝑋𝐾𝑌)) = (𝐹‘(𝐾‘⟨𝑋, 𝑌⟩))
39		df-ov 7370	. . . . . 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 35459	. . . 4 ⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ (𝑇 ∈ (𝑆‘𝑀) ∧ (𝑋𝐾𝑌) ∈ 𝐵 ∧ (𝐹‘(𝑋𝐾𝑌)) ∈ 𝑀)) → (𝑊 ∈ 𝑇 ∧ (𝑋𝐾𝑌) ∈ 𝑊))
45	6, 31, 32, 42, 44	syl13anc 1375	. . 3 ⊢ (𝜑 → (𝑊 ∈ 𝑇 ∧ (𝑋𝐾𝑌) ∈ 𝑊))
46	37	eleq1i 2827	. . . 4 ⊢ ((𝑋𝐾𝑌) ∈ 𝑊 ↔ (𝐾‘⟨𝑋, 𝑌⟩) ∈ 𝑊)
47	46	anbi2i 624	. . 3 ⊢ ((𝑊 ∈ 𝑇 ∧ (𝑋𝐾𝑌) ∈ 𝑊) ↔ (𝑊 ∈ 𝑇 ∧ (𝐾‘⟨𝑋, 𝑌⟩) ∈ 𝑊))
48	45, 47	sylib 218	. 2 ⊢ (𝜑 → (𝑊 ∈ 𝑇 ∧ (𝐾‘⟨𝑋, 𝑌⟩) ∈ 𝑊))
49		xpss12 5646	. . 3 ⊢ ((𝑈 ⊆ (0[,]1) ∧ 𝑉 ⊆ (0[,]1)) → (𝑈 × 𝑉) ⊆ ((0[,]1) × (0[,]1)))
50	20, 26, 49	syl2anc 585	. 2 ⊢ (𝜑 → (𝑈 × 𝑉) ⊆ ((0[,]1) × (0[,]1)))
51		snidg 4604	. . . . . . 7 ⊢ (𝑚 ∈ 𝑈 → 𝑚 ∈ {𝑚})
52	51	ad2antrl 729	. . . . . 6 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → 𝑚 ∈ {𝑚})
53		simprr 773	. . . . . 6 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → 𝑛 ∈ 𝑉)
54		ovres 7533	. . . . . 6 ⊢ ((𝑚 ∈ {𝑚} ∧ 𝑛 ∈ 𝑉) → (𝑚(𝐾 ↾ ({𝑚} × 𝑉))𝑛) = (𝑚𝐾𝑛))
55	52, 53, 54	syl2anc 585	. . . . 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 23596	. . . . . . . . . 10 ⊢ (((II ∈ Top ∧ II ∈ Top) ∧ ({𝑚} ∈ V ∧ 𝑉 ∈ II)) → ((II ×_t II) ↾_t ({𝑚} × 𝑉)) = ((II ↾_t {𝑚}) ×_t (II ↾_t 𝑉)))
62	57, 57, 59, 60, 61	syl22anc 839	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → ((II ×_t II) ↾_t ({𝑚} × 𝑉)) = ((II ↾_t {𝑚}) ×_t (II ↾_t 𝑉)))
63		iitopon 24846	. . . . . . . . . . . 12 ⊢ II ∈ (TopOn‘(0[,]1))
64	20	sselda 3921	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑈) → 𝑚 ∈ (0[,]1))
65	64	adantrr 718	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → 𝑚 ∈ (0[,]1))
66		restsn2 23136	. . . . . . . . . . . 12 ⊢ ((II ∈ (TopOn‘(0[,]1)) ∧ 𝑚 ∈ (0[,]1)) → (II ↾_t {𝑚}) = 𝒫 {𝑚})
67	63, 65, 66	sylancr 588	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → (II ↾_t {𝑚}) = 𝒫 {𝑚})
68		pwsn 4843	. . . . . . . . . . . 12 ⊢ 𝒫 {𝑚} = {∅, {𝑚}}
69		indisconn 23383	. . . . . . . . . . . 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 23654	. . . . . . . . . 10 ⊢ (((II ↾_t {𝑚}) ∈ Conn ∧ (II ↾_t 𝑉) ∈ Conn) → ((II ↾_t {𝑚}) ×_t (II ↾_t 𝑉)) ∈ Conn)
75	71, 73, 74	syl2anc 585	. . . . . . . . 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 35490	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑚 ∈ (0[,]1)) → (𝐾 ↾ ({𝑚} × (0[,]1))) ∈ (((II ×_t II) ↾_t ({𝑚} × (0[,]1))) Cn 𝐶))
78	65, 77	syldan 592	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → (𝐾 ↾ ({𝑚} × (0[,]1))) ∈ (((II ×_t II) ↾_t ({𝑚} × (0[,]1))) Cn 𝐶))
79	26	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → 𝑉 ⊆ (0[,]1))
80		xpss2 5651	. . . . . . . . . . . . 13 ⊢ (𝑉 ⊆ (0[,]1) → ({𝑚} × 𝑉) ⊆ ({𝑚} × (0[,]1)))
81	79, 80	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → ({𝑚} × 𝑉) ⊆ ({𝑚} × (0[,]1)))
82	65	snssd 4730	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → {𝑚} ⊆ (0[,]1))
83		xpss1 5650	. . . . . . . . . . . . . 14 ⊢ ({𝑚} ⊆ (0[,]1) → ({𝑚} × (0[,]1)) ⊆ ((0[,]1) × (0[,]1)))
84	82, 83	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → ({𝑚} × (0[,]1)) ⊆ ((0[,]1) × (0[,]1)))
85	4	restuni 23127	. . . . . . . . . . . . 13 ⊢ (((II ×_t II) ∈ Top ∧ ({𝑚} × (0[,]1)) ⊆ ((0[,]1) × (0[,]1))) → ({𝑚} × (0[,]1)) = ∪ ((II ×_t II) ↾_t ({𝑚} × (0[,]1))))
86	15, 84, 85	sylancr 588	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → ({𝑚} × (0[,]1)) = ∪ ((II ×_t II) ↾_t ({𝑚} × (0[,]1))))
87	81, 86	sseqtrd 3958	. . . . . . . . . . 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 23250	. . . . . . . . . . 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 585	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → ((𝐾 ↾ ({𝑚} × (0[,]1))) ↾ ({𝑚} × 𝑉)) ∈ ((((II ×_t II) ↾_t ({𝑚} × (0[,]1))) ↾_t ({𝑚} × 𝑉)) Cn 𝐶))
91	81	resabs1d 5973	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → ((𝐾 ↾ ({𝑚} × (0[,]1))) ↾ ({𝑚} × 𝑉)) = (𝐾 ↾ ({𝑚} × 𝑉)))
92	15	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → (II ×_t II) ∈ Top)
93		ovex 7400	. . . . . . . . . . . . . 14 ⊢ (0[,]1) ∈ V
94	58, 93	xpex 7707	. . . . . . . . . . . . 13 ⊢ ({𝑚} × (0[,]1)) ∈ V
95	94	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → ({𝑚} × (0[,]1)) ∈ V)
96		restabs 23130	. . . . . . . . . . . 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 1374	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → (((II ×_t II) ↾_t ({𝑚} × (0[,]1))) ↾_t ({𝑚} × 𝑉)) = ((II ×_t II) ↾_t ({𝑚} × 𝑉)))
98	97	oveq1d 7382	. . . . . . . . . 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 35442	. . . . . . . . . . . . 13 ⊢ (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐶 ∈ Top)
101	6, 100	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐶 ∈ Top)
102	101	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → 𝐶 ∈ Top)
103	1	toptopon 22882	. . . . . . . . . . 11 ⊢ (𝐶 ∈ Top ↔ 𝐶 ∈ (TopOn‘𝐵))
104	102, 103	sylib 218	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → 𝐶 ∈ (TopOn‘𝐵))
105		df-ima 5644	. . . . . . . . . . 11 ⊢ (𝐾 “ ({𝑚} × 𝑉)) = ran (𝐾 ↾ ({𝑚} × 𝑉))
106		simprl 771	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → 𝑚 ∈ 𝑈)
107	106	snssd 4730	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → {𝑚} ⊆ 𝑈)
108		xpss1 5650	. . . . . . . . . . . . 13 ⊢ ({𝑚} ⊆ 𝑈 → ({𝑚} × 𝑉) ⊆ (𝑈 × 𝑉))
109		imass2 6067	. . . . . . . . . . . . 13 ⊢ (({𝑚} × 𝑉) ⊆ (𝑈 × 𝑉) → (𝐾 “ ({𝑚} × 𝑉)) ⊆ (𝐾 “ (𝑈 × 𝑉)))
110	107, 108, 109	3syl 18	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → (𝐾 “ ({𝑚} × 𝑉)) ⊆ (𝐾 “ (𝑈 × 𝑉)))
111		cvmlift2lem9.9	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑈 × 𝑉) ⊆ (^◡𝐺 “ 𝑀))
112		imaco 6215	. . . . . . . . . . . . . . . 16 ⊢ ((^◡𝐾 ∘ ^◡𝐹) “ 𝑀) = (^◡𝐾 “ (^◡𝐹 “ 𝑀))
113		cnvco 5840	. . . . . . . . . . . . . . . . . 18 ⊢ ^◡(𝐹 ∘ 𝐾) = (^◡𝐾 ∘ ^◡𝐹)
114	13	cnveqd 5830	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ^◡(𝐹 ∘ 𝐾) = ^◡𝐺)
115	113, 114	eqtr3id 2785	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (^◡𝐾 ∘ ^◡𝐹) = ^◡𝐺)
116	115	imaeq1d 6024	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((^◡𝐾 ∘ ^◡𝐹) “ 𝑀) = (^◡𝐺 “ 𝑀))
117	112, 116	eqtr3id 2785	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (^◡𝐾 “ (^◡𝐹 “ 𝑀)) = (^◡𝐺 “ 𝑀))
118	111, 117	sseqtrrd 3959	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑈 × 𝑉) ⊆ (^◡𝐾 “ (^◡𝐹 “ 𝑀)))
119	12	ffund 6672	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → Fun 𝐾)
120	12	fdmd 6678	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → dom 𝐾 = ((0[,]1) × (0[,]1)))
121	50, 120	sseqtrrd 3959	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑈 × 𝑉) ⊆ dom 𝐾)
122		funimass3 7006	. . . . . . . . . . . . . . 15 ⊢ ((Fun 𝐾 ∧ (𝑈 × 𝑉) ⊆ dom 𝐾) → ((𝐾 “ (𝑈 × 𝑉)) ⊆ (^◡𝐹 “ 𝑀) ↔ (𝑈 × 𝑉) ⊆ (^◡𝐾 “ (^◡𝐹 “ 𝑀))))
123	119, 121, 122	syl2anc 585	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐾 “ (𝑈 × 𝑉)) ⊆ (^◡𝐹 “ 𝑀) ↔ (𝑈 × 𝑉) ⊆ (^◡𝐾 “ (^◡𝐹 “ 𝑀))))
124	118, 123	mpbird 257	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐾 “ (𝑈 × 𝑉)) ⊆ (^◡𝐹 “ 𝑀))
125	124	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → (𝐾 “ (𝑈 × 𝑉)) ⊆ (^◡𝐹 “ 𝑀))
126	110, 125	sstrd 3932	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → (𝐾 “ ({𝑚} × 𝑉)) ⊆ (^◡𝐹 “ 𝑀))
127	105, 126	eqsstrrid 3961	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → ran (𝐾 ↾ ({𝑚} × 𝑉)) ⊆ (^◡𝐹 “ 𝑀))
128		cnvimass 6047	. . . . . . . . . . . 12 ⊢ (^◡𝐹 “ 𝑀) ⊆ dom 𝐹
129		cvmcn 35444	. . . . . . . . . . . . . 14 ⊢ (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐹 ∈ (𝐶 Cn 𝐽))
130	6, 129	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐹 ∈ (𝐶 Cn 𝐽))
131		eqid 2736	. . . . . . . . . . . . . 14 ⊢ ∪ 𝐽 = ∪ 𝐽
132	1, 131	cnf 23211	. . . . . . . . . . . . 13 ⊢ (𝐹 ∈ (𝐶 Cn 𝐽) → 𝐹:𝐵⟶∪ 𝐽)
133		fdm 6677	. . . . . . . . . . . . 13 ⊢ (𝐹:𝐵⟶∪ 𝐽 → dom 𝐹 = 𝐵)
134	130, 132, 133	3syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → dom 𝐹 = 𝐵)
135	128, 134	sseqtrid 3964	. . . . . . . . . . 11 ⊢ (𝜑 → (^◡𝐹 “ 𝑀) ⊆ 𝐵)
136	135	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → (^◡𝐹 “ 𝑀) ⊆ 𝐵)
137		cnrest2 23251	. . . . . . . . . 10 ⊢ ((𝐶 ∈ (TopOn‘𝐵) ∧ ran (𝐾 ↾ ({𝑚} × 𝑉)) ⊆ (^◡𝐹 “ 𝑀) ∧ (^◡𝐹 “ 𝑀) ⊆ 𝐵) → ((𝐾 ↾ ({𝑚} × 𝑉)) ∈ (((II ×_t II) ↾_t ({𝑚} × 𝑉)) Cn 𝐶) ↔ (𝐾 ↾ ({𝑚} × 𝑉)) ∈ (((II ×_t II) ↾_t ({𝑚} × 𝑉)) Cn (𝐶 ↾_t (^◡𝐹 “ 𝑀)))))
138	104, 127, 136, 137	syl3anc 1374	. . . . . . . . 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 35449	. . . . . . . . . . . 12 ⊢ (𝑇 ∈ (𝑆‘𝑀) → 𝑇 ⊆ 𝐶)
141	31, 140	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑇 ⊆ 𝐶)
142	45	simpld 494	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑊 ∈ 𝑇)
143	141, 142	sseldd 3922	. . . . . . . . . 10 ⊢ (𝜑 → 𝑊 ∈ 𝐶)
144		elssuni 4881	. . . . . . . . . . . 12 ⊢ (𝑊 ∈ 𝑇 → 𝑊 ⊆ ∪ 𝑇)
145	142, 144	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑊 ⊆ ∪ 𝑇)
146	5	cvmsuni 35451	. . . . . . . . . . . 12 ⊢ (𝑇 ∈ (𝑆‘𝑀) → ∪ 𝑇 = (^◡𝐹 “ 𝑀))
147	31, 146	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → ∪ 𝑇 = (^◡𝐹 “ 𝑀))
148	145, 147	sseqtrd 3958	. . . . . . . . . 10 ⊢ (𝜑 → 𝑊 ⊆ (^◡𝐹 “ 𝑀))
149	5	cvmsrcl 35446	. . . . . . . . . . . . 13 ⊢ (𝑇 ∈ (𝑆‘𝑀) → 𝑀 ∈ 𝐽)
150	31, 149	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑀 ∈ 𝐽)
151		cnima 23230	. . . . . . . . . . . 12 ⊢ ((𝐹 ∈ (𝐶 Cn 𝐽) ∧ 𝑀 ∈ 𝐽) → (^◡𝐹 “ 𝑀) ∈ 𝐶)
152	130, 150, 151	syl2anc 585	. . . . . . . . . . 11 ⊢ (𝜑 → (^◡𝐹 “ 𝑀) ∈ 𝐶)
153		restopn2 23142	. . . . . . . . . . 11 ⊢ ((𝐶 ∈ Top ∧ (^◡𝐹 “ 𝑀) ∈ 𝐶) → (𝑊 ∈ (𝐶 ↾_t (^◡𝐹 “ 𝑀)) ↔ (𝑊 ∈ 𝐶 ∧ 𝑊 ⊆ (^◡𝐹 “ 𝑀))))
154	101, 152, 153	syl2anc 585	. . . . . . . . . 10 ⊢ (𝜑 → (𝑊 ∈ (𝐶 ↾_t (^◡𝐹 “ 𝑀)) ↔ (𝑊 ∈ 𝐶 ∧ 𝑊 ⊆ (^◡𝐹 “ 𝑀))))
155	143, 148, 154	mpbir2and 714	. . . . . . . . 9 ⊢ (𝜑 → 𝑊 ∈ (𝐶 ↾_t (^◡𝐹 “ 𝑀)))
156	155	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → 𝑊 ∈ (𝐶 ↾_t (^◡𝐹 “ 𝑀)))
157	5	cvmscld 35455	. . . . . . . . . 10 ⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑇 ∈ (𝑆‘𝑀) ∧ 𝑊 ∈ 𝑇) → 𝑊 ∈ (Clsd‘(𝐶 ↾_t (^◡𝐹 “ 𝑀))))
158	6, 31, 142, 157	syl3anc 1374	. . . . . . . . 9 ⊢ (𝜑 → 𝑊 ∈ (Clsd‘(𝐶 ↾_t (^◡𝐹 “ 𝑀))))
159	158	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → 𝑊 ∈ (Clsd‘(𝐶 ↾_t (^◡𝐹 “ 𝑀))))
160		cvmlift2lem9.10	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑍 ∈ 𝑉)
161	160	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → 𝑍 ∈ 𝑉)
162		opelxpi 5668	. . . . . . . . . 10 ⊢ ((𝑚 ∈ {𝑚} ∧ 𝑍 ∈ 𝑉) → ⟨𝑚, 𝑍⟩ ∈ ({𝑚} × 𝑉))
163	52, 161, 162	syl2anc 585	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → ⟨𝑚, 𝑍⟩ ∈ ({𝑚} × 𝑉))
164	81, 84	sstrd 3932	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → ({𝑚} × 𝑉) ⊆ ((0[,]1) × (0[,]1)))
165	4	restuni 23127	. . . . . . . . . 10 ⊢ (((II ×_t II) ∈ Top ∧ ({𝑚} × 𝑉) ⊆ ((0[,]1) × (0[,]1))) → ({𝑚} × 𝑉) = ∪ ((II ×_t II) ↾_t ({𝑚} × 𝑉)))
166	15, 164, 165	sylancr 588	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → ({𝑚} × 𝑉) = ∪ ((II ×_t II) ↾_t ({𝑚} × 𝑉)))
167	163, 166	eleqtrd 2838	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → ⟨𝑚, 𝑍⟩ ∈ ∪ ((II ×_t II) ↾_t ({𝑚} × 𝑉)))
168		df-ov 7370	. . . . . . . . . 10 ⊢ (𝑚(𝐾 ↾ ({𝑚} × 𝑉))𝑍) = ((𝐾 ↾ ({𝑚} × 𝑉))‘⟨𝑚, 𝑍⟩)
169		ovres 7533	. . . . . . . . . . . 12 ⊢ ((𝑚 ∈ {𝑚} ∧ 𝑍 ∈ 𝑉) → (𝑚(𝐾 ↾ ({𝑚} × 𝑉))𝑍) = (𝑚𝐾𝑍))
170	52, 161, 169	syl2anc 585	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → (𝑚(𝐾 ↾ ({𝑚} × 𝑉))𝑍) = (𝑚𝐾𝑍))
171		snidg 4604	. . . . . . . . . . . . . 14 ⊢ (𝑍 ∈ 𝑉 → 𝑍 ∈ {𝑍})
172	160, 171	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑍 ∈ {𝑍})
173	172	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → 𝑍 ∈ {𝑍})
174		ovres 7533	. . . . . . . . . . . 12 ⊢ ((𝑚 ∈ 𝑈 ∧ 𝑍 ∈ {𝑍}) → (𝑚(𝐾 ↾ (𝑈 × {𝑍}))𝑍) = (𝑚𝐾𝑍))
175	106, 173, 174	syl2anc 585	. . . . . . . . . . 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 23596	. . . . . . . . . . . . . . 15 ⊢ (((II ∈ Top ∧ II ∈ Top) ∧ (𝑈 ∈ II ∧ {𝑍} ∈ V)) → ((II ×_t II) ↾_t (𝑈 × {𝑍})) = ((II ↾_t 𝑈) ×_t (II ↾_t {𝑍})))
183	179, 179, 17, 181, 182	syl22anc 839	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((II ×_t II) ↾_t (𝑈 × {𝑍})) = ((II ↾_t 𝑈) ×_t (II ↾_t {𝑍})))
184		cvmlift2lem9.5	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (II ↾_t 𝑈) ∈ Conn)
185	26, 160	sseldd 3922	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑍 ∈ (0[,]1))
186		restsn2 23136	. . . . . . . . . . . . . . . . 17 ⊢ ((II ∈ (TopOn‘(0[,]1)) ∧ 𝑍 ∈ (0[,]1)) → (II ↾_t {𝑍}) = 𝒫 {𝑍})
187	63, 185, 186	sylancr 588	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (II ↾_t {𝑍}) = 𝒫 {𝑍})
188		pwsn 4843	. . . . . . . . . . . . . . . . 17 ⊢ 𝒫 {𝑍} = {∅, {𝑍}}
189		indisconn 23383	. . . . . . . . . . . . . . . . 17 ⊢ {∅, {𝑍}} ∈ Conn
190	188, 189	eqeltri 2832	. . . . . . . . . . . . . . . 16 ⊢ 𝒫 {𝑍} ∈ Conn
191	187, 190	eqeltrdi 2844	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (II ↾_t {𝑍}) ∈ Conn)
192		txconn 23654	. . . . . . . . . . . . . . 15 ⊢ (((II ↾_t 𝑈) ∈ Conn ∧ (II ↾_t {𝑍}) ∈ Conn) → ((II ↾_t 𝑈) ×_t (II ↾_t {𝑍})) ∈ Conn)
193	184, 191, 192	syl2anc 585	. . . . . . . . . . . . . 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 5644	. . . . . . . . . . . . . . . 16 ⊢ (𝐾 “ (𝑈 × {𝑍})) = ran (𝐾 ↾ (𝑈 × {𝑍}))
198	160	snssd 4730	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → {𝑍} ⊆ 𝑉)
199		xpss2 5651	. . . . . . . . . . . . . . . . . 18 ⊢ ({𝑍} ⊆ 𝑉 → (𝑈 × {𝑍}) ⊆ (𝑈 × 𝑉))
200		imass2 6067	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑈 × {𝑍}) ⊆ (𝑈 × 𝑉) → (𝐾 “ (𝑈 × {𝑍})) ⊆ (𝐾 “ (𝑈 × 𝑉)))
201	198, 199, 200	3syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐾 “ (𝑈 × {𝑍})) ⊆ (𝐾 “ (𝑈 × 𝑉)))
202	201, 124	sstrd 3932	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐾 “ (𝑈 × {𝑍})) ⊆ (^◡𝐹 “ 𝑀))
203	197, 202	eqsstrrid 3961	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ran (𝐾 ↾ (𝑈 × {𝑍})) ⊆ (^◡𝐹 “ 𝑀))
204		cnrest2 23251	. . . . . . . . . . . . . . 15 ⊢ ((𝐶 ∈ (TopOn‘𝐵) ∧ ran (𝐾 ↾ (𝑈 × {𝑍})) ⊆ (^◡𝐹 “ 𝑀) ∧ (^◡𝐹 “ 𝑀) ⊆ 𝐵) → ((𝐾 ↾ (𝑈 × {𝑍})) ∈ (((II ×_t II) ↾_t (𝑈 × {𝑍})) Cn 𝐶) ↔ (𝐾 ↾ (𝑈 × {𝑍})) ∈ (((II ×_t II) ↾_t (𝑈 × {𝑍})) Cn (𝐶 ↾_t (^◡𝐹 “ 𝑀)))))
205	196, 203, 135, 204	syl3anc 1374	. . . . . . . . . . . . . 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 5668	. . . . . . . . . . . . . . 15 ⊢ ((𝑋 ∈ 𝑈 ∧ 𝑍 ∈ {𝑍}) → ⟨𝑋, 𝑍⟩ ∈ (𝑈 × {𝑍}))
208	21, 172, 207	syl2anc 585	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ⟨𝑋, 𝑍⟩ ∈ (𝑈 × {𝑍}))
209	185	snssd 4730	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → {𝑍} ⊆ (0[,]1))
210		xpss12 5646	. . . . . . . . . . . . . . . 16 ⊢ ((𝑈 ⊆ (0[,]1) ∧ {𝑍} ⊆ (0[,]1)) → (𝑈 × {𝑍}) ⊆ ((0[,]1) × (0[,]1)))
211	20, 209, 210	syl2anc 585	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑈 × {𝑍}) ⊆ ((0[,]1) × (0[,]1)))
212	4	restuni 23127	. . . . . . . . . . . . . . 15 ⊢ (((II ×_t II) ∈ Top ∧ (𝑈 × {𝑍}) ⊆ ((0[,]1) × (0[,]1))) → (𝑈 × {𝑍}) = ∪ ((II ×_t II) ↾_t (𝑈 × {𝑍})))
213	15, 211, 212	sylancr 588	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑈 × {𝑍}) = ∪ ((II ×_t II) ↾_t (𝑈 × {𝑍})))
214	208, 213	eleqtrd 2838	. . . . . . . . . . . . 13 ⊢ (𝜑 → ⟨𝑋, 𝑍⟩ ∈ ∪ ((II ×_t II) ↾_t (𝑈 × {𝑍})))
215		df-ov 7370	. . . . . . . . . . . . . . 15 ⊢ (𝑋(𝐾 ↾ (𝑈 × {𝑍}))𝑍) = ((𝐾 ↾ (𝑈 × {𝑍}))‘⟨𝑋, 𝑍⟩)
216		ovres 7533	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑋 ∈ 𝑈 ∧ 𝑍 ∈ {𝑍}) → (𝑋(𝐾 ↾ (𝑈 × {𝑍}))𝑍) = (𝑋𝐾𝑍))
217	21, 172, 216	syl2anc 585	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑋(𝐾 ↾ (𝑈 × {𝑍}))𝑍) = (𝑋𝐾𝑍))
218		snidg 4604	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑋 ∈ 𝑈 → 𝑋 ∈ {𝑋})
219	21, 218	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑋 ∈ {𝑋})
220		ovres 7533	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑋 ∈ {𝑋} ∧ 𝑍 ∈ 𝑉) → (𝑋(𝐾 ↾ ({𝑋} × 𝑉))𝑍) = (𝑋𝐾𝑍))
221	219, 160, 220	syl2anc 585	. . . . . . . . . . . . . . . 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 23596	. . . . . . . . . . . . . . . . . . 19 ⊢ (((II ∈ Top ∧ II ∈ Top) ∧ ({𝑋} ∈ V ∧ 𝑉 ∈ II)) → ((II ×_t II) ↾_t ({𝑋} × 𝑉)) = ((II ↾_t {𝑋}) ×_t (II ↾_t 𝑉)))
228	179, 179, 226, 23, 227	syl22anc 839	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((II ×_t II) ↾_t ({𝑋} × 𝑉)) = ((II ↾_t {𝑋}) ×_t (II ↾_t 𝑉)))
229		restsn2 23136	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((II ∈ (TopOn‘(0[,]1)) ∧ 𝑋 ∈ (0[,]1)) → (II ↾_t {𝑋}) = 𝒫 {𝑋})
230	63, 22, 229	sylancr 588	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (II ↾_t {𝑋}) = 𝒫 {𝑋})
231		pwsn 4843	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝒫 {𝑋} = {∅, {𝑋}}
232		indisconn 23383	. . . . . . . . . . . . . . . . . . . . 21 ⊢ {∅, {𝑋}} ∈ Conn
233	231, 232	eqeltri 2832	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝒫 {𝑋} ∈ Conn
234	230, 233	eqeltrdi 2844	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (II ↾_t {𝑋}) ∈ Conn)
235		txconn 23654	. . . . . . . . . . . . . . . . . . 19 ⊢ (((II ↾_t {𝑋}) ∈ Conn ∧ (II ↾_t 𝑉) ∈ Conn) → ((II ↾_t {𝑋}) ×_t (II ↾_t 𝑉)) ∈ Conn)
236	234, 72, 235	syl2anc 585	. . . . . . . . . . . . . . . . . 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 35490	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑋 ∈ (0[,]1)) → (𝐾 ↾ ({𝑋} × (0[,]1))) ∈ (((II ×_t II) ↾_t ({𝑋} × (0[,]1))) Cn 𝐶))
239	22, 238	mpdan 688	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐾 ↾ ({𝑋} × (0[,]1))) ∈ (((II ×_t II) ↾_t ({𝑋} × (0[,]1))) Cn 𝐶))
240		xpss2 5651	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑉 ⊆ (0[,]1) → ({𝑋} × 𝑉) ⊆ ({𝑋} × (0[,]1)))
241	23, 25, 240	3syl 18	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ({𝑋} × 𝑉) ⊆ ({𝑋} × (0[,]1)))
242	22	snssd 4730	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → {𝑋} ⊆ (0[,]1))
243		xpss1 5650	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ({𝑋} ⊆ (0[,]1) → ({𝑋} × (0[,]1)) ⊆ ((0[,]1) × (0[,]1)))
244	242, 243	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ({𝑋} × (0[,]1)) ⊆ ((0[,]1) × (0[,]1)))
245	4	restuni 23127	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((II ×_t II) ∈ Top ∧ ({𝑋} × (0[,]1)) ⊆ ((0[,]1) × (0[,]1))) → ({𝑋} × (0[,]1)) = ∪ ((II ×_t II) ↾_t ({𝑋} × (0[,]1))))
246	15, 244, 245	sylancr 588	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ({𝑋} × (0[,]1)) = ∪ ((II ×_t II) ↾_t ({𝑋} × (0[,]1))))
247	241, 246	sseqtrd 3958	. . . . . . . . . . . . . . . . . . . 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 23250	. . . . . . . . . . . . . . . . . . . 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 585	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝐾 ↾ ({𝑋} × (0[,]1))) ↾ ({𝑋} × 𝑉)) ∈ ((((II ×_t II) ↾_t ({𝑋} × (0[,]1))) ↾_t ({𝑋} × 𝑉)) Cn 𝐶))
251	241	resabs1d 5973	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝐾 ↾ ({𝑋} × (0[,]1))) ↾ ({𝑋} × 𝑉)) = (𝐾 ↾ ({𝑋} × 𝑉)))
252	225, 93	xpex 7707	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ({𝑋} × (0[,]1)) ∈ V
253	252	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ({𝑋} × (0[,]1)) ∈ V)
254		restabs 23130	. . . . . . . . . . . . . . . . . . . . 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 1374	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (((II ×_t II) ↾_t ({𝑋} × (0[,]1))) ↾_t ({𝑋} × 𝑉)) = ((II ×_t II) ↾_t ({𝑋} × 𝑉)))
256	255	oveq1d 7382	. . . . . . . . . . . . . . . . . . 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 5644	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐾 “ ({𝑋} × 𝑉)) = ran (𝐾 ↾ ({𝑋} × 𝑉))
259	21	snssd 4730	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → {𝑋} ⊆ 𝑈)
260		xpss1 5650	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ({𝑋} ⊆ 𝑈 → ({𝑋} × 𝑉) ⊆ (𝑈 × 𝑉))
261		imass2 6067	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (({𝑋} × 𝑉) ⊆ (𝑈 × 𝑉) → (𝐾 “ ({𝑋} × 𝑉)) ⊆ (𝐾 “ (𝑈 × 𝑉)))
262	259, 260, 261	3syl 18	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝐾 “ ({𝑋} × 𝑉)) ⊆ (𝐾 “ (𝑈 × 𝑉)))
263	262, 124	sstrd 3932	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐾 “ ({𝑋} × 𝑉)) ⊆ (^◡𝐹 “ 𝑀))
264	258, 263	eqsstrrid 3961	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ran (𝐾 ↾ ({𝑋} × 𝑉)) ⊆ (^◡𝐹 “ 𝑀))
265		cnrest2 23251	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐶 ∈ (TopOn‘𝐵) ∧ ran (𝐾 ↾ ({𝑋} × 𝑉)) ⊆ (^◡𝐹 “ 𝑀) ∧ (^◡𝐹 “ 𝑀) ⊆ 𝐵) → ((𝐾 ↾ ({𝑋} × 𝑉)) ∈ (((II ×_t II) ↾_t ({𝑋} × 𝑉)) Cn 𝐶) ↔ (𝐾 ↾ ({𝑋} × 𝑉)) ∈ (((II ×_t II) ↾_t ({𝑋} × 𝑉)) Cn (𝐶 ↾_t (^◡𝐹 “ 𝑀)))))
266	196, 264, 135, 265	syl3anc 1374	. . . . . . . . . . . . . . . . . 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 5668	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑋 ∈ {𝑋} ∧ 𝑌 ∈ 𝑉) → ⟨𝑋, 𝑌⟩ ∈ ({𝑋} × 𝑉))
269	219, 27, 268	syl2anc 585	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ⟨𝑋, 𝑌⟩ ∈ ({𝑋} × 𝑉))
270	259, 260	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ({𝑋} × 𝑉) ⊆ (𝑈 × 𝑉))
271	270, 50	sstrd 3932	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ({𝑋} × 𝑉) ⊆ ((0[,]1) × (0[,]1)))
272	4	restuni 23127	. . . . . . . . . . . . . . . . . . 19 ⊢ (((II ×_t II) ∈ Top ∧ ({𝑋} × 𝑉) ⊆ ((0[,]1) × (0[,]1))) → ({𝑋} × 𝑉) = ∪ ((II ×_t II) ↾_t ({𝑋} × 𝑉)))
273	15, 271, 272	sylancr 588	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ({𝑋} × 𝑉) = ∪ ((II ×_t II) ↾_t ({𝑋} × 𝑉)))
274	269, 273	eleqtrd 2838	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ⟨𝑋, 𝑌⟩ ∈ ∪ ((II ×_t II) ↾_t ({𝑋} × 𝑉)))
275		df-ov 7370	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑋(𝐾 ↾ ({𝑋} × 𝑉))𝑌) = ((𝐾 ↾ ({𝑋} × 𝑉))‘⟨𝑋, 𝑌⟩)
276		ovres 7533	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑋 ∈ {𝑋} ∧ 𝑌 ∈ 𝑉) → (𝑋(𝐾 ↾ ({𝑋} × 𝑉))𝑌) = (𝑋𝐾𝑌))
277	219, 27, 276	syl2anc 585	. . . . . . . . . . . . . . . . . . 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 23391	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐾 ↾ ({𝑋} × 𝑉)):∪ ((II ×_t II) ↾_t ({𝑋} × 𝑉))⟶𝑊)
282	273	feq2d 6652	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐾 ↾ ({𝑋} × 𝑉)):({𝑋} × 𝑉)⟶𝑊 ↔ (𝐾 ↾ ({𝑋} × 𝑉)):∪ ((II ×_t II) ↾_t ({𝑋} × 𝑉))⟶𝑊))
283	281, 282	mpbird 257	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐾 ↾ ({𝑋} × 𝑉)):({𝑋} × 𝑉)⟶𝑊)
284	283, 219, 160	fovcdmd 7539	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑋(𝐾 ↾ ({𝑋} × 𝑉))𝑍) ∈ 𝑊)
285	223, 284	eqeltrd 2836	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐾 ↾ (𝑈 × {𝑍}))‘⟨𝑋, 𝑍⟩) ∈ 𝑊)
286	178, 194, 206, 155, 158, 214, 285	conncn 23391	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐾 ↾ (𝑈 × {𝑍})):∪ ((II ×_t II) ↾_t (𝑈 × {𝑍}))⟶𝑊)
287	213	feq2d 6652	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐾 ↾ (𝑈 × {𝑍})):(𝑈 × {𝑍})⟶𝑊 ↔ (𝐾 ↾ (𝑈 × {𝑍})):∪ ((II ×_t II) ↾_t (𝑈 × {𝑍}))⟶𝑊))
288	286, 287	mpbird 257	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐾 ↾ (𝑈 × {𝑍})):(𝑈 × {𝑍})⟶𝑊)
289	288	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → (𝐾 ↾ (𝑈 × {𝑍})):(𝑈 × {𝑍})⟶𝑊)
290	289, 106, 173	fovcdmd 7539	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → (𝑚(𝐾 ↾ (𝑈 × {𝑍}))𝑍) ∈ 𝑊)
291	177, 290	eqeltrd 2836	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → ((𝐾 ↾ ({𝑚} × 𝑉))‘⟨𝑚, 𝑍⟩) ∈ 𝑊)
292	56, 76, 139, 156, 159, 167, 291	conncn 23391	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → (𝐾 ↾ ({𝑚} × 𝑉)):∪ ((II ×_t II) ↾_t ({𝑚} × 𝑉))⟶𝑊)
293	166	feq2d 6652	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → ((𝐾 ↾ ({𝑚} × 𝑉)):({𝑚} × 𝑉)⟶𝑊 ↔ (𝐾 ↾ ({𝑚} × 𝑉)):∪ ((II ×_t II) ↾_t ({𝑚} × 𝑉))⟶𝑊))
294	292, 293	mpbird 257	. . . . . 6 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → (𝐾 ↾ ({𝑚} × 𝑉)):({𝑚} × 𝑉)⟶𝑊)
295	294, 52, 53	fovcdmd 7539	. . . . 5 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → (𝑚(𝐾 ↾ ({𝑚} × 𝑉))𝑛) ∈ 𝑊)
296	55, 295	eqeltrrd 2837	. . . 4 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → (𝑚𝐾𝑛) ∈ 𝑊)
297	296	ralrimivva 3180	. . 3 ⊢ (𝜑 → ∀𝑚 ∈ 𝑈 ∀𝑛 ∈ 𝑉 (𝑚𝐾𝑛) ∈ 𝑊)
298		funimassov 7544	. . . 4 ⊢ ((Fun 𝐾 ∧ (𝑈 × 𝑉) ⊆ dom 𝐾) → ((𝐾 “ (𝑈 × 𝑉)) ⊆ 𝑊 ↔ ∀𝑚 ∈ 𝑈 ∀𝑛 ∈ 𝑉 (𝑚𝐾𝑛) ∈ 𝑊))
299	119, 121, 298	syl2anc 585	. . 3 ⊢ (𝜑 → ((𝐾 “ (𝑈 × 𝑉)) ⊆ 𝑊 ↔ ∀𝑚 ∈ 𝑈 ∀𝑛 ∈ 𝑉 (𝑚𝐾𝑛) ∈ 𝑊))
300	297, 299	mpbird 257	. 2 ⊢ (𝜑 → (𝐾 “ (𝑈 × 𝑉)) ⊆ 𝑊)
301	1, 4, 5, 6, 12, 14, 16, 30, 31, 48, 50, 300	cvmlift2lem9a 35485	1 ⊢ (𝜑 → (𝐾 ↾ (𝑈 × 𝑉)) ∈ (((II ×_t II) ↾_t (𝑈 × 𝑉)) Cn 𝐶))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1542 ∈ wcel 2114 ∀wral 3051 {crab 3389 Vcvv 3429 ∖ cdif 3886 ∩ cin 3888 ⊆ wss 3889 ∅c0 4273 𝒫 cpw 4541 {csn 4567 {cpr 4569 ⟨cop 4573 ∪ cuni 4850 ↦ cmpt 5166 × cxp 5629 ^◡ccnv 5630 dom cdm 5631 ran crn 5632 ↾ cres 5633 “ cima 5634 ∘ ccom 5635 Fun wfun 6492 ⟶wf 6494 ‘cfv 6498 ℩crio 7323 (class class class)co 7367 ∈ cmpo 7369 0cc0 11038 1c1 11039 [,]cicc 13301 ↾_t crest 17383 Topctop 22858 TopOnctopon 22875 Clsdccld 22981 Cn ccn 23189 Conncconn 23376 ×_t ctx 23525 Homeochmeo 23718 IIcii 24842 CovMap ccvm 35437

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 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2708 ax-rep 5212 ax-sep 5231 ax-nul 5241 ax-pow 5307 ax-pr 5375 ax-un 7689 ax-inf2 9562 ax-cnex 11094 ax-resscn 11095 ax-1cn 11096 ax-icn 11097 ax-addcl 11098 ax-addrcl 11099 ax-mulcl 11100 ax-mulrcl 11101 ax-mulcom 11102 ax-addass 11103 ax-mulass 11104 ax-distr 11105 ax-i2m1 11106 ax-1ne0 11107 ax-1rid 11108 ax-rnegex 11109 ax-rrecex 11110 ax-cnre 11111 ax-pre-lttri 11112 ax-pre-lttrn 11113 ax-pre-ltadd 11114 ax-pre-mulgt0 11115 ax-pre-sup 11116 ax-addf 11117

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 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 3062 df-rmo 3342 df-reu 3343 df-rab 3390 df-v 3431 df-sbc 3729 df-csb 3838 df-dif 3892 df-un 3894 df-in 3896 df-ss 3906 df-pss 3909 df-nul 4274 df-if 4467 df-pw 4543 df-sn 4568 df-pr 4570 df-tp 4572 df-op 4574 df-uni 4851 df-int 4890 df-iun 4935 df-iin 4936 df-br 5086 df-opab 5148 df-mpt 5167 df-tr 5193 df-id 5526 df-eprel 5531 df-po 5539 df-so 5540 df-fr 5584 df-se 5585 df-we 5586 df-xp 5637 df-rel 5638 df-cnv 5639 df-co 5640 df-dm 5641 df-rn 5642 df-res 5643 df-ima 5644 df-pred 6265 df-ord 6326 df-on 6327 df-lim 6328 df-suc 6329 df-iota 6454 df-fun 6500 df-fn 6501 df-f 6502 df-f1 6503 df-fo 6504 df-f1o 6505 df-fv 6506 df-isom 6507 df-riota 7324 df-ov 7370 df-oprab 7371 df-mpo 7372 df-of 7631 df-om 7818 df-1st 7942 df-2nd 7943 df-supp 8111 df-frecs 8231 df-wrecs 8262 df-recs 8311 df-rdg 8349 df-1o 8405 df-2o 8406 df-er 8643 df-ec 8645 df-map 8775 df-ixp 8846 df-en 8894 df-dom 8895 df-sdom 8896 df-fin 8897 df-fsupp 9275 df-fi 9324 df-sup 9355 df-inf 9356 df-oi 9425 df-card 9863 df-pnf 11181 df-mnf 11182 df-xr 11183 df-ltxr 11184 df-le 11185 df-sub 11379 df-neg 11380 df-div 11808 df-nn 12175 df-2 12244 df-3 12245 df-4 12246 df-5 12247 df-6 12248 df-7 12249 df-8 12250 df-9 12251 df-n0 12438 df-z 12525 df-dec 12645 df-uz 12789 df-q 12899 df-rp 12943 df-xneg 13063 df-xadd 13064 df-xmul 13065 df-ioo 13302 df-ico 13304 df-icc 13305 df-fz 13462 df-fzo 13609 df-fl 13751 df-seq 13964 df-exp 14024 df-hash 14293 df-cj 15061 df-re 15062 df-im 15063 df-sqrt 15197 df-abs 15198 df-clim 15450 df-sum 15649 df-struct 17117 df-sets 17134 df-slot 17152 df-ndx 17164 df-base 17180 df-ress 17201 df-plusg 17233 df-mulr 17234 df-starv 17235 df-sca 17236 df-vsca 17237 df-ip 17238 df-tset 17239 df-ple 17240 df-ds 17242 df-unif 17243 df-hom 17244 df-cco 17245 df-rest 17385 df-topn 17386 df-0g 17404 df-gsum 17405 df-topgen 17406 df-pt 17407 df-prds 17410 df-xrs 17466 df-qtop 17471 df-imas 17472 df-xps 17474 df-mre 17548 df-mrc 17549 df-acs 17551 df-mgm 18608 df-sgrp 18687 df-mnd 18703 df-submnd 18752 df-mulg 19044 df-cntz 19292 df-cmn 19757 df-psmet 21344 df-xmet 21345 df-met 21346 df-bl 21347 df-mopn 21348 df-cnfld 21353 df-top 22859 df-topon 22876 df-topsp 22898 df-bases 22911 df-cld 22984 df-ntr 22985 df-cls 22986 df-nei 23063 df-cn 23192 df-cnp 23193 df-cmp 23352 df-conn 23377 df-lly 23431 df-nlly 23432 df-tx 23527 df-hmeo 23720 df-xms 24285 df-ms 24286 df-tms 24287 df-ii 24844 df-cncf 24845 df-htpy 24937 df-phtpy 24938 df-phtpc 24959 df-pconn 35403 df-sconn 35404 df-cvm 35438

This theorem is referenced by: cvmlift2lem10 35494

W3C validator