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 31892

Description: Lemma for cvmlift2 31897. (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 23091	. . 3 ⊢ II ∈ Top
3		iiuni 23092	. . 3 ⊢ (0[,]1) = ∪ II
4	2, 2, 3, 3	txunii 21805	. 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 31888	. 2 ⊢ (𝜑 → 𝐾:((0[,]1) × (0[,]1))⟶𝐵)
13	1, 6, 7, 8, 9, 10, 11	cvmlift2lem7 31890	. . 3 ⊢ (𝜑 → (𝐹 ∘ 𝐾) = 𝐺)
14	13, 7	eqeltrd 2859	. 2 ⊢ (𝜑 → (𝐹 ∘ 𝐾) ∈ ((II ×_t II) Cn 𝐽))
15	2, 2	txtopi 21802	. . 3 ⊢ (II ×_t II) ∈ Top
16	15	a1i 11	. 2 ⊢ (𝜑 → (II ×_t II) ∈ Top)
17		cvmlift2lem9.3	. . . . 5 ⊢ (𝜑 → 𝑈 ∈ II)
18		elssuni 4702	. . . . . 6 ⊢ (𝑈 ∈ II → 𝑈 ⊆ ∪ II)
19	18, 3	syl6sseqr 3871	. . . . 5 ⊢ (𝑈 ∈ II → 𝑈 ⊆ (0[,]1))
20	17, 19	syl 17	. . . 4 ⊢ (𝜑 → 𝑈 ⊆ (0[,]1))
21		cvmlift2lem9.7	. . . 4 ⊢ (𝜑 → 𝑋 ∈ 𝑈)
22	20, 21	sseldd 3822	. . 3 ⊢ (𝜑 → 𝑋 ∈ (0[,]1))
23		cvmlift2lem9.4	. . . . 5 ⊢ (𝜑 → 𝑉 ∈ II)
24		elssuni 4702	. . . . . 6 ⊢ (𝑉 ∈ II → 𝑉 ⊆ ∪ II)
25	24, 3	syl6sseqr 3871	. . . . 5 ⊢ (𝑉 ∈ II → 𝑉 ⊆ (0[,]1))
26	23, 25	syl 17	. . . 4 ⊢ (𝜑 → 𝑉 ⊆ (0[,]1))
27		cvmlift2lem9.8	. . . 4 ⊢ (𝜑 → 𝑌 ∈ 𝑉)
28	26, 27	sseldd 3822	. . 3 ⊢ (𝜑 → 𝑌 ∈ (0[,]1))
29		opelxpi 5392	. . 3 ⊢ ((𝑋 ∈ (0[,]1) ∧ 𝑌 ∈ (0[,]1)) → ⟨𝑋, 𝑌⟩ ∈ ((0[,]1) × (0[,]1)))
30	22, 28, 29	syl2anc 579	. 2 ⊢ (𝜑 → ⟨𝑋, 𝑌⟩ ∈ ((0[,]1) × (0[,]1)))
31		cvmlift2lem9.2	. 2 ⊢ (𝜑 → 𝑇 ∈ (𝑆‘𝑀))
32	12, 22, 28	fovrnd 7083	. . . 4 ⊢ (𝜑 → (𝑋𝐾𝑌) ∈ 𝐵)
33		fvco3 6535	. . . . . . . 8 ⊢ ((𝐾:((0[,]1) × (0[,]1))⟶𝐵 ∧ ⟨𝑋, 𝑌⟩ ∈ ((0[,]1) × (0[,]1))) → ((𝐹 ∘ 𝐾)‘⟨𝑋, 𝑌⟩) = (𝐹‘(𝐾‘⟨𝑋, 𝑌⟩)))
34	12, 30, 33	syl2anc 579	. . . . . . 7 ⊢ (𝜑 → ((𝐹 ∘ 𝐾)‘⟨𝑋, 𝑌⟩) = (𝐹‘(𝐾‘⟨𝑋, 𝑌⟩)))
35	13	fveq1d 6448	. . . . . . 7 ⊢ (𝜑 → ((𝐹 ∘ 𝐾)‘⟨𝑋, 𝑌⟩) = (𝐺‘⟨𝑋, 𝑌⟩))
36	34, 35	eqtr3d 2816	. . . . . 6 ⊢ (𝜑 → (𝐹‘(𝐾‘⟨𝑋, 𝑌⟩)) = (𝐺‘⟨𝑋, 𝑌⟩))
37		df-ov 6925	. . . . . . 7 ⊢ (𝑋𝐾𝑌) = (𝐾‘⟨𝑋, 𝑌⟩)
38	37	fveq2i 6449	. . . . . 6 ⊢ (𝐹‘(𝑋𝐾𝑌)) = (𝐹‘(𝐾‘⟨𝑋, 𝑌⟩))
39		df-ov 6925	. . . . . 6 ⊢ (𝑋𝐺𝑌) = (𝐺‘⟨𝑋, 𝑌⟩)
40	36, 38, 39	3eqtr4g 2839	. . . . 5 ⊢ (𝜑 → (𝐹‘(𝑋𝐾𝑌)) = (𝑋𝐺𝑌))
41		cvmlift2lem9.1	. . . . 5 ⊢ (𝜑 → (𝑋𝐺𝑌) ∈ 𝑀)
42	40, 41	eqeltrd 2859	. . . 4 ⊢ (𝜑 → (𝐹‘(𝑋𝐾𝑌)) ∈ 𝑀)
43		cvmlift2lem9.w	. . . . 5 ⊢ 𝑊 = (℩𝑏 ∈ 𝑇 (𝑋𝐾𝑌) ∈ 𝑏)
44	5, 1, 43	cvmsiota 31858	. . . 4 ⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ (𝑇 ∈ (𝑆‘𝑀) ∧ (𝑋𝐾𝑌) ∈ 𝐵 ∧ (𝐹‘(𝑋𝐾𝑌)) ∈ 𝑀)) → (𝑊 ∈ 𝑇 ∧ (𝑋𝐾𝑌) ∈ 𝑊))
45	6, 31, 32, 42, 44	syl13anc 1440	. . 3 ⊢ (𝜑 → (𝑊 ∈ 𝑇 ∧ (𝑋𝐾𝑌) ∈ 𝑊))
46	37	eleq1i 2850	. . . 4 ⊢ ((𝑋𝐾𝑌) ∈ 𝑊 ↔ (𝐾‘⟨𝑋, 𝑌⟩) ∈ 𝑊)
47	46	anbi2i 616	. . 3 ⊢ ((𝑊 ∈ 𝑇 ∧ (𝑋𝐾𝑌) ∈ 𝑊) ↔ (𝑊 ∈ 𝑇 ∧ (𝐾‘⟨𝑋, 𝑌⟩) ∈ 𝑊))
48	45, 47	sylib 210	. 2 ⊢ (𝜑 → (𝑊 ∈ 𝑇 ∧ (𝐾‘⟨𝑋, 𝑌⟩) ∈ 𝑊))
49		xpss12 5370	. . 3 ⊢ ((𝑈 ⊆ (0[,]1) ∧ 𝑉 ⊆ (0[,]1)) → (𝑈 × 𝑉) ⊆ ((0[,]1) × (0[,]1)))
50	20, 26, 49	syl2anc 579	. 2 ⊢ (𝜑 → (𝑈 × 𝑉) ⊆ ((0[,]1) × (0[,]1)))
51		snidg 4428	. . . . . . 7 ⊢ (𝑚 ∈ 𝑈 → 𝑚 ∈ {𝑚})
52	51	ad2antrl 718	. . . . . 6 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → 𝑚 ∈ {𝑚})
53		simprr 763	. . . . . 6 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → 𝑛 ∈ 𝑉)
54		ovres 7077	. . . . . 6 ⊢ ((𝑚 ∈ {𝑚} ∧ 𝑛 ∈ 𝑉) → (𝑚(𝐾 ↾ ({𝑚} × 𝑉))𝑛) = (𝑚𝐾𝑛))
55	52, 53, 54	syl2anc 579	. . . . 5 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → (𝑚(𝐾 ↾ ({𝑚} × 𝑉))𝑛) = (𝑚𝐾𝑛))
56		eqid 2778	. . . . . . . 8 ⊢ ∪ ((II ×_t II) ↾_t ({𝑚} × 𝑉)) = ∪ ((II ×_t II) ↾_t ({𝑚} × 𝑉))
57	2	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → II ∈ Top)
58		snex 5140	. . . . . . . . . . 11 ⊢ {𝑚} ∈ V
59	58	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → {𝑚} ∈ V)
60	23	adantr 474	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → 𝑉 ∈ II)
61		txrest 21843	. . . . . . . . . 10 ⊢ (((II ∈ Top ∧ II ∈ Top) ∧ ({𝑚} ∈ V ∧ 𝑉 ∈ II)) → ((II ×_t II) ↾_t ({𝑚} × 𝑉)) = ((II ↾_t {𝑚}) ×_t (II ↾_t 𝑉)))
62	57, 57, 59, 60, 61	syl22anc 829	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → ((II ×_t II) ↾_t ({𝑚} × 𝑉)) = ((II ↾_t {𝑚}) ×_t (II ↾_t 𝑉)))
63		iitopon 23090	. . . . . . . . . . . 12 ⊢ II ∈ (TopOn‘(0[,]1))
64	20	sselda 3821	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑈) → 𝑚 ∈ (0[,]1))
65	64	adantrr 707	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → 𝑚 ∈ (0[,]1))
66		restsn2 21383	. . . . . . . . . . . 12 ⊢ ((II ∈ (TopOn‘(0[,]1)) ∧ 𝑚 ∈ (0[,]1)) → (II ↾_t {𝑚}) = 𝒫 {𝑚})
67	63, 65, 66	sylancr 581	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → (II ↾_t {𝑚}) = 𝒫 {𝑚})
68		pwsn 4663	. . . . . . . . . . . 12 ⊢ 𝒫 {𝑚} = {∅, {𝑚}}
69		indisconn 21630	. . . . . . . . . . . 12 ⊢ {∅, {𝑚}} ∈ Conn
70	68, 69	eqeltri 2855	. . . . . . . . . . 11 ⊢ 𝒫 {𝑚} ∈ Conn
71	67, 70	syl6eqel 2867	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → (II ↾_t {𝑚}) ∈ Conn)
72		cvmlift2lem9.6	. . . . . . . . . . 11 ⊢ (𝜑 → (II ↾_t 𝑉) ∈ Conn)
73	72	adantr 474	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → (II ↾_t 𝑉) ∈ Conn)
74		txconn 21901	. . . . . . . . . 10 ⊢ (((II ↾_t {𝑚}) ∈ Conn ∧ (II ↾_t 𝑉) ∈ Conn) → ((II ↾_t {𝑚}) ×_t (II ↾_t 𝑉)) ∈ Conn)
75	71, 73, 74	syl2anc 579	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → ((II ↾_t {𝑚}) ×_t (II ↾_t 𝑉)) ∈ Conn)
76	62, 75	eqeltrd 2859	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → ((II ×_t II) ↾_t ({𝑚} × 𝑉)) ∈ Conn)
77	1, 6, 7, 8, 9, 10, 11	cvmlift2lem6 31889	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑚 ∈ (0[,]1)) → (𝐾 ↾ ({𝑚} × (0[,]1))) ∈ (((II ×_t II) ↾_t ({𝑚} × (0[,]1))) Cn 𝐶))
78	65, 77	syldan 585	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → (𝐾 ↾ ({𝑚} × (0[,]1))) ∈ (((II ×_t II) ↾_t ({𝑚} × (0[,]1))) Cn 𝐶))
79	26	adantr 474	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → 𝑉 ⊆ (0[,]1))
80		xpss2 5375	. . . . . . . . . . . . 13 ⊢ (𝑉 ⊆ (0[,]1) → ({𝑚} × 𝑉) ⊆ ({𝑚} × (0[,]1)))
81	79, 80	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → ({𝑚} × 𝑉) ⊆ ({𝑚} × (0[,]1)))
82	65	snssd 4571	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → {𝑚} ⊆ (0[,]1))
83		xpss1 5374	. . . . . . . . . . . . . 14 ⊢ ({𝑚} ⊆ (0[,]1) → ({𝑚} × (0[,]1)) ⊆ ((0[,]1) × (0[,]1)))
84	82, 83	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → ({𝑚} × (0[,]1)) ⊆ ((0[,]1) × (0[,]1)))
85	4	restuni 21374	. . . . . . . . . . . . 13 ⊢ (((II ×_t II) ∈ Top ∧ ({𝑚} × (0[,]1)) ⊆ ((0[,]1) × (0[,]1))) → ({𝑚} × (0[,]1)) = ∪ ((II ×_t II) ↾_t ({𝑚} × (0[,]1))))
86	15, 84, 85	sylancr 581	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → ({𝑚} × (0[,]1)) = ∪ ((II ×_t II) ↾_t ({𝑚} × (0[,]1))))
87	81, 86	sseqtrd 3860	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → ({𝑚} × 𝑉) ⊆ ∪ ((II ×_t II) ↾_t ({𝑚} × (0[,]1))))
88		eqid 2778	. . . . . . . . . . . 12 ⊢ ∪ ((II ×_t II) ↾_t ({𝑚} × (0[,]1))) = ∪ ((II ×_t II) ↾_t ({𝑚} × (0[,]1)))
89	88	cnrest 21497	. . . . . . . . . . 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 579	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → ((𝐾 ↾ ({𝑚} × (0[,]1))) ↾ ({𝑚} × 𝑉)) ∈ ((((II ×_t II) ↾_t ({𝑚} × (0[,]1))) ↾_t ({𝑚} × 𝑉)) Cn 𝐶))
91	81	resabs1d 5677	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → ((𝐾 ↾ ({𝑚} × (0[,]1))) ↾ ({𝑚} × 𝑉)) = (𝐾 ↾ ({𝑚} × 𝑉)))
92	15	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → (II ×_t II) ∈ Top)
93		ovex 6954	. . . . . . . . . . . . . 14 ⊢ (0[,]1) ∈ V
94	58, 93	xpex 7240	. . . . . . . . . . . . 13 ⊢ ({𝑚} × (0[,]1)) ∈ V
95	94	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → ({𝑚} × (0[,]1)) ∈ V)
96		restabs 21377	. . . . . . . . . . . 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 1439	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → (((II ×_t II) ↾_t ({𝑚} × (0[,]1))) ↾_t ({𝑚} × 𝑉)) = ((II ×_t II) ↾_t ({𝑚} × 𝑉)))
98	97	oveq1d 6937	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → ((((II ×_t II) ↾_t ({𝑚} × (0[,]1))) ↾_t ({𝑚} × 𝑉)) Cn 𝐶) = (((II ×_t II) ↾_t ({𝑚} × 𝑉)) Cn 𝐶))
99	90, 91, 98	3eltr3d 2873	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → (𝐾 ↾ ({𝑚} × 𝑉)) ∈ (((II ×_t II) ↾_t ({𝑚} × 𝑉)) Cn 𝐶))
100		cvmtop1 31841	. . . . . . . . . . . . 13 ⊢ (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐶 ∈ Top)
101	6, 100	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐶 ∈ Top)
102	101	adantr 474	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → 𝐶 ∈ Top)
103	1	toptopon 21129	. . . . . . . . . . 11 ⊢ (𝐶 ∈ Top ↔ 𝐶 ∈ (TopOn‘𝐵))
104	102, 103	sylib 210	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → 𝐶 ∈ (TopOn‘𝐵))
105		df-ima 5368	. . . . . . . . . . 11 ⊢ (𝐾 “ ({𝑚} × 𝑉)) = ran (𝐾 ↾ ({𝑚} × 𝑉))
106		simprl 761	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → 𝑚 ∈ 𝑈)
107	106	snssd 4571	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → {𝑚} ⊆ 𝑈)
108		xpss1 5374	. . . . . . . . . . . . 13 ⊢ ({𝑚} ⊆ 𝑈 → ({𝑚} × 𝑉) ⊆ (𝑈 × 𝑉))
109		imass2 5755	. . . . . . . . . . . . 13 ⊢ (({𝑚} × 𝑉) ⊆ (𝑈 × 𝑉) → (𝐾 “ ({𝑚} × 𝑉)) ⊆ (𝐾 “ (𝑈 × 𝑉)))
110	107, 108, 109	3syl 18	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → (𝐾 “ ({𝑚} × 𝑉)) ⊆ (𝐾 “ (𝑈 × 𝑉)))
111		cvmlift2lem9.9	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑈 × 𝑉) ⊆ (^◡𝐺 “ 𝑀))
112		imaco 5894	. . . . . . . . . . . . . . . 16 ⊢ ((^◡𝐾 ∘ ^◡𝐹) “ 𝑀) = (^◡𝐾 “ (^◡𝐹 “ 𝑀))
113		cnvco 5553	. . . . . . . . . . . . . . . . . 18 ⊢ ^◡(𝐹 ∘ 𝐾) = (^◡𝐾 ∘ ^◡𝐹)
114	13	cnveqd 5543	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ^◡(𝐹 ∘ 𝐾) = ^◡𝐺)
115	113, 114	syl5eqr 2828	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (^◡𝐾 ∘ ^◡𝐹) = ^◡𝐺)
116	115	imaeq1d 5719	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((^◡𝐾 ∘ ^◡𝐹) “ 𝑀) = (^◡𝐺 “ 𝑀))
117	112, 116	syl5eqr 2828	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (^◡𝐾 “ (^◡𝐹 “ 𝑀)) = (^◡𝐺 “ 𝑀))
118	111, 117	sseqtr4d 3861	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑈 × 𝑉) ⊆ (^◡𝐾 “ (^◡𝐹 “ 𝑀)))
119	12	ffund 6295	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → Fun 𝐾)
120	12	fdmd 6300	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → dom 𝐾 = ((0[,]1) × (0[,]1)))
121	50, 120	sseqtr4d 3861	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑈 × 𝑉) ⊆ dom 𝐾)
122		funimass3 6596	. . . . . . . . . . . . . . 15 ⊢ ((Fun 𝐾 ∧ (𝑈 × 𝑉) ⊆ dom 𝐾) → ((𝐾 “ (𝑈 × 𝑉)) ⊆ (^◡𝐹 “ 𝑀) ↔ (𝑈 × 𝑉) ⊆ (^◡𝐾 “ (^◡𝐹 “ 𝑀))))
123	119, 121, 122	syl2anc 579	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐾 “ (𝑈 × 𝑉)) ⊆ (^◡𝐹 “ 𝑀) ↔ (𝑈 × 𝑉) ⊆ (^◡𝐾 “ (^◡𝐹 “ 𝑀))))
124	118, 123	mpbird 249	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐾 “ (𝑈 × 𝑉)) ⊆ (^◡𝐹 “ 𝑀))
125	124	adantr 474	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → (𝐾 “ (𝑈 × 𝑉)) ⊆ (^◡𝐹 “ 𝑀))
126	110, 125	sstrd 3831	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → (𝐾 “ ({𝑚} × 𝑉)) ⊆ (^◡𝐹 “ 𝑀))
127	105, 126	syl5eqssr 3869	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → ran (𝐾 ↾ ({𝑚} × 𝑉)) ⊆ (^◡𝐹 “ 𝑀))
128		cnvimass 5739	. . . . . . . . . . . 12 ⊢ (^◡𝐹 “ 𝑀) ⊆ dom 𝐹
129		cvmcn 31843	. . . . . . . . . . . . . 14 ⊢ (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐹 ∈ (𝐶 Cn 𝐽))
130	6, 129	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐹 ∈ (𝐶 Cn 𝐽))
131		eqid 2778	. . . . . . . . . . . . . 14 ⊢ ∪ 𝐽 = ∪ 𝐽
132	1, 131	cnf 21458	. . . . . . . . . . . . 13 ⊢ (𝐹 ∈ (𝐶 Cn 𝐽) → 𝐹:𝐵⟶∪ 𝐽)
133		fdm 6299	. . . . . . . . . . . . 13 ⊢ (𝐹:𝐵⟶∪ 𝐽 → dom 𝐹 = 𝐵)
134	130, 132, 133	3syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → dom 𝐹 = 𝐵)
135	128, 134	syl5sseq 3872	. . . . . . . . . . 11 ⊢ (𝜑 → (^◡𝐹 “ 𝑀) ⊆ 𝐵)
136	135	adantr 474	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → (^◡𝐹 “ 𝑀) ⊆ 𝐵)
137		cnrest2 21498	. . . . . . . . . 10 ⊢ ((𝐶 ∈ (TopOn‘𝐵) ∧ ran (𝐾 ↾ ({𝑚} × 𝑉)) ⊆ (^◡𝐹 “ 𝑀) ∧ (^◡𝐹 “ 𝑀) ⊆ 𝐵) → ((𝐾 ↾ ({𝑚} × 𝑉)) ∈ (((II ×_t II) ↾_t ({𝑚} × 𝑉)) Cn 𝐶) ↔ (𝐾 ↾ ({𝑚} × 𝑉)) ∈ (((II ×_t II) ↾_t ({𝑚} × 𝑉)) Cn (𝐶 ↾_t (^◡𝐹 “ 𝑀)))))
138	104, 127, 136, 137	syl3anc 1439	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → ((𝐾 ↾ ({𝑚} × 𝑉)) ∈ (((II ×_t II) ↾_t ({𝑚} × 𝑉)) Cn 𝐶) ↔ (𝐾 ↾ ({𝑚} × 𝑉)) ∈ (((II ×_t II) ↾_t ({𝑚} × 𝑉)) Cn (𝐶 ↾_t (^◡𝐹 “ 𝑀)))))
139	99, 138	mpbid 224	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → (𝐾 ↾ ({𝑚} × 𝑉)) ∈ (((II ×_t II) ↾_t ({𝑚} × 𝑉)) Cn (𝐶 ↾_t (^◡𝐹 “ 𝑀))))
140	5	cvmsss 31848	. . . . . . . . . . . 12 ⊢ (𝑇 ∈ (𝑆‘𝑀) → 𝑇 ⊆ 𝐶)
141	31, 140	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑇 ⊆ 𝐶)
142	45	simpld 490	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑊 ∈ 𝑇)
143	141, 142	sseldd 3822	. . . . . . . . . 10 ⊢ (𝜑 → 𝑊 ∈ 𝐶)
144		elssuni 4702	. . . . . . . . . . . 12 ⊢ (𝑊 ∈ 𝑇 → 𝑊 ⊆ ∪ 𝑇)
145	142, 144	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑊 ⊆ ∪ 𝑇)
146	5	cvmsuni 31850	. . . . . . . . . . . 12 ⊢ (𝑇 ∈ (𝑆‘𝑀) → ∪ 𝑇 = (^◡𝐹 “ 𝑀))
147	31, 146	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → ∪ 𝑇 = (^◡𝐹 “ 𝑀))
148	145, 147	sseqtrd 3860	. . . . . . . . . 10 ⊢ (𝜑 → 𝑊 ⊆ (^◡𝐹 “ 𝑀))
149	5	cvmsrcl 31845	. . . . . . . . . . . . 13 ⊢ (𝑇 ∈ (𝑆‘𝑀) → 𝑀 ∈ 𝐽)
150	31, 149	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑀 ∈ 𝐽)
151		cnima 21477	. . . . . . . . . . . 12 ⊢ ((𝐹 ∈ (𝐶 Cn 𝐽) ∧ 𝑀 ∈ 𝐽) → (^◡𝐹 “ 𝑀) ∈ 𝐶)
152	130, 150, 151	syl2anc 579	. . . . . . . . . . 11 ⊢ (𝜑 → (^◡𝐹 “ 𝑀) ∈ 𝐶)
153		restopn2 21389	. . . . . . . . . . 11 ⊢ ((𝐶 ∈ Top ∧ (^◡𝐹 “ 𝑀) ∈ 𝐶) → (𝑊 ∈ (𝐶 ↾_t (^◡𝐹 “ 𝑀)) ↔ (𝑊 ∈ 𝐶 ∧ 𝑊 ⊆ (^◡𝐹 “ 𝑀))))
154	101, 152, 153	syl2anc 579	. . . . . . . . . 10 ⊢ (𝜑 → (𝑊 ∈ (𝐶 ↾_t (^◡𝐹 “ 𝑀)) ↔ (𝑊 ∈ 𝐶 ∧ 𝑊 ⊆ (^◡𝐹 “ 𝑀))))
155	143, 148, 154	mpbir2and 703	. . . . . . . . 9 ⊢ (𝜑 → 𝑊 ∈ (𝐶 ↾_t (^◡𝐹 “ 𝑀)))
156	155	adantr 474	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → 𝑊 ∈ (𝐶 ↾_t (^◡𝐹 “ 𝑀)))
157	5	cvmscld 31854	. . . . . . . . . 10 ⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑇 ∈ (𝑆‘𝑀) ∧ 𝑊 ∈ 𝑇) → 𝑊 ∈ (Clsd‘(𝐶 ↾_t (^◡𝐹 “ 𝑀))))
158	6, 31, 142, 157	syl3anc 1439	. . . . . . . . 9 ⊢ (𝜑 → 𝑊 ∈ (Clsd‘(𝐶 ↾_t (^◡𝐹 “ 𝑀))))
159	158	adantr 474	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → 𝑊 ∈ (Clsd‘(𝐶 ↾_t (^◡𝐹 “ 𝑀))))
160		cvmlift2lem9.10	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑍 ∈ 𝑉)
161	160	adantr 474	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → 𝑍 ∈ 𝑉)
162		opelxpi 5392	. . . . . . . . . 10 ⊢ ((𝑚 ∈ {𝑚} ∧ 𝑍 ∈ 𝑉) → ⟨𝑚, 𝑍⟩ ∈ ({𝑚} × 𝑉))
163	52, 161, 162	syl2anc 579	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → ⟨𝑚, 𝑍⟩ ∈ ({𝑚} × 𝑉))
164	81, 84	sstrd 3831	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → ({𝑚} × 𝑉) ⊆ ((0[,]1) × (0[,]1)))
165	4	restuni 21374	. . . . . . . . . 10 ⊢ (((II ×_t II) ∈ Top ∧ ({𝑚} × 𝑉) ⊆ ((0[,]1) × (0[,]1))) → ({𝑚} × 𝑉) = ∪ ((II ×_t II) ↾_t ({𝑚} × 𝑉)))
166	15, 164, 165	sylancr 581	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → ({𝑚} × 𝑉) = ∪ ((II ×_t II) ↾_t ({𝑚} × 𝑉)))
167	163, 166	eleqtrd 2861	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → ⟨𝑚, 𝑍⟩ ∈ ∪ ((II ×_t II) ↾_t ({𝑚} × 𝑉)))
168		df-ov 6925	. . . . . . . . . 10 ⊢ (𝑚(𝐾 ↾ ({𝑚} × 𝑉))𝑍) = ((𝐾 ↾ ({𝑚} × 𝑉))‘⟨𝑚, 𝑍⟩)
169		ovres 7077	. . . . . . . . . . . 12 ⊢ ((𝑚 ∈ {𝑚} ∧ 𝑍 ∈ 𝑉) → (𝑚(𝐾 ↾ ({𝑚} × 𝑉))𝑍) = (𝑚𝐾𝑍))
170	52, 161, 169	syl2anc 579	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → (𝑚(𝐾 ↾ ({𝑚} × 𝑉))𝑍) = (𝑚𝐾𝑍))
171		snidg 4428	. . . . . . . . . . . . . 14 ⊢ (𝑍 ∈ 𝑉 → 𝑍 ∈ {𝑍})
172	160, 171	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑍 ∈ {𝑍})
173	172	adantr 474	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → 𝑍 ∈ {𝑍})
174		ovres 7077	. . . . . . . . . . . 12 ⊢ ((𝑚 ∈ 𝑈 ∧ 𝑍 ∈ {𝑍}) → (𝑚(𝐾 ↾ (𝑈 × {𝑍}))𝑍) = (𝑚𝐾𝑍))
175	106, 173, 174	syl2anc 579	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → (𝑚(𝐾 ↾ (𝑈 × {𝑍}))𝑍) = (𝑚𝐾𝑍))
176	170, 175	eqtr4d 2817	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → (𝑚(𝐾 ↾ ({𝑚} × 𝑉))𝑍) = (𝑚(𝐾 ↾ (𝑈 × {𝑍}))𝑍))
177	168, 176	syl5eqr 2828	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → ((𝐾 ↾ ({𝑚} × 𝑉))‘⟨𝑚, 𝑍⟩) = (𝑚(𝐾 ↾ (𝑈 × {𝑍}))𝑍))
178		eqid 2778	. . . . . . . . . . . . 13 ⊢ ∪ ((II ×_t II) ↾_t (𝑈 × {𝑍})) = ∪ ((II ×_t II) ↾_t (𝑈 × {𝑍}))
179	2	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → II ∈ Top)
180		snex 5140	. . . . . . . . . . . . . . . 16 ⊢ {𝑍} ∈ V
181	180	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → {𝑍} ∈ V)
182		txrest 21843	. . . . . . . . . . . . . . 15 ⊢ (((II ∈ Top ∧ II ∈ Top) ∧ (𝑈 ∈ II ∧ {𝑍} ∈ V)) → ((II ×_t II) ↾_t (𝑈 × {𝑍})) = ((II ↾_t 𝑈) ×_t (II ↾_t {𝑍})))
183	179, 179, 17, 181, 182	syl22anc 829	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((II ×_t II) ↾_t (𝑈 × {𝑍})) = ((II ↾_t 𝑈) ×_t (II ↾_t {𝑍})))
184		cvmlift2lem9.5	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (II ↾_t 𝑈) ∈ Conn)
185	26, 160	sseldd 3822	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑍 ∈ (0[,]1))
186		restsn2 21383	. . . . . . . . . . . . . . . . 17 ⊢ ((II ∈ (TopOn‘(0[,]1)) ∧ 𝑍 ∈ (0[,]1)) → (II ↾_t {𝑍}) = 𝒫 {𝑍})
187	63, 185, 186	sylancr 581	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (II ↾_t {𝑍}) = 𝒫 {𝑍})
188		pwsn 4663	. . . . . . . . . . . . . . . . 17 ⊢ 𝒫 {𝑍} = {∅, {𝑍}}
189		indisconn 21630	. . . . . . . . . . . . . . . . 17 ⊢ {∅, {𝑍}} ∈ Conn
190	188, 189	eqeltri 2855	. . . . . . . . . . . . . . . 16 ⊢ 𝒫 {𝑍} ∈ Conn
191	187, 190	syl6eqel 2867	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (II ↾_t {𝑍}) ∈ Conn)
192		txconn 21901	. . . . . . . . . . . . . . 15 ⊢ (((II ↾_t 𝑈) ∈ Conn ∧ (II ↾_t {𝑍}) ∈ Conn) → ((II ↾_t 𝑈) ×_t (II ↾_t {𝑍})) ∈ Conn)
193	184, 191, 192	syl2anc 579	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((II ↾_t 𝑈) ×_t (II ↾_t {𝑍})) ∈ Conn)
194	183, 193	eqeltrd 2859	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((II ×_t II) ↾_t (𝑈 × {𝑍})) ∈ Conn)
195		cvmlift2lem9.11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐾 ↾ (𝑈 × {𝑍})) ∈ (((II ×_t II) ↾_t (𝑈 × {𝑍})) Cn 𝐶))
196	101, 103	sylib 210	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐶 ∈ (TopOn‘𝐵))
197		df-ima 5368	. . . . . . . . . . . . . . . 16 ⊢ (𝐾 “ (𝑈 × {𝑍})) = ran (𝐾 ↾ (𝑈 × {𝑍}))
198	160	snssd 4571	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → {𝑍} ⊆ 𝑉)
199		xpss2 5375	. . . . . . . . . . . . . . . . . 18 ⊢ ({𝑍} ⊆ 𝑉 → (𝑈 × {𝑍}) ⊆ (𝑈 × 𝑉))
200		imass2 5755	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑈 × {𝑍}) ⊆ (𝑈 × 𝑉) → (𝐾 “ (𝑈 × {𝑍})) ⊆ (𝐾 “ (𝑈 × 𝑉)))
201	198, 199, 200	3syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐾 “ (𝑈 × {𝑍})) ⊆ (𝐾 “ (𝑈 × 𝑉)))
202	201, 124	sstrd 3831	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐾 “ (𝑈 × {𝑍})) ⊆ (^◡𝐹 “ 𝑀))
203	197, 202	syl5eqssr 3869	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ran (𝐾 ↾ (𝑈 × {𝑍})) ⊆ (^◡𝐹 “ 𝑀))
204		cnrest2 21498	. . . . . . . . . . . . . . 15 ⊢ ((𝐶 ∈ (TopOn‘𝐵) ∧ ran (𝐾 ↾ (𝑈 × {𝑍})) ⊆ (^◡𝐹 “ 𝑀) ∧ (^◡𝐹 “ 𝑀) ⊆ 𝐵) → ((𝐾 ↾ (𝑈 × {𝑍})) ∈ (((II ×_t II) ↾_t (𝑈 × {𝑍})) Cn 𝐶) ↔ (𝐾 ↾ (𝑈 × {𝑍})) ∈ (((II ×_t II) ↾_t (𝑈 × {𝑍})) Cn (𝐶 ↾_t (^◡𝐹 “ 𝑀)))))
205	196, 203, 135, 204	syl3anc 1439	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐾 ↾ (𝑈 × {𝑍})) ∈ (((II ×_t II) ↾_t (𝑈 × {𝑍})) Cn 𝐶) ↔ (𝐾 ↾ (𝑈 × {𝑍})) ∈ (((II ×_t II) ↾_t (𝑈 × {𝑍})) Cn (𝐶 ↾_t (^◡𝐹 “ 𝑀)))))
206	195, 205	mpbid 224	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐾 ↾ (𝑈 × {𝑍})) ∈ (((II ×_t II) ↾_t (𝑈 × {𝑍})) Cn (𝐶 ↾_t (^◡𝐹 “ 𝑀))))
207		opelxpi 5392	. . . . . . . . . . . . . . 15 ⊢ ((𝑋 ∈ 𝑈 ∧ 𝑍 ∈ {𝑍}) → ⟨𝑋, 𝑍⟩ ∈ (𝑈 × {𝑍}))
208	21, 172, 207	syl2anc 579	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ⟨𝑋, 𝑍⟩ ∈ (𝑈 × {𝑍}))
209	185	snssd 4571	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → {𝑍} ⊆ (0[,]1))
210		xpss12 5370	. . . . . . . . . . . . . . . 16 ⊢ ((𝑈 ⊆ (0[,]1) ∧ {𝑍} ⊆ (0[,]1)) → (𝑈 × {𝑍}) ⊆ ((0[,]1) × (0[,]1)))
211	20, 209, 210	syl2anc 579	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑈 × {𝑍}) ⊆ ((0[,]1) × (0[,]1)))
212	4	restuni 21374	. . . . . . . . . . . . . . 15 ⊢ (((II ×_t II) ∈ Top ∧ (𝑈 × {𝑍}) ⊆ ((0[,]1) × (0[,]1))) → (𝑈 × {𝑍}) = ∪ ((II ×_t II) ↾_t (𝑈 × {𝑍})))
213	15, 211, 212	sylancr 581	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑈 × {𝑍}) = ∪ ((II ×_t II) ↾_t (𝑈 × {𝑍})))
214	208, 213	eleqtrd 2861	. . . . . . . . . . . . 13 ⊢ (𝜑 → ⟨𝑋, 𝑍⟩ ∈ ∪ ((II ×_t II) ↾_t (𝑈 × {𝑍})))
215		df-ov 6925	. . . . . . . . . . . . . . 15 ⊢ (𝑋(𝐾 ↾ (𝑈 × {𝑍}))𝑍) = ((𝐾 ↾ (𝑈 × {𝑍}))‘⟨𝑋, 𝑍⟩)
216		ovres 7077	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑋 ∈ 𝑈 ∧ 𝑍 ∈ {𝑍}) → (𝑋(𝐾 ↾ (𝑈 × {𝑍}))𝑍) = (𝑋𝐾𝑍))
217	21, 172, 216	syl2anc 579	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑋(𝐾 ↾ (𝑈 × {𝑍}))𝑍) = (𝑋𝐾𝑍))
218		snidg 4428	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑋 ∈ 𝑈 → 𝑋 ∈ {𝑋})
219	21, 218	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑋 ∈ {𝑋})
220		ovres 7077	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑋 ∈ {𝑋} ∧ 𝑍 ∈ 𝑉) → (𝑋(𝐾 ↾ ({𝑋} × 𝑉))𝑍) = (𝑋𝐾𝑍))
221	219, 160, 220	syl2anc 579	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑋(𝐾 ↾ ({𝑋} × 𝑉))𝑍) = (𝑋𝐾𝑍))
222	217, 221	eqtr4d 2817	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑋(𝐾 ↾ (𝑈 × {𝑍}))𝑍) = (𝑋(𝐾 ↾ ({𝑋} × 𝑉))𝑍))
223	215, 222	syl5eqr 2828	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐾 ↾ (𝑈 × {𝑍}))‘⟨𝑋, 𝑍⟩) = (𝑋(𝐾 ↾ ({𝑋} × 𝑉))𝑍))
224		eqid 2778	. . . . . . . . . . . . . . . . 17 ⊢ ∪ ((II ×_t II) ↾_t ({𝑋} × 𝑉)) = ∪ ((II ×_t II) ↾_t ({𝑋} × 𝑉))
225		snex 5140	. . . . . . . . . . . . . . . . . . . 20 ⊢ {𝑋} ∈ V
226	225	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → {𝑋} ∈ V)
227		txrest 21843	. . . . . . . . . . . . . . . . . . 19 ⊢ (((II ∈ Top ∧ II ∈ Top) ∧ ({𝑋} ∈ V ∧ 𝑉 ∈ II)) → ((II ×_t II) ↾_t ({𝑋} × 𝑉)) = ((II ↾_t {𝑋}) ×_t (II ↾_t 𝑉)))
228	179, 179, 226, 23, 227	syl22anc 829	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((II ×_t II) ↾_t ({𝑋} × 𝑉)) = ((II ↾_t {𝑋}) ×_t (II ↾_t 𝑉)))
229		restsn2 21383	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((II ∈ (TopOn‘(0[,]1)) ∧ 𝑋 ∈ (0[,]1)) → (II ↾_t {𝑋}) = 𝒫 {𝑋})
230	63, 22, 229	sylancr 581	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (II ↾_t {𝑋}) = 𝒫 {𝑋})
231		pwsn 4663	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝒫 {𝑋} = {∅, {𝑋}}
232		indisconn 21630	. . . . . . . . . . . . . . . . . . . . 21 ⊢ {∅, {𝑋}} ∈ Conn
233	231, 232	eqeltri 2855	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝒫 {𝑋} ∈ Conn
234	230, 233	syl6eqel 2867	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (II ↾_t {𝑋}) ∈ Conn)
235		txconn 21901	. . . . . . . . . . . . . . . . . . 19 ⊢ (((II ↾_t {𝑋}) ∈ Conn ∧ (II ↾_t 𝑉) ∈ Conn) → ((II ↾_t {𝑋}) ×_t (II ↾_t 𝑉)) ∈ Conn)
236	234, 72, 235	syl2anc 579	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((II ↾_t {𝑋}) ×_t (II ↾_t 𝑉)) ∈ Conn)
237	228, 236	eqeltrd 2859	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((II ×_t II) ↾_t ({𝑋} × 𝑉)) ∈ Conn)
238	1, 6, 7, 8, 9, 10, 11	cvmlift2lem6 31889	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑋 ∈ (0[,]1)) → (𝐾 ↾ ({𝑋} × (0[,]1))) ∈ (((II ×_t II) ↾_t ({𝑋} × (0[,]1))) Cn 𝐶))
239	22, 238	mpdan 677	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐾 ↾ ({𝑋} × (0[,]1))) ∈ (((II ×_t II) ↾_t ({𝑋} × (0[,]1))) Cn 𝐶))
240		xpss2 5375	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑉 ⊆ (0[,]1) → ({𝑋} × 𝑉) ⊆ ({𝑋} × (0[,]1)))
241	23, 25, 240	3syl 18	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ({𝑋} × 𝑉) ⊆ ({𝑋} × (0[,]1)))
242	22	snssd 4571	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → {𝑋} ⊆ (0[,]1))
243		xpss1 5374	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ({𝑋} ⊆ (0[,]1) → ({𝑋} × (0[,]1)) ⊆ ((0[,]1) × (0[,]1)))
244	242, 243	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ({𝑋} × (0[,]1)) ⊆ ((0[,]1) × (0[,]1)))
245	4	restuni 21374	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((II ×_t II) ∈ Top ∧ ({𝑋} × (0[,]1)) ⊆ ((0[,]1) × (0[,]1))) → ({𝑋} × (0[,]1)) = ∪ ((II ×_t II) ↾_t ({𝑋} × (0[,]1))))
246	15, 244, 245	sylancr 581	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ({𝑋} × (0[,]1)) = ∪ ((II ×_t II) ↾_t ({𝑋} × (0[,]1))))
247	241, 246	sseqtrd 3860	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ({𝑋} × 𝑉) ⊆ ∪ ((II ×_t II) ↾_t ({𝑋} × (0[,]1))))
248		eqid 2778	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ∪ ((II ×_t II) ↾_t ({𝑋} × (0[,]1))) = ∪ ((II ×_t II) ↾_t ({𝑋} × (0[,]1)))
249	248	cnrest 21497	. . . . . . . . . . . . . . . . . . . 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 579	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝐾 ↾ ({𝑋} × (0[,]1))) ↾ ({𝑋} × 𝑉)) ∈ ((((II ×_t II) ↾_t ({𝑋} × (0[,]1))) ↾_t ({𝑋} × 𝑉)) Cn 𝐶))
251	241	resabs1d 5677	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝐾 ↾ ({𝑋} × (0[,]1))) ↾ ({𝑋} × 𝑉)) = (𝐾 ↾ ({𝑋} × 𝑉)))
252	225, 93	xpex 7240	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ({𝑋} × (0[,]1)) ∈ V
253	252	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ({𝑋} × (0[,]1)) ∈ V)
254		restabs 21377	. . . . . . . . . . . . . . . . . . . . 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 1439	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (((II ×_t II) ↾_t ({𝑋} × (0[,]1))) ↾_t ({𝑋} × 𝑉)) = ((II ×_t II) ↾_t ({𝑋} × 𝑉)))
256	255	oveq1d 6937	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((((II ×_t II) ↾_t ({𝑋} × (0[,]1))) ↾_t ({𝑋} × 𝑉)) Cn 𝐶) = (((II ×_t II) ↾_t ({𝑋} × 𝑉)) Cn 𝐶))
257	250, 251, 256	3eltr3d 2873	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐾 ↾ ({𝑋} × 𝑉)) ∈ (((II ×_t II) ↾_t ({𝑋} × 𝑉)) Cn 𝐶))
258		df-ima 5368	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐾 “ ({𝑋} × 𝑉)) = ran (𝐾 ↾ ({𝑋} × 𝑉))
259	21	snssd 4571	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → {𝑋} ⊆ 𝑈)
260		xpss1 5374	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ({𝑋} ⊆ 𝑈 → ({𝑋} × 𝑉) ⊆ (𝑈 × 𝑉))
261		imass2 5755	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (({𝑋} × 𝑉) ⊆ (𝑈 × 𝑉) → (𝐾 “ ({𝑋} × 𝑉)) ⊆ (𝐾 “ (𝑈 × 𝑉)))
262	259, 260, 261	3syl 18	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝐾 “ ({𝑋} × 𝑉)) ⊆ (𝐾 “ (𝑈 × 𝑉)))
263	262, 124	sstrd 3831	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐾 “ ({𝑋} × 𝑉)) ⊆ (^◡𝐹 “ 𝑀))
264	258, 263	syl5eqssr 3869	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ran (𝐾 ↾ ({𝑋} × 𝑉)) ⊆ (^◡𝐹 “ 𝑀))
265		cnrest2 21498	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐶 ∈ (TopOn‘𝐵) ∧ ran (𝐾 ↾ ({𝑋} × 𝑉)) ⊆ (^◡𝐹 “ 𝑀) ∧ (^◡𝐹 “ 𝑀) ⊆ 𝐵) → ((𝐾 ↾ ({𝑋} × 𝑉)) ∈ (((II ×_t II) ↾_t ({𝑋} × 𝑉)) Cn 𝐶) ↔ (𝐾 ↾ ({𝑋} × 𝑉)) ∈ (((II ×_t II) ↾_t ({𝑋} × 𝑉)) Cn (𝐶 ↾_t (^◡𝐹 “ 𝑀)))))
266	196, 264, 135, 265	syl3anc 1439	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝐾 ↾ ({𝑋} × 𝑉)) ∈ (((II ×_t II) ↾_t ({𝑋} × 𝑉)) Cn 𝐶) ↔ (𝐾 ↾ ({𝑋} × 𝑉)) ∈ (((II ×_t II) ↾_t ({𝑋} × 𝑉)) Cn (𝐶 ↾_t (^◡𝐹 “ 𝑀)))))
267	257, 266	mpbid 224	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐾 ↾ ({𝑋} × 𝑉)) ∈ (((II ×_t II) ↾_t ({𝑋} × 𝑉)) Cn (𝐶 ↾_t (^◡𝐹 “ 𝑀))))
268		opelxpi 5392	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑋 ∈ {𝑋} ∧ 𝑌 ∈ 𝑉) → ⟨𝑋, 𝑌⟩ ∈ ({𝑋} × 𝑉))
269	219, 27, 268	syl2anc 579	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ⟨𝑋, 𝑌⟩ ∈ ({𝑋} × 𝑉))
270	259, 260	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ({𝑋} × 𝑉) ⊆ (𝑈 × 𝑉))
271	270, 50	sstrd 3831	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ({𝑋} × 𝑉) ⊆ ((0[,]1) × (0[,]1)))
272	4	restuni 21374	. . . . . . . . . . . . . . . . . . 19 ⊢ (((II ×_t II) ∈ Top ∧ ({𝑋} × 𝑉) ⊆ ((0[,]1) × (0[,]1))) → ({𝑋} × 𝑉) = ∪ ((II ×_t II) ↾_t ({𝑋} × 𝑉)))
273	15, 271, 272	sylancr 581	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ({𝑋} × 𝑉) = ∪ ((II ×_t II) ↾_t ({𝑋} × 𝑉)))
274	269, 273	eleqtrd 2861	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ⟨𝑋, 𝑌⟩ ∈ ∪ ((II ×_t II) ↾_t ({𝑋} × 𝑉)))
275		df-ov 6925	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑋(𝐾 ↾ ({𝑋} × 𝑉))𝑌) = ((𝐾 ↾ ({𝑋} × 𝑉))‘⟨𝑋, 𝑌⟩)
276		ovres 7077	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑋 ∈ {𝑋} ∧ 𝑌 ∈ 𝑉) → (𝑋(𝐾 ↾ ({𝑋} × 𝑉))𝑌) = (𝑋𝐾𝑌))
277	219, 27, 276	syl2anc 579	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑋(𝐾 ↾ ({𝑋} × 𝑉))𝑌) = (𝑋𝐾𝑌))
278	275, 277	syl5eqr 2828	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝐾 ↾ ({𝑋} × 𝑉))‘⟨𝑋, 𝑌⟩) = (𝑋𝐾𝑌))
279	45	simprd 491	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑋𝐾𝑌) ∈ 𝑊)
280	278, 279	eqeltrd 2859	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝐾 ↾ ({𝑋} × 𝑉))‘⟨𝑋, 𝑌⟩) ∈ 𝑊)
281	224, 237, 267, 155, 158, 274, 280	conncn 21638	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐾 ↾ ({𝑋} × 𝑉)):∪ ((II ×_t II) ↾_t ({𝑋} × 𝑉))⟶𝑊)
282	273	feq2d 6277	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐾 ↾ ({𝑋} × 𝑉)):({𝑋} × 𝑉)⟶𝑊 ↔ (𝐾 ↾ ({𝑋} × 𝑉)):∪ ((II ×_t II) ↾_t ({𝑋} × 𝑉))⟶𝑊))
283	281, 282	mpbird 249	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐾 ↾ ({𝑋} × 𝑉)):({𝑋} × 𝑉)⟶𝑊)
284	283, 219, 160	fovrnd 7083	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑋(𝐾 ↾ ({𝑋} × 𝑉))𝑍) ∈ 𝑊)
285	223, 284	eqeltrd 2859	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐾 ↾ (𝑈 × {𝑍}))‘⟨𝑋, 𝑍⟩) ∈ 𝑊)
286	178, 194, 206, 155, 158, 214, 285	conncn 21638	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐾 ↾ (𝑈 × {𝑍})):∪ ((II ×_t II) ↾_t (𝑈 × {𝑍}))⟶𝑊)
287	213	feq2d 6277	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐾 ↾ (𝑈 × {𝑍})):(𝑈 × {𝑍})⟶𝑊 ↔ (𝐾 ↾ (𝑈 × {𝑍})):∪ ((II ×_t II) ↾_t (𝑈 × {𝑍}))⟶𝑊))
288	286, 287	mpbird 249	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐾 ↾ (𝑈 × {𝑍})):(𝑈 × {𝑍})⟶𝑊)
289	288	adantr 474	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → (𝐾 ↾ (𝑈 × {𝑍})):(𝑈 × {𝑍})⟶𝑊)
290	289, 106, 173	fovrnd 7083	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → (𝑚(𝐾 ↾ (𝑈 × {𝑍}))𝑍) ∈ 𝑊)
291	177, 290	eqeltrd 2859	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → ((𝐾 ↾ ({𝑚} × 𝑉))‘⟨𝑚, 𝑍⟩) ∈ 𝑊)
292	56, 76, 139, 156, 159, 167, 291	conncn 21638	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → (𝐾 ↾ ({𝑚} × 𝑉)):∪ ((II ×_t II) ↾_t ({𝑚} × 𝑉))⟶𝑊)
293	166	feq2d 6277	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → ((𝐾 ↾ ({𝑚} × 𝑉)):({𝑚} × 𝑉)⟶𝑊 ↔ (𝐾 ↾ ({𝑚} × 𝑉)):∪ ((II ×_t II) ↾_t ({𝑚} × 𝑉))⟶𝑊))
294	292, 293	mpbird 249	. . . . . 6 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → (𝐾 ↾ ({𝑚} × 𝑉)):({𝑚} × 𝑉)⟶𝑊)
295	294, 52, 53	fovrnd 7083	. . . . 5 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → (𝑚(𝐾 ↾ ({𝑚} × 𝑉))𝑛) ∈ 𝑊)
296	55, 295	eqeltrrd 2860	. . . 4 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → (𝑚𝐾𝑛) ∈ 𝑊)
297	296	ralrimivva 3153	. . 3 ⊢ (𝜑 → ∀𝑚 ∈ 𝑈 ∀𝑛 ∈ 𝑉 (𝑚𝐾𝑛) ∈ 𝑊)
298		funimassov 7088	. . . 4 ⊢ ((Fun 𝐾 ∧ (𝑈 × 𝑉) ⊆ dom 𝐾) → ((𝐾 “ (𝑈 × 𝑉)) ⊆ 𝑊 ↔ ∀𝑚 ∈ 𝑈 ∀𝑛 ∈ 𝑉 (𝑚𝐾𝑛) ∈ 𝑊))
299	119, 121, 298	syl2anc 579	. . 3 ⊢ (𝜑 → ((𝐾 “ (𝑈 × 𝑉)) ⊆ 𝑊 ↔ ∀𝑚 ∈ 𝑈 ∀𝑛 ∈ 𝑉 (𝑚𝐾𝑛) ∈ 𝑊))
300	297, 299	mpbird 249	. 2 ⊢ (𝜑 → (𝐾 “ (𝑈 × 𝑉)) ⊆ 𝑊)
301	1, 4, 5, 6, 12, 14, 16, 30, 31, 48, 50, 300	cvmlift2lem9a 31884	1 ⊢ (𝜑 → (𝐾 ↾ (𝑈 × 𝑉)) ∈ (((II ×_t II) ↾_t (𝑈 × 𝑉)) Cn 𝐶))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 198 ∧ wa 386 = wceq 1601 ∈ wcel 2107 ∀wral 3090 {crab 3094 Vcvv 3398 ∖ cdif 3789 ∩ cin 3791 ⊆ wss 3792 ∅c0 4141 𝒫 cpw 4379 {csn 4398 {cpr 4400 ⟨cop 4404 ∪ cuni 4671 ↦ cmpt 4965 × cxp 5353 ^◡ccnv 5354 dom cdm 5355 ran crn 5356 ↾ cres 5357 “ cima 5358 ∘ ccom 5359 Fun wfun 6129 ⟶wf 6131 ‘cfv 6135 ℩crio 6882 (class class class)co 6922 ↦ cmpt2 6924 0cc0 10272 1c1 10273 [,]cicc 12490 ↾_t crest 16467 Topctop 21105 TopOnctopon 21122 Clsdccld 21228 Cn ccn 21436 Conncconn 21623 ×_t ctx 21772 Homeochmeo 21965 IIcii 23086 CovMap ccvm 31836

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 ax-6 2021 ax-7 2055 ax-8 2109 ax-9 2116 ax-10 2135 ax-11 2150 ax-12 2163 ax-13 2334 ax-ext 2754 ax-rep 5006 ax-sep 5017 ax-nul 5025 ax-pow 5077 ax-pr 5138 ax-un 7226 ax-inf2 8835 ax-cnex 10328 ax-resscn 10329 ax-1cn 10330 ax-icn 10331 ax-addcl 10332 ax-addrcl 10333 ax-mulcl 10334 ax-mulrcl 10335 ax-mulcom 10336 ax-addass 10337 ax-mulass 10338 ax-distr 10339 ax-i2m1 10340 ax-1ne0 10341 ax-1rid 10342 ax-rnegex 10343 ax-rrecex 10344 ax-cnre 10345 ax-pre-lttri 10346 ax-pre-lttrn 10347 ax-pre-ltadd 10348 ax-pre-mulgt0 10349 ax-pre-sup 10350 ax-addf 10351 ax-mulf 10352

This theorem depends on definitions: df-bi 199 df-an 387 df-or 837 df-3or 1072 df-3an 1073 df-tru 1605 df-fal 1615 df-ex 1824 df-nf 1828 df-sb 2012 df-mo 2551 df-eu 2587 df-clab 2764 df-cleq 2770 df-clel 2774 df-nfc 2921 df-ne 2970 df-nel 3076 df-ral 3095 df-rex 3096 df-reu 3097 df-rmo 3098 df-rab 3099 df-v 3400 df-sbc 3653 df-csb 3752 df-dif 3795 df-un 3797 df-in 3799 df-ss 3806 df-pss 3808 df-nul 4142 df-if 4308 df-pw 4381 df-sn 4399 df-pr 4401 df-tp 4403 df-op 4405 df-uni 4672 df-int 4711 df-iun 4755 df-iin 4756 df-br 4887 df-opab 4949 df-mpt 4966 df-tr 4988 df-id 5261 df-eprel 5266 df-po 5274 df-so 5275 df-fr 5314 df-se 5315 df-we 5316 df-xp 5361 df-rel 5362 df-cnv 5363 df-co 5364 df-dm 5365 df-rn 5366 df-res 5367 df-ima 5368 df-pred 5933 df-ord 5979 df-on 5980 df-lim 5981 df-suc 5982 df-iota 6099 df-fun 6137 df-fn 6138 df-f 6139 df-f1 6140 df-fo 6141 df-f1o 6142 df-fv 6143 df-isom 6144 df-riota 6883 df-ov 6925 df-oprab 6926 df-mpt2 6927 df-of 7174 df-om 7344 df-1st 7445 df-2nd 7446 df-supp 7577 df-wrecs 7689 df-recs 7751 df-rdg 7789 df-1o 7843 df-2o 7844 df-oadd 7847 df-er 8026 df-ec 8028 df-map 8142 df-ixp 8195 df-en 8242 df-dom 8243 df-sdom 8244 df-fin 8245 df-fsupp 8564 df-fi 8605 df-sup 8636 df-inf 8637 df-oi 8704 df-card 9098 df-cda 9325 df-pnf 10413 df-mnf 10414 df-xr 10415 df-ltxr 10416 df-le 10417 df-sub 10608 df-neg 10609 df-div 11033 df-nn 11375 df-2 11438 df-3 11439 df-4 11440 df-5 11441 df-6 11442 df-7 11443 df-8 11444 df-9 11445 df-n0 11643 df-z 11729 df-dec 11846 df-uz 11993 df-q 12096 df-rp 12138 df-xneg 12257 df-xadd 12258 df-xmul 12259 df-ioo 12491 df-ico 12493 df-icc 12494 df-fz 12644 df-fzo 12785 df-fl 12912 df-seq 13120 df-exp 13179 df-hash 13436 df-cj 14246 df-re 14247 df-im 14248 df-sqrt 14382 df-abs 14383 df-clim 14627 df-sum 14825 df-struct 16257 df-ndx 16258 df-slot 16259 df-base 16261 df-sets 16262 df-ress 16263 df-plusg 16351 df-mulr 16352 df-starv 16353 df-sca 16354 df-vsca 16355 df-ip 16356 df-tset 16357 df-ple 16358 df-ds 16360 df-unif 16361 df-hom 16362 df-cco 16363 df-rest 16469 df-topn 16470 df-0g 16488 df-gsum 16489 df-topgen 16490 df-pt 16491 df-prds 16494 df-xrs 16548 df-qtop 16553 df-imas 16554 df-xps 16556 df-mre 16632 df-mrc 16633 df-acs 16635 df-mgm 17628 df-sgrp 17670 df-mnd 17681 df-submnd 17722 df-mulg 17928 df-cntz 18133 df-cmn 18581 df-psmet 20134 df-xmet 20135 df-met 20136 df-bl 20137 df-mopn 20138 df-cnfld 20143 df-top 21106 df-topon 21123 df-topsp 21145 df-bases 21158 df-cld 21231 df-ntr 21232 df-cls 21233 df-nei 21310 df-cn 21439 df-cnp 21440 df-cmp 21599 df-conn 21624 df-lly 21678 df-nlly 21679 df-tx 21774 df-hmeo 21967 df-xms 22533 df-ms 22534 df-tms 22535 df-ii 23088 df-htpy 23177 df-phtpy 23178 df-phtpc 23199 df-pconn 31802 df-sconn 31803 df-cvm 31837

This theorem is referenced by: cvmlift2lem10 31893

W3C validator