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 32674

Description: Lemma for cvmlift2 32676. (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 32667	. 2 ⊢ (𝜑 → 𝐾:((0[,]1) × (0[,]1))⟶𝐵)
9		iunid 4947	. . . . . . 7 ⊢ ∪ 𝑎 ∈ (0[,]1){𝑎} = (0[,]1)
10	9	xpeq2i 5546	. . . . . 6 ⊢ ((0[,]1) × ∪ 𝑎 ∈ (0[,]1){𝑎}) = ((0[,]1) × (0[,]1))
11		xpiundi 5586	. . . . . 6 ⊢ ((0[,]1) × ∪ 𝑎 ∈ (0[,]1){𝑎}) = ∪ 𝑎 ∈ (0[,]1)((0[,]1) × {𝑎})
12	10, 11	eqtr3i 2823	. . . . 5 ⊢ ((0[,]1) × (0[,]1)) = ∪ 𝑎 ∈ (0[,]1)((0[,]1) × {𝑎})
13		cvmlift2.a	. . . . . . . 8 ⊢ 𝐴 = {𝑎 ∈ (0[,]1) ∣ ((0[,]1) × {𝑎}) ⊆ 𝑀}
14		iiuni 23486	. . . . . . . . 9 ⊢ (0[,]1) = ∪ II
15		iiconn 23492	. . . . . . . . . 10 ⊢ II ∈ Conn
16	15	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → II ∈ Conn)
17		inss1 4155	. . . . . . . . . 10 ⊢ (II ∩ (Clsd‘II)) ⊆ II
18		iicmp 23491	. . . . . . . . . . . . . . 15 ⊢ II ∈ Comp
19	18	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑎 ∈ (0[,]1)) → II ∈ Comp)
20		iitop 23485	. . . . . . . . . . . . . . 15 ⊢ II ∈ Top
21	20	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑎 ∈ (0[,]1)) → II ∈ Top)
22	20, 20	txtopi 22195	. . . . . . . . . . . . . . . 16 ⊢ (II ×_t II) ∈ Top
23	14	neiss2 21706	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((II ∈ Top ∧ 𝑢 ∈ ((nei‘II)‘{𝑟})) → {𝑟} ⊆ (0[,]1))
24	20, 23	mpan 689	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑢 ∈ ((nei‘II)‘{𝑟}) → {𝑟} ⊆ (0[,]1))
25		vex 3444	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 𝑟 ∈ V
26	25	snss 4679	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑟 ∈ (0[,]1) ↔ {𝑟} ⊆ (0[,]1))
27	24, 26	sylibr 237	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑢 ∈ ((nei‘II)‘{𝑟}) → 𝑟 ∈ (0[,]1))
28	27	a1d 25	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑢 ∈ ((nei‘II)‘{𝑟}) → (((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀) → 𝑟 ∈ (0[,]1)))
29	28	rexlimiv 3239	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀) → 𝑟 ∈ (0[,]1))
30	29	adantl 485	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀)) → 𝑟 ∈ (0[,]1))
31		simpl 486	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀)) → 𝑡 ∈ (0[,]1))
32	30, 31	jca 515	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀)) → (𝑟 ∈ (0[,]1) ∧ 𝑡 ∈ (0[,]1)))
33	32	ssopab2i 5402	. . . . . . . . . . . . . . . . 17 ⊢ {⟨𝑟, 𝑡⟩ ∣ (𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀))} ⊆ {⟨𝑟, 𝑡⟩ ∣ (𝑟 ∈ (0[,]1) ∧ 𝑡 ∈ (0[,]1))}
34		cvmlift2.s	. . . . . . . . . . . . . . . . 17 ⊢ 𝑆 = {⟨𝑟, 𝑡⟩ ∣ (𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀))}
35		df-xp 5525	. . . . . . . . . . . . . . . . 17 ⊢ ((0[,]1) × (0[,]1)) = {⟨𝑟, 𝑡⟩ ∣ (𝑟 ∈ (0[,]1) ∧ 𝑡 ∈ (0[,]1))}
36	33, 34, 35	3sstr4i 3958	. . . . . . . . . . . . . . . 16 ⊢ 𝑆 ⊆ ((0[,]1) × (0[,]1))
37	20, 20, 14, 14	txunii 22198	. . . . . . . . . . . . . . . . 17 ⊢ ((0[,]1) × (0[,]1)) = ∪ (II ×_t II)
38	37	ntropn 21654	. . . . . . . . . . . . . . . 16 ⊢ (((II ×_t II) ∈ Top ∧ 𝑆 ⊆ ((0[,]1) × (0[,]1))) → ((int‘(II ×_t II))‘𝑆) ∈ (II ×_t II))
39	22, 36, 38	mp2an 691	. . . . . . . . . . . . . . 15 ⊢ ((int‘(II ×_t II))‘𝑆) ∈ (II ×_t II)
40	39	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑎 ∈ (0[,]1)) → ((int‘(II ×_t II))‘𝑆) ∈ (II ×_t II))
41	2	adantr 484	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) → 𝐹 ∈ (𝐶 CovMap 𝐽))
42	3	adantr 484	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) → 𝐺 ∈ ((II ×_t II) Cn 𝐽))
43	4	adantr 484	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) → 𝑃 ∈ 𝐵)
44	5	adantr 484	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) → (𝐹‘𝑃) = (0𝐺0))
45		eqid 2798	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (^◡𝐹 “ 𝑘) ∧ ∀𝑐 ∈ 𝑠 (∀𝑑 ∈ (𝑠 ∖ {𝑐})(𝑐 ∩ 𝑑) = ∅ ∧ (𝐹 ↾ 𝑐) ∈ ((𝐶 ↾_t 𝑐)Homeo(𝐽 ↾_t 𝑘))))}) = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (^◡𝐹 “ 𝑘) ∧ ∀𝑐 ∈ 𝑠 (∀𝑑 ∈ (𝑠 ∖ {𝑐})(𝑐 ∩ 𝑑) = ∅ ∧ (𝐹 ↾ 𝑐) ∈ ((𝐶 ↾_t 𝑐)Homeo(𝐽 ↾_t 𝑘))))})
46		simprr 772	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) → 𝑏 ∈ (0[,]1))
47		simprl 770	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) → 𝑎 ∈ (0[,]1))
48	1, 41, 42, 43, 44, 6, 7, 45, 46, 47	cvmlift2lem10 32672	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) → ∃𝑢 ∈ II ∃𝑣 ∈ II (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×_t II) ↾_t (𝑢 × 𝑣)) Cn 𝐶))))
49	22	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×_t II) ↾_t (𝑢 × 𝑣)) Cn 𝐶)))) → (II ×_t II) ∈ Top)
50	36	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×_t II) ↾_t (𝑢 × 𝑣)) Cn 𝐶)))) → 𝑆 ⊆ ((0[,]1) × (0[,]1)))
51	20	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×_t II) ↾_t (𝑢 × 𝑣)) Cn 𝐶)))) → II ∈ Top)
52		simplrl 776	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×_t II) ↾_t (𝑢 × 𝑣)) Cn 𝐶)))) → 𝑢 ∈ II)
53		simplrr 777	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×_t II) ↾_t (𝑢 × 𝑣)) Cn 𝐶)))) → 𝑣 ∈ II)
54		txopn 22207	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((II ∈ Top ∧ II ∈ Top) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) → (𝑢 × 𝑣) ∈ (II ×_t II))
55	51, 51, 52, 53, 54	syl22anc 837	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×_t II) ↾_t (𝑢 × 𝑣)) Cn 𝐶)))) → (𝑢 × 𝑣) ∈ (II ×_t II))
56		simpr 488	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣) → 𝑡 ∈ 𝑣)
57		elunii 4805	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑡 ∈ 𝑣 ∧ 𝑣 ∈ II) → 𝑡 ∈ ∪ II)
58	57, 14	eleqtrrdi 2901	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑡 ∈ 𝑣 ∧ 𝑣 ∈ II) → 𝑡 ∈ (0[,]1))
59	56, 53, 58	syl2anr 599	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×_t II) ↾_t (𝑢 × 𝑣)) Cn 𝐶)))) ∧ (𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣)) → 𝑡 ∈ (0[,]1))
60	20	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×_t II) ↾_t (𝑢 × 𝑣)) Cn 𝐶)))) ∧ (𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣)) → II ∈ Top)
61	52	adantr 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×_t II) ↾_t (𝑢 × 𝑣)) Cn 𝐶)))) ∧ (𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣)) → 𝑢 ∈ II)
62		simprl 770	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×_t II) ↾_t (𝑢 × 𝑣)) Cn 𝐶)))) ∧ (𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣)) → 𝑟 ∈ 𝑢)
63		opnneip 21724	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((II ∈ Top ∧ 𝑢 ∈ II ∧ 𝑟 ∈ 𝑢) → 𝑢 ∈ ((nei‘II)‘{𝑟}))
64	60, 61, 62, 63	syl3anc 1368	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×_t II) ↾_t (𝑢 × 𝑣)) Cn 𝐶)))) ∧ (𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣)) → 𝑢 ∈ ((nei‘II)‘{𝑟}))
65	41	ad3antrrr 729	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×_t II) ↾_t (𝑢 × 𝑣)) Cn 𝐶)))) ∧ (𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣)) → 𝐹 ∈ (𝐶 CovMap 𝐽))
66	42	ad3antrrr 729	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×_t II) ↾_t (𝑢 × 𝑣)) Cn 𝐶)))) ∧ (𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣)) → 𝐺 ∈ ((II ×_t II) Cn 𝐽))
67	43	ad3antrrr 729	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×_t II) ↾_t (𝑢 × 𝑣)) Cn 𝐶)))) ∧ (𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣)) → 𝑃 ∈ 𝐵)
68	44	ad3antrrr 729	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×_t II) ↾_t (𝑢 × 𝑣)) Cn 𝐶)))) ∧ (𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣)) → (𝐹‘𝑃) = (0𝐺0))
69		cvmlift2.m	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ 𝑀 = {𝑧 ∈ ((0[,]1) × (0[,]1)) ∣ 𝐾 ∈ (((II ×_t II) CnP 𝐶)‘𝑧)}
70	53	adantr 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×_t II) ↾_t (𝑢 × 𝑣)) Cn 𝐶)))) ∧ (𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣)) → 𝑣 ∈ II)
71		simplr2 1213	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×_t II) ↾_t (𝑢 × 𝑣)) Cn 𝐶)))) ∧ (𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣)) → 𝑎 ∈ 𝑣)
72		simprr 772	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×_t II) ↾_t (𝑢 × 𝑣)) Cn 𝐶)))) ∧ (𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣)) → 𝑡 ∈ 𝑣)
73		sneq 4535	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑐 = 𝑤 → {𝑐} = {𝑤})
74	73	xpeq2d 5549	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑐 = 𝑤 → (𝑢 × {𝑐}) = (𝑢 × {𝑤}))
75	74	reseq2d 5818	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑐 = 𝑤 → (𝐾 ↾ (𝑢 × {𝑐})) = (𝐾 ↾ (𝑢 × {𝑤})))
76	74	oveq2d 7151	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑐 = 𝑤 → ((II ×_t II) ↾_t (𝑢 × {𝑐})) = ((II ×_t II) ↾_t (𝑢 × {𝑤})))
77	76	oveq1d 7150	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑐 = 𝑤 → (((II ×_t II) ↾_t (𝑢 × {𝑐})) Cn 𝐶) = (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶))
78	75, 77	eleq12d 2884	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑐 = 𝑤 → ((𝐾 ↾ (𝑢 × {𝑐})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑐})) Cn 𝐶) ↔ (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶)))
79	78	cbvrexvw 3397	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (∃𝑐 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑐})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑐})) Cn 𝐶) ↔ ∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶))
80		simplr3 1214	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 𝐶)))
81	79, 80	syl5bi 245	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 𝐶)))
82	1, 65, 66, 67, 68, 6, 7, 69, 61, 70, 71, 72, 81	cvmlift2lem11 32673	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×_t II) ↾_t (𝑢 × 𝑣)) Cn 𝐶)))) ∧ (𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣)) → ((𝑢 × {𝑎}) ⊆ 𝑀 → (𝑢 × {𝑡}) ⊆ 𝑀))
83	1, 65, 66, 67, 68, 6, 7, 69, 61, 70, 72, 71, 81	cvmlift2lem11 32673	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×_t II) ↾_t (𝑢 × 𝑣)) Cn 𝐶)))) ∧ (𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣)) → ((𝑢 × {𝑡}) ⊆ 𝑀 → (𝑢 × {𝑎}) ⊆ 𝑀))
84	82, 83	impbid 215	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×_t II) ↾_t (𝑢 × 𝑣)) Cn 𝐶)))) ∧ (𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣)) → ((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀))
85		rspe 3263	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑢 ∈ ((nei‘II)‘{𝑟}) ∧ ((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀)) → ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀))
86	64, 84, 85	syl2anc 587	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×_t II) ↾_t (𝑢 × 𝑣)) Cn 𝐶)))) ∧ (𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣)) → ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀))
87	59, 86	jca 515	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×_t II) ↾_t (𝑢 × 𝑣)) Cn 𝐶)))) ∧ (𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣)) → (𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀)))
88	87	ex 416	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×_t II) ↾_t (𝑢 × 𝑣)) Cn 𝐶)))) → ((𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣) → (𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀))))
89	88	alrimivv 1929	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×_t II) ↾_t (𝑢 × 𝑣)) Cn 𝐶)))) → ∀𝑟∀𝑡((𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣) → (𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀))))
90		df-xp 5525	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑢 × 𝑣) = {⟨𝑟, 𝑡⟩ ∣ (𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣)}
91	90, 34	sseq12i 3945	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑢 × 𝑣) ⊆ 𝑆 ↔ {⟨𝑟, 𝑡⟩ ∣ (𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣)} ⊆ {⟨𝑟, 𝑡⟩ ∣ (𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀))})
92		ssopab2bw 5399	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ({⟨𝑟, 𝑡⟩ ∣ (𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣)} ⊆ {⟨𝑟, 𝑡⟩ ∣ (𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀))} ↔ ∀𝑟∀𝑡((𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣) → (𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀))))
93	91, 92	bitri 278	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑢 × 𝑣) ⊆ 𝑆 ↔ ∀𝑟∀𝑡((𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣) → (𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀))))
94	89, 93	sylibr 237	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×_t II) ↾_t (𝑢 × 𝑣)) Cn 𝐶)))) → (𝑢 × 𝑣) ⊆ 𝑆)
95	37	ssntr 21663	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((II ×_t II) ∈ Top ∧ 𝑆 ⊆ ((0[,]1) × (0[,]1))) ∧ ((𝑢 × 𝑣) ∈ (II ×_t II) ∧ (𝑢 × 𝑣) ⊆ 𝑆)) → (𝑢 × 𝑣) ⊆ ((int‘(II ×_t II))‘𝑆))
96	49, 50, 55, 94, 95	syl22anc 837	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×_t II) ↾_t (𝑢 × 𝑣)) Cn 𝐶)))) → (𝑢 × 𝑣) ⊆ ((int‘(II ×_t II))‘𝑆))
97		simpr1 1191	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×_t II) ↾_t (𝑢 × 𝑣)) Cn 𝐶)))) → 𝑏 ∈ 𝑢)
98		simpr2 1192	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×_t II) ↾_t (𝑢 × 𝑣)) Cn 𝐶)))) → 𝑎 ∈ 𝑣)
99		opelxpi 5556	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣) → ⟨𝑏, 𝑎⟩ ∈ (𝑢 × 𝑣))
100	97, 98, 99	syl2anc 587	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×_t II) ↾_t (𝑢 × 𝑣)) Cn 𝐶)))) → ⟨𝑏, 𝑎⟩ ∈ (𝑢 × 𝑣))
101	96, 100	sseldd 3916	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×_t II) ↾_t (𝑢 × 𝑣)) Cn 𝐶)))) → ⟨𝑏, 𝑎⟩ ∈ ((int‘(II ×_t II))‘𝑆))
102	101	ex 416	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) → ((𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×_t II) ↾_t (𝑢 × 𝑣)) Cn 𝐶))) → ⟨𝑏, 𝑎⟩ ∈ ((int‘(II ×_t II))‘𝑆)))
103	102	rexlimdvva 3253	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) → (∃𝑢 ∈ II ∃𝑣 ∈ II (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×_t II) ↾_t (𝑢 × 𝑣)) Cn 𝐶))) → ⟨𝑏, 𝑎⟩ ∈ ((int‘(II ×_t II))‘𝑆)))
104	48, 103	mpd 15	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) → ⟨𝑏, 𝑎⟩ ∈ ((int‘(II ×_t II))‘𝑆))
105		vex 3444	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑎 ∈ V
106		opeq2 4765	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 = 𝑎 → ⟨𝑏, 𝑤⟩ = ⟨𝑏, 𝑎⟩)
107	106	eleq1d 2874	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 = 𝑎 → (⟨𝑏, 𝑤⟩ ∈ ((int‘(II ×_t II))‘𝑆) ↔ ⟨𝑏, 𝑎⟩ ∈ ((int‘(II ×_t II))‘𝑆)))
108	105, 107	ralsn 4579	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑤 ∈ {𝑎}⟨𝑏, 𝑤⟩ ∈ ((int‘(II ×_t II))‘𝑆) ↔ ⟨𝑏, 𝑎⟩ ∈ ((int‘(II ×_t II))‘𝑆))
109	104, 108	sylibr 237	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) → ∀𝑤 ∈ {𝑎}⟨𝑏, 𝑤⟩ ∈ ((int‘(II ×_t II))‘𝑆))
110	109	anassrs 471	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑎 ∈ (0[,]1)) ∧ 𝑏 ∈ (0[,]1)) → ∀𝑤 ∈ {𝑎}⟨𝑏, 𝑤⟩ ∈ ((int‘(II ×_t II))‘𝑆))
111	110	ralrimiva 3149	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑎 ∈ (0[,]1)) → ∀𝑏 ∈ (0[,]1)∀𝑤 ∈ {𝑎}⟨𝑏, 𝑤⟩ ∈ ((int‘(II ×_t II))‘𝑆))
112		dfss3 3903	. . . . . . . . . . . . . . . 16 ⊢ (((0[,]1) × {𝑎}) ⊆ ((int‘(II ×_t II))‘𝑆) ↔ ∀𝑢 ∈ ((0[,]1) × {𝑎})𝑢 ∈ ((int‘(II ×_t II))‘𝑆))
113		eleq1 2877	. . . . . . . . . . . . . . . . 17 ⊢ (𝑢 = ⟨𝑏, 𝑤⟩ → (𝑢 ∈ ((int‘(II ×_t II))‘𝑆) ↔ ⟨𝑏, 𝑤⟩ ∈ ((int‘(II ×_t II))‘𝑆)))
114	113	ralxp 5676	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑢 ∈ ((0[,]1) × {𝑎})𝑢 ∈ ((int‘(II ×_t II))‘𝑆) ↔ ∀𝑏 ∈ (0[,]1)∀𝑤 ∈ {𝑎}⟨𝑏, 𝑤⟩ ∈ ((int‘(II ×_t II))‘𝑆))
115	112, 114	bitri 278	. . . . . . . . . . . . . . 15 ⊢ (((0[,]1) × {𝑎}) ⊆ ((int‘(II ×_t II))‘𝑆) ↔ ∀𝑏 ∈ (0[,]1)∀𝑤 ∈ {𝑎}⟨𝑏, 𝑤⟩ ∈ ((int‘(II ×_t II))‘𝑆))
116	111, 115	sylibr 237	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑎 ∈ (0[,]1)) → ((0[,]1) × {𝑎}) ⊆ ((int‘(II ×_t II))‘𝑆))
117		simpr 488	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑎 ∈ (0[,]1)) → 𝑎 ∈ (0[,]1))
118	14, 14, 19, 21, 40, 116, 117	txtube 22245	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑎 ∈ (0[,]1)) → ∃𝑣 ∈ II (𝑎 ∈ 𝑣 ∧ ((0[,]1) × 𝑣) ⊆ ((int‘(II ×_t II))‘𝑆)))
119	37	ntrss2 21662	. . . . . . . . . . . . . . . . . . 19 ⊢ (((II ×_t II) ∈ Top ∧ 𝑆 ⊆ ((0[,]1) × (0[,]1))) → ((int‘(II ×_t II))‘𝑆) ⊆ 𝑆)
120	22, 36, 119	mp2an 691	. . . . . . . . . . . . . . . . . 18 ⊢ ((int‘(II ×_t II))‘𝑆) ⊆ 𝑆
121		sstr 3923	. . . . . . . . . . . . . . . . . 18 ⊢ ((((0[,]1) × 𝑣) ⊆ ((int‘(II ×_t II))‘𝑆) ∧ ((int‘(II ×_t II))‘𝑆) ⊆ 𝑆) → ((0[,]1) × 𝑣) ⊆ 𝑆)
122	120, 121	mpan2 690	. . . . . . . . . . . . . . . . 17 ⊢ (((0[,]1) × 𝑣) ⊆ ((int‘(II ×_t II))‘𝑆) → ((0[,]1) × 𝑣) ⊆ 𝑆)
123		df-xp 5525	. . . . . . . . . . . . . . . . . . 19 ⊢ ((0[,]1) × 𝑣) = {⟨𝑟, 𝑡⟩ ∣ (𝑟 ∈ (0[,]1) ∧ 𝑡 ∈ 𝑣)}
124	123, 34	sseq12i 3945	. . . . . . . . . . . . . . . . . 18 ⊢ (((0[,]1) × 𝑣) ⊆ 𝑆 ↔ {⟨𝑟, 𝑡⟩ ∣ (𝑟 ∈ (0[,]1) ∧ 𝑡 ∈ 𝑣)} ⊆ {⟨𝑟, 𝑡⟩ ∣ (𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀))})
125		ssopab2bw 5399	. . . . . . . . . . . . . . . . . . 19 ⊢ ({⟨𝑟, 𝑡⟩ ∣ (𝑟 ∈ (0[,]1) ∧ 𝑡 ∈ 𝑣)} ⊆ {⟨𝑟, 𝑡⟩ ∣ (𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀))} ↔ ∀𝑟∀𝑡((𝑟 ∈ (0[,]1) ∧ 𝑡 ∈ 𝑣) → (𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀))))
126		r2al 3166	. . . . . . . . . . . . . . . . . . 19 ⊢ (∀𝑟 ∈ (0[,]1)∀𝑡 ∈ 𝑣 (𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀)) ↔ ∀𝑟∀𝑡((𝑟 ∈ (0[,]1) ∧ 𝑡 ∈ 𝑣) → (𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀))))
127		ralcom 3307	. . . . . . . . . . . . . . . . . . 19 ⊢ (∀𝑟 ∈ (0[,]1)∀𝑡 ∈ 𝑣 (𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀)) ↔ ∀𝑡 ∈ 𝑣 ∀𝑟 ∈ (0[,]1)(𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀)))
128	125, 126, 127	3bitr2i 302	. . . . . . . . . . . . . . . . . 18 ⊢ ({⟨𝑟, 𝑡⟩ ∣ (𝑟 ∈ (0[,]1) ∧ 𝑡 ∈ 𝑣)} ⊆ {⟨𝑟, 𝑡⟩ ∣ (𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀))} ↔ ∀𝑡 ∈ 𝑣 ∀𝑟 ∈ (0[,]1)(𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀)))
129	124, 128	bitri 278	. . . . . . . . . . . . . . . . 17 ⊢ (((0[,]1) × 𝑣) ⊆ 𝑆 ↔ ∀𝑡 ∈ 𝑣 ∀𝑟 ∈ (0[,]1)(𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀)))
130	122, 129	sylib 221	. . . . . . . . . . . . . . . 16 ⊢ (((0[,]1) × 𝑣) ⊆ ((int‘(II ×_t II))‘𝑆) → ∀𝑡 ∈ 𝑣 ∀𝑟 ∈ (0[,]1)(𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀)))
131		simpr 488	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀)) → ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀))
132	131	ralimi 3128	. . . . . . . . . . . . . . . . . . 19 ⊢ (∀𝑟 ∈ (0[,]1)(𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀)) → ∀𝑟 ∈ (0[,]1)∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀))
133		cvmlift2lem1 32662	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∀𝑟 ∈ (0[,]1)∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀) → (((0[,]1) × {𝑎}) ⊆ 𝑀 → ((0[,]1) × {𝑡}) ⊆ 𝑀))
134		bicom 225	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀) ↔ ((𝑢 × {𝑡}) ⊆ 𝑀 ↔ (𝑢 × {𝑎}) ⊆ 𝑀))
135	134	rexbii 3210	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀) ↔ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑡}) ⊆ 𝑀 ↔ (𝑢 × {𝑎}) ⊆ 𝑀))
136	135	ralbii 3133	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∀𝑟 ∈ (0[,]1)∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀) ↔ ∀𝑟 ∈ (0[,]1)∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑡}) ⊆ 𝑀 ↔ (𝑢 × {𝑎}) ⊆ 𝑀))
137		cvmlift2lem1 32662	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∀𝑟 ∈ (0[,]1)∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑡}) ⊆ 𝑀 ↔ (𝑢 × {𝑎}) ⊆ 𝑀) → (((0[,]1) × {𝑡}) ⊆ 𝑀 → ((0[,]1) × {𝑎}) ⊆ 𝑀))
138	136, 137	sylbi 220	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∀𝑟 ∈ (0[,]1)∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀) → (((0[,]1) × {𝑡}) ⊆ 𝑀 → ((0[,]1) × {𝑎}) ⊆ 𝑀))
139	133, 138	impbid 215	. . . . . . . . . . . . . . . . . . 19 ⊢ (∀𝑟 ∈ (0[,]1)∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀) → (((0[,]1) × {𝑎}) ⊆ 𝑀 ↔ ((0[,]1) × {𝑡}) ⊆ 𝑀))
140	132, 139	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑟 ∈ (0[,]1)(𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀)) → (((0[,]1) × {𝑎}) ⊆ 𝑀 ↔ ((0[,]1) × {𝑡}) ⊆ 𝑀))
141	13	rabeq2i 3435	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎 ∈ 𝐴 ↔ (𝑎 ∈ (0[,]1) ∧ ((0[,]1) × {𝑎}) ⊆ 𝑀))
142	141	baib 539	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 ∈ (0[,]1) → (𝑎 ∈ 𝐴 ↔ ((0[,]1) × {𝑎}) ⊆ 𝑀))
143	142	ad3antlr 730	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑎 ∈ (0[,]1)) ∧ 𝑣 ∈ II) ∧ 𝑡 ∈ 𝑣) → (𝑎 ∈ 𝐴 ↔ ((0[,]1) × {𝑎}) ⊆ 𝑀))
144		elssuni 4830	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑣 ∈ II → 𝑣 ⊆ ∪ II)
145	144, 14	sseqtrrdi 3966	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑣 ∈ II → 𝑣 ⊆ (0[,]1))
146	145	adantl 485	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑎 ∈ (0[,]1)) ∧ 𝑣 ∈ II) → 𝑣 ⊆ (0[,]1))
147	146	sselda 3915	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑎 ∈ (0[,]1)) ∧ 𝑣 ∈ II) ∧ 𝑡 ∈ 𝑣) → 𝑡 ∈ (0[,]1))
148		sneq 4535	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑎 = 𝑡 → {𝑎} = {𝑡})
149	148	xpeq2d 5549	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑎 = 𝑡 → ((0[,]1) × {𝑎}) = ((0[,]1) × {𝑡}))
150	149	sseq1d 3946	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑎 = 𝑡 → (((0[,]1) × {𝑎}) ⊆ 𝑀 ↔ ((0[,]1) × {𝑡}) ⊆ 𝑀))
151	150, 13	elrab2 3631	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑡 ∈ 𝐴 ↔ (𝑡 ∈ (0[,]1) ∧ ((0[,]1) × {𝑡}) ⊆ 𝑀))
152	151	baib 539	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 ∈ (0[,]1) → (𝑡 ∈ 𝐴 ↔ ((0[,]1) × {𝑡}) ⊆ 𝑀))
153	147, 152	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑎 ∈ (0[,]1)) ∧ 𝑣 ∈ II) ∧ 𝑡 ∈ 𝑣) → (𝑡 ∈ 𝐴 ↔ ((0[,]1) × {𝑡}) ⊆ 𝑀))
154	143, 153	bibi12d 349	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑎 ∈ (0[,]1)) ∧ 𝑣 ∈ II) ∧ 𝑡 ∈ 𝑣) → ((𝑎 ∈ 𝐴 ↔ 𝑡 ∈ 𝐴) ↔ (((0[,]1) × {𝑎}) ⊆ 𝑀 ↔ ((0[,]1) × {𝑡}) ⊆ 𝑀)))
155	140, 154	syl5ibr 249	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑎 ∈ (0[,]1)) ∧ 𝑣 ∈ II) ∧ 𝑡 ∈ 𝑣) → (∀𝑟 ∈ (0[,]1)(𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀)) → (𝑎 ∈ 𝐴 ↔ 𝑡 ∈ 𝐴)))
156	155	ralimdva 3144	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑎 ∈ (0[,]1)) ∧ 𝑣 ∈ II) → (∀𝑡 ∈ 𝑣 ∀𝑟 ∈ (0[,]1)(𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀)) → ∀𝑡 ∈ 𝑣 (𝑎 ∈ 𝐴 ↔ 𝑡 ∈ 𝐴)))
157	130, 156	syl5 34	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑎 ∈ (0[,]1)) ∧ 𝑣 ∈ II) → (((0[,]1) × 𝑣) ⊆ ((int‘(II ×_t II))‘𝑆) → ∀𝑡 ∈ 𝑣 (𝑎 ∈ 𝐴 ↔ 𝑡 ∈ 𝐴)))
158	157	anim2d 614	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑎 ∈ (0[,]1)) ∧ 𝑣 ∈ II) → ((𝑎 ∈ 𝑣 ∧ ((0[,]1) × 𝑣) ⊆ ((int‘(II ×_t II))‘𝑆)) → (𝑎 ∈ 𝑣 ∧ ∀𝑡 ∈ 𝑣 (𝑎 ∈ 𝐴 ↔ 𝑡 ∈ 𝐴))))
159	158	reximdva 3233	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑎 ∈ (0[,]1)) → (∃𝑣 ∈ II (𝑎 ∈ 𝑣 ∧ ((0[,]1) × 𝑣) ⊆ ((int‘(II ×_t II))‘𝑆)) → ∃𝑣 ∈ II (𝑎 ∈ 𝑣 ∧ ∀𝑡 ∈ 𝑣 (𝑎 ∈ 𝐴 ↔ 𝑡 ∈ 𝐴))))
160	118, 159	mpd 15	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑎 ∈ (0[,]1)) → ∃𝑣 ∈ II (𝑎 ∈ 𝑣 ∧ ∀𝑡 ∈ 𝑣 (𝑎 ∈ 𝐴 ↔ 𝑡 ∈ 𝐴)))
161	160	ralrimiva 3149	. . . . . . . . . . 11 ⊢ (𝜑 → ∀𝑎 ∈ (0[,]1)∃𝑣 ∈ II (𝑎 ∈ 𝑣 ∧ ∀𝑡 ∈ 𝑣 (𝑎 ∈ 𝐴 ↔ 𝑡 ∈ 𝐴)))
162		ssrab2 4007	. . . . . . . . . . . . 13 ⊢ {𝑎 ∈ (0[,]1) ∣ ((0[,]1) × {𝑎}) ⊆ 𝑀} ⊆ (0[,]1)
163	13, 162	eqsstri 3949	. . . . . . . . . . . 12 ⊢ 𝐴 ⊆ (0[,]1)
164	14	isclo 21692	. . . . . . . . . . . 12 ⊢ ((II ∈ Top ∧ 𝐴 ⊆ (0[,]1)) → (𝐴 ∈ (II ∩ (Clsd‘II)) ↔ ∀𝑎 ∈ (0[,]1)∃𝑣 ∈ II (𝑎 ∈ 𝑣 ∧ ∀𝑡 ∈ 𝑣 (𝑎 ∈ 𝐴 ↔ 𝑡 ∈ 𝐴))))
165	20, 163, 164	mp2an 691	. . . . . . . . . . 11 ⊢ (𝐴 ∈ (II ∩ (Clsd‘II)) ↔ ∀𝑎 ∈ (0[,]1)∃𝑣 ∈ II (𝑎 ∈ 𝑣 ∧ ∀𝑡 ∈ 𝑣 (𝑎 ∈ 𝐴 ↔ 𝑡 ∈ 𝐴)))
166	161, 165	sylibr 237	. . . . . . . . . 10 ⊢ (𝜑 → 𝐴 ∈ (II ∩ (Clsd‘II)))
167	17, 166	sseldi 3913	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 ∈ II)
168		0elunit 12847	. . . . . . . . . . . 12 ⊢ 0 ∈ (0[,]1)
169	168	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → 0 ∈ (0[,]1))
170		relxp 5537	. . . . . . . . . . . . 13 ⊢ Rel ((0[,]1) × {0})
171	170	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → Rel ((0[,]1) × {0}))
172		opelxp 5555	. . . . . . . . . . . . 13 ⊢ (⟨𝑟, 𝑎⟩ ∈ ((0[,]1) × {0}) ↔ (𝑟 ∈ (0[,]1) ∧ 𝑎 ∈ {0}))
173		id 22	. . . . . . . . . . . . . . . . 17 ⊢ (𝑟 ∈ (0[,]1) → 𝑟 ∈ (0[,]1))
174		opelxpi 5556	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑟 ∈ (0[,]1) ∧ 0 ∈ (0[,]1)) → ⟨𝑟, 0⟩ ∈ ((0[,]1) × (0[,]1)))
175	173, 169, 174	syl2anr 599	. . . . . . . . . . . . . . . 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, 45, 180, 181	cvmlift2lem10 32672	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑟 ∈ (0[,]1)) → ∃𝑢 ∈ II ∃𝑣 ∈ II (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×_t II) ↾_t (𝑢 × 𝑣)) Cn 𝐶))))
183		df-3an 1086	. . . . . . . . . . . . . . . . . . 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 729	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → 𝐾:((0[,]1) × (0[,]1))⟶𝐵)
186	185	ffnd 6488	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → 𝐾 Fn ((0[,]1) × (0[,]1)))
187		fnov 7261	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝐾 Fn ((0[,]1) × (0[,]1)) ↔ 𝐾 = (𝑏 ∈ (0[,]1), 𝑤 ∈ (0[,]1) ↦ (𝑏𝐾𝑤)))
188	186, 187	sylib 221	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → 𝐾 = (𝑏 ∈ (0[,]1), 𝑤 ∈ (0[,]1) ↦ (𝑏𝐾𝑤)))
189	188	reseq1d 5817	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → (𝐾 ↾ (𝑢 × {0})) = ((𝑏 ∈ (0[,]1), 𝑤 ∈ (0[,]1) ↦ (𝑏𝐾𝑤)) ↾ (𝑢 × {0})))
190		simplrl 776	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → 𝑢 ∈ II)
191		elssuni 4830	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑢 ∈ II → 𝑢 ⊆ ∪ II)
192	191, 14	sseqtrrdi 3966	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑢 ∈ II → 𝑢 ⊆ (0[,]1))
193	190, 192	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → 𝑢 ⊆ (0[,]1))
194	169	snssd 4702	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → {0} ⊆ (0[,]1))
195	194	ad3antrrr 729	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → {0} ⊆ (0[,]1))
196		resmpo 7251	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑢 ⊆ (0[,]1) ∧ {0} ⊆ (0[,]1)) → ((𝑏 ∈ (0[,]1), 𝑤 ∈ (0[,]1) ↦ (𝑏𝐾𝑤)) ↾ (𝑢 × {0})) = (𝑏 ∈ 𝑢, 𝑤 ∈ {0} ↦ (𝑏𝐾𝑤)))
197	193, 195, 196	syl2anc 587	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → ((𝑏 ∈ (0[,]1), 𝑤 ∈ (0[,]1) ↦ (𝑏𝐾𝑤)) ↾ (𝑢 × {0})) = (𝑏 ∈ 𝑢, 𝑤 ∈ {0} ↦ (𝑏𝐾𝑤)))
198	193	sselda 3915	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 32670	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑏 ∈ (0[,]1)) → (𝑏𝐾0) = (𝐻‘𝑏))
201	199, 200	sylan 583	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) ∧ 𝑏 ∈ (0[,]1)) → (𝑏𝐾0) = (𝐻‘𝑏))
202	198, 201	syldan 594	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) ∧ 𝑏 ∈ 𝑢) → (𝑏𝐾0) = (𝐻‘𝑏))
203		elsni 4542	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑤 ∈ {0} → 𝑤 = 0)
204	203	oveq2d 7151	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑤 ∈ {0} → (𝑏𝐾𝑤) = (𝑏𝐾0))
205	204	eqeq1d 2800	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑤 ∈ {0} → ((𝑏𝐾𝑤) = (𝐻‘𝑏) ↔ (𝑏𝐾0) = (𝐻‘𝑏)))
206	202, 205	syl5ibrcom 250	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) ∧ 𝑏 ∈ 𝑢) → (𝑤 ∈ {0} → (𝑏𝐾𝑤) = (𝐻‘𝑏)))
207	206	3impia 1114	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) ∧ 𝑏 ∈ 𝑢 ∧ 𝑤 ∈ {0}) → (𝑏𝐾𝑤) = (𝐻‘𝑏))
208	207	mpoeq3dva 7210	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → (𝑏 ∈ 𝑢, 𝑤 ∈ {0} ↦ (𝑏𝐾𝑤)) = (𝑏 ∈ 𝑢, 𝑤 ∈ {0} ↦ (𝐻‘𝑏)))
209	189, 197, 208	3eqtrd 2837	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → (𝐾 ↾ (𝑢 × {0})) = (𝑏 ∈ 𝑢, 𝑤 ∈ {0} ↦ (𝐻‘𝑏)))
210		eqid 2798	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (II ↾_t 𝑢) = (II ↾_t 𝑢)
211		iitopon 23484	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ II ∈ (TopOn‘(0[,]1))
212	211	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → II ∈ (TopOn‘(0[,]1)))
213		eqid 2798	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (II ↾_t {0}) = (II ↾_t {0})
214	212, 212	cnmpt1st 22273	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → (𝑏 ∈ (0[,]1), 𝑤 ∈ (0[,]1) ↦ 𝑏) ∈ ((II ×_t II) Cn II))
215	1, 2, 3, 4, 5, 6	cvmlift2lem2 32664	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → (𝐻 ∈ (II Cn 𝐶) ∧ (𝐹 ∘ 𝐻) = (𝑧 ∈ (0[,]1) ↦ (𝑧𝐺0)) ∧ (𝐻‘0) = 𝑃))
216	215	simp1d 1139	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → 𝐻 ∈ (II Cn 𝐶))
217	199, 216	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → 𝐻 ∈ (II Cn 𝐶))
218	212, 212, 214, 217	cnmpt21f 22277	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → (𝑏 ∈ (0[,]1), 𝑤 ∈ (0[,]1) ↦ (𝐻‘𝑏)) ∈ ((II ×_t II) Cn 𝐶))
219	210, 212, 193, 213, 212, 195, 218	cnmpt2res 22282	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → (𝑏 ∈ 𝑢, 𝑤 ∈ {0} ↦ (𝐻‘𝑏)) ∈ (((II ↾_t 𝑢) ×_t (II ↾_t {0})) Cn 𝐶))
220		vex 3444	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ 𝑢 ∈ V
221		snex 5297	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ {0} ∈ V
222		txrest 22236	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((II ∈ Top ∧ II ∈ Top) ∧ (𝑢 ∈ V ∧ {0} ∈ V)) → ((II ×_t II) ↾_t (𝑢 × {0})) = ((II ↾_t 𝑢) ×_t (II ↾_t {0})))
223	20, 20, 220, 221, 222	mp4an 692	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((II ×_t II) ↾_t (𝑢 × {0})) = ((II ↾_t 𝑢) ×_t (II ↾_t {0}))
224	223	oveq1i 7145	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((II ×_t II) ↾_t (𝑢 × {0})) Cn 𝐶) = (((II ↾_t 𝑢) ×_t (II ↾_t {0})) Cn 𝐶)
225	219, 224	eleqtrrdi 2901	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → (𝑏 ∈ 𝑢, 𝑤 ∈ {0} ↦ (𝐻‘𝑏)) ∈ (((II ×_t II) ↾_t (𝑢 × {0})) Cn 𝐶))
226	209, 225	eqeltrd 2890	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → (𝐾 ↾ (𝑢 × {0})) ∈ (((II ×_t II) ↾_t (𝑢 × {0})) Cn 𝐶))
227		sneq 4535	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑤 = 0 → {𝑤} = {0})
228	227	xpeq2d 5549	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑤 = 0 → (𝑢 × {𝑤}) = (𝑢 × {0}))
229	228	reseq2d 5818	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑤 = 0 → (𝐾 ↾ (𝑢 × {𝑤})) = (𝐾 ↾ (𝑢 × {0})))
230	228	oveq2d 7151	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑤 = 0 → ((II ×_t II) ↾_t (𝑢 × {𝑤})) = ((II ×_t II) ↾_t (𝑢 × {0})))
231	230	oveq1d 7150	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑤 = 0 → (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶) = (((II ×_t II) ↾_t (𝑢 × {0})) Cn 𝐶))
232	229, 231	eleq12d 2884	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 = 0 → ((𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶) ↔ (𝐾 ↾ (𝑢 × {0})) ∈ (((II ×_t II) ↾_t (𝑢 × {0})) Cn 𝐶)))
233	232	rspcev 3571	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((0 ∈ 𝑣 ∧ (𝐾 ↾ (𝑢 × {0})) ∈ (((II ×_t II) ↾_t (𝑢 × {0})) Cn 𝐶)) → ∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶))
234	184, 226, 233	syl2anc 587	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → ∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶))
235		opelxpi 5556	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣) → ⟨𝑟, 0⟩ ∈ (𝑢 × 𝑣))
236	235	adantl 485	. . . . . . . . . . . . . . . . . . . . . . . 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 5534	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑢 ⊆ (0[,]1) ∧ 𝑣 ⊆ (0[,]1)) → (𝑢 × 𝑣) ⊆ ((0[,]1) × (0[,]1)))
240	193, 238, 239	syl2anc 587	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → (𝑢 × 𝑣) ⊆ ((0[,]1) × (0[,]1)))
241	37	restuni 21767	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((II ×_t II) ∈ Top ∧ (𝑢 × 𝑣) ⊆ ((0[,]1) × (0[,]1))) → (𝑢 × 𝑣) = ∪ ((II ×_t II) ↾_t (𝑢 × 𝑣)))
242	22, 240, 241	sylancr 590	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → (𝑢 × 𝑣) = ∪ ((II ×_t II) ↾_t (𝑢 × 𝑣)))
243	236, 242	eleqtrd 2892	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → ⟨𝑟, 0⟩ ∈ ∪ ((II ×_t II) ↾_t (𝑢 × 𝑣)))
244		eqid 2798	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ∪ ((II ×_t II) ↾_t (𝑢 × 𝑣)) = ∪ ((II ×_t II) ↾_t (𝑢 × 𝑣))
245	244	cncnpi 21883	. . . . . . . . . . . . . . . . . . . . . . . 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	22	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → (II ×_t II) ∈ Top)
249	20	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → II ∈ Top)
250	249, 249, 190, 237, 54	syl22anc 837	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → (𝑢 × 𝑣) ∈ (II ×_t II))
251		isopn3i 21687	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((II ×_t II) ∈ Top ∧ (𝑢 × 𝑣) ∈ (II ×_t II)) → ((int‘(II ×_t II))‘(𝑢 × 𝑣)) = (𝑢 × 𝑣))
252	22, 250, 251	sylancr 590	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → ((int‘(II ×_t II))‘(𝑢 × 𝑣)) = (𝑢 × 𝑣))
253	236, 252	eleqtrrd 2893	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → ⟨𝑟, 0⟩ ∈ ((int‘(II ×_t II))‘(𝑢 × 𝑣)))
254	37, 1	cnprest 21894	. . . . . . . . . . . . . . . . . . . . . . 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 837	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → (𝐾 ∈ (((II ×_t II) CnP 𝐶)‘⟨𝑟, 0⟩) ↔ (𝐾 ↾ (𝑢 × 𝑣)) ∈ ((((II ×_t II) ↾_t (𝑢 × 𝑣)) CnP 𝐶)‘⟨𝑟, 0⟩)))
256	247, 255	sylibrd 262	. . . . . . . . . . . . . . . . . . . . 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	syl5bi 245	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) → ((𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×_t II) ↾_t (𝑢 × 𝑣)) Cn 𝐶))) → 𝐾 ∈ (((II ×_t II) CnP 𝐶)‘⟨𝑟, 0⟩)))
260	259	rexlimdvva 3253	. . . . . . . . . . . . . . . . 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 6645	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = ⟨𝑟, 0⟩ → (((II ×_t II) CnP 𝐶)‘𝑧) = (((II ×_t II) CnP 𝐶)‘⟨𝑟, 0⟩))
263	262	eleq2d 2875	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = ⟨𝑟, 0⟩ → (𝐾 ∈ (((II ×_t II) CnP 𝐶)‘𝑧) ↔ 𝐾 ∈ (((II ×_t II) CnP 𝐶)‘⟨𝑟, 0⟩)))
264	263, 69	elrab2 3631	. . . . . . . . . . . . . . . 16 ⊢ (⟨𝑟, 0⟩ ∈ 𝑀 ↔ (⟨𝑟, 0⟩ ∈ ((0[,]1) × (0[,]1)) ∧ 𝐾 ∈ (((II ×_t II) CnP 𝐶)‘⟨𝑟, 0⟩)))
265	175, 261, 264	sylanbrc 586	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑟 ∈ (0[,]1)) → ⟨𝑟, 0⟩ ∈ 𝑀)
266		elsni 4542	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 ∈ {0} → 𝑎 = 0)
267	266	opeq2d 4772	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 ∈ {0} → ⟨𝑟, 𝑎⟩ = ⟨𝑟, 0⟩)
268	267	eleq1d 2874	. . . . . . . . . . . . . . 15 ⊢ (𝑎 ∈ {0} → (⟨𝑟, 𝑎⟩ ∈ 𝑀 ↔ ⟨𝑟, 0⟩ ∈ 𝑀))
269	265, 268	syl5ibrcom 250	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑟 ∈ (0[,]1)) → (𝑎 ∈ {0} → ⟨𝑟, 𝑎⟩ ∈ 𝑀))
270	269	expimpd 457	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑟 ∈ (0[,]1) ∧ 𝑎 ∈ {0}) → ⟨𝑟, 𝑎⟩ ∈ 𝑀))
271	172, 270	syl5bi 245	. . . . . . . . . . . 12 ⊢ (𝜑 → (⟨𝑟, 𝑎⟩ ∈ ((0[,]1) × {0}) → ⟨𝑟, 𝑎⟩ ∈ 𝑀))
272	171, 271	relssdv 5625	. . . . . . . . . . 11 ⊢ (𝜑 → ((0[,]1) × {0}) ⊆ 𝑀)
273		sneq 4535	. . . . . . . . . . . . . 14 ⊢ (𝑎 = 0 → {𝑎} = {0})
274	273	xpeq2d 5549	. . . . . . . . . . . . 13 ⊢ (𝑎 = 0 → ((0[,]1) × {𝑎}) = ((0[,]1) × {0}))
275	274	sseq1d 3946	. . . . . . . . . . . 12 ⊢ (𝑎 = 0 → (((0[,]1) × {𝑎}) ⊆ 𝑀 ↔ ((0[,]1) × {0}) ⊆ 𝑀))
276	275, 13	elrab2 3631	. . . . . . . . . . 11 ⊢ (0 ∈ 𝐴 ↔ (0 ∈ (0[,]1) ∧ ((0[,]1) × {0}) ⊆ 𝑀))
277	169, 272, 276	sylanbrc 586	. . . . . . . . . 10 ⊢ (𝜑 → 0 ∈ 𝐴)
278	277	ne0d 4251	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 ≠ ∅)
279		inss2 4156	. . . . . . . . . 10 ⊢ (II ∩ (Clsd‘II)) ⊆ (Clsd‘II)
280	279, 166	sseldi 3913	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 ∈ (Clsd‘II))
281	14, 16, 167, 278, 280	connclo 22020	. . . . . . . 8 ⊢ (𝜑 → 𝐴 = (0[,]1))
282	13, 281	syl5reqr 2848	. . . . . . 7 ⊢ (𝜑 → (0[,]1) = {𝑎 ∈ (0[,]1) ∣ ((0[,]1) × {𝑎}) ⊆ 𝑀})
283		rabid2 3334	. . . . . . 7 ⊢ ((0[,]1) = {𝑎 ∈ (0[,]1) ∣ ((0[,]1) × {𝑎}) ⊆ 𝑀} ↔ ∀𝑎 ∈ (0[,]1)((0[,]1) × {𝑎}) ⊆ 𝑀)
284	282, 283	sylib 221	. . . . . 6 ⊢ (𝜑 → ∀𝑎 ∈ (0[,]1)((0[,]1) × {𝑎}) ⊆ 𝑀)
285		iunss 4932	. . . . . 6 ⊢ (∪ 𝑎 ∈ (0[,]1)((0[,]1) × {𝑎}) ⊆ 𝑀 ↔ ∀𝑎 ∈ (0[,]1)((0[,]1) × {𝑎}) ⊆ 𝑀)
286	284, 285	sylibr 237	. . . . 5 ⊢ (𝜑 → ∪ 𝑎 ∈ (0[,]1)((0[,]1) × {𝑎}) ⊆ 𝑀)
287	12, 286	eqsstrid 3963	. . . 4 ⊢ (𝜑 → ((0[,]1) × (0[,]1)) ⊆ 𝑀)
288	287, 69	sseqtrdi 3965	. . 3 ⊢ (𝜑 → ((0[,]1) × (0[,]1)) ⊆ {𝑧 ∈ ((0[,]1) × (0[,]1)) ∣ 𝐾 ∈ (((II ×_t II) CnP 𝐶)‘𝑧)})
289		ssrab 4000	. . . 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 500	. . 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 22196	. . . 4 ⊢ ((II ∈ (TopOn‘(0[,]1)) ∧ II ∈ (TopOn‘(0[,]1))) → (II ×_t II) ∈ (TopOn‘((0[,]1) × (0[,]1))))
293	211, 211, 292	mp2an 691	. . 3 ⊢ (II ×_t II) ∈ (TopOn‘((0[,]1) × (0[,]1)))
294		cvmtop1 32620	. . . . 5 ⊢ (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐶 ∈ Top)
295	2, 294	syl 17	. . . 4 ⊢ (𝜑 → 𝐶 ∈ Top)
296	1	toptopon 21522	. . . 4 ⊢ (𝐶 ∈ Top ↔ 𝐶 ∈ (TopOn‘𝐵))
297	295, 296	sylib 221	. . 3 ⊢ (𝜑 → 𝐶 ∈ (TopOn‘𝐵))
298		cncnp 21885	. . 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 590	. 2 ⊢ (𝜑 → (𝐾 ∈ ((II ×_t II) Cn 𝐶) ↔ (𝐾:((0[,]1) × (0[,]1))⟶𝐵 ∧ ∀𝑧 ∈ ((0[,]1) × (0[,]1))𝐾 ∈ (((II ×_t II) CnP 𝐶)‘𝑧))))
300	8, 291, 299	mpbir2and 712	1 ⊢ (𝜑 → 𝐾 ∈ ((II ×_t II) Cn 𝐶))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 209 ∧ wa 399 ∧ w3a 1084 ∀wal 1536 = wceq 1538 ∈ wcel 2111 ∀wral 3106 ∃wrex 3107 {crab 3110 Vcvv 3441 ∖ cdif 3878 ∩ cin 3880 ⊆ wss 3881 ∅c0 4243 𝒫 cpw 4497 {csn 4525 ⟨cop 4531 ∪ cuni 4800 ∪ ciun 4881 {copab 5092 ↦ cmpt 5110 × cxp 5517 ^◡ccnv 5518 ↾ cres 5521 “ cima 5522 ∘ ccom 5523 Rel wrel 5524 Fn wfn 6319 ⟶wf 6320 ‘cfv 6324 ℩crio 7092 (class class class)co 7135 ∈ cmpo 7137 0cc0 10526 1c1 10527 [,]cicc 12729 ↾_t crest 16686 Topctop 21498 TopOnctopon 21515 Clsdccld 21621 intcnt 21622 neicnei 21702 Cn ccn 21829 CnP ccnp 21830 Compccmp 21991 Conncconn 22016 ×_t ctx 22165 Homeochmeo 22358 IIcii 23480 CovMap ccvm 32615

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2158 ax-12 2175 ax-ext 2770 ax-rep 5154 ax-sep 5167 ax-nul 5174 ax-pow 5231 ax-pr 5295 ax-un 7441 ax-inf2 9088 ax-cnex 10582 ax-resscn 10583 ax-1cn 10584 ax-icn 10585 ax-addcl 10586 ax-addrcl 10587 ax-mulcl 10588 ax-mulrcl 10589 ax-mulcom 10590 ax-addass 10591 ax-mulass 10592 ax-distr 10593 ax-i2m1 10594 ax-1ne0 10595 ax-1rid 10596 ax-rnegex 10597 ax-rrecex 10598 ax-cnre 10599 ax-pre-lttri 10600 ax-pre-lttrn 10601 ax-pre-ltadd 10602 ax-pre-mulgt0 10603 ax-pre-sup 10604 ax-addf 10605 ax-mulf 10606

This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-3or 1085 df-3an 1086 df-tru 1541 df-fal 1551 df-ex 1782 df-nf 1786 df-sb 2070 df-mo 2598 df-eu 2629 df-clab 2777 df-cleq 2791 df-clel 2870 df-nfc 2938 df-ne 2988 df-nel 3092 df-ral 3111 df-rex 3112 df-reu 3113 df-rmo 3114 df-rab 3115 df-v 3443 df-sbc 3721 df-csb 3829 df-dif 3884 df-un 3886 df-in 3888 df-ss 3898 df-pss 3900 df-nul 4244 df-if 4426 df-pw 4499 df-sn 4526 df-pr 4528 df-tp 4530 df-op 4532 df-uni 4801 df-int 4839 df-iun 4883 df-iin 4884 df-br 5031 df-opab 5093 df-mpt 5111 df-tr 5137 df-id 5425 df-eprel 5430 df-po 5438 df-so 5439 df-fr 5478 df-se 5479 df-we 5480 df-xp 5525 df-rel 5526 df-cnv 5527 df-co 5528 df-dm 5529 df-rn 5530 df-res 5531 df-ima 5532 df-pred 6116 df-ord 6162 df-on 6163 df-lim 6164 df-suc 6165 df-iota 6283 df-fun 6326 df-fn 6327 df-f 6328 df-f1 6329 df-fo 6330 df-f1o 6331 df-fv 6332 df-isom 6333 df-riota 7093 df-ov 7138 df-oprab 7139 df-mpo 7140 df-of 7389 df-om 7561 df-1st 7671 df-2nd 7672 df-supp 7814 df-wrecs 7930 df-recs 7991 df-rdg 8029 df-1o 8085 df-2o 8086 df-oadd 8089 df-er 8272 df-ec 8274 df-map 8391 df-ixp 8445 df-en 8493 df-dom 8494 df-sdom 8495 df-fin 8496 df-fsupp 8818 df-fi 8859 df-sup 8890 df-inf 8891 df-oi 8958 df-card 9352 df-pnf 10666 df-mnf 10667 df-xr 10668 df-ltxr 10669 df-le 10670 df-sub 10861 df-neg 10862 df-div 11287 df-nn 11626 df-2 11688 df-3 11689 df-4 11690 df-5 11691 df-6 11692 df-7 11693 df-8 11694 df-9 11695 df-n0 11886 df-z 11970 df-dec 12087 df-uz 12232 df-q 12337 df-rp 12378 df-xneg 12495 df-xadd 12496 df-xmul 12497 df-ioo 12730 df-ico 12732 df-icc 12733 df-fz 12886 df-fzo 13029 df-fl 13157 df-seq 13365 df-exp 13426 df-hash 13687 df-cj 14450 df-re 14451 df-im 14452 df-sqrt 14586 df-abs 14587 df-clim 14837 df-sum 15035 df-struct 16477 df-ndx 16478 df-slot 16479 df-base 16481 df-sets 16482 df-ress 16483 df-plusg 16570 df-mulr 16571 df-starv 16572 df-sca 16573 df-vsca 16574 df-ip 16575 df-tset 16576 df-ple 16577 df-ds 16579 df-unif 16580 df-hom 16581 df-cco 16582 df-rest 16688 df-topn 16689 df-0g 16707 df-gsum 16708 df-topgen 16709 df-pt 16710 df-prds 16713 df-xrs 16767 df-qtop 16772 df-imas 16773 df-xps 16775 df-mre 16849 df-mrc 16850 df-acs 16852 df-mgm 17844 df-sgrp 17893 df-mnd 17904 df-submnd 17949 df-mulg 18217 df-cntz 18439 df-cmn 18900 df-psmet 20083 df-xmet 20084 df-met 20085 df-bl 20086 df-mopn 20087 df-cnfld 20092 df-top 21499 df-topon 21516 df-topsp 21538 df-bases 21551 df-cld 21624 df-ntr 21625 df-cls 21626 df-nei 21703 df-cn 21832 df-cnp 21833 df-cmp 21992 df-conn 22017 df-lly 22071 df-nlly 22072 df-tx 22167 df-hmeo 22360 df-xms 22927 df-ms 22928 df-tms 22929 df-ii 23482 df-htpy 23575 df-phtpy 23576 df-phtpc 23597 df-pconn 32581 df-sconn 32582 df-cvm 32616

This theorem is referenced by: cvmlift2lem13 32675

W3C validator