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 35283

Description: Lemma for cvmlift2 35288. (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 24789	. . 3 ⊢ II ∈ Top
3		iiuni 24790	. . 3 ⊢ (0[,]1) = ∪ II
4	2, 2, 3, 3	txunii 23496	. 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 35279	. 2 ⊢ (𝜑 → 𝐾:((0[,]1) × (0[,]1))⟶𝐵)
13	1, 6, 7, 8, 9, 10, 11	cvmlift2lem7 35281	. . 3 ⊢ (𝜑 → (𝐹 ∘ 𝐾) = 𝐺)
14	13, 7	eqeltrd 2828	. 2 ⊢ (𝜑 → (𝐹 ∘ 𝐾) ∈ ((II ×_t II) Cn 𝐽))
15	2, 2	txtopi 23493	. . 3 ⊢ (II ×_t II) ∈ Top
16	15	a1i 11	. 2 ⊢ (𝜑 → (II ×_t II) ∈ Top)
17		cvmlift2lem9.3	. . . . 5 ⊢ (𝜑 → 𝑈 ∈ II)
18		elssuni 4891	. . . . . 6 ⊢ (𝑈 ∈ II → 𝑈 ⊆ ∪ II)
19	18, 3	sseqtrrdi 3979	. . . . 5 ⊢ (𝑈 ∈ II → 𝑈 ⊆ (0[,]1))
20	17, 19	syl 17	. . . 4 ⊢ (𝜑 → 𝑈 ⊆ (0[,]1))
21		cvmlift2lem9.7	. . . 4 ⊢ (𝜑 → 𝑋 ∈ 𝑈)
22	20, 21	sseldd 3938	. . 3 ⊢ (𝜑 → 𝑋 ∈ (0[,]1))
23		cvmlift2lem9.4	. . . . 5 ⊢ (𝜑 → 𝑉 ∈ II)
24		elssuni 4891	. . . . . 6 ⊢ (𝑉 ∈ II → 𝑉 ⊆ ∪ II)
25	24, 3	sseqtrrdi 3979	. . . . 5 ⊢ (𝑉 ∈ II → 𝑉 ⊆ (0[,]1))
26	23, 25	syl 17	. . . 4 ⊢ (𝜑 → 𝑉 ⊆ (0[,]1))
27		cvmlift2lem9.8	. . . 4 ⊢ (𝜑 → 𝑌 ∈ 𝑉)
28	26, 27	sseldd 3938	. . 3 ⊢ (𝜑 → 𝑌 ∈ (0[,]1))
29		opelxpi 5660	. . 3 ⊢ ((𝑋 ∈ (0[,]1) ∧ 𝑌 ∈ (0[,]1)) → ⟨𝑋, 𝑌⟩ ∈ ((0[,]1) × (0[,]1)))
30	22, 28, 29	syl2anc 584	. 2 ⊢ (𝜑 → ⟨𝑋, 𝑌⟩ ∈ ((0[,]1) × (0[,]1)))
31		cvmlift2lem9.2	. 2 ⊢ (𝜑 → 𝑇 ∈ (𝑆‘𝑀))
32	12, 22, 28	fovcdmd 7525	. . . 4 ⊢ (𝜑 → (𝑋𝐾𝑌) ∈ 𝐵)
33		fvco3 6926	. . . . . . . 8 ⊢ ((𝐾:((0[,]1) × (0[,]1))⟶𝐵 ∧ ⟨𝑋, 𝑌⟩ ∈ ((0[,]1) × (0[,]1))) → ((𝐹 ∘ 𝐾)‘⟨𝑋, 𝑌⟩) = (𝐹‘(𝐾‘⟨𝑋, 𝑌⟩)))
34	12, 30, 33	syl2anc 584	. . . . . . 7 ⊢ (𝜑 → ((𝐹 ∘ 𝐾)‘⟨𝑋, 𝑌⟩) = (𝐹‘(𝐾‘⟨𝑋, 𝑌⟩)))
35	13	fveq1d 6828	. . . . . . 7 ⊢ (𝜑 → ((𝐹 ∘ 𝐾)‘⟨𝑋, 𝑌⟩) = (𝐺‘⟨𝑋, 𝑌⟩))
36	34, 35	eqtr3d 2766	. . . . . 6 ⊢ (𝜑 → (𝐹‘(𝐾‘⟨𝑋, 𝑌⟩)) = (𝐺‘⟨𝑋, 𝑌⟩))
37		df-ov 7356	. . . . . . 7 ⊢ (𝑋𝐾𝑌) = (𝐾‘⟨𝑋, 𝑌⟩)
38	37	fveq2i 6829	. . . . . 6 ⊢ (𝐹‘(𝑋𝐾𝑌)) = (𝐹‘(𝐾‘⟨𝑋, 𝑌⟩))
39		df-ov 7356	. . . . . 6 ⊢ (𝑋𝐺𝑌) = (𝐺‘⟨𝑋, 𝑌⟩)
40	36, 38, 39	3eqtr4g 2789	. . . . 5 ⊢ (𝜑 → (𝐹‘(𝑋𝐾𝑌)) = (𝑋𝐺𝑌))
41		cvmlift2lem9.1	. . . . 5 ⊢ (𝜑 → (𝑋𝐺𝑌) ∈ 𝑀)
42	40, 41	eqeltrd 2828	. . . 4 ⊢ (𝜑 → (𝐹‘(𝑋𝐾𝑌)) ∈ 𝑀)
43		cvmlift2lem9.w	. . . . 5 ⊢ 𝑊 = (℩𝑏 ∈ 𝑇 (𝑋𝐾𝑌) ∈ 𝑏)
44	5, 1, 43	cvmsiota 35249	. . . 4 ⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ (𝑇 ∈ (𝑆‘𝑀) ∧ (𝑋𝐾𝑌) ∈ 𝐵 ∧ (𝐹‘(𝑋𝐾𝑌)) ∈ 𝑀)) → (𝑊 ∈ 𝑇 ∧ (𝑋𝐾𝑌) ∈ 𝑊))
45	6, 31, 32, 42, 44	syl13anc 1374	. . 3 ⊢ (𝜑 → (𝑊 ∈ 𝑇 ∧ (𝑋𝐾𝑌) ∈ 𝑊))
46	37	eleq1i 2819	. . . 4 ⊢ ((𝑋𝐾𝑌) ∈ 𝑊 ↔ (𝐾‘⟨𝑋, 𝑌⟩) ∈ 𝑊)
47	46	anbi2i 623	. . 3 ⊢ ((𝑊 ∈ 𝑇 ∧ (𝑋𝐾𝑌) ∈ 𝑊) ↔ (𝑊 ∈ 𝑇 ∧ (𝐾‘⟨𝑋, 𝑌⟩) ∈ 𝑊))
48	45, 47	sylib 218	. 2 ⊢ (𝜑 → (𝑊 ∈ 𝑇 ∧ (𝐾‘⟨𝑋, 𝑌⟩) ∈ 𝑊))
49		xpss12 5638	. . 3 ⊢ ((𝑈 ⊆ (0[,]1) ∧ 𝑉 ⊆ (0[,]1)) → (𝑈 × 𝑉) ⊆ ((0[,]1) × (0[,]1)))
50	20, 26, 49	syl2anc 584	. 2 ⊢ (𝜑 → (𝑈 × 𝑉) ⊆ ((0[,]1) × (0[,]1)))
51		snidg 4614	. . . . . . 7 ⊢ (𝑚 ∈ 𝑈 → 𝑚 ∈ {𝑚})
52	51	ad2antrl 728	. . . . . 6 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → 𝑚 ∈ {𝑚})
53		simprr 772	. . . . . 6 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → 𝑛 ∈ 𝑉)
54		ovres 7519	. . . . . 6 ⊢ ((𝑚 ∈ {𝑚} ∧ 𝑛 ∈ 𝑉) → (𝑚(𝐾 ↾ ({𝑚} × 𝑉))𝑛) = (𝑚𝐾𝑛))
55	52, 53, 54	syl2anc 584	. . . . 5 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → (𝑚(𝐾 ↾ ({𝑚} × 𝑉))𝑛) = (𝑚𝐾𝑛))
56		eqid 2729	. . . . . . . 8 ⊢ ∪ ((II ×_t II) ↾_t ({𝑚} × 𝑉)) = ∪ ((II ×_t II) ↾_t ({𝑚} × 𝑉))
57	2	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → II ∈ Top)
58		snex 5378	. . . . . . . . . . 11 ⊢ {𝑚} ∈ V
59	58	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → {𝑚} ∈ V)
60	23	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → 𝑉 ∈ II)
61		txrest 23534	. . . . . . . . . 10 ⊢ (((II ∈ Top ∧ II ∈ Top) ∧ ({𝑚} ∈ V ∧ 𝑉 ∈ II)) → ((II ×_t II) ↾_t ({𝑚} × 𝑉)) = ((II ↾_t {𝑚}) ×_t (II ↾_t 𝑉)))
62	57, 57, 59, 60, 61	syl22anc 838	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → ((II ×_t II) ↾_t ({𝑚} × 𝑉)) = ((II ↾_t {𝑚}) ×_t (II ↾_t 𝑉)))
63		iitopon 24788	. . . . . . . . . . . 12 ⊢ II ∈ (TopOn‘(0[,]1))
64	20	sselda 3937	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑈) → 𝑚 ∈ (0[,]1))
65	64	adantrr 717	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → 𝑚 ∈ (0[,]1))
66		restsn2 23074	. . . . . . . . . . . 12 ⊢ ((II ∈ (TopOn‘(0[,]1)) ∧ 𝑚 ∈ (0[,]1)) → (II ↾_t {𝑚}) = 𝒫 {𝑚})
67	63, 65, 66	sylancr 587	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → (II ↾_t {𝑚}) = 𝒫 {𝑚})
68		pwsn 4854	. . . . . . . . . . . 12 ⊢ 𝒫 {𝑚} = {∅, {𝑚}}
69		indisconn 23321	. . . . . . . . . . . 12 ⊢ {∅, {𝑚}} ∈ Conn
70	68, 69	eqeltri 2824	. . . . . . . . . . 11 ⊢ 𝒫 {𝑚} ∈ Conn
71	67, 70	eqeltrdi 2836	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → (II ↾_t {𝑚}) ∈ Conn)
72		cvmlift2lem9.6	. . . . . . . . . . 11 ⊢ (𝜑 → (II ↾_t 𝑉) ∈ Conn)
73	72	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → (II ↾_t 𝑉) ∈ Conn)
74		txconn 23592	. . . . . . . . . 10 ⊢ (((II ↾_t {𝑚}) ∈ Conn ∧ (II ↾_t 𝑉) ∈ Conn) → ((II ↾_t {𝑚}) ×_t (II ↾_t 𝑉)) ∈ Conn)
75	71, 73, 74	syl2anc 584	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → ((II ↾_t {𝑚}) ×_t (II ↾_t 𝑉)) ∈ Conn)
76	62, 75	eqeltrd 2828	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → ((II ×_t II) ↾_t ({𝑚} × 𝑉)) ∈ Conn)
77	1, 6, 7, 8, 9, 10, 11	cvmlift2lem6 35280	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑚 ∈ (0[,]1)) → (𝐾 ↾ ({𝑚} × (0[,]1))) ∈ (((II ×_t II) ↾_t ({𝑚} × (0[,]1))) Cn 𝐶))
78	65, 77	syldan 591	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → (𝐾 ↾ ({𝑚} × (0[,]1))) ∈ (((II ×_t II) ↾_t ({𝑚} × (0[,]1))) Cn 𝐶))
79	26	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → 𝑉 ⊆ (0[,]1))
80		xpss2 5643	. . . . . . . . . . . . 13 ⊢ (𝑉 ⊆ (0[,]1) → ({𝑚} × 𝑉) ⊆ ({𝑚} × (0[,]1)))
81	79, 80	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → ({𝑚} × 𝑉) ⊆ ({𝑚} × (0[,]1)))
82	65	snssd 4763	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → {𝑚} ⊆ (0[,]1))
83		xpss1 5642	. . . . . . . . . . . . . 14 ⊢ ({𝑚} ⊆ (0[,]1) → ({𝑚} × (0[,]1)) ⊆ ((0[,]1) × (0[,]1)))
84	82, 83	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → ({𝑚} × (0[,]1)) ⊆ ((0[,]1) × (0[,]1)))
85	4	restuni 23065	. . . . . . . . . . . . 13 ⊢ (((II ×_t II) ∈ Top ∧ ({𝑚} × (0[,]1)) ⊆ ((0[,]1) × (0[,]1))) → ({𝑚} × (0[,]1)) = ∪ ((II ×_t II) ↾_t ({𝑚} × (0[,]1))))
86	15, 84, 85	sylancr 587	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → ({𝑚} × (0[,]1)) = ∪ ((II ×_t II) ↾_t ({𝑚} × (0[,]1))))
87	81, 86	sseqtrd 3974	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → ({𝑚} × 𝑉) ⊆ ∪ ((II ×_t II) ↾_t ({𝑚} × (0[,]1))))
88		eqid 2729	. . . . . . . . . . . 12 ⊢ ∪ ((II ×_t II) ↾_t ({𝑚} × (0[,]1))) = ∪ ((II ×_t II) ↾_t ({𝑚} × (0[,]1)))
89	88	cnrest 23188	. . . . . . . . . . 11 ⊢ (((𝐾 ↾ ({𝑚} × (0[,]1))) ∈ (((II ×_t II) ↾_t ({𝑚} × (0[,]1))) Cn 𝐶) ∧ ({𝑚} × 𝑉) ⊆ ∪ ((II ×_t II) ↾_t ({𝑚} × (0[,]1)))) → ((𝐾 ↾ ({𝑚} × (0[,]1))) ↾ ({𝑚} × 𝑉)) ∈ ((((II ×_t II) ↾_t ({𝑚} × (0[,]1))) ↾_t ({𝑚} × 𝑉)) Cn 𝐶))
90	78, 87, 89	syl2anc 584	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → ((𝐾 ↾ ({𝑚} × (0[,]1))) ↾ ({𝑚} × 𝑉)) ∈ ((((II ×_t II) ↾_t ({𝑚} × (0[,]1))) ↾_t ({𝑚} × 𝑉)) Cn 𝐶))
91	81	resabs1d 5963	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → ((𝐾 ↾ ({𝑚} × (0[,]1))) ↾ ({𝑚} × 𝑉)) = (𝐾 ↾ ({𝑚} × 𝑉)))
92	15	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → (II ×_t II) ∈ Top)
93		ovex 7386	. . . . . . . . . . . . . 14 ⊢ (0[,]1) ∈ V
94	58, 93	xpex 7693	. . . . . . . . . . . . 13 ⊢ ({𝑚} × (0[,]1)) ∈ V
95	94	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → ({𝑚} × (0[,]1)) ∈ V)
96		restabs 23068	. . . . . . . . . . . 12 ⊢ (((II ×_t II) ∈ Top ∧ ({𝑚} × 𝑉) ⊆ ({𝑚} × (0[,]1)) ∧ ({𝑚} × (0[,]1)) ∈ V) → (((II ×_t II) ↾_t ({𝑚} × (0[,]1))) ↾_t ({𝑚} × 𝑉)) = ((II ×_t II) ↾_t ({𝑚} × 𝑉)))
97	92, 81, 95, 96	syl3anc 1373	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → (((II ×_t II) ↾_t ({𝑚} × (0[,]1))) ↾_t ({𝑚} × 𝑉)) = ((II ×_t II) ↾_t ({𝑚} × 𝑉)))
98	97	oveq1d 7368	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → ((((II ×_t II) ↾_t ({𝑚} × (0[,]1))) ↾_t ({𝑚} × 𝑉)) Cn 𝐶) = (((II ×_t II) ↾_t ({𝑚} × 𝑉)) Cn 𝐶))
99	90, 91, 98	3eltr3d 2842	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → (𝐾 ↾ ({𝑚} × 𝑉)) ∈ (((II ×_t II) ↾_t ({𝑚} × 𝑉)) Cn 𝐶))
100		cvmtop1 35232	. . . . . . . . . . . . 13 ⊢ (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐶 ∈ Top)
101	6, 100	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐶 ∈ Top)
102	101	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → 𝐶 ∈ Top)
103	1	toptopon 22820	. . . . . . . . . . 11 ⊢ (𝐶 ∈ Top ↔ 𝐶 ∈ (TopOn‘𝐵))
104	102, 103	sylib 218	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → 𝐶 ∈ (TopOn‘𝐵))
105		df-ima 5636	. . . . . . . . . . 11 ⊢ (𝐾 “ ({𝑚} × 𝑉)) = ran (𝐾 ↾ ({𝑚} × 𝑉))
106		simprl 770	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → 𝑚 ∈ 𝑈)
107	106	snssd 4763	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → {𝑚} ⊆ 𝑈)
108		xpss1 5642	. . . . . . . . . . . . 13 ⊢ ({𝑚} ⊆ 𝑈 → ({𝑚} × 𝑉) ⊆ (𝑈 × 𝑉))
109		imass2 6057	. . . . . . . . . . . . 13 ⊢ (({𝑚} × 𝑉) ⊆ (𝑈 × 𝑉) → (𝐾 “ ({𝑚} × 𝑉)) ⊆ (𝐾 “ (𝑈 × 𝑉)))
110	107, 108, 109	3syl 18	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → (𝐾 “ ({𝑚} × 𝑉)) ⊆ (𝐾 “ (𝑈 × 𝑉)))
111		cvmlift2lem9.9	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑈 × 𝑉) ⊆ (^◡𝐺 “ 𝑀))
112		imaco 6204	. . . . . . . . . . . . . . . 16 ⊢ ((^◡𝐾 ∘ ^◡𝐹) “ 𝑀) = (^◡𝐾 “ (^◡𝐹 “ 𝑀))
113		cnvco 5832	. . . . . . . . . . . . . . . . . 18 ⊢ ^◡(𝐹 ∘ 𝐾) = (^◡𝐾 ∘ ^◡𝐹)
114	13	cnveqd 5822	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ^◡(𝐹 ∘ 𝐾) = ^◡𝐺)
115	113, 114	eqtr3id 2778	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (^◡𝐾 ∘ ^◡𝐹) = ^◡𝐺)
116	115	imaeq1d 6014	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((^◡𝐾 ∘ ^◡𝐹) “ 𝑀) = (^◡𝐺 “ 𝑀))
117	112, 116	eqtr3id 2778	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (^◡𝐾 “ (^◡𝐹 “ 𝑀)) = (^◡𝐺 “ 𝑀))
118	111, 117	sseqtrrd 3975	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑈 × 𝑉) ⊆ (^◡𝐾 “ (^◡𝐹 “ 𝑀)))
119	12	ffund 6660	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → Fun 𝐾)
120	12	fdmd 6666	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → dom 𝐾 = ((0[,]1) × (0[,]1)))
121	50, 120	sseqtrrd 3975	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑈 × 𝑉) ⊆ dom 𝐾)
122		funimass3 6992	. . . . . . . . . . . . . . 15 ⊢ ((Fun 𝐾 ∧ (𝑈 × 𝑉) ⊆ dom 𝐾) → ((𝐾 “ (𝑈 × 𝑉)) ⊆ (^◡𝐹 “ 𝑀) ↔ (𝑈 × 𝑉) ⊆ (^◡𝐾 “ (^◡𝐹 “ 𝑀))))
123	119, 121, 122	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐾 “ (𝑈 × 𝑉)) ⊆ (^◡𝐹 “ 𝑀) ↔ (𝑈 × 𝑉) ⊆ (^◡𝐾 “ (^◡𝐹 “ 𝑀))))
124	118, 123	mpbird 257	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐾 “ (𝑈 × 𝑉)) ⊆ (^◡𝐹 “ 𝑀))
125	124	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → (𝐾 “ (𝑈 × 𝑉)) ⊆ (^◡𝐹 “ 𝑀))
126	110, 125	sstrd 3948	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → (𝐾 “ ({𝑚} × 𝑉)) ⊆ (^◡𝐹 “ 𝑀))
127	105, 126	eqsstrrid 3977	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → ran (𝐾 ↾ ({𝑚} × 𝑉)) ⊆ (^◡𝐹 “ 𝑀))
128		cnvimass 6037	. . . . . . . . . . . 12 ⊢ (^◡𝐹 “ 𝑀) ⊆ dom 𝐹
129		cvmcn 35234	. . . . . . . . . . . . . 14 ⊢ (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐹 ∈ (𝐶 Cn 𝐽))
130	6, 129	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐹 ∈ (𝐶 Cn 𝐽))
131		eqid 2729	. . . . . . . . . . . . . 14 ⊢ ∪ 𝐽 = ∪ 𝐽
132	1, 131	cnf 23149	. . . . . . . . . . . . 13 ⊢ (𝐹 ∈ (𝐶 Cn 𝐽) → 𝐹:𝐵⟶∪ 𝐽)
133		fdm 6665	. . . . . . . . . . . . 13 ⊢ (𝐹:𝐵⟶∪ 𝐽 → dom 𝐹 = 𝐵)
134	130, 132, 133	3syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → dom 𝐹 = 𝐵)
135	128, 134	sseqtrid 3980	. . . . . . . . . . 11 ⊢ (𝜑 → (^◡𝐹 “ 𝑀) ⊆ 𝐵)
136	135	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → (^◡𝐹 “ 𝑀) ⊆ 𝐵)
137		cnrest2 23189	. . . . . . . . . 10 ⊢ ((𝐶 ∈ (TopOn‘𝐵) ∧ ran (𝐾 ↾ ({𝑚} × 𝑉)) ⊆ (^◡𝐹 “ 𝑀) ∧ (^◡𝐹 “ 𝑀) ⊆ 𝐵) → ((𝐾 ↾ ({𝑚} × 𝑉)) ∈ (((II ×_t II) ↾_t ({𝑚} × 𝑉)) Cn 𝐶) ↔ (𝐾 ↾ ({𝑚} × 𝑉)) ∈ (((II ×_t II) ↾_t ({𝑚} × 𝑉)) Cn (𝐶 ↾_t (^◡𝐹 “ 𝑀)))))
138	104, 127, 136, 137	syl3anc 1373	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → ((𝐾 ↾ ({𝑚} × 𝑉)) ∈ (((II ×_t II) ↾_t ({𝑚} × 𝑉)) Cn 𝐶) ↔ (𝐾 ↾ ({𝑚} × 𝑉)) ∈ (((II ×_t II) ↾_t ({𝑚} × 𝑉)) Cn (𝐶 ↾_t (^◡𝐹 “ 𝑀)))))
139	99, 138	mpbid 232	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → (𝐾 ↾ ({𝑚} × 𝑉)) ∈ (((II ×_t II) ↾_t ({𝑚} × 𝑉)) Cn (𝐶 ↾_t (^◡𝐹 “ 𝑀))))
140	5	cvmsss 35239	. . . . . . . . . . . 12 ⊢ (𝑇 ∈ (𝑆‘𝑀) → 𝑇 ⊆ 𝐶)
141	31, 140	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑇 ⊆ 𝐶)
142	45	simpld 494	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑊 ∈ 𝑇)
143	141, 142	sseldd 3938	. . . . . . . . . 10 ⊢ (𝜑 → 𝑊 ∈ 𝐶)
144		elssuni 4891	. . . . . . . . . . . 12 ⊢ (𝑊 ∈ 𝑇 → 𝑊 ⊆ ∪ 𝑇)
145	142, 144	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑊 ⊆ ∪ 𝑇)
146	5	cvmsuni 35241	. . . . . . . . . . . 12 ⊢ (𝑇 ∈ (𝑆‘𝑀) → ∪ 𝑇 = (^◡𝐹 “ 𝑀))
147	31, 146	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → ∪ 𝑇 = (^◡𝐹 “ 𝑀))
148	145, 147	sseqtrd 3974	. . . . . . . . . 10 ⊢ (𝜑 → 𝑊 ⊆ (^◡𝐹 “ 𝑀))
149	5	cvmsrcl 35236	. . . . . . . . . . . . 13 ⊢ (𝑇 ∈ (𝑆‘𝑀) → 𝑀 ∈ 𝐽)
150	31, 149	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑀 ∈ 𝐽)
151		cnima 23168	. . . . . . . . . . . 12 ⊢ ((𝐹 ∈ (𝐶 Cn 𝐽) ∧ 𝑀 ∈ 𝐽) → (^◡𝐹 “ 𝑀) ∈ 𝐶)
152	130, 150, 151	syl2anc 584	. . . . . . . . . . 11 ⊢ (𝜑 → (^◡𝐹 “ 𝑀) ∈ 𝐶)
153		restopn2 23080	. . . . . . . . . . 11 ⊢ ((𝐶 ∈ Top ∧ (^◡𝐹 “ 𝑀) ∈ 𝐶) → (𝑊 ∈ (𝐶 ↾_t (^◡𝐹 “ 𝑀)) ↔ (𝑊 ∈ 𝐶 ∧ 𝑊 ⊆ (^◡𝐹 “ 𝑀))))
154	101, 152, 153	syl2anc 584	. . . . . . . . . 10 ⊢ (𝜑 → (𝑊 ∈ (𝐶 ↾_t (^◡𝐹 “ 𝑀)) ↔ (𝑊 ∈ 𝐶 ∧ 𝑊 ⊆ (^◡𝐹 “ 𝑀))))
155	143, 148, 154	mpbir2and 713	. . . . . . . . 9 ⊢ (𝜑 → 𝑊 ∈ (𝐶 ↾_t (^◡𝐹 “ 𝑀)))
156	155	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → 𝑊 ∈ (𝐶 ↾_t (^◡𝐹 “ 𝑀)))
157	5	cvmscld 35245	. . . . . . . . . 10 ⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑇 ∈ (𝑆‘𝑀) ∧ 𝑊 ∈ 𝑇) → 𝑊 ∈ (Clsd‘(𝐶 ↾_t (^◡𝐹 “ 𝑀))))
158	6, 31, 142, 157	syl3anc 1373	. . . . . . . . 9 ⊢ (𝜑 → 𝑊 ∈ (Clsd‘(𝐶 ↾_t (^◡𝐹 “ 𝑀))))
159	158	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → 𝑊 ∈ (Clsd‘(𝐶 ↾_t (^◡𝐹 “ 𝑀))))
160		cvmlift2lem9.10	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑍 ∈ 𝑉)
161	160	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → 𝑍 ∈ 𝑉)
162		opelxpi 5660	. . . . . . . . . 10 ⊢ ((𝑚 ∈ {𝑚} ∧ 𝑍 ∈ 𝑉) → ⟨𝑚, 𝑍⟩ ∈ ({𝑚} × 𝑉))
163	52, 161, 162	syl2anc 584	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → ⟨𝑚, 𝑍⟩ ∈ ({𝑚} × 𝑉))
164	81, 84	sstrd 3948	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → ({𝑚} × 𝑉) ⊆ ((0[,]1) × (0[,]1)))
165	4	restuni 23065	. . . . . . . . . 10 ⊢ (((II ×_t II) ∈ Top ∧ ({𝑚} × 𝑉) ⊆ ((0[,]1) × (0[,]1))) → ({𝑚} × 𝑉) = ∪ ((II ×_t II) ↾_t ({𝑚} × 𝑉)))
166	15, 164, 165	sylancr 587	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → ({𝑚} × 𝑉) = ∪ ((II ×_t II) ↾_t ({𝑚} × 𝑉)))
167	163, 166	eleqtrd 2830	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → ⟨𝑚, 𝑍⟩ ∈ ∪ ((II ×_t II) ↾_t ({𝑚} × 𝑉)))
168		df-ov 7356	. . . . . . . . . 10 ⊢ (𝑚(𝐾 ↾ ({𝑚} × 𝑉))𝑍) = ((𝐾 ↾ ({𝑚} × 𝑉))‘⟨𝑚, 𝑍⟩)
169		ovres 7519	. . . . . . . . . . . 12 ⊢ ((𝑚 ∈ {𝑚} ∧ 𝑍 ∈ 𝑉) → (𝑚(𝐾 ↾ ({𝑚} × 𝑉))𝑍) = (𝑚𝐾𝑍))
170	52, 161, 169	syl2anc 584	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → (𝑚(𝐾 ↾ ({𝑚} × 𝑉))𝑍) = (𝑚𝐾𝑍))
171		snidg 4614	. . . . . . . . . . . . . 14 ⊢ (𝑍 ∈ 𝑉 → 𝑍 ∈ {𝑍})
172	160, 171	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑍 ∈ {𝑍})
173	172	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → 𝑍 ∈ {𝑍})
174		ovres 7519	. . . . . . . . . . . 12 ⊢ ((𝑚 ∈ 𝑈 ∧ 𝑍 ∈ {𝑍}) → (𝑚(𝐾 ↾ (𝑈 × {𝑍}))𝑍) = (𝑚𝐾𝑍))
175	106, 173, 174	syl2anc 584	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → (𝑚(𝐾 ↾ (𝑈 × {𝑍}))𝑍) = (𝑚𝐾𝑍))
176	170, 175	eqtr4d 2767	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → (𝑚(𝐾 ↾ ({𝑚} × 𝑉))𝑍) = (𝑚(𝐾 ↾ (𝑈 × {𝑍}))𝑍))
177	168, 176	eqtr3id 2778	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → ((𝐾 ↾ ({𝑚} × 𝑉))‘⟨𝑚, 𝑍⟩) = (𝑚(𝐾 ↾ (𝑈 × {𝑍}))𝑍))
178		eqid 2729	. . . . . . . . . . . . 13 ⊢ ∪ ((II ×_t II) ↾_t (𝑈 × {𝑍})) = ∪ ((II ×_t II) ↾_t (𝑈 × {𝑍}))
179	2	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → II ∈ Top)
180		snex 5378	. . . . . . . . . . . . . . . 16 ⊢ {𝑍} ∈ V
181	180	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → {𝑍} ∈ V)
182		txrest 23534	. . . . . . . . . . . . . . 15 ⊢ (((II ∈ Top ∧ II ∈ Top) ∧ (𝑈 ∈ II ∧ {𝑍} ∈ V)) → ((II ×_t II) ↾_t (𝑈 × {𝑍})) = ((II ↾_t 𝑈) ×_t (II ↾_t {𝑍})))
183	179, 179, 17, 181, 182	syl22anc 838	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((II ×_t II) ↾_t (𝑈 × {𝑍})) = ((II ↾_t 𝑈) ×_t (II ↾_t {𝑍})))
184		cvmlift2lem9.5	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (II ↾_t 𝑈) ∈ Conn)
185	26, 160	sseldd 3938	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑍 ∈ (0[,]1))
186		restsn2 23074	. . . . . . . . . . . . . . . . 17 ⊢ ((II ∈ (TopOn‘(0[,]1)) ∧ 𝑍 ∈ (0[,]1)) → (II ↾_t {𝑍}) = 𝒫 {𝑍})
187	63, 185, 186	sylancr 587	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (II ↾_t {𝑍}) = 𝒫 {𝑍})
188		pwsn 4854	. . . . . . . . . . . . . . . . 17 ⊢ 𝒫 {𝑍} = {∅, {𝑍}}
189		indisconn 23321	. . . . . . . . . . . . . . . . 17 ⊢ {∅, {𝑍}} ∈ Conn
190	188, 189	eqeltri 2824	. . . . . . . . . . . . . . . 16 ⊢ 𝒫 {𝑍} ∈ Conn
191	187, 190	eqeltrdi 2836	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (II ↾_t {𝑍}) ∈ Conn)
192		txconn 23592	. . . . . . . . . . . . . . 15 ⊢ (((II ↾_t 𝑈) ∈ Conn ∧ (II ↾_t {𝑍}) ∈ Conn) → ((II ↾_t 𝑈) ×_t (II ↾_t {𝑍})) ∈ Conn)
193	184, 191, 192	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((II ↾_t 𝑈) ×_t (II ↾_t {𝑍})) ∈ Conn)
194	183, 193	eqeltrd 2828	. . . . . . . . . . . . 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 5636	. . . . . . . . . . . . . . . 16 ⊢ (𝐾 “ (𝑈 × {𝑍})) = ran (𝐾 ↾ (𝑈 × {𝑍}))
198	160	snssd 4763	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → {𝑍} ⊆ 𝑉)
199		xpss2 5643	. . . . . . . . . . . . . . . . . 18 ⊢ ({𝑍} ⊆ 𝑉 → (𝑈 × {𝑍}) ⊆ (𝑈 × 𝑉))
200		imass2 6057	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑈 × {𝑍}) ⊆ (𝑈 × 𝑉) → (𝐾 “ (𝑈 × {𝑍})) ⊆ (𝐾 “ (𝑈 × 𝑉)))
201	198, 199, 200	3syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐾 “ (𝑈 × {𝑍})) ⊆ (𝐾 “ (𝑈 × 𝑉)))
202	201, 124	sstrd 3948	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐾 “ (𝑈 × {𝑍})) ⊆ (^◡𝐹 “ 𝑀))
203	197, 202	eqsstrrid 3977	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ran (𝐾 ↾ (𝑈 × {𝑍})) ⊆ (^◡𝐹 “ 𝑀))
204		cnrest2 23189	. . . . . . . . . . . . . . 15 ⊢ ((𝐶 ∈ (TopOn‘𝐵) ∧ ran (𝐾 ↾ (𝑈 × {𝑍})) ⊆ (^◡𝐹 “ 𝑀) ∧ (^◡𝐹 “ 𝑀) ⊆ 𝐵) → ((𝐾 ↾ (𝑈 × {𝑍})) ∈ (((II ×_t II) ↾_t (𝑈 × {𝑍})) Cn 𝐶) ↔ (𝐾 ↾ (𝑈 × {𝑍})) ∈ (((II ×_t II) ↾_t (𝑈 × {𝑍})) Cn (𝐶 ↾_t (^◡𝐹 “ 𝑀)))))
205	196, 203, 135, 204	syl3anc 1373	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐾 ↾ (𝑈 × {𝑍})) ∈ (((II ×_t II) ↾_t (𝑈 × {𝑍})) Cn 𝐶) ↔ (𝐾 ↾ (𝑈 × {𝑍})) ∈ (((II ×_t II) ↾_t (𝑈 × {𝑍})) Cn (𝐶 ↾_t (^◡𝐹 “ 𝑀)))))
206	195, 205	mpbid 232	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐾 ↾ (𝑈 × {𝑍})) ∈ (((II ×_t II) ↾_t (𝑈 × {𝑍})) Cn (𝐶 ↾_t (^◡𝐹 “ 𝑀))))
207		opelxpi 5660	. . . . . . . . . . . . . . 15 ⊢ ((𝑋 ∈ 𝑈 ∧ 𝑍 ∈ {𝑍}) → ⟨𝑋, 𝑍⟩ ∈ (𝑈 × {𝑍}))
208	21, 172, 207	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ⟨𝑋, 𝑍⟩ ∈ (𝑈 × {𝑍}))
209	185	snssd 4763	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → {𝑍} ⊆ (0[,]1))
210		xpss12 5638	. . . . . . . . . . . . . . . 16 ⊢ ((𝑈 ⊆ (0[,]1) ∧ {𝑍} ⊆ (0[,]1)) → (𝑈 × {𝑍}) ⊆ ((0[,]1) × (0[,]1)))
211	20, 209, 210	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑈 × {𝑍}) ⊆ ((0[,]1) × (0[,]1)))
212	4	restuni 23065	. . . . . . . . . . . . . . 15 ⊢ (((II ×_t II) ∈ Top ∧ (𝑈 × {𝑍}) ⊆ ((0[,]1) × (0[,]1))) → (𝑈 × {𝑍}) = ∪ ((II ×_t II) ↾_t (𝑈 × {𝑍})))
213	15, 211, 212	sylancr 587	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑈 × {𝑍}) = ∪ ((II ×_t II) ↾_t (𝑈 × {𝑍})))
214	208, 213	eleqtrd 2830	. . . . . . . . . . . . 13 ⊢ (𝜑 → ⟨𝑋, 𝑍⟩ ∈ ∪ ((II ×_t II) ↾_t (𝑈 × {𝑍})))
215		df-ov 7356	. . . . . . . . . . . . . . 15 ⊢ (𝑋(𝐾 ↾ (𝑈 × {𝑍}))𝑍) = ((𝐾 ↾ (𝑈 × {𝑍}))‘⟨𝑋, 𝑍⟩)
216		ovres 7519	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑋 ∈ 𝑈 ∧ 𝑍 ∈ {𝑍}) → (𝑋(𝐾 ↾ (𝑈 × {𝑍}))𝑍) = (𝑋𝐾𝑍))
217	21, 172, 216	syl2anc 584	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑋(𝐾 ↾ (𝑈 × {𝑍}))𝑍) = (𝑋𝐾𝑍))
218		snidg 4614	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑋 ∈ 𝑈 → 𝑋 ∈ {𝑋})
219	21, 218	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑋 ∈ {𝑋})
220		ovres 7519	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑋 ∈ {𝑋} ∧ 𝑍 ∈ 𝑉) → (𝑋(𝐾 ↾ ({𝑋} × 𝑉))𝑍) = (𝑋𝐾𝑍))
221	219, 160, 220	syl2anc 584	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑋(𝐾 ↾ ({𝑋} × 𝑉))𝑍) = (𝑋𝐾𝑍))
222	217, 221	eqtr4d 2767	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑋(𝐾 ↾ (𝑈 × {𝑍}))𝑍) = (𝑋(𝐾 ↾ ({𝑋} × 𝑉))𝑍))
223	215, 222	eqtr3id 2778	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐾 ↾ (𝑈 × {𝑍}))‘⟨𝑋, 𝑍⟩) = (𝑋(𝐾 ↾ ({𝑋} × 𝑉))𝑍))
224		eqid 2729	. . . . . . . . . . . . . . . . 17 ⊢ ∪ ((II ×_t II) ↾_t ({𝑋} × 𝑉)) = ∪ ((II ×_t II) ↾_t ({𝑋} × 𝑉))
225		snex 5378	. . . . . . . . . . . . . . . . . . . 20 ⊢ {𝑋} ∈ V
226	225	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → {𝑋} ∈ V)
227		txrest 23534	. . . . . . . . . . . . . . . . . . 19 ⊢ (((II ∈ Top ∧ II ∈ Top) ∧ ({𝑋} ∈ V ∧ 𝑉 ∈ II)) → ((II ×_t II) ↾_t ({𝑋} × 𝑉)) = ((II ↾_t {𝑋}) ×_t (II ↾_t 𝑉)))
228	179, 179, 226, 23, 227	syl22anc 838	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((II ×_t II) ↾_t ({𝑋} × 𝑉)) = ((II ↾_t {𝑋}) ×_t (II ↾_t 𝑉)))
229		restsn2 23074	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((II ∈ (TopOn‘(0[,]1)) ∧ 𝑋 ∈ (0[,]1)) → (II ↾_t {𝑋}) = 𝒫 {𝑋})
230	63, 22, 229	sylancr 587	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (II ↾_t {𝑋}) = 𝒫 {𝑋})
231		pwsn 4854	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝒫 {𝑋} = {∅, {𝑋}}
232		indisconn 23321	. . . . . . . . . . . . . . . . . . . . 21 ⊢ {∅, {𝑋}} ∈ Conn
233	231, 232	eqeltri 2824	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝒫 {𝑋} ∈ Conn
234	230, 233	eqeltrdi 2836	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (II ↾_t {𝑋}) ∈ Conn)
235		txconn 23592	. . . . . . . . . . . . . . . . . . 19 ⊢ (((II ↾_t {𝑋}) ∈ Conn ∧ (II ↾_t 𝑉) ∈ Conn) → ((II ↾_t {𝑋}) ×_t (II ↾_t 𝑉)) ∈ Conn)
236	234, 72, 235	syl2anc 584	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((II ↾_t {𝑋}) ×_t (II ↾_t 𝑉)) ∈ Conn)
237	228, 236	eqeltrd 2828	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((II ×_t II) ↾_t ({𝑋} × 𝑉)) ∈ Conn)
238	1, 6, 7, 8, 9, 10, 11	cvmlift2lem6 35280	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑋 ∈ (0[,]1)) → (𝐾 ↾ ({𝑋} × (0[,]1))) ∈ (((II ×_t II) ↾_t ({𝑋} × (0[,]1))) Cn 𝐶))
239	22, 238	mpdan 687	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐾 ↾ ({𝑋} × (0[,]1))) ∈ (((II ×_t II) ↾_t ({𝑋} × (0[,]1))) Cn 𝐶))
240		xpss2 5643	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑉 ⊆ (0[,]1) → ({𝑋} × 𝑉) ⊆ ({𝑋} × (0[,]1)))
241	23, 25, 240	3syl 18	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ({𝑋} × 𝑉) ⊆ ({𝑋} × (0[,]1)))
242	22	snssd 4763	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → {𝑋} ⊆ (0[,]1))
243		xpss1 5642	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ({𝑋} ⊆ (0[,]1) → ({𝑋} × (0[,]1)) ⊆ ((0[,]1) × (0[,]1)))
244	242, 243	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ({𝑋} × (0[,]1)) ⊆ ((0[,]1) × (0[,]1)))
245	4	restuni 23065	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((II ×_t II) ∈ Top ∧ ({𝑋} × (0[,]1)) ⊆ ((0[,]1) × (0[,]1))) → ({𝑋} × (0[,]1)) = ∪ ((II ×_t II) ↾_t ({𝑋} × (0[,]1))))
246	15, 244, 245	sylancr 587	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ({𝑋} × (0[,]1)) = ∪ ((II ×_t II) ↾_t ({𝑋} × (0[,]1))))
247	241, 246	sseqtrd 3974	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ({𝑋} × 𝑉) ⊆ ∪ ((II ×_t II) ↾_t ({𝑋} × (0[,]1))))
248		eqid 2729	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ∪ ((II ×_t II) ↾_t ({𝑋} × (0[,]1))) = ∪ ((II ×_t II) ↾_t ({𝑋} × (0[,]1)))
249	248	cnrest 23188	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐾 ↾ ({𝑋} × (0[,]1))) ∈ (((II ×_t II) ↾_t ({𝑋} × (0[,]1))) Cn 𝐶) ∧ ({𝑋} × 𝑉) ⊆ ∪ ((II ×_t II) ↾_t ({𝑋} × (0[,]1)))) → ((𝐾 ↾ ({𝑋} × (0[,]1))) ↾ ({𝑋} × 𝑉)) ∈ ((((II ×_t II) ↾_t ({𝑋} × (0[,]1))) ↾_t ({𝑋} × 𝑉)) Cn 𝐶))
250	239, 247, 249	syl2anc 584	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝐾 ↾ ({𝑋} × (0[,]1))) ↾ ({𝑋} × 𝑉)) ∈ ((((II ×_t II) ↾_t ({𝑋} × (0[,]1))) ↾_t ({𝑋} × 𝑉)) Cn 𝐶))
251	241	resabs1d 5963	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝐾 ↾ ({𝑋} × (0[,]1))) ↾ ({𝑋} × 𝑉)) = (𝐾 ↾ ({𝑋} × 𝑉)))
252	225, 93	xpex 7693	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ({𝑋} × (0[,]1)) ∈ V
253	252	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ({𝑋} × (0[,]1)) ∈ V)
254		restabs 23068	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((II ×_t II) ∈ Top ∧ ({𝑋} × 𝑉) ⊆ ({𝑋} × (0[,]1)) ∧ ({𝑋} × (0[,]1)) ∈ V) → (((II ×_t II) ↾_t ({𝑋} × (0[,]1))) ↾_t ({𝑋} × 𝑉)) = ((II ×_t II) ↾_t ({𝑋} × 𝑉)))
255	16, 241, 253, 254	syl3anc 1373	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (((II ×_t II) ↾_t ({𝑋} × (0[,]1))) ↾_t ({𝑋} × 𝑉)) = ((II ×_t II) ↾_t ({𝑋} × 𝑉)))
256	255	oveq1d 7368	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((((II ×_t II) ↾_t ({𝑋} × (0[,]1))) ↾_t ({𝑋} × 𝑉)) Cn 𝐶) = (((II ×_t II) ↾_t ({𝑋} × 𝑉)) Cn 𝐶))
257	250, 251, 256	3eltr3d 2842	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐾 ↾ ({𝑋} × 𝑉)) ∈ (((II ×_t II) ↾_t ({𝑋} × 𝑉)) Cn 𝐶))
258		df-ima 5636	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐾 “ ({𝑋} × 𝑉)) = ran (𝐾 ↾ ({𝑋} × 𝑉))
259	21	snssd 4763	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → {𝑋} ⊆ 𝑈)
260		xpss1 5642	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ({𝑋} ⊆ 𝑈 → ({𝑋} × 𝑉) ⊆ (𝑈 × 𝑉))
261		imass2 6057	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (({𝑋} × 𝑉) ⊆ (𝑈 × 𝑉) → (𝐾 “ ({𝑋} × 𝑉)) ⊆ (𝐾 “ (𝑈 × 𝑉)))
262	259, 260, 261	3syl 18	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝐾 “ ({𝑋} × 𝑉)) ⊆ (𝐾 “ (𝑈 × 𝑉)))
263	262, 124	sstrd 3948	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐾 “ ({𝑋} × 𝑉)) ⊆ (^◡𝐹 “ 𝑀))
264	258, 263	eqsstrrid 3977	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ran (𝐾 ↾ ({𝑋} × 𝑉)) ⊆ (^◡𝐹 “ 𝑀))
265		cnrest2 23189	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐶 ∈ (TopOn‘𝐵) ∧ ran (𝐾 ↾ ({𝑋} × 𝑉)) ⊆ (^◡𝐹 “ 𝑀) ∧ (^◡𝐹 “ 𝑀) ⊆ 𝐵) → ((𝐾 ↾ ({𝑋} × 𝑉)) ∈ (((II ×_t II) ↾_t ({𝑋} × 𝑉)) Cn 𝐶) ↔ (𝐾 ↾ ({𝑋} × 𝑉)) ∈ (((II ×_t II) ↾_t ({𝑋} × 𝑉)) Cn (𝐶 ↾_t (^◡𝐹 “ 𝑀)))))
266	196, 264, 135, 265	syl3anc 1373	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝐾 ↾ ({𝑋} × 𝑉)) ∈ (((II ×_t II) ↾_t ({𝑋} × 𝑉)) Cn 𝐶) ↔ (𝐾 ↾ ({𝑋} × 𝑉)) ∈ (((II ×_t II) ↾_t ({𝑋} × 𝑉)) Cn (𝐶 ↾_t (^◡𝐹 “ 𝑀)))))
267	257, 266	mpbid 232	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐾 ↾ ({𝑋} × 𝑉)) ∈ (((II ×_t II) ↾_t ({𝑋} × 𝑉)) Cn (𝐶 ↾_t (^◡𝐹 “ 𝑀))))
268		opelxpi 5660	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑋 ∈ {𝑋} ∧ 𝑌 ∈ 𝑉) → ⟨𝑋, 𝑌⟩ ∈ ({𝑋} × 𝑉))
269	219, 27, 268	syl2anc 584	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ⟨𝑋, 𝑌⟩ ∈ ({𝑋} × 𝑉))
270	259, 260	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ({𝑋} × 𝑉) ⊆ (𝑈 × 𝑉))
271	270, 50	sstrd 3948	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ({𝑋} × 𝑉) ⊆ ((0[,]1) × (0[,]1)))
272	4	restuni 23065	. . . . . . . . . . . . . . . . . . 19 ⊢ (((II ×_t II) ∈ Top ∧ ({𝑋} × 𝑉) ⊆ ((0[,]1) × (0[,]1))) → ({𝑋} × 𝑉) = ∪ ((II ×_t II) ↾_t ({𝑋} × 𝑉)))
273	15, 271, 272	sylancr 587	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ({𝑋} × 𝑉) = ∪ ((II ×_t II) ↾_t ({𝑋} × 𝑉)))
274	269, 273	eleqtrd 2830	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ⟨𝑋, 𝑌⟩ ∈ ∪ ((II ×_t II) ↾_t ({𝑋} × 𝑉)))
275		df-ov 7356	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑋(𝐾 ↾ ({𝑋} × 𝑉))𝑌) = ((𝐾 ↾ ({𝑋} × 𝑉))‘⟨𝑋, 𝑌⟩)
276		ovres 7519	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑋 ∈ {𝑋} ∧ 𝑌 ∈ 𝑉) → (𝑋(𝐾 ↾ ({𝑋} × 𝑉))𝑌) = (𝑋𝐾𝑌))
277	219, 27, 276	syl2anc 584	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑋(𝐾 ↾ ({𝑋} × 𝑉))𝑌) = (𝑋𝐾𝑌))
278	275, 277	eqtr3id 2778	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝐾 ↾ ({𝑋} × 𝑉))‘⟨𝑋, 𝑌⟩) = (𝑋𝐾𝑌))
279	45	simprd 495	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑋𝐾𝑌) ∈ 𝑊)
280	278, 279	eqeltrd 2828	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝐾 ↾ ({𝑋} × 𝑉))‘⟨𝑋, 𝑌⟩) ∈ 𝑊)
281	224, 237, 267, 155, 158, 274, 280	conncn 23329	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐾 ↾ ({𝑋} × 𝑉)):∪ ((II ×_t II) ↾_t ({𝑋} × 𝑉))⟶𝑊)
282	273	feq2d 6640	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐾 ↾ ({𝑋} × 𝑉)):({𝑋} × 𝑉)⟶𝑊 ↔ (𝐾 ↾ ({𝑋} × 𝑉)):∪ ((II ×_t II) ↾_t ({𝑋} × 𝑉))⟶𝑊))
283	281, 282	mpbird 257	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐾 ↾ ({𝑋} × 𝑉)):({𝑋} × 𝑉)⟶𝑊)
284	283, 219, 160	fovcdmd 7525	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑋(𝐾 ↾ ({𝑋} × 𝑉))𝑍) ∈ 𝑊)
285	223, 284	eqeltrd 2828	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐾 ↾ (𝑈 × {𝑍}))‘⟨𝑋, 𝑍⟩) ∈ 𝑊)
286	178, 194, 206, 155, 158, 214, 285	conncn 23329	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐾 ↾ (𝑈 × {𝑍})):∪ ((II ×_t II) ↾_t (𝑈 × {𝑍}))⟶𝑊)
287	213	feq2d 6640	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐾 ↾ (𝑈 × {𝑍})):(𝑈 × {𝑍})⟶𝑊 ↔ (𝐾 ↾ (𝑈 × {𝑍})):∪ ((II ×_t II) ↾_t (𝑈 × {𝑍}))⟶𝑊))
288	286, 287	mpbird 257	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐾 ↾ (𝑈 × {𝑍})):(𝑈 × {𝑍})⟶𝑊)
289	288	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → (𝐾 ↾ (𝑈 × {𝑍})):(𝑈 × {𝑍})⟶𝑊)
290	289, 106, 173	fovcdmd 7525	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → (𝑚(𝐾 ↾ (𝑈 × {𝑍}))𝑍) ∈ 𝑊)
291	177, 290	eqeltrd 2828	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → ((𝐾 ↾ ({𝑚} × 𝑉))‘⟨𝑚, 𝑍⟩) ∈ 𝑊)
292	56, 76, 139, 156, 159, 167, 291	conncn 23329	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → (𝐾 ↾ ({𝑚} × 𝑉)):∪ ((II ×_t II) ↾_t ({𝑚} × 𝑉))⟶𝑊)
293	166	feq2d 6640	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → ((𝐾 ↾ ({𝑚} × 𝑉)):({𝑚} × 𝑉)⟶𝑊 ↔ (𝐾 ↾ ({𝑚} × 𝑉)):∪ ((II ×_t II) ↾_t ({𝑚} × 𝑉))⟶𝑊))
294	292, 293	mpbird 257	. . . . . 6 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → (𝐾 ↾ ({𝑚} × 𝑉)):({𝑚} × 𝑉)⟶𝑊)
295	294, 52, 53	fovcdmd 7525	. . . . 5 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → (𝑚(𝐾 ↾ ({𝑚} × 𝑉))𝑛) ∈ 𝑊)
296	55, 295	eqeltrrd 2829	. . . 4 ⊢ ((𝜑 ∧ (𝑚 ∈ 𝑈 ∧ 𝑛 ∈ 𝑉)) → (𝑚𝐾𝑛) ∈ 𝑊)
297	296	ralrimivva 3172	. . 3 ⊢ (𝜑 → ∀𝑚 ∈ 𝑈 ∀𝑛 ∈ 𝑉 (𝑚𝐾𝑛) ∈ 𝑊)
298		funimassov 7530	. . . 4 ⊢ ((Fun 𝐾 ∧ (𝑈 × 𝑉) ⊆ dom 𝐾) → ((𝐾 “ (𝑈 × 𝑉)) ⊆ 𝑊 ↔ ∀𝑚 ∈ 𝑈 ∀𝑛 ∈ 𝑉 (𝑚𝐾𝑛) ∈ 𝑊))
299	119, 121, 298	syl2anc 584	. . 3 ⊢ (𝜑 → ((𝐾 “ (𝑈 × 𝑉)) ⊆ 𝑊 ↔ ∀𝑚 ∈ 𝑈 ∀𝑛 ∈ 𝑉 (𝑚𝐾𝑛) ∈ 𝑊))
300	297, 299	mpbird 257	. 2 ⊢ (𝜑 → (𝐾 “ (𝑈 × 𝑉)) ⊆ 𝑊)
301	1, 4, 5, 6, 12, 14, 16, 30, 31, 48, 50, 300	cvmlift2lem9a 35275	1 ⊢ (𝜑 → (𝐾 ↾ (𝑈 × 𝑉)) ∈ (((II ×_t II) ↾_t (𝑈 × 𝑉)) Cn 𝐶))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1540 ∈ wcel 2109 ∀wral 3044 {crab 3396 Vcvv 3438 ∖ cdif 3902 ∩ cin 3904 ⊆ wss 3905 ∅c0 4286 𝒫 cpw 4553 {csn 4579 {cpr 4581 ⟨cop 4585 ∪ cuni 4861 ↦ cmpt 5176 × cxp 5621 ^◡ccnv 5622 dom cdm 5623 ran crn 5624 ↾ cres 5625 “ cima 5626 ∘ ccom 5627 Fun wfun 6480 ⟶wf 6482 ‘cfv 6486 ℩crio 7309 (class class class)co 7353 ∈ cmpo 7355 0cc0 11028 1c1 11029 [,]cicc 13269 ↾_t crest 17342 Topctop 22796 TopOnctopon 22813 Clsdccld 22919 Cn ccn 23127 Conncconn 23314 ×_t ctx 23463 Homeochmeo 23656 IIcii 24784 CovMap ccvm 35227

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-rep 5221 ax-sep 5238 ax-nul 5248 ax-pow 5307 ax-pr 5374 ax-un 7675 ax-inf2 9556 ax-cnex 11084 ax-resscn 11085 ax-1cn 11086 ax-icn 11087 ax-addcl 11088 ax-addrcl 11089 ax-mulcl 11090 ax-mulrcl 11091 ax-mulcom 11092 ax-addass 11093 ax-mulass 11094 ax-distr 11095 ax-i2m1 11096 ax-1ne0 11097 ax-1rid 11098 ax-rnegex 11099 ax-rrecex 11100 ax-cnre 11101 ax-pre-lttri 11102 ax-pre-lttrn 11103 ax-pre-ltadd 11104 ax-pre-mulgt0 11105 ax-pre-sup 11106 ax-addf 11107

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-nel 3030 df-ral 3045 df-rex 3054 df-rmo 3345 df-reu 3346 df-rab 3397 df-v 3440 df-sbc 3745 df-csb 3854 df-dif 3908 df-un 3910 df-in 3912 df-ss 3922 df-pss 3925 df-nul 4287 df-if 4479 df-pw 4555 df-sn 4580 df-pr 4582 df-tp 4584 df-op 4586 df-uni 4862 df-int 4900 df-iun 4946 df-iin 4947 df-br 5096 df-opab 5158 df-mpt 5177 df-tr 5203 df-id 5518 df-eprel 5523 df-po 5531 df-so 5532 df-fr 5576 df-se 5577 df-we 5578 df-xp 5629 df-rel 5630 df-cnv 5631 df-co 5632 df-dm 5633 df-rn 5634 df-res 5635 df-ima 5636 df-pred 6253 df-ord 6314 df-on 6315 df-lim 6316 df-suc 6317 df-iota 6442 df-fun 6488 df-fn 6489 df-f 6490 df-f1 6491 df-fo 6492 df-f1o 6493 df-fv 6494 df-isom 6495 df-riota 7310 df-ov 7356 df-oprab 7357 df-mpo 7358 df-of 7617 df-om 7807 df-1st 7931 df-2nd 7932 df-supp 8101 df-frecs 8221 df-wrecs 8252 df-recs 8301 df-rdg 8339 df-1o 8395 df-2o 8396 df-er 8632 df-ec 8634 df-map 8762 df-ixp 8832 df-en 8880 df-dom 8881 df-sdom 8882 df-fin 8883 df-fsupp 9271 df-fi 9320 df-sup 9351 df-inf 9352 df-oi 9421 df-card 9854 df-pnf 11170 df-mnf 11171 df-xr 11172 df-ltxr 11173 df-le 11174 df-sub 11367 df-neg 11368 df-div 11796 df-nn 12147 df-2 12209 df-3 12210 df-4 12211 df-5 12212 df-6 12213 df-7 12214 df-8 12215 df-9 12216 df-n0 12403 df-z 12490 df-dec 12610 df-uz 12754 df-q 12868 df-rp 12912 df-xneg 13032 df-xadd 13033 df-xmul 13034 df-ioo 13270 df-ico 13272 df-icc 13273 df-fz 13429 df-fzo 13576 df-fl 13714 df-seq 13927 df-exp 13987 df-hash 14256 df-cj 15024 df-re 15025 df-im 15026 df-sqrt 15160 df-abs 15161 df-clim 15413 df-sum 15612 df-struct 17076 df-sets 17093 df-slot 17111 df-ndx 17123 df-base 17139 df-ress 17160 df-plusg 17192 df-mulr 17193 df-starv 17194 df-sca 17195 df-vsca 17196 df-ip 17197 df-tset 17198 df-ple 17199 df-ds 17201 df-unif 17202 df-hom 17203 df-cco 17204 df-rest 17344 df-topn 17345 df-0g 17363 df-gsum 17364 df-topgen 17365 df-pt 17366 df-prds 17369 df-xrs 17424 df-qtop 17429 df-imas 17430 df-xps 17432 df-mre 17506 df-mrc 17507 df-acs 17509 df-mgm 18532 df-sgrp 18611 df-mnd 18627 df-submnd 18676 df-mulg 18965 df-cntz 19214 df-cmn 19679 df-psmet 21271 df-xmet 21272 df-met 21273 df-bl 21274 df-mopn 21275 df-cnfld 21280 df-top 22797 df-topon 22814 df-topsp 22836 df-bases 22849 df-cld 22922 df-ntr 22923 df-cls 22924 df-nei 23001 df-cn 23130 df-cnp 23131 df-cmp 23290 df-conn 23315 df-lly 23369 df-nlly 23370 df-tx 23465 df-hmeo 23658 df-xms 24224 df-ms 24225 df-tms 24226 df-ii 24786 df-cncf 24787 df-htpy 24885 df-phtpy 24886 df-phtpc 24907 df-pconn 35193 df-sconn 35194 df-cvm 35228

This theorem is referenced by: cvmlift2lem10 35284

W3C validator