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 35308

Description: Lemma for cvmlift2 35310. (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 35301	. 2 ⊢ (𝜑 → 𝐾:((0[,]1) × (0[,]1))⟶𝐵)
9		iunid 5027	. . . . . . 7 ⊢ ∪ 𝑎 ∈ (0[,]1){𝑎} = (0[,]1)
10	9	xpeq2i 5668	. . . . . 6 ⊢ ((0[,]1) × ∪ 𝑎 ∈ (0[,]1){𝑎}) = ((0[,]1) × (0[,]1))
11		xpiundi 5712	. . . . . 6 ⊢ ((0[,]1) × ∪ 𝑎 ∈ (0[,]1){𝑎}) = ∪ 𝑎 ∈ (0[,]1)((0[,]1) × {𝑎})
12	10, 11	eqtr3i 2755	. . . . 5 ⊢ ((0[,]1) × (0[,]1)) = ∪ 𝑎 ∈ (0[,]1)((0[,]1) × {𝑎})
13		iiuni 24781	. . . . . . . . 9 ⊢ (0[,]1) = ∪ II
14		iiconn 24787	. . . . . . . . . 10 ⊢ II ∈ Conn
15	14	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → II ∈ Conn)
16		inss1 4203	. . . . . . . . . 10 ⊢ (II ∩ (Clsd‘II)) ⊆ II
17		iicmp 24786	. . . . . . . . . . . . . . 15 ⊢ II ∈ Comp
18	17	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑎 ∈ (0[,]1)) → II ∈ Comp)
19		iitop 24780	. . . . . . . . . . . . . . 15 ⊢ II ∈ Top
20	19	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑎 ∈ (0[,]1)) → II ∈ Top)
21	19, 19	txtopi 23484	. . . . . . . . . . . . . . . 16 ⊢ (II ×_t II) ∈ Top
22	13	neiss2 22995	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((II ∈ Top ∧ 𝑢 ∈ ((nei‘II)‘{𝑟})) → {𝑟} ⊆ (0[,]1))
23	19, 22	mpan 690	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑢 ∈ ((nei‘II)‘{𝑟}) → {𝑟} ⊆ (0[,]1))
24		vex 3454	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 𝑟 ∈ V
25	24	snss 4752	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑟 ∈ (0[,]1) ↔ {𝑟} ⊆ (0[,]1))
26	23, 25	sylibr 234	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑢 ∈ ((nei‘II)‘{𝑟}) → 𝑟 ∈ (0[,]1))
27	26	a1d 25	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑢 ∈ ((nei‘II)‘{𝑟}) → (((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀) → 𝑟 ∈ (0[,]1)))
28	27	rexlimiv 3128	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀) → 𝑟 ∈ (0[,]1))
29	28	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀)) → 𝑟 ∈ (0[,]1))
30		simpl 482	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀)) → 𝑡 ∈ (0[,]1))
31	29, 30	jca 511	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀)) → (𝑟 ∈ (0[,]1) ∧ 𝑡 ∈ (0[,]1)))
32	31	ssopab2i 5513	. . . . . . . . . . . . . . . . 17 ⊢ {⟨𝑟, 𝑡⟩ ∣ (𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀))} ⊆ {⟨𝑟, 𝑡⟩ ∣ (𝑟 ∈ (0[,]1) ∧ 𝑡 ∈ (0[,]1))}
33		cvmlift2.s	. . . . . . . . . . . . . . . . 17 ⊢ 𝑆 = {⟨𝑟, 𝑡⟩ ∣ (𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀))}
34		df-xp 5647	. . . . . . . . . . . . . . . . 17 ⊢ ((0[,]1) × (0[,]1)) = {⟨𝑟, 𝑡⟩ ∣ (𝑟 ∈ (0[,]1) ∧ 𝑡 ∈ (0[,]1))}
35	32, 33, 34	3sstr4i 4001	. . . . . . . . . . . . . . . 16 ⊢ 𝑆 ⊆ ((0[,]1) × (0[,]1))
36	19, 19, 13, 13	txunii 23487	. . . . . . . . . . . . . . . . 17 ⊢ ((0[,]1) × (0[,]1)) = ∪ (II ×_t II)
37	36	ntropn 22943	. . . . . . . . . . . . . . . 16 ⊢ (((II ×_t II) ∈ Top ∧ 𝑆 ⊆ ((0[,]1) × (0[,]1))) → ((int‘(II ×_t II))‘𝑆) ∈ (II ×_t II))
38	21, 35, 37	mp2an 692	. . . . . . . . . . . . . . 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 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) → 𝐹 ∈ (𝐶 CovMap 𝐽))
41	3	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) → 𝐺 ∈ ((II ×_t II) Cn 𝐽))
42	4	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) → 𝑃 ∈ 𝐵)
43	5	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) → (𝐹‘𝑃) = (0𝐺0))
44		eqid 2730	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (^◡𝐹 “ 𝑘) ∧ ∀𝑐 ∈ 𝑠 (∀𝑑 ∈ (𝑠 ∖ {𝑐})(𝑐 ∩ 𝑑) = ∅ ∧ (𝐹 ↾ 𝑐) ∈ ((𝐶 ↾_t 𝑐)Homeo(𝐽 ↾_t 𝑘))))}) = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (^◡𝐹 “ 𝑘) ∧ ∀𝑐 ∈ 𝑠 (∀𝑑 ∈ (𝑠 ∖ {𝑐})(𝑐 ∩ 𝑑) = ∅ ∧ (𝐹 ↾ 𝑐) ∈ ((𝐶 ↾_t 𝑐)Homeo(𝐽 ↾_t 𝑘))))})
45		simprr 772	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) → 𝑏 ∈ (0[,]1))
46		simprl 770	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) → 𝑎 ∈ (0[,]1))
47	1, 40, 41, 42, 43, 6, 7, 44, 45, 46	cvmlift2lem10 35306	. . . . . . . . . . . . . . . . . . 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 776	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×_t II) ↾_t (𝑢 × 𝑣)) Cn 𝐶)))) → 𝑢 ∈ II)
52		simplrr 777	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×_t II) ↾_t (𝑢 × 𝑣)) Cn 𝐶)))) → 𝑣 ∈ II)
53		txopn 23496	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((II ∈ Top ∧ II ∈ Top) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) → (𝑢 × 𝑣) ∈ (II ×_t II))
54	50, 50, 51, 52, 53	syl22anc 838	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×_t II) ↾_t (𝑢 × 𝑣)) Cn 𝐶)))) → (𝑢 × 𝑣) ∈ (II ×_t II))
55		simpr 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣) → 𝑡 ∈ 𝑣)
56		elunii 4879	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑡 ∈ 𝑣 ∧ 𝑣 ∈ II) → 𝑡 ∈ ∪ II)
57	56, 13	eleqtrrdi 2840	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑡 ∈ 𝑣 ∧ 𝑣 ∈ II) → 𝑡 ∈ (0[,]1))
58	55, 52, 57	syl2anr 597	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×_t II) ↾_t (𝑢 × 𝑣)) Cn 𝐶)))) ∧ (𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣)) → 𝑢 ∈ II)
61		simprl 770	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×_t II) ↾_t (𝑢 × 𝑣)) Cn 𝐶)))) ∧ (𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣)) → 𝑟 ∈ 𝑢)
62		opnneip 23013	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((II ∈ Top ∧ 𝑢 ∈ II ∧ 𝑟 ∈ 𝑢) → 𝑢 ∈ ((nei‘II)‘{𝑟}))
63	59, 60, 61, 62	syl3anc 1373	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×_t II) ↾_t (𝑢 × 𝑣)) Cn 𝐶)))) ∧ (𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣)) → 𝑢 ∈ ((nei‘II)‘{𝑟}))
64	40	ad3antrrr 730	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×_t II) ↾_t (𝑢 × 𝑣)) Cn 𝐶)))) ∧ (𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣)) → 𝐹 ∈ (𝐶 CovMap 𝐽))
65	41	ad3antrrr 730	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×_t II) ↾_t (𝑢 × 𝑣)) Cn 𝐶)))) ∧ (𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣)) → 𝐺 ∈ ((II ×_t II) Cn 𝐽))
66	42	ad3antrrr 730	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×_t II) ↾_t (𝑢 × 𝑣)) Cn 𝐶)))) ∧ (𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣)) → 𝑃 ∈ 𝐵)
67	43	ad3antrrr 730	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×_t II) ↾_t (𝑢 × 𝑣)) Cn 𝐶)))) ∧ (𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣)) → 𝑣 ∈ II)
70		simplr2 1217	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×_t II) ↾_t (𝑢 × 𝑣)) Cn 𝐶)))) ∧ (𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣)) → 𝑎 ∈ 𝑣)
71		simprr 772	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×_t II) ↾_t (𝑢 × 𝑣)) Cn 𝐶)))) ∧ (𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣)) → 𝑡 ∈ 𝑣)
72		sneq 4602	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑐 = 𝑤 → {𝑐} = {𝑤})
73	72	xpeq2d 5671	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑐 = 𝑤 → (𝑢 × {𝑐}) = (𝑢 × {𝑤}))
74	73	reseq2d 5953	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑐 = 𝑤 → (𝐾 ↾ (𝑢 × {𝑐})) = (𝐾 ↾ (𝑢 × {𝑤})))
75	73	oveq2d 7406	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑐 = 𝑤 → ((II ×_t II) ↾_t (𝑢 × {𝑐})) = ((II ×_t II) ↾_t (𝑢 × {𝑤})))
76	75	oveq1d 7405	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑐 = 𝑤 → (((II ×_t II) ↾_t (𝑢 × {𝑐})) Cn 𝐶) = (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶))
77	74, 76	eleq12d 2823	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑐 = 𝑤 → ((𝐾 ↾ (𝑢 × {𝑐})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑐})) Cn 𝐶) ↔ (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶)))
78	77	cbvrexvw 3217	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (∃𝑐 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑐})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑐})) Cn 𝐶) ↔ ∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶))
79		simplr3 1218	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 242	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 35307	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 35307	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×_t II) ↾_t (𝑢 × 𝑣)) Cn 𝐶)))) ∧ (𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣)) → ((𝑢 × {𝑡}) ⊆ 𝑀 → (𝑢 × {𝑎}) ⊆ 𝑀))
83	81, 82	impbid 212	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×_t II) ↾_t (𝑢 × 𝑣)) Cn 𝐶)))) ∧ (𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣)) → ((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀))
84		rspe 3228	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑢 ∈ ((nei‘II)‘{𝑟}) ∧ ((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀)) → ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀))
85	63, 83, 84	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×_t II) ↾_t (𝑢 × 𝑣)) Cn 𝐶)))) ∧ (𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣)) → ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀))
86	58, 85	jca 511	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×_t II) ↾_t (𝑢 × 𝑣)) Cn 𝐶)))) ∧ (𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣)) → (𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀)))
87	86	ex 412	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×_t II) ↾_t (𝑢 × 𝑣)) Cn 𝐶)))) → ((𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣) → (𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀))))
88	87	alrimivv 1928	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×_t II) ↾_t (𝑢 × 𝑣)) Cn 𝐶)))) → ∀𝑟∀𝑡((𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣) → (𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀))))
89		df-xp 5647	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑢 × 𝑣) = {⟨𝑟, 𝑡⟩ ∣ (𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣)}
90	89, 33	sseq12i 3980	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑢 × 𝑣) ⊆ 𝑆 ↔ {⟨𝑟, 𝑡⟩ ∣ (𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣)} ⊆ {⟨𝑟, 𝑡⟩ ∣ (𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀))})
91		ssopab2bw 5510	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ({⟨𝑟, 𝑡⟩ ∣ (𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣)} ⊆ {⟨𝑟, 𝑡⟩ ∣ (𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀))} ↔ ∀𝑟∀𝑡((𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣) → (𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀))))
92	90, 91	bitri 275	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑢 × 𝑣) ⊆ 𝑆 ↔ ∀𝑟∀𝑡((𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣) → (𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀))))
93	88, 92	sylibr 234	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×_t II) ↾_t (𝑢 × 𝑣)) Cn 𝐶)))) → (𝑢 × 𝑣) ⊆ 𝑆)
94	36	ssntr 22952	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((II ×_t II) ∈ Top ∧ 𝑆 ⊆ ((0[,]1) × (0[,]1))) ∧ ((𝑢 × 𝑣) ∈ (II ×_t II) ∧ (𝑢 × 𝑣) ⊆ 𝑆)) → (𝑢 × 𝑣) ⊆ ((int‘(II ×_t II))‘𝑆))
95	48, 49, 54, 93, 94	syl22anc 838	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×_t II) ↾_t (𝑢 × 𝑣)) Cn 𝐶)))) → (𝑢 × 𝑣) ⊆ ((int‘(II ×_t II))‘𝑆))
96		simpr1 1195	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×_t II) ↾_t (𝑢 × 𝑣)) Cn 𝐶)))) → 𝑏 ∈ 𝑢)
97		simpr2 1196	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×_t II) ↾_t (𝑢 × 𝑣)) Cn 𝐶)))) → 𝑎 ∈ 𝑣)
98		opelxpi 5678	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣) → ⟨𝑏, 𝑎⟩ ∈ (𝑢 × 𝑣))
99	96, 97, 98	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×_t II) ↾_t (𝑢 × 𝑣)) Cn 𝐶)))) → ⟨𝑏, 𝑎⟩ ∈ (𝑢 × 𝑣))
100	95, 99	sseldd 3950	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×_t II) ↾_t (𝑢 × 𝑣)) Cn 𝐶)))) → ⟨𝑏, 𝑎⟩ ∈ ((int‘(II ×_t II))‘𝑆))
101	100	ex 412	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) → ((𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×_t II) ↾_t (𝑢 × 𝑣)) Cn 𝐶))) → ⟨𝑏, 𝑎⟩ ∈ ((int‘(II ×_t II))‘𝑆)))
102	101	rexlimdvva 3195	. . . . . . . . . . . . . . . . . . 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 3454	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑎 ∈ V
105		opeq2 4841	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 = 𝑎 → ⟨𝑏, 𝑤⟩ = ⟨𝑏, 𝑎⟩)
106	105	eleq1d 2814	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 = 𝑎 → (⟨𝑏, 𝑤⟩ ∈ ((int‘(II ×_t II))‘𝑆) ↔ ⟨𝑏, 𝑎⟩ ∈ ((int‘(II ×_t II))‘𝑆)))
107	104, 106	ralsn 4648	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑤 ∈ {𝑎}⟨𝑏, 𝑤⟩ ∈ ((int‘(II ×_t II))‘𝑆) ↔ ⟨𝑏, 𝑎⟩ ∈ ((int‘(II ×_t II))‘𝑆))
108	103, 107	sylibr 234	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) → ∀𝑤 ∈ {𝑎}⟨𝑏, 𝑤⟩ ∈ ((int‘(II ×_t II))‘𝑆))
109	108	anassrs 467	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑎 ∈ (0[,]1)) ∧ 𝑏 ∈ (0[,]1)) → ∀𝑤 ∈ {𝑎}⟨𝑏, 𝑤⟩ ∈ ((int‘(II ×_t II))‘𝑆))
110	109	ralrimiva 3126	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑎 ∈ (0[,]1)) → ∀𝑏 ∈ (0[,]1)∀𝑤 ∈ {𝑎}⟨𝑏, 𝑤⟩ ∈ ((int‘(II ×_t II))‘𝑆))
111		dfss3 3938	. . . . . . . . . . . . . . . 16 ⊢ (((0[,]1) × {𝑎}) ⊆ ((int‘(II ×_t II))‘𝑆) ↔ ∀𝑢 ∈ ((0[,]1) × {𝑎})𝑢 ∈ ((int‘(II ×_t II))‘𝑆))
112		eleq1 2817	. . . . . . . . . . . . . . . . 17 ⊢ (𝑢 = ⟨𝑏, 𝑤⟩ → (𝑢 ∈ ((int‘(II ×_t II))‘𝑆) ↔ ⟨𝑏, 𝑤⟩ ∈ ((int‘(II ×_t II))‘𝑆)))
113	112	ralxp 5808	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑢 ∈ ((0[,]1) × {𝑎})𝑢 ∈ ((int‘(II ×_t II))‘𝑆) ↔ ∀𝑏 ∈ (0[,]1)∀𝑤 ∈ {𝑎}⟨𝑏, 𝑤⟩ ∈ ((int‘(II ×_t II))‘𝑆))
114	111, 113	bitri 275	. . . . . . . . . . . . . . 15 ⊢ (((0[,]1) × {𝑎}) ⊆ ((int‘(II ×_t II))‘𝑆) ↔ ∀𝑏 ∈ (0[,]1)∀𝑤 ∈ {𝑎}⟨𝑏, 𝑤⟩ ∈ ((int‘(II ×_t II))‘𝑆))
115	110, 114	sylibr 234	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑎 ∈ (0[,]1)) → ((0[,]1) × {𝑎}) ⊆ ((int‘(II ×_t II))‘𝑆))
116		simpr 484	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑎 ∈ (0[,]1)) → 𝑎 ∈ (0[,]1))
117	13, 13, 18, 20, 39, 115, 116	txtube 23534	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑎 ∈ (0[,]1)) → ∃𝑣 ∈ II (𝑎 ∈ 𝑣 ∧ ((0[,]1) × 𝑣) ⊆ ((int‘(II ×_t II))‘𝑆)))
118	36	ntrss2 22951	. . . . . . . . . . . . . . . . . . 19 ⊢ (((II ×_t II) ∈ Top ∧ 𝑆 ⊆ ((0[,]1) × (0[,]1))) → ((int‘(II ×_t II))‘𝑆) ⊆ 𝑆)
119	21, 35, 118	mp2an 692	. . . . . . . . . . . . . . . . . 18 ⊢ ((int‘(II ×_t II))‘𝑆) ⊆ 𝑆
120		sstr 3958	. . . . . . . . . . . . . . . . . 18 ⊢ ((((0[,]1) × 𝑣) ⊆ ((int‘(II ×_t II))‘𝑆) ∧ ((int‘(II ×_t II))‘𝑆) ⊆ 𝑆) → ((0[,]1) × 𝑣) ⊆ 𝑆)
121	119, 120	mpan2 691	. . . . . . . . . . . . . . . . 17 ⊢ (((0[,]1) × 𝑣) ⊆ ((int‘(II ×_t II))‘𝑆) → ((0[,]1) × 𝑣) ⊆ 𝑆)
122		df-xp 5647	. . . . . . . . . . . . . . . . . . 19 ⊢ ((0[,]1) × 𝑣) = {⟨𝑟, 𝑡⟩ ∣ (𝑟 ∈ (0[,]1) ∧ 𝑡 ∈ 𝑣)}
123	122, 33	sseq12i 3980	. . . . . . . . . . . . . . . . . 18 ⊢ (((0[,]1) × 𝑣) ⊆ 𝑆 ↔ {⟨𝑟, 𝑡⟩ ∣ (𝑟 ∈ (0[,]1) ∧ 𝑡 ∈ 𝑣)} ⊆ {⟨𝑟, 𝑡⟩ ∣ (𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀))})
124		ssopab2bw 5510	. . . . . . . . . . . . . . . . . . 19 ⊢ ({⟨𝑟, 𝑡⟩ ∣ (𝑟 ∈ (0[,]1) ∧ 𝑡 ∈ 𝑣)} ⊆ {⟨𝑟, 𝑡⟩ ∣ (𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀))} ↔ ∀𝑟∀𝑡((𝑟 ∈ (0[,]1) ∧ 𝑡 ∈ 𝑣) → (𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀))))
125		r2al 3174	. . . . . . . . . . . . . . . . . . 19 ⊢ (∀𝑟 ∈ (0[,]1)∀𝑡 ∈ 𝑣 (𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀)) ↔ ∀𝑟∀𝑡((𝑟 ∈ (0[,]1) ∧ 𝑡 ∈ 𝑣) → (𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀))))
126		ralcom 3266	. . . . . . . . . . . . . . . . . . 19 ⊢ (∀𝑟 ∈ (0[,]1)∀𝑡 ∈ 𝑣 (𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀)) ↔ ∀𝑡 ∈ 𝑣 ∀𝑟 ∈ (0[,]1)(𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀)))
127	124, 125, 126	3bitr2i 299	. . . . . . . . . . . . . . . . . 18 ⊢ ({⟨𝑟, 𝑡⟩ ∣ (𝑟 ∈ (0[,]1) ∧ 𝑡 ∈ 𝑣)} ⊆ {⟨𝑟, 𝑡⟩ ∣ (𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀))} ↔ ∀𝑡 ∈ 𝑣 ∀𝑟 ∈ (0[,]1)(𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀)))
128	123, 127	bitri 275	. . . . . . . . . . . . . . . . 17 ⊢ (((0[,]1) × 𝑣) ⊆ 𝑆 ↔ ∀𝑡 ∈ 𝑣 ∀𝑟 ∈ (0[,]1)(𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀)))
129	121, 128	sylib 218	. . . . . . . . . . . . . . . 16 ⊢ (((0[,]1) × 𝑣) ⊆ ((int‘(II ×_t II))‘𝑆) → ∀𝑡 ∈ 𝑣 ∀𝑟 ∈ (0[,]1)(𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀)))
130		simpr 484	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀)) → ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀))
131	130	ralimi 3067	. . . . . . . . . . . . . . . . . . 19 ⊢ (∀𝑟 ∈ (0[,]1)(𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀)) → ∀𝑟 ∈ (0[,]1)∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀))
132		cvmlift2lem1 35296	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∀𝑟 ∈ (0[,]1)∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀) → (((0[,]1) × {𝑎}) ⊆ 𝑀 → ((0[,]1) × {𝑡}) ⊆ 𝑀))
133		bicom 222	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀) ↔ ((𝑢 × {𝑡}) ⊆ 𝑀 ↔ (𝑢 × {𝑎}) ⊆ 𝑀))
134	133	rexbii 3077	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀) ↔ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑡}) ⊆ 𝑀 ↔ (𝑢 × {𝑎}) ⊆ 𝑀))
135	134	ralbii 3076	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∀𝑟 ∈ (0[,]1)∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀) ↔ ∀𝑟 ∈ (0[,]1)∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑡}) ⊆ 𝑀 ↔ (𝑢 × {𝑎}) ⊆ 𝑀))
136		cvmlift2lem1 35296	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∀𝑟 ∈ (0[,]1)∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑡}) ⊆ 𝑀 ↔ (𝑢 × {𝑎}) ⊆ 𝑀) → (((0[,]1) × {𝑡}) ⊆ 𝑀 → ((0[,]1) × {𝑎}) ⊆ 𝑀))
137	135, 136	sylbi 217	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∀𝑟 ∈ (0[,]1)∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀) → (((0[,]1) × {𝑡}) ⊆ 𝑀 → ((0[,]1) × {𝑎}) ⊆ 𝑀))
138	132, 137	impbid 212	. . . . . . . . . . . . . . . . . . 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 3432	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎 ∈ 𝐴 ↔ (𝑎 ∈ (0[,]1) ∧ ((0[,]1) × {𝑎}) ⊆ 𝑀))
142	141	baib 535	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 ∈ (0[,]1) → (𝑎 ∈ 𝐴 ↔ ((0[,]1) × {𝑎}) ⊆ 𝑀))
143	142	ad3antlr 731	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑎 ∈ (0[,]1)) ∧ 𝑣 ∈ II) ∧ 𝑡 ∈ 𝑣) → (𝑎 ∈ 𝐴 ↔ ((0[,]1) × {𝑎}) ⊆ 𝑀))
144		elssuni 4904	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑣 ∈ II → 𝑣 ⊆ ∪ II)
145	144, 13	sseqtrrdi 3991	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑣 ∈ II → 𝑣 ⊆ (0[,]1))
146	145	adantl 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑎 ∈ (0[,]1)) ∧ 𝑣 ∈ II) → 𝑣 ⊆ (0[,]1))
147	146	sselda 3949	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑎 ∈ (0[,]1)) ∧ 𝑣 ∈ II) ∧ 𝑡 ∈ 𝑣) → 𝑡 ∈ (0[,]1))
148		sneq 4602	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑎 = 𝑡 → {𝑎} = {𝑡})
149	148	xpeq2d 5671	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑎 = 𝑡 → ((0[,]1) × {𝑎}) = ((0[,]1) × {𝑡}))
150	149	sseq1d 3981	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑎 = 𝑡 → (((0[,]1) × {𝑎}) ⊆ 𝑀 ↔ ((0[,]1) × {𝑡}) ⊆ 𝑀))
151	150, 140	elrab2 3665	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑡 ∈ 𝐴 ↔ (𝑡 ∈ (0[,]1) ∧ ((0[,]1) × {𝑡}) ⊆ 𝑀))
152	151	baib 535	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 ∈ (0[,]1) → (𝑡 ∈ 𝐴 ↔ ((0[,]1) × {𝑡}) ⊆ 𝑀))
153	147, 152	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑎 ∈ (0[,]1)) ∧ 𝑣 ∈ II) ∧ 𝑡 ∈ 𝑣) → (𝑡 ∈ 𝐴 ↔ ((0[,]1) × {𝑡}) ⊆ 𝑀))
154	143, 153	bibi12d 345	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑎 ∈ (0[,]1)) ∧ 𝑣 ∈ II) ∧ 𝑡 ∈ 𝑣) → ((𝑎 ∈ 𝐴 ↔ 𝑡 ∈ 𝐴) ↔ (((0[,]1) × {𝑎}) ⊆ 𝑀 ↔ ((0[,]1) × {𝑡}) ⊆ 𝑀)))
155	139, 154	imbitrrid 246	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑎 ∈ (0[,]1)) ∧ 𝑣 ∈ II) ∧ 𝑡 ∈ 𝑣) → (∀𝑟 ∈ (0[,]1)(𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀)) → (𝑎 ∈ 𝐴 ↔ 𝑡 ∈ 𝐴)))
156	155	ralimdva 3146	. . . . . . . . . . . . . . . 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 612	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑎 ∈ (0[,]1)) ∧ 𝑣 ∈ II) → ((𝑎 ∈ 𝑣 ∧ ((0[,]1) × 𝑣) ⊆ ((int‘(II ×_t II))‘𝑆)) → (𝑎 ∈ 𝑣 ∧ ∀𝑡 ∈ 𝑣 (𝑎 ∈ 𝐴 ↔ 𝑡 ∈ 𝐴))))
159	158	reximdva 3147	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑎 ∈ (0[,]1)) → (∃𝑣 ∈ II (𝑎 ∈ 𝑣 ∧ ((0[,]1) × 𝑣) ⊆ ((int‘(II ×_t II))‘𝑆)) → ∃𝑣 ∈ II (𝑎 ∈ 𝑣 ∧ ∀𝑡 ∈ 𝑣 (𝑎 ∈ 𝐴 ↔ 𝑡 ∈ 𝐴))))
160	117, 159	mpd 15	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑎 ∈ (0[,]1)) → ∃𝑣 ∈ II (𝑎 ∈ 𝑣 ∧ ∀𝑡 ∈ 𝑣 (𝑎 ∈ 𝐴 ↔ 𝑡 ∈ 𝐴)))
161	160	ralrimiva 3126	. . . . . . . . . . 11 ⊢ (𝜑 → ∀𝑎 ∈ (0[,]1)∃𝑣 ∈ II (𝑎 ∈ 𝑣 ∧ ∀𝑡 ∈ 𝑣 (𝑎 ∈ 𝐴 ↔ 𝑡 ∈ 𝐴)))
162		ssrab2 4046	. . . . . . . . . . . . 13 ⊢ {𝑎 ∈ (0[,]1) ∣ ((0[,]1) × {𝑎}) ⊆ 𝑀} ⊆ (0[,]1)
163	140, 162	eqsstri 3996	. . . . . . . . . . . 12 ⊢ 𝐴 ⊆ (0[,]1)
164	13	isclo 22981	. . . . . . . . . . . 12 ⊢ ((II ∈ Top ∧ 𝐴 ⊆ (0[,]1)) → (𝐴 ∈ (II ∩ (Clsd‘II)) ↔ ∀𝑎 ∈ (0[,]1)∃𝑣 ∈ II (𝑎 ∈ 𝑣 ∧ ∀𝑡 ∈ 𝑣 (𝑎 ∈ 𝐴 ↔ 𝑡 ∈ 𝐴))))
165	19, 163, 164	mp2an 692	. . . . . . . . . . 11 ⊢ (𝐴 ∈ (II ∩ (Clsd‘II)) ↔ ∀𝑎 ∈ (0[,]1)∃𝑣 ∈ II (𝑎 ∈ 𝑣 ∧ ∀𝑡 ∈ 𝑣 (𝑎 ∈ 𝐴 ↔ 𝑡 ∈ 𝐴)))
166	161, 165	sylibr 234	. . . . . . . . . 10 ⊢ (𝜑 → 𝐴 ∈ (II ∩ (Clsd‘II)))
167	16, 166	sselid 3947	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 ∈ II)
168		0elunit 13437	. . . . . . . . . . . 12 ⊢ 0 ∈ (0[,]1)
169	168	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → 0 ∈ (0[,]1))
170		relxp 5659	. . . . . . . . . . . . 13 ⊢ Rel ((0[,]1) × {0})
171	170	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → Rel ((0[,]1) × {0}))
172		opelxp 5677	. . . . . . . . . . . . 13 ⊢ (⟨𝑟, 𝑎⟩ ∈ ((0[,]1) × {0}) ↔ (𝑟 ∈ (0[,]1) ∧ 𝑎 ∈ {0}))
173		id 22	. . . . . . . . . . . . . . . . 17 ⊢ (𝑟 ∈ (0[,]1) → 𝑟 ∈ (0[,]1))
174		opelxpi 5678	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑟 ∈ (0[,]1) ∧ 0 ∈ (0[,]1)) → ⟨𝑟, 0⟩ ∈ ((0[,]1) × (0[,]1)))
175	173, 169, 174	syl2anr 597	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑟 ∈ (0[,]1)) → ⟨𝑟, 0⟩ ∈ ((0[,]1) × (0[,]1)))
176	2	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑟 ∈ (0[,]1)) → 𝐹 ∈ (𝐶 CovMap 𝐽))
177	3	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑟 ∈ (0[,]1)) → 𝐺 ∈ ((II ×_t II) Cn 𝐽))
178	4	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑟 ∈ (0[,]1)) → 𝑃 ∈ 𝐵)
179	5	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑟 ∈ (0[,]1)) → (𝐹‘𝑃) = (0𝐺0))
180		simpr 484	. . . . . . . . . . . . . . . . . 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 35306	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑟 ∈ (0[,]1)) → ∃𝑢 ∈ II ∃𝑣 ∈ II (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×_t II) ↾_t (𝑢 × 𝑣)) Cn 𝐶))))
183		df-3an 1088	. . . . . . . . . . . . . . . . . . 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 772	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → 0 ∈ 𝑣)
185	8	ad3antrrr 730	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → 𝐾:((0[,]1) × (0[,]1))⟶𝐵)
186	185	ffnd 6692	. . . . . . . . . . . . . . . . . . . . . . . . . 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 218	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → 𝐾 = (𝑏 ∈ (0[,]1), 𝑤 ∈ (0[,]1) ↦ (𝑏𝐾𝑤)))
189	188	reseq1d 5952	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → (𝐾 ↾ (𝑢 × {0})) = ((𝑏 ∈ (0[,]1), 𝑤 ∈ (0[,]1) ↦ (𝑏𝐾𝑤)) ↾ (𝑢 × {0})))
190		simplrl 776	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → 𝑢 ∈ II)
191		elssuni 4904	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑢 ∈ II → 𝑢 ⊆ ∪ II)
192	191, 13	sseqtrrdi 3991	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑢 ∈ II → 𝑢 ⊆ (0[,]1))
193	190, 192	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → 𝑢 ⊆ (0[,]1))
194	169	snssd 4776	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → {0} ⊆ (0[,]1))
195	194	ad3antrrr 730	. . . . . . . . . . . . . . . . . . . . . . . . 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 584	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → ((𝑏 ∈ (0[,]1), 𝑤 ∈ (0[,]1) ↦ (𝑏𝐾𝑤)) ↾ (𝑢 × {0})) = (𝑏 ∈ 𝑢, 𝑤 ∈ {0} ↦ (𝑏𝐾𝑤)))
198	193	sselda 3949	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) ∧ 𝑏 ∈ 𝑢) → 𝑏 ∈ (0[,]1))
199		simplll 774	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → 𝜑)
200	1, 2, 3, 4, 5, 6, 7	cvmlift2lem8 35304	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑏 ∈ (0[,]1)) → (𝑏𝐾0) = (𝐻‘𝑏))
201	199, 200	sylan 580	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) ∧ 𝑏 ∈ (0[,]1)) → (𝑏𝐾0) = (𝐻‘𝑏))
202	198, 201	syldan 591	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) ∧ 𝑏 ∈ 𝑢) → (𝑏𝐾0) = (𝐻‘𝑏))
203		elsni 4609	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑤 ∈ {0} → 𝑤 = 0)
204	203	oveq2d 7406	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑤 ∈ {0} → (𝑏𝐾𝑤) = (𝑏𝐾0))
205	204	eqeq1d 2732	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑤 ∈ {0} → ((𝑏𝐾𝑤) = (𝐻‘𝑏) ↔ (𝑏𝐾0) = (𝐻‘𝑏)))
206	202, 205	syl5ibrcom 247	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) ∧ 𝑏 ∈ 𝑢) → (𝑤 ∈ {0} → (𝑏𝐾𝑤) = (𝐻‘𝑏)))
207	206	3impia 1117	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) ∧ 𝑏 ∈ 𝑢 ∧ 𝑤 ∈ {0}) → (𝑏𝐾𝑤) = (𝐻‘𝑏))
208	207	mpoeq3dva 7469	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → (𝑏 ∈ 𝑢, 𝑤 ∈ {0} ↦ (𝑏𝐾𝑤)) = (𝑏 ∈ 𝑢, 𝑤 ∈ {0} ↦ (𝐻‘𝑏)))
209	189, 197, 208	3eqtrd 2769	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → (𝐾 ↾ (𝑢 × {0})) = (𝑏 ∈ 𝑢, 𝑤 ∈ {0} ↦ (𝐻‘𝑏)))
210		eqid 2730	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (II ↾_t 𝑢) = (II ↾_t 𝑢)
211		iitopon 24779	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ II ∈ (TopOn‘(0[,]1))
212	211	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → II ∈ (TopOn‘(0[,]1)))
213		eqid 2730	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (II ↾_t {0}) = (II ↾_t {0})
214	212, 212	cnmpt1st 23562	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → (𝑏 ∈ (0[,]1), 𝑤 ∈ (0[,]1) ↦ 𝑏) ∈ ((II ×_t II) Cn II))
215	1, 2, 3, 4, 5, 6	cvmlift2lem2 35298	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → (𝐻 ∈ (II Cn 𝐶) ∧ (𝐹 ∘ 𝐻) = (𝑧 ∈ (0[,]1) ↦ (𝑧𝐺0)) ∧ (𝐻‘0) = 𝑃))
216	215	simp1d 1142	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → 𝐻 ∈ (II Cn 𝐶))
217	199, 216	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → 𝐻 ∈ (II Cn 𝐶))
218	212, 212, 214, 217	cnmpt21f 23566	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → (𝑏 ∈ (0[,]1), 𝑤 ∈ (0[,]1) ↦ (𝐻‘𝑏)) ∈ ((II ×_t II) Cn 𝐶))
219	210, 212, 193, 213, 212, 195, 218	cnmpt2res 23571	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → (𝑏 ∈ 𝑢, 𝑤 ∈ {0} ↦ (𝐻‘𝑏)) ∈ (((II ↾_t 𝑢) ×_t (II ↾_t {0})) Cn 𝐶))
220		vex 3454	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ 𝑢 ∈ V
221		snex 5394	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ {0} ∈ V
222		txrest 23525	. . . . . . . . . . . . . . . . . . . . . . . . . 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 693	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((II ×_t II) ↾_t (𝑢 × {0})) = ((II ↾_t 𝑢) ×_t (II ↾_t {0}))
224	223	oveq1i 7400	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((II ×_t II) ↾_t (𝑢 × {0})) Cn 𝐶) = (((II ↾_t 𝑢) ×_t (II ↾_t {0})) Cn 𝐶)
225	219, 224	eleqtrrdi 2840	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → (𝑏 ∈ 𝑢, 𝑤 ∈ {0} ↦ (𝐻‘𝑏)) ∈ (((II ×_t II) ↾_t (𝑢 × {0})) Cn 𝐶))
226	209, 225	eqeltrd 2829	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → (𝐾 ↾ (𝑢 × {0})) ∈ (((II ×_t II) ↾_t (𝑢 × {0})) Cn 𝐶))
227		sneq 4602	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑤 = 0 → {𝑤} = {0})
228	227	xpeq2d 5671	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑤 = 0 → (𝑢 × {𝑤}) = (𝑢 × {0}))
229	228	reseq2d 5953	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑤 = 0 → (𝐾 ↾ (𝑢 × {𝑤})) = (𝐾 ↾ (𝑢 × {0})))
230	228	oveq2d 7406	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑤 = 0 → ((II ×_t II) ↾_t (𝑢 × {𝑤})) = ((II ×_t II) ↾_t (𝑢 × {0})))
231	230	oveq1d 7405	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑤 = 0 → (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶) = (((II ×_t II) ↾_t (𝑢 × {0})) Cn 𝐶))
232	229, 231	eleq12d 2823	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 = 0 → ((𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶) ↔ (𝐾 ↾ (𝑢 × {0})) ∈ (((II ×_t II) ↾_t (𝑢 × {0})) Cn 𝐶)))
233	232	rspcev 3591	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((0 ∈ 𝑣 ∧ (𝐾 ↾ (𝑢 × {0})) ∈ (((II ×_t II) ↾_t (𝑢 × {0})) Cn 𝐶)) → ∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶))
234	184, 226, 233	syl2anc 584	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → ∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶))
235		opelxpi 5678	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣) → ⟨𝑟, 0⟩ ∈ (𝑢 × 𝑣))
236	235	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → ⟨𝑟, 0⟩ ∈ (𝑢 × 𝑣))
237		simplrr 777	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → 𝑣 ∈ II)
238	237, 145	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → 𝑣 ⊆ (0[,]1))
239		xpss12 5656	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑢 ⊆ (0[,]1) ∧ 𝑣 ⊆ (0[,]1)) → (𝑢 × 𝑣) ⊆ ((0[,]1) × (0[,]1)))
240	193, 238, 239	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → (𝑢 × 𝑣) ⊆ ((0[,]1) × (0[,]1)))
241	36	restuni 23056	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((II ×_t II) ∈ Top ∧ (𝑢 × 𝑣) ⊆ ((0[,]1) × (0[,]1))) → (𝑢 × 𝑣) = ∪ ((II ×_t II) ↾_t (𝑢 × 𝑣)))
242	21, 240, 241	sylancr 587	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → (𝑢 × 𝑣) = ∪ ((II ×_t II) ↾_t (𝑢 × 𝑣)))
243	236, 242	eleqtrd 2831	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → ⟨𝑟, 0⟩ ∈ ∪ ((II ×_t II) ↾_t (𝑢 × 𝑣)))
244		eqid 2730	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ∪ ((II ×_t II) ↾_t (𝑢 × 𝑣)) = ∪ ((II ×_t II) ↾_t (𝑢 × 𝑣))
245	244	cncnpi 23172	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×_t II) ↾_t (𝑢 × 𝑣)) Cn 𝐶) ∧ ⟨𝑟, 0⟩ ∈ ∪ ((II ×_t II) ↾_t (𝑢 × 𝑣))) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ ((((II ×_t II) ↾_t (𝑢 × 𝑣)) CnP 𝐶)‘⟨𝑟, 0⟩))
246	245	expcom 413	. . . . . . . . . . . . . . . . . . . . . . 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 838	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → (𝑢 × 𝑣) ∈ (II ×_t II))
251		isopn3i 22976	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((II ×_t II) ∈ Top ∧ (𝑢 × 𝑣) ∈ (II ×_t II)) → ((int‘(II ×_t II))‘(𝑢 × 𝑣)) = (𝑢 × 𝑣))
252	21, 250, 251	sylancr 587	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → ((int‘(II ×_t II))‘(𝑢 × 𝑣)) = (𝑢 × 𝑣))
253	236, 252	eleqtrrd 2832	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → ⟨𝑟, 0⟩ ∈ ((int‘(II ×_t II))‘(𝑢 × 𝑣)))
254	36, 1	cnprest 23183	. . . . . . . . . . . . . . . . . . . . . . 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 838	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → (𝐾 ∈ (((II ×_t II) CnP 𝐶)‘⟨𝑟, 0⟩) ↔ (𝐾 ↾ (𝑢 × 𝑣)) ∈ ((((II ×_t II) ↾_t (𝑢 × 𝑣)) CnP 𝐶)‘⟨𝑟, 0⟩)))
256	247, 255	sylibrd 259	. . . . . . . . . . . . . . . . . . . . 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 453	. . . . . . . . . . . . . . . . . . 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 242	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) → ((𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×_t II) ↾_t (𝑢 × 𝑣)) Cn 𝐶))) → 𝐾 ∈ (((II ×_t II) CnP 𝐶)‘⟨𝑟, 0⟩)))
260	259	rexlimdvva 3195	. . . . . . . . . . . . . . . . 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 6861	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = ⟨𝑟, 0⟩ → (((II ×_t II) CnP 𝐶)‘𝑧) = (((II ×_t II) CnP 𝐶)‘⟨𝑟, 0⟩))
263	262	eleq2d 2815	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = ⟨𝑟, 0⟩ → (𝐾 ∈ (((II ×_t II) CnP 𝐶)‘𝑧) ↔ 𝐾 ∈ (((II ×_t II) CnP 𝐶)‘⟨𝑟, 0⟩)))
264	263, 68	elrab2 3665	. . . . . . . . . . . . . . . 16 ⊢ (⟨𝑟, 0⟩ ∈ 𝑀 ↔ (⟨𝑟, 0⟩ ∈ ((0[,]1) × (0[,]1)) ∧ 𝐾 ∈ (((II ×_t II) CnP 𝐶)‘⟨𝑟, 0⟩)))
265	175, 261, 264	sylanbrc 583	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑟 ∈ (0[,]1)) → ⟨𝑟, 0⟩ ∈ 𝑀)
266		elsni 4609	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 ∈ {0} → 𝑎 = 0)
267	266	opeq2d 4847	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 ∈ {0} → ⟨𝑟, 𝑎⟩ = ⟨𝑟, 0⟩)
268	267	eleq1d 2814	. . . . . . . . . . . . . . 15 ⊢ (𝑎 ∈ {0} → (⟨𝑟, 𝑎⟩ ∈ 𝑀 ↔ ⟨𝑟, 0⟩ ∈ 𝑀))
269	265, 268	syl5ibrcom 247	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑟 ∈ (0[,]1)) → (𝑎 ∈ {0} → ⟨𝑟, 𝑎⟩ ∈ 𝑀))
270	269	expimpd 453	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑟 ∈ (0[,]1) ∧ 𝑎 ∈ {0}) → ⟨𝑟, 𝑎⟩ ∈ 𝑀))
271	172, 270	biimtrid 242	. . . . . . . . . . . 12 ⊢ (𝜑 → (⟨𝑟, 𝑎⟩ ∈ ((0[,]1) × {0}) → ⟨𝑟, 𝑎⟩ ∈ 𝑀))
272	171, 271	relssdv 5754	. . . . . . . . . . 11 ⊢ (𝜑 → ((0[,]1) × {0}) ⊆ 𝑀)
273		sneq 4602	. . . . . . . . . . . . . 14 ⊢ (𝑎 = 0 → {𝑎} = {0})
274	273	xpeq2d 5671	. . . . . . . . . . . . 13 ⊢ (𝑎 = 0 → ((0[,]1) × {𝑎}) = ((0[,]1) × {0}))
275	274	sseq1d 3981	. . . . . . . . . . . 12 ⊢ (𝑎 = 0 → (((0[,]1) × {𝑎}) ⊆ 𝑀 ↔ ((0[,]1) × {0}) ⊆ 𝑀))
276	275, 140	elrab2 3665	. . . . . . . . . . 11 ⊢ (0 ∈ 𝐴 ↔ (0 ∈ (0[,]1) ∧ ((0[,]1) × {0}) ⊆ 𝑀))
277	169, 272, 276	sylanbrc 583	. . . . . . . . . 10 ⊢ (𝜑 → 0 ∈ 𝐴)
278	277	ne0d 4308	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 ≠ ∅)
279		inss2 4204	. . . . . . . . . 10 ⊢ (II ∩ (Clsd‘II)) ⊆ (Clsd‘II)
280	279, 166	sselid 3947	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 ∈ (Clsd‘II))
281	13, 15, 167, 278, 280	connclo 23309	. . . . . . . 8 ⊢ (𝜑 → 𝐴 = (0[,]1))
282	281, 140	eqtr3di 2780	. . . . . . 7 ⊢ (𝜑 → (0[,]1) = {𝑎 ∈ (0[,]1) ∣ ((0[,]1) × {𝑎}) ⊆ 𝑀})
283		rabid2 3442	. . . . . . 7 ⊢ ((0[,]1) = {𝑎 ∈ (0[,]1) ∣ ((0[,]1) × {𝑎}) ⊆ 𝑀} ↔ ∀𝑎 ∈ (0[,]1)((0[,]1) × {𝑎}) ⊆ 𝑀)
284	282, 283	sylib 218	. . . . . 6 ⊢ (𝜑 → ∀𝑎 ∈ (0[,]1)((0[,]1) × {𝑎}) ⊆ 𝑀)
285		iunss 5012	. . . . . 6 ⊢ (∪ 𝑎 ∈ (0[,]1)((0[,]1) × {𝑎}) ⊆ 𝑀 ↔ ∀𝑎 ∈ (0[,]1)((0[,]1) × {𝑎}) ⊆ 𝑀)
286	284, 285	sylibr 234	. . . . 5 ⊢ (𝜑 → ∪ 𝑎 ∈ (0[,]1)((0[,]1) × {𝑎}) ⊆ 𝑀)
287	12, 286	eqsstrid 3988	. . . 4 ⊢ (𝜑 → ((0[,]1) × (0[,]1)) ⊆ 𝑀)
288	287, 68	sseqtrdi 3990	. . 3 ⊢ (𝜑 → ((0[,]1) × (0[,]1)) ⊆ {𝑧 ∈ ((0[,]1) × (0[,]1)) ∣ 𝐾 ∈ (((II ×_t II) CnP 𝐶)‘𝑧)})
289		ssrab 4039	. . . 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 496	. . 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 23485	. . . 4 ⊢ ((II ∈ (TopOn‘(0[,]1)) ∧ II ∈ (TopOn‘(0[,]1))) → (II ×_t II) ∈ (TopOn‘((0[,]1) × (0[,]1))))
293	211, 211, 292	mp2an 692	. . 3 ⊢ (II ×_t II) ∈ (TopOn‘((0[,]1) × (0[,]1)))
294		cvmtop1 35254	. . . . 5 ⊢ (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐶 ∈ Top)
295	2, 294	syl 17	. . . 4 ⊢ (𝜑 → 𝐶 ∈ Top)
296	1	toptopon 22811	. . . 4 ⊢ (𝐶 ∈ Top ↔ 𝐶 ∈ (TopOn‘𝐵))
297	295, 296	sylib 218	. . 3 ⊢ (𝜑 → 𝐶 ∈ (TopOn‘𝐵))
298		cncnp 23174	. . 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 587	. 2 ⊢ (𝜑 → (𝐾 ∈ ((II ×_t II) Cn 𝐶) ↔ (𝐾:((0[,]1) × (0[,]1))⟶𝐵 ∧ ∀𝑧 ∈ ((0[,]1) × (0[,]1))𝐾 ∈ (((II ×_t II) CnP 𝐶)‘𝑧))))
300	8, 291, 299	mpbir2and 713	1 ⊢ (𝜑 → 𝐾 ∈ ((II ×_t II) Cn 𝐶))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1086 ∀wal 1538 = wceq 1540 ∈ wcel 2109 ∀wral 3045 ∃wrex 3054 {crab 3408 Vcvv 3450 ∖ cdif 3914 ∩ cin 3916 ⊆ wss 3917 ∅c0 4299 𝒫 cpw 4566 {csn 4592 ⟨cop 4598 ∪ cuni 4874 ∪ ciun 4958 {copab 5172 ↦ cmpt 5191 × cxp 5639 ^◡ccnv 5640 ↾ cres 5643 “ cima 5644 ∘ ccom 5645 Rel wrel 5646 Fn wfn 6509 ⟶wf 6510 ‘cfv 6514 ℩crio 7346 (class class class)co 7390 ∈ cmpo 7392 0cc0 11075 1c1 11076 [,]cicc 13316 ↾_t crest 17390 Topctop 22787 TopOnctopon 22804 Clsdccld 22910 intcnt 22911 neicnei 22991 Cn ccn 23118 CnP ccnp 23119 Compccmp 23280 Conncconn 23305 ×_t ctx 23454 Homeochmeo 23647 IIcii 24775 CovMap ccvm 35249

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 2702 ax-rep 5237 ax-sep 5254 ax-nul 5264 ax-pow 5323 ax-pr 5390 ax-un 7714 ax-inf2 9601 ax-cnex 11131 ax-resscn 11132 ax-1cn 11133 ax-icn 11134 ax-addcl 11135 ax-addrcl 11136 ax-mulcl 11137 ax-mulrcl 11138 ax-mulcom 11139 ax-addass 11140 ax-mulass 11141 ax-distr 11142 ax-i2m1 11143 ax-1ne0 11144 ax-1rid 11145 ax-rnegex 11146 ax-rrecex 11147 ax-cnre 11148 ax-pre-lttri 11149 ax-pre-lttrn 11150 ax-pre-ltadd 11151 ax-pre-mulgt0 11152 ax-pre-sup 11153 ax-addf 11154

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 2534 df-eu 2563 df-clab 2709 df-cleq 2722 df-clel 2804 df-nfc 2879 df-ne 2927 df-nel 3031 df-ral 3046 df-rex 3055 df-rmo 3356 df-reu 3357 df-rab 3409 df-v 3452 df-sbc 3757 df-csb 3866 df-dif 3920 df-un 3922 df-in 3924 df-ss 3934 df-pss 3937 df-nul 4300 df-if 4492 df-pw 4568 df-sn 4593 df-pr 4595 df-tp 4597 df-op 4599 df-uni 4875 df-int 4914 df-iun 4960 df-iin 4961 df-br 5111 df-opab 5173 df-mpt 5192 df-tr 5218 df-id 5536 df-eprel 5541 df-po 5549 df-so 5550 df-fr 5594 df-se 5595 df-we 5596 df-xp 5647 df-rel 5648 df-cnv 5649 df-co 5650 df-dm 5651 df-rn 5652 df-res 5653 df-ima 5654 df-pred 6277 df-ord 6338 df-on 6339 df-lim 6340 df-suc 6341 df-iota 6467 df-fun 6516 df-fn 6517 df-f 6518 df-f1 6519 df-fo 6520 df-f1o 6521 df-fv 6522 df-isom 6523 df-riota 7347 df-ov 7393 df-oprab 7394 df-mpo 7395 df-of 7656 df-om 7846 df-1st 7971 df-2nd 7972 df-supp 8143 df-frecs 8263 df-wrecs 8294 df-recs 8343 df-rdg 8381 df-1o 8437 df-2o 8438 df-er 8674 df-ec 8676 df-map 8804 df-ixp 8874 df-en 8922 df-dom 8923 df-sdom 8924 df-fin 8925 df-fsupp 9320 df-fi 9369 df-sup 9400 df-inf 9401 df-oi 9470 df-card 9899 df-pnf 11217 df-mnf 11218 df-xr 11219 df-ltxr 11220 df-le 11221 df-sub 11414 df-neg 11415 df-div 11843 df-nn 12194 df-2 12256 df-3 12257 df-4 12258 df-5 12259 df-6 12260 df-7 12261 df-8 12262 df-9 12263 df-n0 12450 df-z 12537 df-dec 12657 df-uz 12801 df-q 12915 df-rp 12959 df-xneg 13079 df-xadd 13080 df-xmul 13081 df-ioo 13317 df-ico 13319 df-icc 13320 df-fz 13476 df-fzo 13623 df-fl 13761 df-seq 13974 df-exp 14034 df-hash 14303 df-cj 15072 df-re 15073 df-im 15074 df-sqrt 15208 df-abs 15209 df-clim 15461 df-sum 15660 df-struct 17124 df-sets 17141 df-slot 17159 df-ndx 17171 df-base 17187 df-ress 17208 df-plusg 17240 df-mulr 17241 df-starv 17242 df-sca 17243 df-vsca 17244 df-ip 17245 df-tset 17246 df-ple 17247 df-ds 17249 df-unif 17250 df-hom 17251 df-cco 17252 df-rest 17392 df-topn 17393 df-0g 17411 df-gsum 17412 df-topgen 17413 df-pt 17414 df-prds 17417 df-xrs 17472 df-qtop 17477 df-imas 17478 df-xps 17480 df-mre 17554 df-mrc 17555 df-acs 17557 df-mgm 18574 df-sgrp 18653 df-mnd 18669 df-submnd 18718 df-mulg 19007 df-cntz 19256 df-cmn 19719 df-psmet 21263 df-xmet 21264 df-met 21265 df-bl 21266 df-mopn 21267 df-cnfld 21272 df-top 22788 df-topon 22805 df-topsp 22827 df-bases 22840 df-cld 22913 df-ntr 22914 df-cls 22915 df-nei 22992 df-cn 23121 df-cnp 23122 df-cmp 23281 df-conn 23306 df-lly 23360 df-nlly 23361 df-tx 23456 df-hmeo 23649 df-xms 24215 df-ms 24216 df-tms 24217 df-ii 24777 df-cncf 24778 df-htpy 24876 df-phtpy 24877 df-phtpc 24898 df-pconn 35215 df-sconn 35216 df-cvm 35250

This theorem is referenced by: cvmlift2lem13 35309

W3C validator