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 35524

Description: Lemma for cvmlift2 35529. (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 24841	. . 3 ⊢ II ∈ Top
3		iiuni 24842	. . 3 ⊢ (0[,]1) = ∪ II
4	2, 2, 3, 3	txunii 23549	. 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 35520	. 2 ⊢ (𝜑 → 𝐾:((0[,]1) × (0[,]1))⟶𝐵)
13	1, 6, 7, 8, 9, 10, 11	cvmlift2lem7 35522	. . 3 ⊢ (𝜑 → (𝐹 ∘ 𝐾) = 𝐺)
14	13, 7	eqeltrd 2837	. 2 ⊢ (𝜑 → (𝐹 ∘ 𝐾) ∈ ((II ×_t II) Cn 𝐽))
15	2, 2	txtopi 23546	. . 3 ⊢ (II ×_t II) ∈ Top
16	15	a1i 11	. 2 ⊢ (𝜑 → (II ×_t II) ∈ Top)
17		cvmlift2lem9.3	. . . . 5 ⊢ (𝜑 → 𝑈 ∈ II)
18		elssuni 4896	. . . . . 6 ⊢ (𝑈 ∈ II → 𝑈 ⊆ ∪ II)
19	18, 3	sseqtrrdi 3977	. . . . 5 ⊢ (𝑈 ∈ II → 𝑈 ⊆ (0[,]1))
20	17, 19	syl 17	. . . 4 ⊢ (𝜑 → 𝑈 ⊆ (0[,]1))
21		cvmlift2lem9.7	. . . 4 ⊢ (𝜑 → 𝑋 ∈ 𝑈)
22	20, 21	sseldd 3936	. . 3 ⊢ (𝜑 → 𝑋 ∈ (0[,]1))
23		cvmlift2lem9.4	. . . . 5 ⊢ (𝜑 → 𝑉 ∈ II)
24		elssuni 4896	. . . . . 6 ⊢ (𝑉 ∈ II → 𝑉 ⊆ ∪ II)
25	24, 3	sseqtrrdi 3977	. . . . 5 ⊢ (𝑉 ∈ II → 𝑉 ⊆ (0[,]1))
26	23, 25	syl 17	. . . 4 ⊢ (𝜑 → 𝑉 ⊆ (0[,]1))
27		cvmlift2lem9.8	. . . 4 ⊢ (𝜑 → 𝑌 ∈ 𝑉)
28	26, 27	sseldd 3936	. . 3 ⊢ (𝜑 → 𝑌 ∈ (0[,]1))
29		opelxpi 5669	. . 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 7540	. . . 4 ⊢ (𝜑 → (𝑋𝐾𝑌) ∈ 𝐵)
33		fvco3 6941	. . . . . . . 8 ⊢ ((𝐾:((0[,]1) × (0[,]1))⟶𝐵 ∧ ⟨𝑋, 𝑌⟩ ∈ ((0[,]1) × (0[,]1))) → ((𝐹 ∘ 𝐾)‘⟨𝑋, 𝑌⟩) = (𝐹‘(𝐾‘⟨𝑋, 𝑌⟩)))
34	12, 30, 33	syl2anc 585	. . . . . . 7 ⊢ (𝜑 → ((𝐹 ∘ 𝐾)‘⟨𝑋, 𝑌⟩) = (𝐹‘(𝐾‘⟨𝑋, 𝑌⟩)))
35	13	fveq1d 6844	. . . . . . 7 ⊢ (𝜑 → ((𝐹 ∘ 𝐾)‘⟨𝑋, 𝑌⟩) = (𝐺‘⟨𝑋, 𝑌⟩))
36	34, 35	eqtr3d 2774	. . . . . 6 ⊢ (𝜑 → (𝐹‘(𝐾‘⟨𝑋, 𝑌⟩)) = (𝐺‘⟨𝑋, 𝑌⟩))
37		df-ov 7371	. . . . . . 7 ⊢ (𝑋𝐾𝑌) = (𝐾‘⟨𝑋, 𝑌⟩)
38	37	fveq2i 6845	. . . . . 6 ⊢ (𝐹‘(𝑋𝐾𝑌)) = (𝐹‘(𝐾‘⟨𝑋, 𝑌⟩))
39		df-ov 7371	. . . . . 6 ⊢ (𝑋𝐺𝑌) = (𝐺‘⟨𝑋, 𝑌⟩)
40	36, 38, 39	3eqtr4g 2797	. . . . 5 ⊢ (𝜑 → (𝐹‘(𝑋𝐾𝑌)) = (𝑋𝐺𝑌))
41		cvmlift2lem9.1	. . . . 5 ⊢ (𝜑 → (𝑋𝐺𝑌) ∈ 𝑀)
42	40, 41	eqeltrd 2837	. . . 4 ⊢ (𝜑 → (𝐹‘(𝑋𝐾𝑌)) ∈ 𝑀)
43		cvmlift2lem9.w	. . . . 5 ⊢ 𝑊 = (℩𝑏 ∈ 𝑇 (𝑋𝐾𝑌) ∈ 𝑏)
44	5, 1, 43	cvmsiota 35490	. . . 4 ⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ (𝑇 ∈ (𝑆‘𝑀) ∧ (𝑋𝐾𝑌) ∈ 𝐵 ∧ (𝐹‘(𝑋𝐾𝑌)) ∈ 𝑀)) → (𝑊 ∈ 𝑇 ∧ (𝑋𝐾𝑌) ∈ 𝑊))
45	6, 31, 32, 42, 44	syl13anc 1375	. . 3 ⊢ (𝜑 → (𝑊 ∈ 𝑇 ∧ (𝑋𝐾𝑌) ∈ 𝑊))
46	37	eleq1i 2828	. . . 4 ⊢ ((𝑋𝐾𝑌) ∈ 𝑊 ↔ (𝐾‘⟨𝑋, 𝑌⟩) ∈ 𝑊)
47	46	anbi2i 624	. . 3 ⊢ ((𝑊 ∈ 𝑇 ∧ (𝑋𝐾𝑌) ∈ 𝑊) ↔ (𝑊 ∈ 𝑇 ∧ (𝐾‘⟨𝑋, 𝑌⟩) ∈ 𝑊))
48	45, 47	sylib 218	. 2 ⊢ (𝜑 → (𝑊 ∈ 𝑇 ∧ (𝐾‘⟨𝑋, 𝑌⟩) ∈ 𝑊))
49		xpss12 5647	. . 3 ⊢ ((𝑈 ⊆ (0[,]1) ∧ 𝑉 ⊆ (0[,]1)) → (𝑈 × 𝑉) ⊆ ((0[,]1) × (0[,]1)))
50	20, 26, 49	syl2anc 585	. 2 ⊢ (𝜑 → (𝑈 × 𝑉) ⊆ ((0[,]1) × (0[,]1)))
51		snidg 4619	. . . . . . 7 ⊢ (𝑚 ∈ 𝑈 → 𝑚 ∈ {𝑚})
52	51	ad2antrl 729	. . . . . 6 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → 𝑚 ∈ {𝑚})
53		simprr 773	. . . . . 6 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → 𝑛 ∈ 𝑉)
54		ovres 7534	. . . . . 6 ⊢ ((𝑚 ∈ {𝑚} ∧ 𝑛 ∈ 𝑉) → (𝑚(𝐾 ↾ ({𝑚} × 𝑉))𝑛) = (𝑚𝐾𝑛))
55	52, 53, 54	syl2anc 585	. . . . 5 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → (𝑚(𝐾 ↾ ({𝑚} × 𝑉))𝑛) = (𝑚𝐾𝑛))
56		eqid 2737	. . . . . . . 8 ⊢ ∪ ((II ×_t II) ↾_t ({𝑚} × 𝑉)) = ∪ ((II ×_t II) ↾_t ({𝑚} × 𝑉))
57	2	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → II ∈ Top)
58		snex 5385	. . . . . . . . . . 11 ⊢ {𝑚} ∈ V
59	58	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → {𝑚} ∈ V)
60	23	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → 𝑉 ∈ II)
61		txrest 23587	. . . . . . . . . 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 24840	. . . . . . . . . . . 12 ⊢ II ∈ (TopOn‘(0[,]1))
64	20	sselda 3935	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑈) → 𝑚 ∈ (0[,]1))
65	64	adantrr 718	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → 𝑚 ∈ (0[,]1))
66		restsn2 23127	. . . . . . . . . . . 12 ⊢ ((II ∈ (TopOn‘(0[,]1)) ∧ 𝑚 ∈ (0[,]1)) → (II ↾_t {𝑚}) = 𝒫 {𝑚})
67	63, 65, 66	sylancr 588	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → (II ↾_t {𝑚}) = 𝒫 {𝑚})
68		pwsn 4858	. . . . . . . . . . . 12 ⊢ 𝒫 {𝑚} = {∅, {𝑚}}
69		indisconn 23374	. . . . . . . . . . . 12 ⊢ {∅, {𝑚}} ∈ Conn
70	68, 69	eqeltri 2833	. . . . . . . . . . 11 ⊢ 𝒫 {𝑚} ∈ Conn
71	67, 70	eqeltrdi 2845	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → (II ↾_t {𝑚}) ∈ Conn)
72		cvmlift2lem9.6	. . . . . . . . . . 11 ⊢ (𝜑 → (II ↾_t 𝑉) ∈ Conn)
73	72	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → (II ↾_t 𝑉) ∈ Conn)
74		txconn 23645	. . . . . . . . . 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 2837	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → ((II ×_t II) ↾_t ({𝑚} × 𝑉)) ∈ Conn)
77	1, 6, 7, 8, 9, 10, 11	cvmlift2lem6 35521	. . . . . . . . . . . 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 5652	. . . . . . . . . . . . 13 ⊢ (𝑉 ⊆ (0[,]1) → ({𝑚} × 𝑉) ⊆ ({𝑚} × (0[,]1)))
81	79, 80	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → ({𝑚} × 𝑉) ⊆ ({𝑚} × (0[,]1)))
82	65	snssd 4767	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → {𝑚} ⊆ (0[,]1))
83		xpss1 5651	. . . . . . . . . . . . . 14 ⊢ ({𝑚} ⊆ (0[,]1) → ({𝑚} × (0[,]1)) ⊆ ((0[,]1) × (0[,]1)))
84	82, 83	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → ({𝑚} × (0[,]1)) ⊆ ((0[,]1) × (0[,]1)))
85	4	restuni 23118	. . . . . . . . . . . . 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 3972	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → ({𝑚} × 𝑉) ⊆ ∪ ((II ×_t II) ↾_t ({𝑚} × (0[,]1))))
88		eqid 2737	. . . . . . . . . . . 12 ⊢ ∪ ((II ×_t II) ↾_t ({𝑚} × (0[,]1))) = ∪ ((II ×_t II) ↾_t ({𝑚} × (0[,]1)))
89	88	cnrest 23241	. . . . . . . . . . 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 5975	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → ((𝐾 ↾ ({𝑚} × (0[,]1))) ↾ ({𝑚} × 𝑉)) = (𝐾 ↾ ({𝑚} × 𝑉)))
92	15	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → (II ×_t II) ∈ Top)
93		ovex 7401	. . . . . . . . . . . . . 14 ⊢ (0[,]1) ∈ V
94	58, 93	xpex 7708	. . . . . . . . . . . . 13 ⊢ ({𝑚} × (0[,]1)) ∈ V
95	94	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → ({𝑚} × (0[,]1)) ∈ V)
96		restabs 23121	. . . . . . . . . . . 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 7383	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → ((((II ×_t II) ↾_t ({𝑚} × (0[,]1))) ↾_t ({𝑚} × 𝑉)) Cn 𝐶) = (((II ×_t II) ↾_t ({𝑚} × 𝑉)) Cn 𝐶))
99	90, 91, 98	3eltr3d 2851	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → (𝐾 ↾ ({𝑚} × 𝑉)) ∈ (((II ×_t II) ↾_t ({𝑚} × 𝑉)) Cn 𝐶))
100		cvmtop1 35473	. . . . . . . . . . . . 13 ⊢ (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐶 ∈ Top)
101	6, 100	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐶 ∈ Top)
102	101	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → 𝐶 ∈ Top)
103	1	toptopon 22873	. . . . . . . . . . 11 ⊢ (𝐶 ∈ Top ↔ 𝐶 ∈ (TopOn‘𝐵))
104	102, 103	sylib 218	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → 𝐶 ∈ (TopOn‘𝐵))
105		df-ima 5645	. . . . . . . . . . 11 ⊢ (𝐾 “ ({𝑚} × 𝑉)) = ran (𝐾 ↾ ({𝑚} × 𝑉))
106		simprl 771	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → 𝑚 ∈ 𝑈)
107	106	snssd 4767	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → {𝑚} ⊆ 𝑈)
108		xpss1 5651	. . . . . . . . . . . . 13 ⊢ ({𝑚} ⊆ 𝑈 → ({𝑚} × 𝑉) ⊆ (𝑈 × 𝑉))
109		imass2 6069	. . . . . . . . . . . . 13 ⊢ (({𝑚} × 𝑉) ⊆ (𝑈 × 𝑉) → (𝐾 “ ({𝑚} × 𝑉)) ⊆ (𝐾 “ (𝑈 × 𝑉)))
110	107, 108, 109	3syl 18	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → (𝐾 “ ({𝑚} × 𝑉)) ⊆ (𝐾 “ (𝑈 × 𝑉)))
111		cvmlift2lem9.9	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑈 × 𝑉) ⊆ (^◡𝐺 “ 𝑀))
112		imaco 6217	. . . . . . . . . . . . . . . 16 ⊢ ((^◡𝐾 ∘ ^◡𝐹) “ 𝑀) = (^◡𝐾 “ (^◡𝐹 “ 𝑀))
113		cnvco 5842	. . . . . . . . . . . . . . . . . 18 ⊢ ^◡(𝐹 ∘ 𝐾) = (^◡𝐾 ∘ ^◡𝐹)
114	13	cnveqd 5832	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ^◡(𝐹 ∘ 𝐾) = ^◡𝐺)
115	113, 114	eqtr3id 2786	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (^◡𝐾 ∘ ^◡𝐹) = ^◡𝐺)
116	115	imaeq1d 6026	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((^◡𝐾 ∘ ^◡𝐹) “ 𝑀) = (^◡𝐺 “ 𝑀))
117	112, 116	eqtr3id 2786	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (^◡𝐾 “ (^◡𝐹 “ 𝑀)) = (^◡𝐺 “ 𝑀))
118	111, 117	sseqtrrd 3973	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑈 × 𝑉) ⊆ (^◡𝐾 “ (^◡𝐹 “ 𝑀)))
119	12	ffund 6674	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → Fun 𝐾)
120	12	fdmd 6680	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → dom 𝐾 = ((0[,]1) × (0[,]1)))
121	50, 120	sseqtrrd 3973	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑈 × 𝑉) ⊆ dom 𝐾)
122		funimass3 7008	. . . . . . . . . . . . . . 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 3946	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → (𝐾 “ ({𝑚} × 𝑉)) ⊆ (^◡𝐹 “ 𝑀))
127	105, 126	eqsstrrid 3975	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → ran (𝐾 ↾ ({𝑚} × 𝑉)) ⊆ (^◡𝐹 “ 𝑀))
128		cnvimass 6049	. . . . . . . . . . . 12 ⊢ (^◡𝐹 “ 𝑀) ⊆ dom 𝐹
129		cvmcn 35475	. . . . . . . . . . . . . 14 ⊢ (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐹 ∈ (𝐶 Cn 𝐽))
130	6, 129	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐹 ∈ (𝐶 Cn 𝐽))
131		eqid 2737	. . . . . . . . . . . . . 14 ⊢ ∪ 𝐽 = ∪ 𝐽
132	1, 131	cnf 23202	. . . . . . . . . . . . 13 ⊢ (𝐹 ∈ (𝐶 Cn 𝐽) → 𝐹:𝐵⟶∪ 𝐽)
133		fdm 6679	. . . . . . . . . . . . 13 ⊢ (𝐹:𝐵⟶∪ 𝐽 → dom 𝐹 = 𝐵)
134	130, 132, 133	3syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → dom 𝐹 = 𝐵)
135	128, 134	sseqtrid 3978	. . . . . . . . . . 11 ⊢ (𝜑 → (^◡𝐹 “ 𝑀) ⊆ 𝐵)
136	135	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → (^◡𝐹 “ 𝑀) ⊆ 𝐵)
137		cnrest2 23242	. . . . . . . . . 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 35480	. . . . . . . . . . . 12 ⊢ (𝑇 ∈ (𝑆‘𝑀) → 𝑇 ⊆ 𝐶)
141	31, 140	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑇 ⊆ 𝐶)
142	45	simpld 494	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑊 ∈ 𝑇)
143	141, 142	sseldd 3936	. . . . . . . . . 10 ⊢ (𝜑 → 𝑊 ∈ 𝐶)
144		elssuni 4896	. . . . . . . . . . . 12 ⊢ (𝑊 ∈ 𝑇 → 𝑊 ⊆ ∪ 𝑇)
145	142, 144	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑊 ⊆ ∪ 𝑇)
146	5	cvmsuni 35482	. . . . . . . . . . . 12 ⊢ (𝑇 ∈ (𝑆‘𝑀) → ∪ 𝑇 = (^◡𝐹 “ 𝑀))
147	31, 146	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → ∪ 𝑇 = (^◡𝐹 “ 𝑀))
148	145, 147	sseqtrd 3972	. . . . . . . . . 10 ⊢ (𝜑 → 𝑊 ⊆ (^◡𝐹 “ 𝑀))
149	5	cvmsrcl 35477	. . . . . . . . . . . . 13 ⊢ (𝑇 ∈ (𝑆‘𝑀) → 𝑀 ∈ 𝐽)
150	31, 149	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑀 ∈ 𝐽)
151		cnima 23221	. . . . . . . . . . . 12 ⊢ ((𝐹 ∈ (𝐶 Cn 𝐽) ∧ 𝑀 ∈ 𝐽) → (^◡𝐹 “ 𝑀) ∈ 𝐶)
152	130, 150, 151	syl2anc 585	. . . . . . . . . . 11 ⊢ (𝜑 → (^◡𝐹 “ 𝑀) ∈ 𝐶)
153		restopn2 23133	. . . . . . . . . . 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 35486	. . . . . . . . . 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 5669	. . . . . . . . . 10 ⊢ ((𝑚 ∈ {𝑚} ∧ 𝑍 ∈ 𝑉) → ⟨𝑚, 𝑍⟩ ∈ ({𝑚} × 𝑉))
163	52, 161, 162	syl2anc 585	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → ⟨𝑚, 𝑍⟩ ∈ ({𝑚} × 𝑉))
164	81, 84	sstrd 3946	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → ({𝑚} × 𝑉) ⊆ ((0[,]1) × (0[,]1)))
165	4	restuni 23118	. . . . . . . . . 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 2839	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → ⟨𝑚, 𝑍⟩ ∈ ∪ ((II ×_t II) ↾_t ({𝑚} × 𝑉)))
168		df-ov 7371	. . . . . . . . . 10 ⊢ (𝑚(𝐾 ↾ ({𝑚} × 𝑉))𝑍) = ((𝐾 ↾ ({𝑚} × 𝑉))‘⟨𝑚, 𝑍⟩)
169		ovres 7534	. . . . . . . . . . . 12 ⊢ ((𝑚 ∈ {𝑚} ∧ 𝑍 ∈ 𝑉) → (𝑚(𝐾 ↾ ({𝑚} × 𝑉))𝑍) = (𝑚𝐾𝑍))
170	52, 161, 169	syl2anc 585	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → (𝑚(𝐾 ↾ ({𝑚} × 𝑉))𝑍) = (𝑚𝐾𝑍))
171		snidg 4619	. . . . . . . . . . . . . 14 ⊢ (𝑍 ∈ 𝑉 → 𝑍 ∈ {𝑍})
172	160, 171	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑍 ∈ {𝑍})
173	172	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → 𝑍 ∈ {𝑍})
174		ovres 7534	. . . . . . . . . . . 12 ⊢ ((𝑚 ∈ 𝑈 ∧ 𝑍 ∈ {𝑍}) → (𝑚(𝐾 ↾ (𝑈 × {𝑍}))𝑍) = (𝑚𝐾𝑍))
175	106, 173, 174	syl2anc 585	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → (𝑚(𝐾 ↾ (𝑈 × {𝑍}))𝑍) = (𝑚𝐾𝑍))
176	170, 175	eqtr4d 2775	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → (𝑚(𝐾 ↾ ({𝑚} × 𝑉))𝑍) = (𝑚(𝐾 ↾ (𝑈 × {𝑍}))𝑍))
177	168, 176	eqtr3id 2786	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → ((𝐾 ↾ ({𝑚} × 𝑉))‘⟨𝑚, 𝑍⟩) = (𝑚(𝐾 ↾ (𝑈 × {𝑍}))𝑍))
178		eqid 2737	. . . . . . . . . . . . 13 ⊢ ∪ ((II ×_t II) ↾_t (𝑈 × {𝑍})) = ∪ ((II ×_t II) ↾_t (𝑈 × {𝑍}))
179	2	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → II ∈ Top)
180		snex 5385	. . . . . . . . . . . . . . . 16 ⊢ {𝑍} ∈ V
181	180	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → {𝑍} ∈ V)
182		txrest 23587	. . . . . . . . . . . . . . 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 3936	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑍 ∈ (0[,]1))
186		restsn2 23127	. . . . . . . . . . . . . . . . 17 ⊢ ((II ∈ (TopOn‘(0[,]1)) ∧ 𝑍 ∈ (0[,]1)) → (II ↾_t {𝑍}) = 𝒫 {𝑍})
187	63, 185, 186	sylancr 588	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (II ↾_t {𝑍}) = 𝒫 {𝑍})
188		pwsn 4858	. . . . . . . . . . . . . . . . 17 ⊢ 𝒫 {𝑍} = {∅, {𝑍}}
189		indisconn 23374	. . . . . . . . . . . . . . . . 17 ⊢ {∅, {𝑍}} ∈ Conn
190	188, 189	eqeltri 2833	. . . . . . . . . . . . . . . 16 ⊢ 𝒫 {𝑍} ∈ Conn
191	187, 190	eqeltrdi 2845	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (II ↾_t {𝑍}) ∈ Conn)
192		txconn 23645	. . . . . . . . . . . . . . 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 2837	. . . . . . . . . . . . 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 5645	. . . . . . . . . . . . . . . 16 ⊢ (𝐾 “ (𝑈 × {𝑍})) = ran (𝐾 ↾ (𝑈 × {𝑍}))
198	160	snssd 4767	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → {𝑍} ⊆ 𝑉)
199		xpss2 5652	. . . . . . . . . . . . . . . . . 18 ⊢ ({𝑍} ⊆ 𝑉 → (𝑈 × {𝑍}) ⊆ (𝑈 × 𝑉))
200		imass2 6069	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑈 × {𝑍}) ⊆ (𝑈 × 𝑉) → (𝐾 “ (𝑈 × {𝑍})) ⊆ (𝐾 “ (𝑈 × 𝑉)))
201	198, 199, 200	3syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐾 “ (𝑈 × {𝑍})) ⊆ (𝐾 “ (𝑈 × 𝑉)))
202	201, 124	sstrd 3946	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐾 “ (𝑈 × {𝑍})) ⊆ (^◡𝐹 “ 𝑀))
203	197, 202	eqsstrrid 3975	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ran (𝐾 ↾ (𝑈 × {𝑍})) ⊆ (^◡𝐹 “ 𝑀))
204		cnrest2 23242	. . . . . . . . . . . . . . 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 5669	. . . . . . . . . . . . . . 15 ⊢ ((𝑋 ∈ 𝑈 ∧ 𝑍 ∈ {𝑍}) → ⟨𝑋, 𝑍⟩ ∈ (𝑈 × {𝑍}))
208	21, 172, 207	syl2anc 585	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ⟨𝑋, 𝑍⟩ ∈ (𝑈 × {𝑍}))
209	185	snssd 4767	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → {𝑍} ⊆ (0[,]1))
210		xpss12 5647	. . . . . . . . . . . . . . . 16 ⊢ ((𝑈 ⊆ (0[,]1) ∧ {𝑍} ⊆ (0[,]1)) → (𝑈 × {𝑍}) ⊆ ((0[,]1) × (0[,]1)))
211	20, 209, 210	syl2anc 585	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑈 × {𝑍}) ⊆ ((0[,]1) × (0[,]1)))
212	4	restuni 23118	. . . . . . . . . . . . . . 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 2839	. . . . . . . . . . . . 13 ⊢ (𝜑 → ⟨𝑋, 𝑍⟩ ∈ ∪ ((II ×_t II) ↾_t (𝑈 × {𝑍})))
215		df-ov 7371	. . . . . . . . . . . . . . 15 ⊢ (𝑋(𝐾 ↾ (𝑈 × {𝑍}))𝑍) = ((𝐾 ↾ (𝑈 × {𝑍}))‘⟨𝑋, 𝑍⟩)
216		ovres 7534	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑋 ∈ 𝑈 ∧ 𝑍 ∈ {𝑍}) → (𝑋(𝐾 ↾ (𝑈 × {𝑍}))𝑍) = (𝑋𝐾𝑍))
217	21, 172, 216	syl2anc 585	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑋(𝐾 ↾ (𝑈 × {𝑍}))𝑍) = (𝑋𝐾𝑍))
218		snidg 4619	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑋 ∈ 𝑈 → 𝑋 ∈ {𝑋})
219	21, 218	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑋 ∈ {𝑋})
220		ovres 7534	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑋 ∈ {𝑋} ∧ 𝑍 ∈ 𝑉) → (𝑋(𝐾 ↾ ({𝑋} × 𝑉))𝑍) = (𝑋𝐾𝑍))
221	219, 160, 220	syl2anc 585	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑋(𝐾 ↾ ({𝑋} × 𝑉))𝑍) = (𝑋𝐾𝑍))
222	217, 221	eqtr4d 2775	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑋(𝐾 ↾ (𝑈 × {𝑍}))𝑍) = (𝑋(𝐾 ↾ ({𝑋} × 𝑉))𝑍))
223	215, 222	eqtr3id 2786	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐾 ↾ (𝑈 × {𝑍}))‘⟨𝑋, 𝑍⟩) = (𝑋(𝐾 ↾ ({𝑋} × 𝑉))𝑍))
224		eqid 2737	. . . . . . . . . . . . . . . . 17 ⊢ ∪ ((II ×_t II) ↾_t ({𝑋} × 𝑉)) = ∪ ((II ×_t II) ↾_t ({𝑋} × 𝑉))
225		snex 5385	. . . . . . . . . . . . . . . . . . . 20 ⊢ {𝑋} ∈ V
226	225	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → {𝑋} ∈ V)
227		txrest 23587	. . . . . . . . . . . . . . . . . . 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 23127	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((II ∈ (TopOn‘(0[,]1)) ∧ 𝑋 ∈ (0[,]1)) → (II ↾_t {𝑋}) = 𝒫 {𝑋})
230	63, 22, 229	sylancr 588	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (II ↾_t {𝑋}) = 𝒫 {𝑋})
231		pwsn 4858	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝒫 {𝑋} = {∅, {𝑋}}
232		indisconn 23374	. . . . . . . . . . . . . . . . . . . . 21 ⊢ {∅, {𝑋}} ∈ Conn
233	231, 232	eqeltri 2833	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝒫 {𝑋} ∈ Conn
234	230, 233	eqeltrdi 2845	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (II ↾_t {𝑋}) ∈ Conn)
235		txconn 23645	. . . . . . . . . . . . . . . . . . 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 2837	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((II ×_t II) ↾_t ({𝑋} × 𝑉)) ∈ Conn)
238	1, 6, 7, 8, 9, 10, 11	cvmlift2lem6 35521	. . . . . . . . . . . . . . . . . . . . 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 5652	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑉 ⊆ (0[,]1) → ({𝑋} × 𝑉) ⊆ ({𝑋} × (0[,]1)))
241	23, 25, 240	3syl 18	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ({𝑋} × 𝑉) ⊆ ({𝑋} × (0[,]1)))
242	22	snssd 4767	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → {𝑋} ⊆ (0[,]1))
243		xpss1 5651	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ({𝑋} ⊆ (0[,]1) → ({𝑋} × (0[,]1)) ⊆ ((0[,]1) × (0[,]1)))
244	242, 243	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ({𝑋} × (0[,]1)) ⊆ ((0[,]1) × (0[,]1)))
245	4	restuni 23118	. . . . . . . . . . . . . . . . . . . . . 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 3972	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ({𝑋} × 𝑉) ⊆ ∪ ((II ×_t II) ↾_t ({𝑋} × (0[,]1))))
248		eqid 2737	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ∪ ((II ×_t II) ↾_t ({𝑋} × (0[,]1))) = ∪ ((II ×_t II) ↾_t ({𝑋} × (0[,]1)))
249	248	cnrest 23241	. . . . . . . . . . . . . . . . . . . 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 5975	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝐾 ↾ ({𝑋} × (0[,]1))) ↾ ({𝑋} × 𝑉)) = (𝐾 ↾ ({𝑋} × 𝑉)))
252	225, 93	xpex 7708	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ({𝑋} × (0[,]1)) ∈ V
253	252	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ({𝑋} × (0[,]1)) ∈ V)
254		restabs 23121	. . . . . . . . . . . . . . . . . . . . 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 7383	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((((II ×_t II) ↾_t ({𝑋} × (0[,]1))) ↾_t ({𝑋} × 𝑉)) Cn 𝐶) = (((II ×_t II) ↾_t ({𝑋} × 𝑉)) Cn 𝐶))
257	250, 251, 256	3eltr3d 2851	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐾 ↾ ({𝑋} × 𝑉)) ∈ (((II ×_t II) ↾_t ({𝑋} × 𝑉)) Cn 𝐶))
258		df-ima 5645	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐾 “ ({𝑋} × 𝑉)) = ran (𝐾 ↾ ({𝑋} × 𝑉))
259	21	snssd 4767	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → {𝑋} ⊆ 𝑈)
260		xpss1 5651	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ({𝑋} ⊆ 𝑈 → ({𝑋} × 𝑉) ⊆ (𝑈 × 𝑉))
261		imass2 6069	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (({𝑋} × 𝑉) ⊆ (𝑈 × 𝑉) → (𝐾 “ ({𝑋} × 𝑉)) ⊆ (𝐾 “ (𝑈 × 𝑉)))
262	259, 260, 261	3syl 18	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝐾 “ ({𝑋} × 𝑉)) ⊆ (𝐾 “ (𝑈 × 𝑉)))
263	262, 124	sstrd 3946	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐾 “ ({𝑋} × 𝑉)) ⊆ (^◡𝐹 “ 𝑀))
264	258, 263	eqsstrrid 3975	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ran (𝐾 ↾ ({𝑋} × 𝑉)) ⊆ (^◡𝐹 “ 𝑀))
265		cnrest2 23242	. . . . . . . . . . . . . . . . . . 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 5669	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑋 ∈ {𝑋} ∧ 𝑌 ∈ 𝑉) → ⟨𝑋, 𝑌⟩ ∈ ({𝑋} × 𝑉))
269	219, 27, 268	syl2anc 585	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ⟨𝑋, 𝑌⟩ ∈ ({𝑋} × 𝑉))
270	259, 260	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ({𝑋} × 𝑉) ⊆ (𝑈 × 𝑉))
271	270, 50	sstrd 3946	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ({𝑋} × 𝑉) ⊆ ((0[,]1) × (0[,]1)))
272	4	restuni 23118	. . . . . . . . . . . . . . . . . . 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 2839	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ⟨𝑋, 𝑌⟩ ∈ ∪ ((II ×_t II) ↾_t ({𝑋} × 𝑉)))
275		df-ov 7371	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑋(𝐾 ↾ ({𝑋} × 𝑉))𝑌) = ((𝐾 ↾ ({𝑋} × 𝑉))‘⟨𝑋, 𝑌⟩)
276		ovres 7534	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑋 ∈ {𝑋} ∧ 𝑌 ∈ 𝑉) → (𝑋(𝐾 ↾ ({𝑋} × 𝑉))𝑌) = (𝑋𝐾𝑌))
277	219, 27, 276	syl2anc 585	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑋(𝐾 ↾ ({𝑋} × 𝑉))𝑌) = (𝑋𝐾𝑌))
278	275, 277	eqtr3id 2786	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝐾 ↾ ({𝑋} × 𝑉))‘⟨𝑋, 𝑌⟩) = (𝑋𝐾𝑌))
279	45	simprd 495	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑋𝐾𝑌) ∈ 𝑊)
280	278, 279	eqeltrd 2837	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝐾 ↾ ({𝑋} × 𝑉))‘⟨𝑋, 𝑌⟩) ∈ 𝑊)
281	224, 237, 267, 155, 158, 274, 280	conncn 23382	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐾 ↾ ({𝑋} × 𝑉)):∪ ((II ×_t II) ↾_t ({𝑋} × 𝑉))⟶𝑊)
282	273	feq2d 6654	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐾 ↾ ({𝑋} × 𝑉)):({𝑋} × 𝑉)⟶𝑊 ↔ (𝐾 ↾ ({𝑋} × 𝑉)):∪ ((II ×_t II) ↾_t ({𝑋} × 𝑉))⟶𝑊))
283	281, 282	mpbird 257	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐾 ↾ ({𝑋} × 𝑉)):({𝑋} × 𝑉)⟶𝑊)
284	283, 219, 160	fovcdmd 7540	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑋(𝐾 ↾ ({𝑋} × 𝑉))𝑍) ∈ 𝑊)
285	223, 284	eqeltrd 2837	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐾 ↾ (𝑈 × {𝑍}))‘⟨𝑋, 𝑍⟩) ∈ 𝑊)
286	178, 194, 206, 155, 158, 214, 285	conncn 23382	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐾 ↾ (𝑈 × {𝑍})):∪ ((II ×_t II) ↾_t (𝑈 × {𝑍}))⟶𝑊)
287	213	feq2d 6654	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐾 ↾ (𝑈 × {𝑍})):(𝑈 × {𝑍})⟶𝑊 ↔ (𝐾 ↾ (𝑈 × {𝑍})):∪ ((II ×_t II) ↾_t (𝑈 × {𝑍}))⟶𝑊))
288	286, 287	mpbird 257	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐾 ↾ (𝑈 × {𝑍})):(𝑈 × {𝑍})⟶𝑊)
289	288	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → (𝐾 ↾ (𝑈 × {𝑍})):(𝑈 × {𝑍})⟶𝑊)
290	289, 106, 173	fovcdmd 7540	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → (𝑚(𝐾 ↾ (𝑈 × {𝑍}))𝑍) ∈ 𝑊)
291	177, 290	eqeltrd 2837	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → ((𝐾 ↾ ({𝑚} × 𝑉))‘⟨𝑚, 𝑍⟩) ∈ 𝑊)
292	56, 76, 139, 156, 159, 167, 291	conncn 23382	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → (𝐾 ↾ ({𝑚} × 𝑉)):∪ ((II ×_t II) ↾_t ({𝑚} × 𝑉))⟶𝑊)
293	166	feq2d 6654	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → ((𝐾 ↾ ({𝑚} × 𝑉)):({𝑚} × 𝑉)⟶𝑊 ↔ (𝐾 ↾ ({𝑚} × 𝑉)):∪ ((II ×_t II) ↾_t ({𝑚} × 𝑉))⟶𝑊))
294	292, 293	mpbird 257	. . . . . 6 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → (𝐾 ↾ ({𝑚} × 𝑉)):({𝑚} × 𝑉)⟶𝑊)
295	294, 52, 53	fovcdmd 7540	. . . . 5 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → (𝑚(𝐾 ↾ ({𝑚} × 𝑉))𝑛) ∈ 𝑊)
296	55, 295	eqeltrrd 2838	. . . 4 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → (𝑚𝐾𝑛) ∈ 𝑊)
297	296	ralrimivva 3181	. . 3 ⊢ (𝜑 → ∀𝑚 ∈ 𝑈 ∀𝑛 ∈ 𝑉 (𝑚𝐾𝑛) ∈ 𝑊)
298		funimassov 7545	. . . 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 35516	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 3052 {crab 3401 Vcvv 3442 ∖ cdif 3900 ∩ cin 3902 ⊆ wss 3903 ∅c0 4287 𝒫 cpw 4556 {csn 4582 {cpr 4584 ⟨cop 4588 ∪ cuni 4865 ↦ cmpt 5181 × cxp 5630 ^◡ccnv 5631 dom cdm 5632 ran crn 5633 ↾ cres 5634 “ cima 5635 ∘ ccom 5636 Fun wfun 6494 ⟶wf 6496 ‘cfv 6500 ℩crio 7324 (class class class)co 7368 ∈ cmpo 7370 0cc0 11038 1c1 11039 [,]cicc 13276 ↾_t crest 17352 Topctop 22849 TopOnctopon 22866 Clsdccld 22972 Cn ccn 23180 Conncconn 23367 ×_t ctx 23516 Homeochmeo 23709 IIcii 24836 CovMap ccvm 35468

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 2709 ax-rep 5226 ax-sep 5243 ax-nul 5253 ax-pow 5312 ax-pr 5379 ax-un 7690 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 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3063 df-rmo 3352 df-reu 3353 df-rab 3402 df-v 3444 df-sbc 3743 df-csb 3852 df-dif 3906 df-un 3908 df-in 3910 df-ss 3920 df-pss 3923 df-nul 4288 df-if 4482 df-pw 4558 df-sn 4583 df-pr 4585 df-tp 4587 df-op 4589 df-uni 4866 df-int 4905 df-iun 4950 df-iin 4951 df-br 5101 df-opab 5163 df-mpt 5182 df-tr 5208 df-id 5527 df-eprel 5532 df-po 5540 df-so 5541 df-fr 5585 df-se 5586 df-we 5587 df-xp 5638 df-rel 5639 df-cnv 5640 df-co 5641 df-dm 5642 df-rn 5643 df-res 5644 df-ima 5645 df-pred 6267 df-ord 6328 df-on 6329 df-lim 6330 df-suc 6331 df-iota 6456 df-fun 6502 df-fn 6503 df-f 6504 df-f1 6505 df-fo 6506 df-f1o 6507 df-fv 6508 df-isom 6509 df-riota 7325 df-ov 7371 df-oprab 7372 df-mpo 7373 df-of 7632 df-om 7819 df-1st 7943 df-2nd 7944 df-supp 8113 df-frecs 8233 df-wrecs 8264 df-recs 8313 df-rdg 8351 df-1o 8407 df-2o 8408 df-er 8645 df-ec 8647 df-map 8777 df-ixp 8848 df-en 8896 df-dom 8897 df-sdom 8898 df-fin 8899 df-fsupp 9277 df-fi 9326 df-sup 9357 df-inf 9358 df-oi 9427 df-card 9863 df-pnf 11180 df-mnf 11181 df-xr 11182 df-ltxr 11183 df-le 11184 df-sub 11378 df-neg 11379 df-div 11807 df-nn 12158 df-2 12220 df-3 12221 df-4 12222 df-5 12223 df-6 12224 df-7 12225 df-8 12226 df-9 12227 df-n0 12414 df-z 12501 df-dec 12620 df-uz 12764 df-q 12874 df-rp 12918 df-xneg 13038 df-xadd 13039 df-xmul 13040 df-ioo 13277 df-ico 13279 df-icc 13280 df-fz 13436 df-fzo 13583 df-fl 13724 df-seq 13937 df-exp 13997 df-hash 14266 df-cj 15034 df-re 15035 df-im 15036 df-sqrt 15170 df-abs 15171 df-clim 15423 df-sum 15622 df-struct 17086 df-sets 17103 df-slot 17121 df-ndx 17133 df-base 17149 df-ress 17170 df-plusg 17202 df-mulr 17203 df-starv 17204 df-sca 17205 df-vsca 17206 df-ip 17207 df-tset 17208 df-ple 17209 df-ds 17211 df-unif 17212 df-hom 17213 df-cco 17214 df-rest 17354 df-topn 17355 df-0g 17373 df-gsum 17374 df-topgen 17375 df-pt 17376 df-prds 17379 df-xrs 17435 df-qtop 17440 df-imas 17441 df-xps 17443 df-mre 17517 df-mrc 17518 df-acs 17520 df-mgm 18577 df-sgrp 18656 df-mnd 18672 df-submnd 18721 df-mulg 19010 df-cntz 19258 df-cmn 19723 df-psmet 21313 df-xmet 21314 df-met 21315 df-bl 21316 df-mopn 21317 df-cnfld 21322 df-top 22850 df-topon 22867 df-topsp 22889 df-bases 22902 df-cld 22975 df-ntr 22976 df-cls 22977 df-nei 23054 df-cn 23183 df-cnp 23184 df-cmp 23343 df-conn 23368 df-lly 23422 df-nlly 23423 df-tx 23518 df-hmeo 23711 df-xms 24276 df-ms 24277 df-tms 24278 df-ii 24838 df-cncf 24839 df-htpy 24937 df-phtpy 24938 df-phtpc 24959 df-pconn 35434 df-sconn 35435 df-cvm 35469

This theorem is referenced by: cvmlift2lem10 35525

W3C validator