cvmlift2lem12 - Mathbox for Mario Carneiro

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

Theorem cvmlift2lem12 35628

Description: Lemma for cvmlift2 35630. (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) = (𝐻‘𝑥)))‘𝑦))
cvmlift2.m	⊢ 𝑀 = {𝑧 ∈ ((0[,]1) × (0[,]1)) ∣ 𝐾 ∈ (((II ×_t II) CnP 𝐶)‘𝑧)}
cvmlift2.a	⊢ 𝐴 = {𝑎 ∈ (0[,]1) ∣ ((0[,]1) × {𝑎}) ⊆ 𝑀}
cvmlift2.s	⊢ 𝑆 = {⟨𝑟, 𝑡⟩ ∣ (𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀))}

**Assertion**
Ref	Expression
cvmlift2lem12	⊢ (𝜑 → 𝐾 ∈ ((II ×_t II) Cn 𝐶))

Distinct variable groups: 𝑢,𝑓,𝑥,𝑦,𝑧,𝐹 𝑓,𝑎,𝑟,𝑡,𝑢,𝑥,𝑦,𝑧,𝜑 𝐴,𝑎,𝑡,𝑥 𝑀,𝑎,𝑟,𝑢,𝑥,𝑦,𝑧 𝑆,𝑓,𝑡,𝑢,𝑥,𝑦,𝑧 𝑓,𝐽,𝑢,𝑥,𝑦,𝑧 𝐺,𝑎,𝑓,𝑡,𝑢,𝑥,𝑦,𝑧 𝑓,𝐻,𝑢,𝑥,𝑦,𝑧 𝐶,𝑎,𝑓,𝑟,𝑡,𝑢,𝑥,𝑦,𝑧 𝑃,𝑓,𝑢,𝑥,𝑦,𝑧 𝑥,𝐵,𝑦,𝑧 𝐾,𝑎,𝑓,𝑟,𝑡,𝑢,𝑥,𝑦,𝑧 Allowed substitution hints: 𝐴(𝑦,𝑧,𝑢,𝑓,𝑟) 𝐵(𝑢,𝑡,𝑓,𝑟,𝑎) 𝑃(𝑡,𝑟,𝑎) 𝑆(𝑟,𝑎) 𝐹(𝑡,𝑟,𝑎) 𝐺(𝑟) 𝐻(𝑡,𝑟,𝑎) 𝐽(𝑡,𝑟,𝑎) 𝑀(𝑡,𝑓)

Proof of Theorem cvmlift2lem12 Dummy variables 𝑏 𝑐 𝑑 𝑘 𝑠 𝑣 𝑤 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		cvmlift2.b	. . 3 ⊢ 𝐵 = ∪ 𝐶
2		cvmlift2.f	. . 3 ⊢ (𝜑 → 𝐹 ∈ (𝐶 CovMap 𝐽))
3		cvmlift2.g	. . 3 ⊢ (𝜑 → 𝐺 ∈ ((II ×_t II) Cn 𝐽))
4		cvmlift2.p	. . 3 ⊢ (𝜑 → 𝑃 ∈ 𝐵)
5		cvmlift2.i	. . 3 ⊢ (𝜑 → (𝐹‘𝑃) = (0𝐺0))
6		cvmlift2.h	. . 3 ⊢ 𝐻 = (℩𝑓 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑓) = (𝑧 ∈ (0[,]1) ↦ (𝑧𝐺0)) ∧ (𝑓‘0) = 𝑃))
7		cvmlift2.k	. . 3 ⊢ 𝐾 = (𝑥 ∈ (0[,]1), 𝑦 ∈ (0[,]1) ↦ ((℩𝑓 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑓) = (𝑧 ∈ (0[,]1) ↦ (𝑥𝐺𝑧)) ∧ (𝑓‘0) = (𝐻‘𝑥)))‘𝑦))
8	1, 2, 3, 4, 5, 6, 7	cvmlift2lem5 35621	. 2 ⊢ (𝜑 → 𝐾:((0[,]1) × (0[,]1))⟶𝐵)
9		iunid 5017	. . . . . . 7 ⊢ ∪ 𝑎 ∈ (0[,]1){𝑎} = (0[,]1)
10	9	xpeq2i 5672	. . . . . 6 ⊢ ((0[,]1) × ∪ 𝑎 ∈ (0[,]1){𝑎}) = ((0[,]1) × (0[,]1))
11		xpiundi 5716	. . . . . 6 ⊢ ((0[,]1) × ∪ 𝑎 ∈ (0[,]1){𝑎}) = ∪ 𝑎 ∈ (0[,]1)((0[,]1) × {𝑎})
12	10, 11	eqtr3i 2786	. . . . 5 ⊢ ((0[,]1) × (0[,]1)) = ∪ 𝑎 ∈ (0[,]1)((0[,]1) × {𝑎})
13		iiuni 24923	. . . . . . . . 9 ⊢ (0[,]1) = ∪ II
14		iiconn 24929	. . . . . . . . . 10 ⊢ II ∈ Conn
15	14	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → II ∈ Conn)
16		inss1 4188	. . . . . . . . . 10 ⊢ (II ∩ (Clsd‘II)) ⊆ II
17		iicmp 24928	. . . . . . . . . . . . . . 15 ⊢ II ∈ Comp
18	17	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑎 ∈ (0[,]1)) → II ∈ Comp)
19		iitop 24922	. . . . . . . . . . . . . . 15 ⊢ II ∈ Top
20	19	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑎 ∈ (0[,]1)) → II ∈ Top)
21	19, 19	txtopi 23630	. . . . . . . . . . . . . . . 16 ⊢ (II ×_t II) ∈ Top
22	13	neiss2 23141	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((II ∈ Top ∧ 𝑢 ∈ ((nei‘II)‘{𝑟})) → {𝑟} ⊆ (0[,]1))
23	19, 22	mpan 700	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑢 ∈ ((nei‘II)‘{𝑟}) → {𝑟} ⊆ (0[,]1))
24		vex 3457	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 𝑟 ∈ V
25	24	snss 4742	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑟 ∈ (0[,]1) ↔ {𝑟} ⊆ (0[,]1))
26	23, 25	sylibr 236	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑢 ∈ ((nei‘II)‘{𝑟}) → 𝑟 ∈ (0[,]1))
27	26	a1d 25	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑢 ∈ ((nei‘II)‘{𝑟}) → (((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀) → 𝑟 ∈ (0[,]1)))
28	27	rexlimiv 3155	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀) → 𝑟 ∈ (0[,]1))
29	28	adantl 485	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀)) → 𝑟 ∈ (0[,]1))
30		simpl 486	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀)) → 𝑡 ∈ (0[,]1))
31	29, 30	jca 519	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀)) → (𝑟 ∈ (0[,]1) ∧ 𝑡 ∈ (0[,]1)))
32	31	ssopab2i 5519	. . . . . . . . . . . . . . . . 17 ⊢ {⟨𝑟, 𝑡⟩ ∣ (𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀))} ⊆ {⟨𝑟, 𝑡⟩ ∣ (𝑟 ∈ (0[,]1) ∧ 𝑡 ∈ (0[,]1))}
33		cvmlift2.s	. . . . . . . . . . . . . . . . 17 ⊢ 𝑆 = {⟨𝑟, 𝑡⟩ ∣ (𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀))}
34		df-xp 5651	. . . . . . . . . . . . . . . . 17 ⊢ ((0[,]1) × (0[,]1)) = {⟨𝑟, 𝑡⟩ ∣ (𝑟 ∈ (0[,]1) ∧ 𝑡 ∈ (0[,]1))}
35	32, 33, 34	3sstr4i 3987	. . . . . . . . . . . . . . . 16 ⊢ 𝑆 ⊆ ((0[,]1) × (0[,]1))
36	19, 19, 13, 13	txunii 23633	. . . . . . . . . . . . . . . . 17 ⊢ ((0[,]1) × (0[,]1)) = ∪ (II ×_t II)
37	36	ntropn 23089	. . . . . . . . . . . . . . . 16 ⊢ (((II ×_t II) ∈ Top ∧ 𝑆 ⊆ ((0[,]1) × (0[,]1))) → ((int‘(II ×_t II))‘𝑆) ∈ (II ×_t II))
38	21, 35, 37	mp2an 702	. . . . . . . . . . . . . . 15 ⊢ ((int‘(II ×_t II))‘𝑆) ∈ (II ×_t II)
39	38	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑎 ∈ (0[,]1)) → ((int‘(II ×_t II))‘𝑆) ∈ (II ×_t II))
40	2	adantr 484	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) → 𝐹 ∈ (𝐶 CovMap 𝐽))
41	3	adantr 484	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) → 𝐺 ∈ ((II ×_t II) Cn 𝐽))
42	4	adantr 484	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) → 𝑃 ∈ 𝐵)
43	5	adantr 484	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) → (𝐹‘𝑃) = (0𝐺0))
44		eqid 2761	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (^◡𝐹 “ 𝑘) ∧ ∀𝑐 ∈ 𝑠 (∀𝑑 ∈ (𝑠 ∖ {𝑐})(𝑐 ∩ 𝑑) = ∅ ∧ (𝐹 ↾ 𝑐) ∈ ((𝐶 ↾_t 𝑐)Homeo(𝐽 ↾_t 𝑘))))}) = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (^◡𝐹 “ 𝑘) ∧ ∀𝑐 ∈ 𝑠 (∀𝑑 ∈ (𝑠 ∖ {𝑐})(𝑐 ∩ 𝑑) = ∅ ∧ (𝐹 ↾ 𝑐) ∈ ((𝐶 ↾_t 𝑐)Homeo(𝐽 ↾_t 𝑘))))})
45		simprr 782	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) → 𝑏 ∈ (0[,]1))
46		simprl 780	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) → 𝑎 ∈ (0[,]1))
47	1, 40, 41, 42, 43, 6, 7, 44, 45, 46	cvmlift2lem10 35626	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) → ∃𝑢 ∈ II ∃𝑣 ∈ II (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×_t II) ↾_t (𝑢 × 𝑣)) Cn 𝐶))))
48	21	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×_t II) ↾_t (𝑢 × 𝑣)) Cn 𝐶)))) → (II ×_t II) ∈ Top)
49	35	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×_t II) ↾_t (𝑢 × 𝑣)) Cn 𝐶)))) → 𝑆 ⊆ ((0[,]1) × (0[,]1)))
50	19	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×_t II) ↾_t (𝑢 × 𝑣)) Cn 𝐶)))) → II ∈ Top)
51		simplrl 786	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×_t II) ↾_t (𝑢 × 𝑣)) Cn 𝐶)))) → 𝑢 ∈ II)
52		simplrr 787	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×_t II) ↾_t (𝑢 × 𝑣)) Cn 𝐶)))) → 𝑣 ∈ II)
53		txopn 23642	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((II ∈ Top ∧ II ∈ Top) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) → (𝑢 × 𝑣) ∈ (II ×_t II))
54	50, 50, 51, 52, 53	syl22anc 849	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×_t II) ↾_t (𝑢 × 𝑣)) Cn 𝐶)))) → (𝑢 × 𝑣) ∈ (II ×_t II))
55		simpr 488	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣) → 𝑡 ∈ 𝑣)
56		elunii 4869	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑡 ∈ 𝑣 ∧ 𝑣 ∈ II) → 𝑡 ∈ ∪ II)
57	56, 13	eleqtrrdi 2872	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑡 ∈ 𝑣 ∧ 𝑣 ∈ II) → 𝑡 ∈ (0[,]1))
58	55, 52, 57	syl2anr 606	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×_t II) ↾_t (𝑢 × 𝑣)) Cn 𝐶)))) ∧ (𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣)) → 𝑡 ∈ (0[,]1))
59	19	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×_t II) ↾_t (𝑢 × 𝑣)) Cn 𝐶)))) ∧ (𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣)) → II ∈ Top)
60	51	adantr 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×_t II) ↾_t (𝑢 × 𝑣)) Cn 𝐶)))) ∧ (𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣)) → 𝑢 ∈ II)
61		simprl 780	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×_t II) ↾_t (𝑢 × 𝑣)) Cn 𝐶)))) ∧ (𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣)) → 𝑟 ∈ 𝑢)
62		opnneip 23159	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((II ∈ Top ∧ 𝑢 ∈ II ∧ 𝑟 ∈ 𝑢) → 𝑢 ∈ ((nei‘II)‘{𝑟}))
63	59, 60, 61, 62	syl3anc 1389	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×_t II) ↾_t (𝑢 × 𝑣)) Cn 𝐶)))) ∧ (𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣)) → 𝑢 ∈ ((nei‘II)‘{𝑟}))
64	40	ad3antrrr 740	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×_t II) ↾_t (𝑢 × 𝑣)) Cn 𝐶)))) ∧ (𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣)) → 𝐹 ∈ (𝐶 CovMap 𝐽))
65	41	ad3antrrr 740	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×_t II) ↾_t (𝑢 × 𝑣)) Cn 𝐶)))) ∧ (𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣)) → 𝐺 ∈ ((II ×_t II) Cn 𝐽))
66	42	ad3antrrr 740	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×_t II) ↾_t (𝑢 × 𝑣)) Cn 𝐶)))) ∧ (𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣)) → 𝑃 ∈ 𝐵)
67	43	ad3antrrr 740	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×_t II) ↾_t (𝑢 × 𝑣)) Cn 𝐶)))) ∧ (𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣)) → (𝐹‘𝑃) = (0𝐺0))
68		cvmlift2.m	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ 𝑀 = {𝑧 ∈ ((0[,]1) × (0[,]1)) ∣ 𝐾 ∈ (((II ×_t II) CnP 𝐶)‘𝑧)}
69	52	adantr 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×_t II) ↾_t (𝑢 × 𝑣)) Cn 𝐶)))) ∧ (𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣)) → 𝑣 ∈ II)
70		simplr2 1229	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×_t II) ↾_t (𝑢 × 𝑣)) Cn 𝐶)))) ∧ (𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣)) → 𝑎 ∈ 𝑣)
71		simprr 782	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×_t II) ↾_t (𝑢 × 𝑣)) Cn 𝐶)))) ∧ (𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣)) → 𝑡 ∈ 𝑣)
72		sneq 4591	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑐 = 𝑤 → {𝑐} = {𝑤})
73	72	xpeq2d 5675	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑐 = 𝑤 → (𝑢 × {𝑐}) = (𝑢 × {𝑤}))
74	73	reseq2d 5963	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑐 = 𝑤 → (𝐾 ↾ (𝑢 × {𝑐})) = (𝐾 ↾ (𝑢 × {𝑤})))
75	73	oveq2d 7408	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑐 = 𝑤 → ((II ×_t II) ↾_t (𝑢 × {𝑐})) = ((II ×_t II) ↾_t (𝑢 × {𝑤})))
76	75	oveq1d 7407	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑐 = 𝑤 → (((II ×_t II) ↾_t (𝑢 × {𝑐})) Cn 𝐶) = (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶))
77	74, 76	eleq12d 2855	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑐 = 𝑤 → ((𝐾 ↾ (𝑢 × {𝑐})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑐})) Cn 𝐶) ↔ (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶)))
78	77	cbvrexvw 3240	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (∃𝑐 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑐})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑐})) Cn 𝐶) ↔ ∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶))
79		simplr3 1230	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×_t II) ↾_t (𝑢 × 𝑣)) Cn 𝐶)))) ∧ (𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣)) → (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×_t II) ↾_t (𝑢 × 𝑣)) Cn 𝐶)))
80	78, 79	biimtrid 244	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×_t II) ↾_t (𝑢 × 𝑣)) Cn 𝐶)))) ∧ (𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣)) → (∃𝑐 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑐})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑐})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×_t II) ↾_t (𝑢 × 𝑣)) Cn 𝐶)))
81	1, 64, 65, 66, 67, 6, 7, 68, 60, 69, 70, 71, 80	cvmlift2lem11 35627	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×_t II) ↾_t (𝑢 × 𝑣)) Cn 𝐶)))) ∧ (𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣)) → ((𝑢 × {𝑎}) ⊆ 𝑀 → (𝑢 × {𝑡}) ⊆ 𝑀))
82	1, 64, 65, 66, 67, 6, 7, 68, 60, 69, 71, 70, 80	cvmlift2lem11 35627	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×_t II) ↾_t (𝑢 × 𝑣)) Cn 𝐶)))) ∧ (𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣)) → ((𝑢 × {𝑡}) ⊆ 𝑀 → (𝑢 × {𝑎}) ⊆ 𝑀))
83	81, 82	impbid 214	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×_t II) ↾_t (𝑢 × 𝑣)) Cn 𝐶)))) ∧ (𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣)) → ((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀))
84		rspe 3251	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑢 ∈ ((nei‘II)‘{𝑟}) ∧ ((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀)) → ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀))
85	63, 83, 84	syl2anc 593	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×_t II) ↾_t (𝑢 × 𝑣)) Cn 𝐶)))) ∧ (𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣)) → ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀))
86	58, 85	jca 519	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×_t II) ↾_t (𝑢 × 𝑣)) Cn 𝐶)))) ∧ (𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣)) → (𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀)))
87	86	ex 416	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×_t II) ↾_t (𝑢 × 𝑣)) Cn 𝐶)))) → ((𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣) → (𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀))))
88	87	alrimivv 1947	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×_t II) ↾_t (𝑢 × 𝑣)) Cn 𝐶)))) → ∀𝑟∀𝑡((𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣) → (𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀))))
89		df-xp 5651	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑢 × 𝑣) = {⟨𝑟, 𝑡⟩ ∣ (𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣)}
90	89, 33	sseq12i 3966	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑢 × 𝑣) ⊆ 𝑆 ↔ {⟨𝑟, 𝑡⟩ ∣ (𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣)} ⊆ {⟨𝑟, 𝑡⟩ ∣ (𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀))})
91		ssopab2bw 5516	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ({⟨𝑟, 𝑡⟩ ∣ (𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣)} ⊆ {⟨𝑟, 𝑡⟩ ∣ (𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀))} ↔ ∀𝑟∀𝑡((𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣) → (𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀))))
92	90, 91	bitri 277	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑢 × 𝑣) ⊆ 𝑆 ↔ ∀𝑟∀𝑡((𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣) → (𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀))))
93	88, 92	sylibr 236	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×_t II) ↾_t (𝑢 × 𝑣)) Cn 𝐶)))) → (𝑢 × 𝑣) ⊆ 𝑆)
94	36	ssntr 23098	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((II ×_t II) ∈ Top ∧ 𝑆 ⊆ ((0[,]1) × (0[,]1))) ∧ ((𝑢 × 𝑣) ∈ (II ×_t II) ∧ (𝑢 × 𝑣) ⊆ 𝑆)) → (𝑢 × 𝑣) ⊆ ((int‘(II ×_t II))‘𝑆))
95	48, 49, 54, 93, 94	syl22anc 849	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×_t II) ↾_t (𝑢 × 𝑣)) Cn 𝐶)))) → (𝑢 × 𝑣) ⊆ ((int‘(II ×_t II))‘𝑆))
96		simpr1 1207	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×_t II) ↾_t (𝑢 × 𝑣)) Cn 𝐶)))) → 𝑏 ∈ 𝑢)
97		simpr2 1208	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×_t II) ↾_t (𝑢 × 𝑣)) Cn 𝐶)))) → 𝑎 ∈ 𝑣)
98		opelxpi 5682	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣) → ⟨𝑏, 𝑎⟩ ∈ (𝑢 × 𝑣))
99	96, 97, 98	syl2anc 593	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×_t II) ↾_t (𝑢 × 𝑣)) Cn 𝐶)))) → ⟨𝑏, 𝑎⟩ ∈ (𝑢 × 𝑣))
100	95, 99	sseldd 3937	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×_t II) ↾_t (𝑢 × 𝑣)) Cn 𝐶)))) → ⟨𝑏, 𝑎⟩ ∈ ((int‘(II ×_t II))‘𝑆))
101	100	ex 416	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) → ((𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×_t II) ↾_t (𝑢 × 𝑣)) Cn 𝐶))) → ⟨𝑏, 𝑎⟩ ∈ ((int‘(II ×_t II))‘𝑆)))
102	101	rexlimdvva 3218	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) → (∃𝑢 ∈ II ∃𝑣 ∈ II (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×_t II) ↾_t (𝑢 × 𝑣)) Cn 𝐶))) → ⟨𝑏, 𝑎⟩ ∈ ((int‘(II ×_t II))‘𝑆)))
103	47, 102	mpd 15	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) → ⟨𝑏, 𝑎⟩ ∈ ((int‘(II ×_t II))‘𝑆))
104		vex 3457	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑎 ∈ V
105		opeq2 4831	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 = 𝑎 → ⟨𝑏, 𝑤⟩ = ⟨𝑏, 𝑎⟩)
106	105	eleq1d 2846	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 = 𝑎 → (⟨𝑏, 𝑤⟩ ∈ ((int‘(II ×_t II))‘𝑆) ↔ ⟨𝑏, 𝑎⟩ ∈ ((int‘(II ×_t II))‘𝑆)))
107	104, 106	ralsn 4639	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑤 ∈ {𝑎}⟨𝑏, 𝑤⟩ ∈ ((int‘(II ×_t II))‘𝑆) ↔ ⟨𝑏, 𝑎⟩ ∈ ((int‘(II ×_t II))‘𝑆))
108	103, 107	sylibr 236	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) → ∀𝑤 ∈ {𝑎}⟨𝑏, 𝑤⟩ ∈ ((int‘(II ×_t II))‘𝑆))
109	108	anassrs 471	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑎 ∈ (0[,]1)) ∧ 𝑏 ∈ (0[,]1)) → ∀𝑤 ∈ {𝑎}⟨𝑏, 𝑤⟩ ∈ ((int‘(II ×_t II))‘𝑆))
110	109	ralrimiva 3153	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑎 ∈ (0[,]1)) → ∀𝑏 ∈ (0[,]1)∀𝑤 ∈ {𝑎}⟨𝑏, 𝑤⟩ ∈ ((int‘(II ×_t II))‘𝑆))
111		dfss3 3925	. . . . . . . . . . . . . . . 16 ⊢ (((0[,]1) × {𝑎}) ⊆ ((int‘(II ×_t II))‘𝑆) ↔ ∀𝑢 ∈ ((0[,]1) × {𝑎})𝑢 ∈ ((int‘(II ×_t II))‘𝑆))
112		eleq1 2849	. . . . . . . . . . . . . . . . 17 ⊢ (𝑢 = ⟨𝑏, 𝑤⟩ → (𝑢 ∈ ((int‘(II ×_t II))‘𝑆) ↔ ⟨𝑏, 𝑤⟩ ∈ ((int‘(II ×_t II))‘𝑆)))
113	112	ralxp 5811	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑢 ∈ ((0[,]1) × {𝑎})𝑢 ∈ ((int‘(II ×_t II))‘𝑆) ↔ ∀𝑏 ∈ (0[,]1)∀𝑤 ∈ {𝑎}⟨𝑏, 𝑤⟩ ∈ ((int‘(II ×_t II))‘𝑆))
114	111, 113	bitri 277	. . . . . . . . . . . . . . 15 ⊢ (((0[,]1) × {𝑎}) ⊆ ((int‘(II ×_t II))‘𝑆) ↔ ∀𝑏 ∈ (0[,]1)∀𝑤 ∈ {𝑎}⟨𝑏, 𝑤⟩ ∈ ((int‘(II ×_t II))‘𝑆))
115	110, 114	sylibr 236	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑎 ∈ (0[,]1)) → ((0[,]1) × {𝑎}) ⊆ ((int‘(II ×_t II))‘𝑆))
116		simpr 488	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑎 ∈ (0[,]1)) → 𝑎 ∈ (0[,]1))
117	13, 13, 18, 20, 39, 115, 116	txtube 23680	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑎 ∈ (0[,]1)) → ∃𝑣 ∈ II (𝑎 ∈ 𝑣 ∧ ((0[,]1) × 𝑣) ⊆ ((int‘(II ×_t II))‘𝑆)))
118	36	ntrss2 23097	. . . . . . . . . . . . . . . . . . 19 ⊢ (((II ×_t II) ∈ Top ∧ 𝑆 ⊆ ((0[,]1) × (0[,]1))) → ((int‘(II ×_t II))‘𝑆) ⊆ 𝑆)
119	21, 35, 118	mp2an 702	. . . . . . . . . . . . . . . . . 18 ⊢ ((int‘(II ×_t II))‘𝑆) ⊆ 𝑆
120		sstr 3944	. . . . . . . . . . . . . . . . . 18 ⊢ ((((0[,]1) × 𝑣) ⊆ ((int‘(II ×_t II))‘𝑆) ∧ ((int‘(II ×_t II))‘𝑆) ⊆ 𝑆) → ((0[,]1) × 𝑣) ⊆ 𝑆)
121	119, 120	mpan2 701	. . . . . . . . . . . . . . . . 17 ⊢ (((0[,]1) × 𝑣) ⊆ ((int‘(II ×_t II))‘𝑆) → ((0[,]1) × 𝑣) ⊆ 𝑆)
122		df-xp 5651	. . . . . . . . . . . . . . . . . . 19 ⊢ ((0[,]1) × 𝑣) = {⟨𝑟, 𝑡⟩ ∣ (𝑟 ∈ (0[,]1) ∧ 𝑡 ∈ 𝑣)}
123	122, 33	sseq12i 3966	. . . . . . . . . . . . . . . . . 18 ⊢ (((0[,]1) × 𝑣) ⊆ 𝑆 ↔ {⟨𝑟, 𝑡⟩ ∣ (𝑟 ∈ (0[,]1) ∧ 𝑡 ∈ 𝑣)} ⊆ {⟨𝑟, 𝑡⟩ ∣ (𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀))})
124		ssopab2bw 5516	. . . . . . . . . . . . . . . . . . 19 ⊢ ({⟨𝑟, 𝑡⟩ ∣ (𝑟 ∈ (0[,]1) ∧ 𝑡 ∈ 𝑣)} ⊆ {⟨𝑟, 𝑡⟩ ∣ (𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀))} ↔ ∀𝑟∀𝑡((𝑟 ∈ (0[,]1) ∧ 𝑡 ∈ 𝑣) → (𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀))))
125		r2al 3197	. . . . . . . . . . . . . . . . . . 19 ⊢ (∀𝑟 ∈ (0[,]1)∀𝑡 ∈ 𝑣 (𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀)) ↔ ∀𝑟∀𝑡((𝑟 ∈ (0[,]1) ∧ 𝑡 ∈ 𝑣) → (𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀))))
126		ralcom 3289	. . . . . . . . . . . . . . . . . . 19 ⊢ (∀𝑟 ∈ (0[,]1)∀𝑡 ∈ 𝑣 (𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀)) ↔ ∀𝑡 ∈ 𝑣 ∀𝑟 ∈ (0[,]1)(𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀)))
127	124, 125, 126	3bitr2i 301	. . . . . . . . . . . . . . . . . 18 ⊢ ({⟨𝑟, 𝑡⟩ ∣ (𝑟 ∈ (0[,]1) ∧ 𝑡 ∈ 𝑣)} ⊆ {⟨𝑟, 𝑡⟩ ∣ (𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀))} ↔ ∀𝑡 ∈ 𝑣 ∀𝑟 ∈ (0[,]1)(𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀)))
128	123, 127	bitri 277	. . . . . . . . . . . . . . . . 17 ⊢ (((0[,]1) × 𝑣) ⊆ 𝑆 ↔ ∀𝑡 ∈ 𝑣 ∀𝑟 ∈ (0[,]1)(𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀)))
129	121, 128	sylib 220	. . . . . . . . . . . . . . . 16 ⊢ (((0[,]1) × 𝑣) ⊆ ((int‘(II ×_t II))‘𝑆) → ∀𝑡 ∈ 𝑣 ∀𝑟 ∈ (0[,]1)(𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀)))
130		simpr 488	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀)) → ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀))
131	130	ralimi 3098	. . . . . . . . . . . . . . . . . . 19 ⊢ (∀𝑟 ∈ (0[,]1)(𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀)) → ∀𝑟 ∈ (0[,]1)∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀))
132		cvmlift2lem1 35616	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∀𝑟 ∈ (0[,]1)∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀) → (((0[,]1) × {𝑎}) ⊆ 𝑀 → ((0[,]1) × {𝑡}) ⊆ 𝑀))
133		bicom 224	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀) ↔ ((𝑢 × {𝑡}) ⊆ 𝑀 ↔ (𝑢 × {𝑎}) ⊆ 𝑀))
134	133	rexbii 3108	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀) ↔ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑡}) ⊆ 𝑀 ↔ (𝑢 × {𝑎}) ⊆ 𝑀))
135	134	ralbii 3107	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∀𝑟 ∈ (0[,]1)∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀) ↔ ∀𝑟 ∈ (0[,]1)∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑡}) ⊆ 𝑀 ↔ (𝑢 × {𝑎}) ⊆ 𝑀))
136		cvmlift2lem1 35616	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∀𝑟 ∈ (0[,]1)∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑡}) ⊆ 𝑀 ↔ (𝑢 × {𝑎}) ⊆ 𝑀) → (((0[,]1) × {𝑡}) ⊆ 𝑀 → ((0[,]1) × {𝑎}) ⊆ 𝑀))
137	135, 136	sylbi 219	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∀𝑟 ∈ (0[,]1)∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀) → (((0[,]1) × {𝑡}) ⊆ 𝑀 → ((0[,]1) × {𝑎}) ⊆ 𝑀))
138	132, 137	impbid 214	. . . . . . . . . . . . . . . . . . 19 ⊢ (∀𝑟 ∈ (0[,]1)∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀) → (((0[,]1) × {𝑎}) ⊆ 𝑀 ↔ ((0[,]1) × {𝑡}) ⊆ 𝑀))
139	131, 138	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑟 ∈ (0[,]1)(𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀)) → (((0[,]1) × {𝑎}) ⊆ 𝑀 ↔ ((0[,]1) × {𝑡}) ⊆ 𝑀))
140		cvmlift2.a	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝐴 = {𝑎 ∈ (0[,]1) ∣ ((0[,]1) × {𝑎}) ⊆ 𝑀}
141	140	reqabi 3436	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎 ∈ 𝐴 ↔ (𝑎 ∈ (0[,]1) ∧ ((0[,]1) × {𝑎}) ⊆ 𝑀))
142	141	baib 543	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 ∈ (0[,]1) → (𝑎 ∈ 𝐴 ↔ ((0[,]1) × {𝑎}) ⊆ 𝑀))
143	142	ad3antlr 741	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑎 ∈ (0[,]1)) ∧ 𝑣 ∈ II) ∧ 𝑡 ∈ 𝑣) → (𝑎 ∈ 𝐴 ↔ ((0[,]1) × {𝑎}) ⊆ 𝑀))
144		elssuni 4896	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑣 ∈ II → 𝑣 ⊆ ∪ II)
145	144, 13	sseqtrrdi 3977	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑣 ∈ II → 𝑣 ⊆ (0[,]1))
146	145	adantl 485	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑎 ∈ (0[,]1)) ∧ 𝑣 ∈ II) → 𝑣 ⊆ (0[,]1))
147	146	sselda 3936	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑎 ∈ (0[,]1)) ∧ 𝑣 ∈ II) ∧ 𝑡 ∈ 𝑣) → 𝑡 ∈ (0[,]1))
148		sneq 4591	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑎 = 𝑡 → {𝑎} = {𝑡})
149	148	xpeq2d 5675	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑎 = 𝑡 → ((0[,]1) × {𝑎}) = ((0[,]1) × {𝑡}))
150	149	sseq1d 3967	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑎 = 𝑡 → (((0[,]1) × {𝑎}) ⊆ 𝑀 ↔ ((0[,]1) × {𝑡}) ⊆ 𝑀))
151	150, 140	elrab2 3653	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑡 ∈ 𝐴 ↔ (𝑡 ∈ (0[,]1) ∧ ((0[,]1) × {𝑡}) ⊆ 𝑀))
152	151	baib 543	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 ∈ (0[,]1) → (𝑡 ∈ 𝐴 ↔ ((0[,]1) × {𝑡}) ⊆ 𝑀))
153	147, 152	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑎 ∈ (0[,]1)) ∧ 𝑣 ∈ II) ∧ 𝑡 ∈ 𝑣) → (𝑡 ∈ 𝐴 ↔ ((0[,]1) × {𝑡}) ⊆ 𝑀))
154	143, 153	bibi12d 347	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑎 ∈ (0[,]1)) ∧ 𝑣 ∈ II) ∧ 𝑡 ∈ 𝑣) → ((𝑎 ∈ 𝐴 ↔ 𝑡 ∈ 𝐴) ↔ (((0[,]1) × {𝑎}) ⊆ 𝑀 ↔ ((0[,]1) × {𝑡}) ⊆ 𝑀)))
155	139, 154	imbitrrid 248	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑎 ∈ (0[,]1)) ∧ 𝑣 ∈ II) ∧ 𝑡 ∈ 𝑣) → (∀𝑟 ∈ (0[,]1)(𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀)) → (𝑎 ∈ 𝐴 ↔ 𝑡 ∈ 𝐴)))
156	155	ralimdva 3173	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑎 ∈ (0[,]1)) ∧ 𝑣 ∈ II) → (∀𝑡 ∈ 𝑣 ∀𝑟 ∈ (0[,]1)(𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀)) → ∀𝑡 ∈ 𝑣 (𝑎 ∈ 𝐴 ↔ 𝑡 ∈ 𝐴)))
157	129, 156	syl5 34	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑎 ∈ (0[,]1)) ∧ 𝑣 ∈ II) → (((0[,]1) × 𝑣) ⊆ ((int‘(II ×_t II))‘𝑆) → ∀𝑡 ∈ 𝑣 (𝑎 ∈ 𝐴 ↔ 𝑡 ∈ 𝐴)))
158	157	anim2d 621	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑎 ∈ (0[,]1)) ∧ 𝑣 ∈ II) → ((𝑎 ∈ 𝑣 ∧ ((0[,]1) × 𝑣) ⊆ ((int‘(II ×_t II))‘𝑆)) → (𝑎 ∈ 𝑣 ∧ ∀𝑡 ∈ 𝑣 (𝑎 ∈ 𝐴 ↔ 𝑡 ∈ 𝐴))))
159	158	reximdva 3174	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑎 ∈ (0[,]1)) → (∃𝑣 ∈ II (𝑎 ∈ 𝑣 ∧ ((0[,]1) × 𝑣) ⊆ ((int‘(II ×_t II))‘𝑆)) → ∃𝑣 ∈ II (𝑎 ∈ 𝑣 ∧ ∀𝑡 ∈ 𝑣 (𝑎 ∈ 𝐴 ↔ 𝑡 ∈ 𝐴))))
160	117, 159	mpd 15	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑎 ∈ (0[,]1)) → ∃𝑣 ∈ II (𝑎 ∈ 𝑣 ∧ ∀𝑡 ∈ 𝑣 (𝑎 ∈ 𝐴 ↔ 𝑡 ∈ 𝐴)))
161	160	ralrimiva 3153	. . . . . . . . . . 11 ⊢ (𝜑 → ∀𝑎 ∈ (0[,]1)∃𝑣 ∈ II (𝑎 ∈ 𝑣 ∧ ∀𝑡 ∈ 𝑣 (𝑎 ∈ 𝐴 ↔ 𝑡 ∈ 𝐴)))
162		ssrab2 4033	. . . . . . . . . . . . 13 ⊢ {𝑎 ∈ (0[,]1) ∣ ((0[,]1) × {𝑎}) ⊆ 𝑀} ⊆ (0[,]1)
163	140, 162	eqsstri 3982	. . . . . . . . . . . 12 ⊢ 𝐴 ⊆ (0[,]1)
164	13	isclo 23127	. . . . . . . . . . . 12 ⊢ ((II ∈ Top ∧ 𝐴 ⊆ (0[,]1)) → (𝐴 ∈ (II ∩ (Clsd‘II)) ↔ ∀𝑎 ∈ (0[,]1)∃𝑣 ∈ II (𝑎 ∈ 𝑣 ∧ ∀𝑡 ∈ 𝑣 (𝑎 ∈ 𝐴 ↔ 𝑡 ∈ 𝐴))))
165	19, 163, 164	mp2an 702	. . . . . . . . . . 11 ⊢ (𝐴 ∈ (II ∩ (Clsd‘II)) ↔ ∀𝑎 ∈ (0[,]1)∃𝑣 ∈ II (𝑎 ∈ 𝑣 ∧ ∀𝑡 ∈ 𝑣 (𝑎 ∈ 𝐴 ↔ 𝑡 ∈ 𝐴)))
166	161, 165	sylibr 236	. . . . . . . . . 10 ⊢ (𝜑 → 𝐴 ∈ (II ∩ (Clsd‘II)))
167	16, 166	sselid 3934	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 ∈ II)
168		0elunit 13470	. . . . . . . . . . . 12 ⊢ 0 ∈ (0[,]1)
169	168	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → 0 ∈ (0[,]1))
170		relxp 5663	. . . . . . . . . . . . 13 ⊢ Rel ((0[,]1) × {0})
171	170	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → Rel ((0[,]1) × {0}))
172		opelxp 5681	. . . . . . . . . . . . 13 ⊢ (⟨𝑟, 𝑎⟩ ∈ ((0[,]1) × {0}) ↔ (𝑟 ∈ (0[,]1) ∧ 𝑎 ∈ {0}))
173		id 22	. . . . . . . . . . . . . . . . 17 ⊢ (𝑟 ∈ (0[,]1) → 𝑟 ∈ (0[,]1))
174		opelxpi 5682	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑟 ∈ (0[,]1) ∧ 0 ∈ (0[,]1)) → ⟨𝑟, 0⟩ ∈ ((0[,]1) × (0[,]1)))
175	173, 169, 174	syl2anr 606	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑟 ∈ (0[,]1)) → ⟨𝑟, 0⟩ ∈ ((0[,]1) × (0[,]1)))
176	2	adantr 484	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑟 ∈ (0[,]1)) → 𝐹 ∈ (𝐶 CovMap 𝐽))
177	3	adantr 484	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑟 ∈ (0[,]1)) → 𝐺 ∈ ((II ×_t II) Cn 𝐽))
178	4	adantr 484	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑟 ∈ (0[,]1)) → 𝑃 ∈ 𝐵)
179	5	adantr 484	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑟 ∈ (0[,]1)) → (𝐹‘𝑃) = (0𝐺0))
180		simpr 488	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑟 ∈ (0[,]1)) → 𝑟 ∈ (0[,]1))
181	168	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑟 ∈ (0[,]1)) → 0 ∈ (0[,]1))
182	1, 176, 177, 178, 179, 6, 7, 44, 180, 181	cvmlift2lem10 35626	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑟 ∈ (0[,]1)) → ∃𝑢 ∈ II ∃𝑣 ∈ II (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×_t II) ↾_t (𝑢 × 𝑣)) Cn 𝐶))))
183		df-3an 1099	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×_t II) ↾_t (𝑢 × 𝑣)) Cn 𝐶))) ↔ ((𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣) ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×_t II) ↾_t (𝑢 × 𝑣)) Cn 𝐶))))
184		simprr 782	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → 0 ∈ 𝑣)
185	8	ad3antrrr 740	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → 𝐾:((0[,]1) × (0[,]1))⟶𝐵)
186	185	ffnd 6688	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → 𝐾 Fn ((0[,]1) × (0[,]1)))
187		fnov 7523	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝐾 Fn ((0[,]1) × (0[,]1)) ↔ 𝐾 = (𝑏 ∈ (0[,]1), 𝑤 ∈ (0[,]1) ↦ (𝑏𝐾𝑤)))
188	186, 187	sylib 220	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → 𝐾 = (𝑏 ∈ (0[,]1), 𝑤 ∈ (0[,]1) ↦ (𝑏𝐾𝑤)))
189	188	reseq1d 5962	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → (𝐾 ↾ (𝑢 × {0})) = ((𝑏 ∈ (0[,]1), 𝑤 ∈ (0[,]1) ↦ (𝑏𝐾𝑤)) ↾ (𝑢 × {0})))
190		simplrl 786	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → 𝑢 ∈ II)
191		elssuni 4896	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑢 ∈ II → 𝑢 ⊆ ∪ II)
192	191, 13	sseqtrrdi 3977	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑢 ∈ II → 𝑢 ⊆ (0[,]1))
193	190, 192	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → 𝑢 ⊆ (0[,]1))
194	169	snssd 4744	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → {0} ⊆ (0[,]1))
195	194	ad3antrrr 740	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → {0} ⊆ (0[,]1))
196		resmpo 7512	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑢 ⊆ (0[,]1) ∧ {0} ⊆ (0[,]1)) → ((𝑏 ∈ (0[,]1), 𝑤 ∈ (0[,]1) ↦ (𝑏𝐾𝑤)) ↾ (𝑢 × {0})) = (𝑏 ∈ 𝑢, 𝑤 ∈ {0} ↦ (𝑏𝐾𝑤)))
197	193, 195, 196	syl2anc 593	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → ((𝑏 ∈ (0[,]1), 𝑤 ∈ (0[,]1) ↦ (𝑏𝐾𝑤)) ↾ (𝑢 × {0})) = (𝑏 ∈ 𝑢, 𝑤 ∈ {0} ↦ (𝑏𝐾𝑤)))
198	193	sselda 3936	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) ∧ 𝑏 ∈ 𝑢) → 𝑏 ∈ (0[,]1))
199		simplll 784	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → 𝜑)
200	1, 2, 3, 4, 5, 6, 7	cvmlift2lem8 35624	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑏 ∈ (0[,]1)) → (𝑏𝐾0) = (𝐻‘𝑏))
201	199, 200	sylan 589	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) ∧ 𝑏 ∈ (0[,]1)) → (𝑏𝐾0) = (𝐻‘𝑏))
202	198, 201	syldan 600	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) ∧ 𝑏 ∈ 𝑢) → (𝑏𝐾0) = (𝐻‘𝑏))
203		elsni 4598	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑤 ∈ {0} → 𝑤 = 0)
204	203	oveq2d 7408	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑤 ∈ {0} → (𝑏𝐾𝑤) = (𝑏𝐾0))
205	204	eqeq1d 2763	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑤 ∈ {0} → ((𝑏𝐾𝑤) = (𝐻‘𝑏) ↔ (𝑏𝐾0) = (𝐻‘𝑏)))
206	202, 205	syl5ibrcom 249	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) ∧ 𝑏 ∈ 𝑢) → (𝑤 ∈ {0} → (𝑏𝐾𝑤) = (𝐻‘𝑏)))
207	206	3impia 1129	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) ∧ 𝑏 ∈ 𝑢 ∧ 𝑤 ∈ {0}) → (𝑏𝐾𝑤) = (𝐻‘𝑏))
208	207	mpoeq3dva 7469	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → (𝑏 ∈ 𝑢, 𝑤 ∈ {0} ↦ (𝑏𝐾𝑤)) = (𝑏 ∈ 𝑢, 𝑤 ∈ {0} ↦ (𝐻‘𝑏)))
209	189, 197, 208	3eqtrd 2800	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → (𝐾 ↾ (𝑢 × {0})) = (𝑏 ∈ 𝑢, 𝑤 ∈ {0} ↦ (𝐻‘𝑏)))
210		eqid 2761	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (II ↾_t 𝑢) = (II ↾_t 𝑢)
211		iitopon 24921	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ II ∈ (TopOn‘(0[,]1))
212	211	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → II ∈ (TopOn‘(0[,]1)))
213		eqid 2761	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (II ↾_t {0}) = (II ↾_t {0})
214	212, 212	cnmpt1st 23708	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → (𝑏 ∈ (0[,]1), 𝑤 ∈ (0[,]1) ↦ 𝑏) ∈ ((II ×_t II) Cn II))
215	1, 2, 3, 4, 5, 6	cvmlift2lem2 35618	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → (𝐻 ∈ (II Cn 𝐶) ∧ (𝐹 ∘ 𝐻) = (𝑧 ∈ (0[,]1) ↦ (𝑧𝐺0)) ∧ (𝐻‘0) = 𝑃))
216	215	simp1d 1154	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → 𝐻 ∈ (II Cn 𝐶))
217	199, 216	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → 𝐻 ∈ (II Cn 𝐶))
218	212, 212, 214, 217	cnmpt21f 23712	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → (𝑏 ∈ (0[,]1), 𝑤 ∈ (0[,]1) ↦ (𝐻‘𝑏)) ∈ ((II ×_t II) Cn 𝐶))
219	210, 212, 193, 213, 212, 195, 218	cnmpt2res 23717	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → (𝑏 ∈ 𝑢, 𝑤 ∈ {0} ↦ (𝐻‘𝑏)) ∈ (((II ↾_t 𝑢) ×_t (II ↾_t {0})) Cn 𝐶))
220		vex 3457	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ 𝑢 ∈ V
221		snex 5395	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ {0} ∈ V
222		txrest 23671	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((II ∈ Top ∧ II ∈ Top) ∧ (𝑢 ∈ V ∧ {0} ∈ V)) → ((II ×_t II) ↾_t (𝑢 × {0})) = ((II ↾_t 𝑢) ×_t (II ↾_t {0})))
223	19, 19, 220, 221, 222	mp4an 703	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((II ×_t II) ↾_t (𝑢 × {0})) = ((II ↾_t 𝑢) ×_t (II ↾_t {0}))
224	223	oveq1i 7402	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((II ×_t II) ↾_t (𝑢 × {0})) Cn 𝐶) = (((II ↾_t 𝑢) ×_t (II ↾_t {0})) Cn 𝐶)
225	219, 224	eleqtrrdi 2872	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → (𝑏 ∈ 𝑢, 𝑤 ∈ {0} ↦ (𝐻‘𝑏)) ∈ (((II ×_t II) ↾_t (𝑢 × {0})) Cn 𝐶))
226	209, 225	eqeltrd 2861	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → (𝐾 ↾ (𝑢 × {0})) ∈ (((II ×_t II) ↾_t (𝑢 × {0})) Cn 𝐶))
227		sneq 4591	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑤 = 0 → {𝑤} = {0})
228	227	xpeq2d 5675	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑤 = 0 → (𝑢 × {𝑤}) = (𝑢 × {0}))
229	228	reseq2d 5963	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑤 = 0 → (𝐾 ↾ (𝑢 × {𝑤})) = (𝐾 ↾ (𝑢 × {0})))
230	228	oveq2d 7408	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑤 = 0 → ((II ×_t II) ↾_t (𝑢 × {𝑤})) = ((II ×_t II) ↾_t (𝑢 × {0})))
231	230	oveq1d 7407	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑤 = 0 → (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶) = (((II ×_t II) ↾_t (𝑢 × {0})) Cn 𝐶))
232	229, 231	eleq12d 2855	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 = 0 → ((𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶) ↔ (𝐾 ↾ (𝑢 × {0})) ∈ (((II ×_t II) ↾_t (𝑢 × {0})) Cn 𝐶)))
233	232	rspcev 3581	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((0 ∈ 𝑣 ∧ (𝐾 ↾ (𝑢 × {0})) ∈ (((II ×_t II) ↾_t (𝑢 × {0})) Cn 𝐶)) → ∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶))
234	184, 226, 233	syl2anc 593	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → ∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶))
235		opelxpi 5682	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣) → ⟨𝑟, 0⟩ ∈ (𝑢 × 𝑣))
236	235	adantl 485	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → ⟨𝑟, 0⟩ ∈ (𝑢 × 𝑣))
237		simplrr 787	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → 𝑣 ∈ II)
238	237, 145	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → 𝑣 ⊆ (0[,]1))
239		xpss12 5660	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑢 ⊆ (0[,]1) ∧ 𝑣 ⊆ (0[,]1)) → (𝑢 × 𝑣) ⊆ ((0[,]1) × (0[,]1)))
240	193, 238, 239	syl2anc 593	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → (𝑢 × 𝑣) ⊆ ((0[,]1) × (0[,]1)))
241	36	restuni 23202	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((II ×_t II) ∈ Top ∧ (𝑢 × 𝑣) ⊆ ((0[,]1) × (0[,]1))) → (𝑢 × 𝑣) = ∪ ((II ×_t II) ↾_t (𝑢 × 𝑣)))
242	21, 240, 241	sylancr 596	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → (𝑢 × 𝑣) = ∪ ((II ×_t II) ↾_t (𝑢 × 𝑣)))
243	236, 242	eleqtrd 2863	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → ⟨𝑟, 0⟩ ∈ ∪ ((II ×_t II) ↾_t (𝑢 × 𝑣)))
244		eqid 2761	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ∪ ((II ×_t II) ↾_t (𝑢 × 𝑣)) = ∪ ((II ×_t II) ↾_t (𝑢 × 𝑣))
245	244	cncnpi 23318	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×_t II) ↾_t (𝑢 × 𝑣)) Cn 𝐶) ∧ ⟨𝑟, 0⟩ ∈ ∪ ((II ×_t II) ↾_t (𝑢 × 𝑣))) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ ((((II ×_t II) ↾_t (𝑢 × 𝑣)) CnP 𝐶)‘⟨𝑟, 0⟩))
246	245	expcom 417	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (⟨𝑟, 0⟩ ∈ ∪ ((II ×_t II) ↾_t (𝑢 × 𝑣)) → ((𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×_t II) ↾_t (𝑢 × 𝑣)) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ ((((II ×_t II) ↾_t (𝑢 × 𝑣)) CnP 𝐶)‘⟨𝑟, 0⟩)))
247	243, 246	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → ((𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×_t II) ↾_t (𝑢 × 𝑣)) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ ((((II ×_t II) ↾_t (𝑢 × 𝑣)) CnP 𝐶)‘⟨𝑟, 0⟩)))
248	21	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → (II ×_t II) ∈ Top)
249	19	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → II ∈ Top)
250	249, 249, 190, 237, 53	syl22anc 849	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → (𝑢 × 𝑣) ∈ (II ×_t II))
251		isopn3i 23122	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((II ×_t II) ∈ Top ∧ (𝑢 × 𝑣) ∈ (II ×_t II)) → ((int‘(II ×_t II))‘(𝑢 × 𝑣)) = (𝑢 × 𝑣))
252	21, 250, 251	sylancr 596	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → ((int‘(II ×_t II))‘(𝑢 × 𝑣)) = (𝑢 × 𝑣))
253	236, 252	eleqtrrd 2864	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → ⟨𝑟, 0⟩ ∈ ((int‘(II ×_t II))‘(𝑢 × 𝑣)))
254	36, 1	cnprest 23329	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((II ×_t II) ∈ Top ∧ (𝑢 × 𝑣) ⊆ ((0[,]1) × (0[,]1))) ∧ (⟨𝑟, 0⟩ ∈ ((int‘(II ×_t II))‘(𝑢 × 𝑣)) ∧ 𝐾:((0[,]1) × (0[,]1))⟶𝐵)) → (𝐾 ∈ (((II ×_t II) CnP 𝐶)‘⟨𝑟, 0⟩) ↔ (𝐾 ↾ (𝑢 × 𝑣)) ∈ ((((II ×_t II) ↾_t (𝑢 × 𝑣)) CnP 𝐶)‘⟨𝑟, 0⟩)))
255	248, 240, 253, 185, 254	syl22anc 849	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → (𝐾 ∈ (((II ×_t II) CnP 𝐶)‘⟨𝑟, 0⟩) ↔ (𝐾 ↾ (𝑢 × 𝑣)) ∈ ((((II ×_t II) ↾_t (𝑢 × 𝑣)) CnP 𝐶)‘⟨𝑟, 0⟩)))
256	247, 255	sylibrd 261	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → ((𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×_t II) ↾_t (𝑢 × 𝑣)) Cn 𝐶) → 𝐾 ∈ (((II ×_t II) CnP 𝐶)‘⟨𝑟, 0⟩)))
257	234, 256	embantd 59	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → ((∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×_t II) ↾_t (𝑢 × 𝑣)) Cn 𝐶)) → 𝐾 ∈ (((II ×_t II) CnP 𝐶)‘⟨𝑟, 0⟩)))
258	257	expimpd 457	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) → (((𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣) ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×_t II) ↾_t (𝑢 × 𝑣)) Cn 𝐶))) → 𝐾 ∈ (((II ×_t II) CnP 𝐶)‘⟨𝑟, 0⟩)))
259	183, 258	biimtrid 244	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) → ((𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×_t II) ↾_t (𝑢 × 𝑣)) Cn 𝐶))) → 𝐾 ∈ (((II ×_t II) CnP 𝐶)‘⟨𝑟, 0⟩)))
260	259	rexlimdvva 3218	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑟 ∈ (0[,]1)) → (∃𝑢 ∈ II ∃𝑣 ∈ II (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×_t II) ↾_t (𝑢 × 𝑣)) Cn 𝐶))) → 𝐾 ∈ (((II ×_t II) CnP 𝐶)‘⟨𝑟, 0⟩)))
261	182, 260	mpd 15	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑟 ∈ (0[,]1)) → 𝐾 ∈ (((II ×_t II) CnP 𝐶)‘⟨𝑟, 0⟩))
262		fveq2 6863	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = ⟨𝑟, 0⟩ → (((II ×_t II) CnP 𝐶)‘𝑧) = (((II ×_t II) CnP 𝐶)‘⟨𝑟, 0⟩))
263	262	eleq2d 2847	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = ⟨𝑟, 0⟩ → (𝐾 ∈ (((II ×_t II) CnP 𝐶)‘𝑧) ↔ 𝐾 ∈ (((II ×_t II) CnP 𝐶)‘⟨𝑟, 0⟩)))
264	263, 68	elrab2 3653	. . . . . . . . . . . . . . . 16 ⊢ (⟨𝑟, 0⟩ ∈ 𝑀 ↔ (⟨𝑟, 0⟩ ∈ ((0[,]1) × (0[,]1)) ∧ 𝐾 ∈ (((II ×_t II) CnP 𝐶)‘⟨𝑟, 0⟩)))
265	175, 261, 264	sylanbrc 592	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑟 ∈ (0[,]1)) → ⟨𝑟, 0⟩ ∈ 𝑀)
266		elsni 4598	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 ∈ {0} → 𝑎 = 0)
267	266	opeq2d 4837	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 ∈ {0} → ⟨𝑟, 𝑎⟩ = ⟨𝑟, 0⟩)
268	267	eleq1d 2846	. . . . . . . . . . . . . . 15 ⊢ (𝑎 ∈ {0} → (⟨𝑟, 𝑎⟩ ∈ 𝑀 ↔ ⟨𝑟, 0⟩ ∈ 𝑀))
269	265, 268	syl5ibrcom 249	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑟 ∈ (0[,]1)) → (𝑎 ∈ {0} → ⟨𝑟, 𝑎⟩ ∈ 𝑀))
270	269	expimpd 457	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑟 ∈ (0[,]1) ∧ 𝑎 ∈ {0}) → ⟨𝑟, 𝑎⟩ ∈ 𝑀))
271	172, 270	biimtrid 244	. . . . . . . . . . . 12 ⊢ (𝜑 → (⟨𝑟, 𝑎⟩ ∈ ((0[,]1) × {0}) → ⟨𝑟, 𝑎⟩ ∈ 𝑀))
272	171, 271	relssdv 5758	. . . . . . . . . . 11 ⊢ (𝜑 → ((0[,]1) × {0}) ⊆ 𝑀)
273		sneq 4591	. . . . . . . . . . . . . 14 ⊢ (𝑎 = 0 → {𝑎} = {0})
274	273	xpeq2d 5675	. . . . . . . . . . . . 13 ⊢ (𝑎 = 0 → ((0[,]1) × {𝑎}) = ((0[,]1) × {0}))
275	274	sseq1d 3967	. . . . . . . . . . . 12 ⊢ (𝑎 = 0 → (((0[,]1) × {𝑎}) ⊆ 𝑀 ↔ ((0[,]1) × {0}) ⊆ 𝑀))
276	275, 140	elrab2 3653	. . . . . . . . . . 11 ⊢ (0 ∈ 𝐴 ↔ (0 ∈ (0[,]1) ∧ ((0[,]1) × {0}) ⊆ 𝑀))
277	169, 272, 276	sylanbrc 592	. . . . . . . . . 10 ⊢ (𝜑 → 0 ∈ 𝐴)
278	277	ne0d 4294	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 ≠ ∅)
279		inss2 4189	. . . . . . . . . 10 ⊢ (II ∩ (Clsd‘II)) ⊆ (Clsd‘II)
280	279, 166	sselid 3934	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 ∈ (Clsd‘II))
281	13, 15, 167, 278, 280	connclo 23455	. . . . . . . 8 ⊢ (𝜑 → 𝐴 = (0[,]1))
282	281, 140	eqtr3di 2811	. . . . . . 7 ⊢ (𝜑 → (0[,]1) = {𝑎 ∈ (0[,]1) ∣ ((0[,]1) × {𝑎}) ⊆ 𝑀})
283		rabid2 3446	. . . . . . 7 ⊢ ((0[,]1) = {𝑎 ∈ (0[,]1) ∣ ((0[,]1) × {𝑎}) ⊆ 𝑀} ↔ ∀𝑎 ∈ (0[,]1)((0[,]1) × {𝑎}) ⊆ 𝑀)
284	282, 283	sylib 220	. . . . . 6 ⊢ (𝜑 → ∀𝑎 ∈ (0[,]1)((0[,]1) × {𝑎}) ⊆ 𝑀)
285		iunss 5001	. . . . . 6 ⊢ (∪ 𝑎 ∈ (0[,]1)((0[,]1) × {𝑎}) ⊆ 𝑀 ↔ ∀𝑎 ∈ (0[,]1)((0[,]1) × {𝑎}) ⊆ 𝑀)
286	284, 285	sylibr 236	. . . . 5 ⊢ (𝜑 → ∪ 𝑎 ∈ (0[,]1)((0[,]1) × {𝑎}) ⊆ 𝑀)
287	12, 286	eqsstrid 3974	. . . 4 ⊢ (𝜑 → ((0[,]1) × (0[,]1)) ⊆ 𝑀)
288	287, 68	sseqtrdi 3976	. . 3 ⊢ (𝜑 → ((0[,]1) × (0[,]1)) ⊆ {𝑧 ∈ ((0[,]1) × (0[,]1)) ∣ 𝐾 ∈ (((II ×_t II) CnP 𝐶)‘𝑧)})
289		ssrab 4024	. . . 4 ⊢ (((0[,]1) × (0[,]1)) ⊆ {𝑧 ∈ ((0[,]1) × (0[,]1)) ∣ 𝐾 ∈ (((II ×_t II) CnP 𝐶)‘𝑧)} ↔ (((0[,]1) × (0[,]1)) ⊆ ((0[,]1) × (0[,]1)) ∧ ∀𝑧 ∈ ((0[,]1) × (0[,]1))𝐾 ∈ (((II ×_t II) CnP 𝐶)‘𝑧)))
290	289	simprbi 501	. . 3 ⊢ (((0[,]1) × (0[,]1)) ⊆ {𝑧 ∈ ((0[,]1) × (0[,]1)) ∣ 𝐾 ∈ (((II ×_t II) CnP 𝐶)‘𝑧)} → ∀𝑧 ∈ ((0[,]1) × (0[,]1))𝐾 ∈ (((II ×_t II) CnP 𝐶)‘𝑧))
291	288, 290	syl 17	. 2 ⊢ (𝜑 → ∀𝑧 ∈ ((0[,]1) × (0[,]1))𝐾 ∈ (((II ×_t II) CnP 𝐶)‘𝑧))
292		txtopon 23631	. . . 4 ⊢ ((II ∈ (TopOn‘(0[,]1)) ∧ II ∈ (TopOn‘(0[,]1))) → (II ×_t II) ∈ (TopOn‘((0[,]1) × (0[,]1))))
293	211, 211, 292	mp2an 702	. . 3 ⊢ (II ×_t II) ∈ (TopOn‘((0[,]1) × (0[,]1)))
294		cvmtop1 35574	. . . . 5 ⊢ (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐶 ∈ Top)
295	2, 294	syl 17	. . . 4 ⊢ (𝜑 → 𝐶 ∈ Top)
296	1	toptopon 22957	. . . 4 ⊢ (𝐶 ∈ Top ↔ 𝐶 ∈ (TopOn‘𝐵))
297	295, 296	sylib 220	. . 3 ⊢ (𝜑 → 𝐶 ∈ (TopOn‘𝐵))
298		cncnp 23320	. . 3 ⊢ (((II ×_t II) ∈ (TopOn‘((0[,]1) × (0[,]1))) ∧ 𝐶 ∈ (TopOn‘𝐵)) → (𝐾 ∈ ((II ×_t II) Cn 𝐶) ↔ (𝐾:((0[,]1) × (0[,]1))⟶𝐵 ∧ ∀𝑧 ∈ ((0[,]1) × (0[,]1))𝐾 ∈ (((II ×_t II) CnP 𝐶)‘𝑧))))
299	293, 297, 298	sylancr 596	. 2 ⊢ (𝜑 → (𝐾 ∈ ((II ×_t II) Cn 𝐶) ↔ (𝐾:((0[,]1) × (0[,]1))⟶𝐵 ∧ ∀𝑧 ∈ ((0[,]1) × (0[,]1))𝐾 ∈ (((II ×_t II) CnP 𝐶)‘𝑧))))
300	8, 291, 299	mpbir2and 723	1 ⊢ (𝜑 → 𝐾 ∈ ((II ×_t II) Cn 𝐶))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 208 ∧ wa 399 ∧ w3a 1097 ∀wal 1557 = wceq 1559 ∈ wcel 2141 ∀wral 3075 ∃wrex 3085 {crab 3413 Vcvv 3453 ∖ cdif 3901 ∩ cin 3903 ⊆ wss 3904 ∅c0 4285 𝒫 cpw 4554 {csn 4581 ⟨cop 4587 ∪ cuni 4864 ∪ ciun 4948 {copab 5161 ↦ cmpt 5180 × cxp 5643 ^◡ccnv 5644 ↾ cres 5647 “ cima 5648 ∘ ccom 5649 Rel wrel 5650 Fn wfn 6512 ⟶wf 6513 ‘cfv 6517 ℩crio 7348 (class class class)co 7392 ∈ cmpo 7394 0cc0 11070 1c1 11071 [,]cicc 13349 ↾_t crest 17432 Topctop 22933 TopOnctopon 22950 Clsdccld 23056 intcnt 23057 neicnei 23137 Cn ccn 23264 CnP ccnp 23265 Compccmp 23426 Conncconn 23451 ×_t ctx 23600 Homeochmeo 23793 IIcii 24917 CovMap ccvm 35569

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1814 ax-4 1828 ax-5 1929 ax-6 1986 ax-7 2027 ax-8 2143 ax-9 2151 ax-10 2174 ax-11 2190 ax-12 2211 ax-ext 2733 ax-rep 5226 ax-sep 5245 ax-nul 5255 ax-pow 5321 ax-pr 5389 ax-un 7714 ax-inf2 9593 ax-cnex 11126 ax-resscn 11127 ax-1cn 11128 ax-icn 11129 ax-addcl 11130 ax-addrcl 11131 ax-mulcl 11132 ax-mulrcl 11133 ax-mulcom 11134 ax-addass 11135 ax-mulass 11136 ax-distr 11137 ax-i2m1 11138 ax-1ne0 11139 ax-1rid 11140 ax-rnegex 11141 ax-rrecex 11142 ax-cnre 11143 ax-pre-lttri 11144 ax-pre-lttrn 11145 ax-pre-ltadd 11146 ax-pre-mulgt0 11147 ax-pre-sup 11148 ax-addf 11149

This theorem depends on definitions: df-bi 209 df-an 400 df-or 859 df-3or 1098 df-3an 1099 df-tru 1562 df-fal 1572 df-ex 1799 df-nf 1803 df-sb 2090 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-nel 3061 df-ral 3076 df-rex 3086 df-rmo 3366 df-reu 3367 df-rab 3414 df-v 3455 df-sbc 3745 df-csb 3853 df-dif 3907 df-un 3909 df-in 3911 df-ss 3921 df-pss 3924 df-nul 4286 df-if 4480 df-pw 4556 df-sn 4582 df-pr 4584 df-tp 4586 df-op 4588 df-uni 4865 df-int 4905 df-iun 4950 df-iin 4951 df-br 5100 df-opab 5162 df-mpt 5181 df-tr 5207 df-id 5540 df-eprel 5545 df-po 5553 df-so 5554 df-fr 5598 df-se 5599 df-we 5600 df-xp 5651 df-rel 5652 df-cnv 5653 df-co 5654 df-dm 5655 df-rn 5656 df-res 5657 df-ima 5658 df-pred 6284 df-ord 6345 df-on 6346 df-lim 6347 df-suc 6348 df-iota 6473 df-fun 6519 df-fn 6520 df-f 6521 df-f1 6522 df-fo 6523 df-f1o 6524 df-fv 6525 df-isom 6526 df-riota 7349 df-ov 7395 df-oprab 7396 df-mpo 7397 df-of 7656 df-om 7843 df-1st 7966 df-2nd 7967 df-supp 8136 df-frecs 8257 df-wrecs 8288 df-recs 8337 df-rdg 8376 df-1o 8432 df-2o 8433 df-er 8673 df-ec 8675 df-map 8805 df-ixp 8876 df-en 8924 df-dom 8925 df-sdom 8926 df-fin 8927 df-fsupp 9305 df-fi 9354 df-sup 9385 df-inf 9386 df-oi 9455 df-card 9894 df-pnf 11215 df-mnf 11216 df-xr 11217 df-ltxr 11218 df-le 11219 df-sub 11413 df-neg 11414 df-div 11842 df-nn 12208 df-2 12277 df-3 12278 df-4 12279 df-5 12280 df-6 12281 df-7 12282 df-8 12283 df-9 12284 df-n0 12479 df-z 12566 df-dec 12686 df-uz 12837 df-q 12947 df-rp 12991 df-xneg 13111 df-xadd 13112 df-xmul 13113 df-ioo 13350 df-ico 13352 df-icc 13353 df-fz 13510 df-fzo 13657 df-fl 13799 df-seq 14012 df-exp 14072 df-hash 14341 df-cj 15109 df-re 15110 df-im 15111 df-sqrt 15245 df-abs 15246 df-clim 15498 df-sum 15697 df-struct 17166 df-sets 17183 df-slot 17201 df-ndx 17213 df-base 17229 df-ress 17250 df-plusg 17282 df-mulr 17283 df-starv 17284 df-sca 17285 df-vsca 17286 df-ip 17287 df-tset 17288 df-ple 17289 df-ds 17291 df-unif 17292 df-hom 17293 df-cco 17294 df-rest 17434 df-topn 17435 df-0g 17453 df-gsum 17454 df-topgen 17455 df-pt 17456 df-prds 17459 df-xrs 17515 df-qtop 17520 df-imas 17521 df-xps 17523 df-mre 17597 df-mrc 17598 df-acs 17600 df-mgm 18657 df-sgrp 18736 df-mnd 18752 df-submnd 18801 df-mulg 19093 df-cntz 19340 df-cmn 19805 df-psmet 21396 df-xmet 21397 df-met 21398 df-bl 21399 df-mopn 21400 df-cnfld 21405 df-top 22934 df-topon 22951 df-topsp 22973 df-bases 22986 df-cld 23059 df-ntr 23060 df-cls 23061 df-nei 23138 df-cn 23267 df-cnp 23268 df-cmp 23427 df-conn 23452 df-lly 23506 df-nlly 23507 df-tx 23602 df-hmeo 23795 df-xms 24360 df-ms 24361 df-tms 24362 df-ii 24919 df-cncf 24920 df-htpy 25012 df-phtpy 25013 df-phtpc 25034 df-pconn 35535 df-sconn 35536 df-cvm 35570

This theorem is referenced by: cvmlift2lem13 35629

W3C validator