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 35286

Description: Lemma for cvmlift2 35288. (Contributed by Mario Carneiro, 1-Jun-2015.)

**Hypotheses**
Ref	Expression
cvmlift2.b	⊢ 𝐵 = ∪ 𝐶
cvmlift2.f	⊢ (𝜑 → 𝐹 ∈ (𝐶 CovMap 𝐽))
cvmlift2.g	⊢ (𝜑 → 𝐺 ∈ ((II ×_t II) Cn 𝐽))
cvmlift2.p	⊢ (𝜑 → 𝑃 ∈ 𝐵)
cvmlift2.i	⊢ (𝜑 → (𝐹‘𝑃) = (0𝐺0))
cvmlift2.h	⊢ 𝐻 = (℩𝑓 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑓) = (𝑧 ∈ (0[,]1) ↦ (𝑧𝐺0)) ∧ (𝑓‘0) = 𝑃))
cvmlift2.k	⊢ 𝐾 = (𝑥 ∈ (0[,]1), 𝑦 ∈ (0[,]1) ↦ ((℩𝑓 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑓) = (𝑧 ∈ (0[,]1) ↦ (𝑥𝐺𝑧)) ∧ (𝑓‘0) = (𝐻‘𝑥)))‘𝑦))
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 35279	. 2 ⊢ (𝜑 → 𝐾:((0[,]1) × (0[,]1))⟶𝐵)
9		iunid 5012	. . . . . . 7 ⊢ ∪ 𝑎 ∈ (0[,]1){𝑎} = (0[,]1)
10	9	xpeq2i 5650	. . . . . 6 ⊢ ((0[,]1) × ∪ 𝑎 ∈ (0[,]1){𝑎}) = ((0[,]1) × (0[,]1))
11		xpiundi 5694	. . . . . 6 ⊢ ((0[,]1) × ∪ 𝑎 ∈ (0[,]1){𝑎}) = ∪ 𝑎 ∈ (0[,]1)((0[,]1) × {𝑎})
12	10, 11	eqtr3i 2754	. . . . 5 ⊢ ((0[,]1) × (0[,]1)) = ∪ 𝑎 ∈ (0[,]1)((0[,]1) × {𝑎})
13		iiuni 24790	. . . . . . . . 9 ⊢ (0[,]1) = ∪ II
14		iiconn 24796	. . . . . . . . . 10 ⊢ II ∈ Conn
15	14	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → II ∈ Conn)
16		inss1 4190	. . . . . . . . . 10 ⊢ (II ∩ (Clsd‘II)) ⊆ II
17		iicmp 24795	. . . . . . . . . . . . . . 15 ⊢ II ∈ Comp
18	17	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑎 ∈ (0[,]1)) → II ∈ Comp)
19		iitop 24789	. . . . . . . . . . . . . . 15 ⊢ II ∈ Top
20	19	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑎 ∈ (0[,]1)) → II ∈ Top)
21	19, 19	txtopi 23493	. . . . . . . . . . . . . . . 16 ⊢ (II ×_t II) ∈ Top
22	13	neiss2 23004	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((II ∈ Top ∧ 𝑢 ∈ ((nei‘II)‘{𝑟})) → {𝑟} ⊆ (0[,]1))
23	19, 22	mpan 690	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑢 ∈ ((nei‘II)‘{𝑟}) → {𝑟} ⊆ (0[,]1))
24		vex 3442	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 𝑟 ∈ V
25	24	snss 4739	. . . . . . . . . . . . . . . . . . . . . . 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 3123	. . . . . . . . . . . . . . . . . . . 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 5497	. . . . . . . . . . . . . . . . 17 ⊢ {⟨𝑟, 𝑡⟩ ∣ (𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀))} ⊆ {⟨𝑟, 𝑡⟩ ∣ (𝑟 ∈ (0[,]1) ∧ 𝑡 ∈ (0[,]1))}
33		cvmlift2.s	. . . . . . . . . . . . . . . . 17 ⊢ 𝑆 = {⟨𝑟, 𝑡⟩ ∣ (𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀))}
34		df-xp 5629	. . . . . . . . . . . . . . . . 17 ⊢ ((0[,]1) × (0[,]1)) = {⟨𝑟, 𝑡⟩ ∣ (𝑟 ∈ (0[,]1) ∧ 𝑡 ∈ (0[,]1))}
35	32, 33, 34	3sstr4i 3989	. . . . . . . . . . . . . . . 16 ⊢ 𝑆 ⊆ ((0[,]1) × (0[,]1))
36	19, 19, 13, 13	txunii 23496	. . . . . . . . . . . . . . . . 17 ⊢ ((0[,]1) × (0[,]1)) = ∪ (II ×_t II)
37	36	ntropn 22952	. . . . . . . . . . . . . . . 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 2729	. . . . . . . . . . . . . . . . . . . 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 35284	. . . . . . . . . . . . . . . . . . 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 23505	. . . . . . . . . . . . . . . . . . . . . . . 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 4866	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑡 ∈ 𝑣 ∧ 𝑣 ∈ II) → 𝑡 ∈ ∪ II)
57	56, 13	eleqtrrdi 2839	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 23022	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4589	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑐 = 𝑤 → {𝑐} = {𝑤})
73	72	xpeq2d 5653	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑐 = 𝑤 → (𝑢 × {𝑐}) = (𝑢 × {𝑤}))
74	73	reseq2d 5934	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑐 = 𝑤 → (𝐾 ↾ (𝑢 × {𝑐})) = (𝐾 ↾ (𝑢 × {𝑤})))
75	73	oveq2d 7369	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑐 = 𝑤 → ((II ×_t II) ↾_t (𝑢 × {𝑐})) = ((II ×_t II) ↾_t (𝑢 × {𝑤})))
76	75	oveq1d 7368	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑐 = 𝑤 → (((II ×_t II) ↾_t (𝑢 × {𝑐})) Cn 𝐶) = (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶))
77	74, 76	eleq12d 2822	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑐 = 𝑤 → ((𝐾 ↾ (𝑢 × {𝑐})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑐})) Cn 𝐶) ↔ (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶)))
78	77	cbvrexvw 3208	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 35285	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 35285	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3219	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5629	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑢 × 𝑣) = {⟨𝑟, 𝑡⟩ ∣ (𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣)}
90	89, 33	sseq12i 3968	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑢 × 𝑣) ⊆ 𝑆 ↔ {⟨𝑟, 𝑡⟩ ∣ (𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣)} ⊆ {⟨𝑟, 𝑡⟩ ∣ (𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀))})
91		ssopab2bw 5494	. . . . . . . . . . . . . . . . . . . . . . . . 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 22961	. . . . . . . . . . . . . . . . . . . . . . 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 5660	. . . . . . . . . . . . . . . . . . . . . . 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 3938	. . . . . . . . . . . . . . . . . . . . 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 3186	. . . . . . . . . . . . . . . . . . 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 3442	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑎 ∈ V
105		opeq2 4828	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 = 𝑎 → ⟨𝑏, 𝑤⟩ = ⟨𝑏, 𝑎⟩)
106	105	eleq1d 2813	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 = 𝑎 → (⟨𝑏, 𝑤⟩ ∈ ((int‘(II ×_t II))‘𝑆) ↔ ⟨𝑏, 𝑎⟩ ∈ ((int‘(II ×_t II))‘𝑆)))
107	104, 106	ralsn 4635	. . . . . . . . . . . . . . . . . 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 3121	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑎 ∈ (0[,]1)) → ∀𝑏 ∈ (0[,]1)∀𝑤 ∈ {𝑎}⟨𝑏, 𝑤⟩ ∈ ((int‘(II ×_t II))‘𝑆))
111		dfss3 3926	. . . . . . . . . . . . . . . 16 ⊢ (((0[,]1) × {𝑎}) ⊆ ((int‘(II ×_t II))‘𝑆) ↔ ∀𝑢 ∈ ((0[,]1) × {𝑎})𝑢 ∈ ((int‘(II ×_t II))‘𝑆))
112		eleq1 2816	. . . . . . . . . . . . . . . . 17 ⊢ (𝑢 = ⟨𝑏, 𝑤⟩ → (𝑢 ∈ ((int‘(II ×_t II))‘𝑆) ↔ ⟨𝑏, 𝑤⟩ ∈ ((int‘(II ×_t II))‘𝑆)))
113	112	ralxp 5788	. . . . . . . . . . . . . . . 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 23543	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑎 ∈ (0[,]1)) → ∃𝑣 ∈ II (𝑎 ∈ 𝑣 ∧ ((0[,]1) × 𝑣) ⊆ ((int‘(II ×_t II))‘𝑆)))
118	36	ntrss2 22960	. . . . . . . . . . . . . . . . . . 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 3946	. . . . . . . . . . . . . . . . . 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 5629	. . . . . . . . . . . . . . . . . . 19 ⊢ ((0[,]1) × 𝑣) = {⟨𝑟, 𝑡⟩ ∣ (𝑟 ∈ (0[,]1) ∧ 𝑡 ∈ 𝑣)}
123	122, 33	sseq12i 3968	. . . . . . . . . . . . . . . . . 18 ⊢ (((0[,]1) × 𝑣) ⊆ 𝑆 ↔ {⟨𝑟, 𝑡⟩ ∣ (𝑟 ∈ (0[,]1) ∧ 𝑡 ∈ 𝑣)} ⊆ {⟨𝑟, 𝑡⟩ ∣ (𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀))})
124		ssopab2bw 5494	. . . . . . . . . . . . . . . . . . 19 ⊢ ({⟨𝑟, 𝑡⟩ ∣ (𝑟 ∈ (0[,]1) ∧ 𝑡 ∈ 𝑣)} ⊆ {⟨𝑟, 𝑡⟩ ∣ (𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀))} ↔ ∀𝑟∀𝑡((𝑟 ∈ (0[,]1) ∧ 𝑡 ∈ 𝑣) → (𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀))))
125		r2al 3165	. . . . . . . . . . . . . . . . . . 19 ⊢ (∀𝑟 ∈ (0[,]1)∀𝑡 ∈ 𝑣 (𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀)) ↔ ∀𝑟∀𝑡((𝑟 ∈ (0[,]1) ∧ 𝑡 ∈ 𝑣) → (𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀))))
126		ralcom 3257	. . . . . . . . . . . . . . . . . . 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 3066	. . . . . . . . . . . . . . . . . . 19 ⊢ (∀𝑟 ∈ (0[,]1)(𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀)) → ∀𝑟 ∈ (0[,]1)∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀))
132		cvmlift2lem1 35274	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∀𝑟 ∈ (0[,]1)∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀) → (((0[,]1) × {𝑎}) ⊆ 𝑀 → ((0[,]1) × {𝑡}) ⊆ 𝑀))
133		bicom 222	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀) ↔ ((𝑢 × {𝑡}) ⊆ 𝑀 ↔ (𝑢 × {𝑎}) ⊆ 𝑀))
134	133	rexbii 3076	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀) ↔ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑡}) ⊆ 𝑀 ↔ (𝑢 × {𝑎}) ⊆ 𝑀))
135	134	ralbii 3075	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∀𝑟 ∈ (0[,]1)∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀) ↔ ∀𝑟 ∈ (0[,]1)∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑡}) ⊆ 𝑀 ↔ (𝑢 × {𝑎}) ⊆ 𝑀))
136		cvmlift2lem1 35274	. . . . . . . . . . . . . . . . . . . . 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 3420	. . . . . . . . . . . . . . . . . . . . 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 4891	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑣 ∈ II → 𝑣 ⊆ ∪ II)
145	144, 13	sseqtrrdi 3979	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑣 ∈ II → 𝑣 ⊆ (0[,]1))
146	145	adantl 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑎 ∈ (0[,]1)) ∧ 𝑣 ∈ II) → 𝑣 ⊆ (0[,]1))
147	146	sselda 3937	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑎 ∈ (0[,]1)) ∧ 𝑣 ∈ II) ∧ 𝑡 ∈ 𝑣) → 𝑡 ∈ (0[,]1))
148		sneq 4589	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑎 = 𝑡 → {𝑎} = {𝑡})
149	148	xpeq2d 5653	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑎 = 𝑡 → ((0[,]1) × {𝑎}) = ((0[,]1) × {𝑡}))
150	149	sseq1d 3969	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑎 = 𝑡 → (((0[,]1) × {𝑎}) ⊆ 𝑀 ↔ ((0[,]1) × {𝑡}) ⊆ 𝑀))
151	150, 140	elrab2 3653	. . . . . . . . . . . . . . . . . . . . 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 3141	. . . . . . . . . . . . . . . 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 3142	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑎 ∈ (0[,]1)) → (∃𝑣 ∈ II (𝑎 ∈ 𝑣 ∧ ((0[,]1) × 𝑣) ⊆ ((int‘(II ×_t II))‘𝑆)) → ∃𝑣 ∈ II (𝑎 ∈ 𝑣 ∧ ∀𝑡 ∈ 𝑣 (𝑎 ∈ 𝐴 ↔ 𝑡 ∈ 𝐴))))
160	117, 159	mpd 15	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑎 ∈ (0[,]1)) → ∃𝑣 ∈ II (𝑎 ∈ 𝑣 ∧ ∀𝑡 ∈ 𝑣 (𝑎 ∈ 𝐴 ↔ 𝑡 ∈ 𝐴)))
161	160	ralrimiva 3121	. . . . . . . . . . 11 ⊢ (𝜑 → ∀𝑎 ∈ (0[,]1)∃𝑣 ∈ II (𝑎 ∈ 𝑣 ∧ ∀𝑡 ∈ 𝑣 (𝑎 ∈ 𝐴 ↔ 𝑡 ∈ 𝐴)))
162		ssrab2 4033	. . . . . . . . . . . . 13 ⊢ {𝑎 ∈ (0[,]1) ∣ ((0[,]1) × {𝑎}) ⊆ 𝑀} ⊆ (0[,]1)
163	140, 162	eqsstri 3984	. . . . . . . . . . . 12 ⊢ 𝐴 ⊆ (0[,]1)
164	13	isclo 22990	. . . . . . . . . . . 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 3935	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 ∈ II)
168		0elunit 13390	. . . . . . . . . . . 12 ⊢ 0 ∈ (0[,]1)
169	168	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → 0 ∈ (0[,]1))
170		relxp 5641	. . . . . . . . . . . . 13 ⊢ Rel ((0[,]1) × {0})
171	170	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → Rel ((0[,]1) × {0}))
172		opelxp 5659	. . . . . . . . . . . . 13 ⊢ (⟨𝑟, 𝑎⟩ ∈ ((0[,]1) × {0}) ↔ (𝑟 ∈ (0[,]1) ∧ 𝑎 ∈ {0}))
173		id 22	. . . . . . . . . . . . . . . . 17 ⊢ (𝑟 ∈ (0[,]1) → 𝑟 ∈ (0[,]1))
174		opelxpi 5660	. . . . . . . . . . . . . . . . 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 35284	. . . . . . . . . . . . . . . . 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 6657	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → 𝐾 Fn ((0[,]1) × (0[,]1)))
187		fnov 7484	. . . . . . . . . . . . . . . . . . . . . . . . . 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 5933	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → (𝐾 ↾ (𝑢 × {0})) = ((𝑏 ∈ (0[,]1), 𝑤 ∈ (0[,]1) ↦ (𝑏𝐾𝑤)) ↾ (𝑢 × {0})))
190		simplrl 776	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → 𝑢 ∈ II)
191		elssuni 4891	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑢 ∈ II → 𝑢 ⊆ ∪ II)
192	191, 13	sseqtrrdi 3979	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑢 ∈ II → 𝑢 ⊆ (0[,]1))
193	190, 192	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → 𝑢 ⊆ (0[,]1))
194	169	snssd 4763	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → {0} ⊆ (0[,]1))
195	194	ad3antrrr 730	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → {0} ⊆ (0[,]1))
196		resmpo 7473	. . . . . . . . . . . . . . . . . . . . . . . . 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 3937	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 35282	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4596	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑤 ∈ {0} → 𝑤 = 0)
204	203	oveq2d 7369	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑤 ∈ {0} → (𝑏𝐾𝑤) = (𝑏𝐾0))
205	204	eqeq1d 2731	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 7430	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → (𝑏 ∈ 𝑢, 𝑤 ∈ {0} ↦ (𝑏𝐾𝑤)) = (𝑏 ∈ 𝑢, 𝑤 ∈ {0} ↦ (𝐻‘𝑏)))
209	189, 197, 208	3eqtrd 2768	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → (𝐾 ↾ (𝑢 × {0})) = (𝑏 ∈ 𝑢, 𝑤 ∈ {0} ↦ (𝐻‘𝑏)))
210		eqid 2729	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (II ↾_t 𝑢) = (II ↾_t 𝑢)
211		iitopon 24788	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ II ∈ (TopOn‘(0[,]1))
212	211	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → II ∈ (TopOn‘(0[,]1)))
213		eqid 2729	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (II ↾_t {0}) = (II ↾_t {0})
214	212, 212	cnmpt1st 23571	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → (𝑏 ∈ (0[,]1), 𝑤 ∈ (0[,]1) ↦ 𝑏) ∈ ((II ×_t II) Cn II))
215	1, 2, 3, 4, 5, 6	cvmlift2lem2 35276	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 23575	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → (𝑏 ∈ (0[,]1), 𝑤 ∈ (0[,]1) ↦ (𝐻‘𝑏)) ∈ ((II ×_t II) Cn 𝐶))
219	210, 212, 193, 213, 212, 195, 218	cnmpt2res 23580	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → (𝑏 ∈ 𝑢, 𝑤 ∈ {0} ↦ (𝐻‘𝑏)) ∈ (((II ↾_t 𝑢) ×_t (II ↾_t {0})) Cn 𝐶))
220		vex 3442	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ 𝑢 ∈ V
221		snex 5378	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ {0} ∈ V
222		txrest 23534	. . . . . . . . . . . . . . . . . . . . . . . . . 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 7363	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((II ×_t II) ↾_t (𝑢 × {0})) Cn 𝐶) = (((II ↾_t 𝑢) ×_t (II ↾_t {0})) Cn 𝐶)
225	219, 224	eleqtrrdi 2839	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → (𝑏 ∈ 𝑢, 𝑤 ∈ {0} ↦ (𝐻‘𝑏)) ∈ (((II ×_t II) ↾_t (𝑢 × {0})) Cn 𝐶))
226	209, 225	eqeltrd 2828	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → (𝐾 ↾ (𝑢 × {0})) ∈ (((II ×_t II) ↾_t (𝑢 × {0})) Cn 𝐶))
227		sneq 4589	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑤 = 0 → {𝑤} = {0})
228	227	xpeq2d 5653	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑤 = 0 → (𝑢 × {𝑤}) = (𝑢 × {0}))
229	228	reseq2d 5934	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑤 = 0 → (𝐾 ↾ (𝑢 × {𝑤})) = (𝐾 ↾ (𝑢 × {0})))
230	228	oveq2d 7369	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑤 = 0 → ((II ×_t II) ↾_t (𝑢 × {𝑤})) = ((II ×_t II) ↾_t (𝑢 × {0})))
231	230	oveq1d 7368	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑤 = 0 → (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶) = (((II ×_t II) ↾_t (𝑢 × {0})) Cn 𝐶))
232	229, 231	eleq12d 2822	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 = 0 → ((𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶) ↔ (𝐾 ↾ (𝑢 × {0})) ∈ (((II ×_t II) ↾_t (𝑢 × {0})) Cn 𝐶)))
233	232	rspcev 3579	. . . . . . . . . . . . . . . . . . . . . 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 5660	. . . . . . . . . . . . . . . . . . . . . . . . 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 5638	. . . . . . . . . . . . . . . . . . . . . . . . . 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 23065	. . . . . . . . . . . . . . . . . . . . . . . . 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 2830	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → ⟨𝑟, 0⟩ ∈ ∪ ((II ×_t II) ↾_t (𝑢 × 𝑣)))
244		eqid 2729	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ∪ ((II ×_t II) ↾_t (𝑢 × 𝑣)) = ∪ ((II ×_t II) ↾_t (𝑢 × 𝑣))
245	244	cncnpi 23181	. . . . . . . . . . . . . . . . . . . . . . . 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 22985	. . . . . . . . . . . . . . . . . . . . . . . . 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 2831	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → ⟨𝑟, 0⟩ ∈ ((int‘(II ×_t II))‘(𝑢 × 𝑣)))
254	36, 1	cnprest 23192	. . . . . . . . . . . . . . . . . . . . . . 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 3186	. . . . . . . . . . . . . . . . 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 6826	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = ⟨𝑟, 0⟩ → (((II ×_t II) CnP 𝐶)‘𝑧) = (((II ×_t II) CnP 𝐶)‘⟨𝑟, 0⟩))
263	262	eleq2d 2814	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = ⟨𝑟, 0⟩ → (𝐾 ∈ (((II ×_t II) CnP 𝐶)‘𝑧) ↔ 𝐾 ∈ (((II ×_t II) CnP 𝐶)‘⟨𝑟, 0⟩)))
264	263, 68	elrab2 3653	. . . . . . . . . . . . . . . 16 ⊢ (⟨𝑟, 0⟩ ∈ 𝑀 ↔ (⟨𝑟, 0⟩ ∈ ((0[,]1) × (0[,]1)) ∧ 𝐾 ∈ (((II ×_t II) CnP 𝐶)‘⟨𝑟, 0⟩)))
265	175, 261, 264	sylanbrc 583	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑟 ∈ (0[,]1)) → ⟨𝑟, 0⟩ ∈ 𝑀)
266		elsni 4596	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 ∈ {0} → 𝑎 = 0)
267	266	opeq2d 4834	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 ∈ {0} → ⟨𝑟, 𝑎⟩ = ⟨𝑟, 0⟩)
268	267	eleq1d 2813	. . . . . . . . . . . . . . 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 5735	. . . . . . . . . . 11 ⊢ (𝜑 → ((0[,]1) × {0}) ⊆ 𝑀)
273		sneq 4589	. . . . . . . . . . . . . 14 ⊢ (𝑎 = 0 → {𝑎} = {0})
274	273	xpeq2d 5653	. . . . . . . . . . . . 13 ⊢ (𝑎 = 0 → ((0[,]1) × {𝑎}) = ((0[,]1) × {0}))
275	274	sseq1d 3969	. . . . . . . . . . . 12 ⊢ (𝑎 = 0 → (((0[,]1) × {𝑎}) ⊆ 𝑀 ↔ ((0[,]1) × {0}) ⊆ 𝑀))
276	275, 140	elrab2 3653	. . . . . . . . . . 11 ⊢ (0 ∈ 𝐴 ↔ (0 ∈ (0[,]1) ∧ ((0[,]1) × {0}) ⊆ 𝑀))
277	169, 272, 276	sylanbrc 583	. . . . . . . . . 10 ⊢ (𝜑 → 0 ∈ 𝐴)
278	277	ne0d 4295	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 ≠ ∅)
279		inss2 4191	. . . . . . . . . 10 ⊢ (II ∩ (Clsd‘II)) ⊆ (Clsd‘II)
280	279, 166	sselid 3935	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 ∈ (Clsd‘II))
281	13, 15, 167, 278, 280	connclo 23318	. . . . . . . 8 ⊢ (𝜑 → 𝐴 = (0[,]1))
282	281, 140	eqtr3di 2779	. . . . . . 7 ⊢ (𝜑 → (0[,]1) = {𝑎 ∈ (0[,]1) ∣ ((0[,]1) × {𝑎}) ⊆ 𝑀})
283		rabid2 3430	. . . . . . 7 ⊢ ((0[,]1) = {𝑎 ∈ (0[,]1) ∣ ((0[,]1) × {𝑎}) ⊆ 𝑀} ↔ ∀𝑎 ∈ (0[,]1)((0[,]1) × {𝑎}) ⊆ 𝑀)
284	282, 283	sylib 218	. . . . . 6 ⊢ (𝜑 → ∀𝑎 ∈ (0[,]1)((0[,]1) × {𝑎}) ⊆ 𝑀)
285		iunss 4997	. . . . . 6 ⊢ (∪ 𝑎 ∈ (0[,]1)((0[,]1) × {𝑎}) ⊆ 𝑀 ↔ ∀𝑎 ∈ (0[,]1)((0[,]1) × {𝑎}) ⊆ 𝑀)
286	284, 285	sylibr 234	. . . . 5 ⊢ (𝜑 → ∪ 𝑎 ∈ (0[,]1)((0[,]1) × {𝑎}) ⊆ 𝑀)
287	12, 286	eqsstrid 3976	. . . 4 ⊢ (𝜑 → ((0[,]1) × (0[,]1)) ⊆ 𝑀)
288	287, 68	sseqtrdi 3978	. . 3 ⊢ (𝜑 → ((0[,]1) × (0[,]1)) ⊆ {𝑧 ∈ ((0[,]1) × (0[,]1)) ∣ 𝐾 ∈ (((II ×_t II) CnP 𝐶)‘𝑧)})
289		ssrab 4026	. . . 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 23494	. . . 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 35232	. . . . 5 ⊢ (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐶 ∈ Top)
295	2, 294	syl 17	. . . 4 ⊢ (𝜑 → 𝐶 ∈ Top)
296	1	toptopon 22820	. . . 4 ⊢ (𝐶 ∈ Top ↔ 𝐶 ∈ (TopOn‘𝐵))
297	295, 296	sylib 218	. . 3 ⊢ (𝜑 → 𝐶 ∈ (TopOn‘𝐵))
298		cncnp 23183	. . 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 3044 ∃wrex 3053 {crab 3396 Vcvv 3438 ∖ cdif 3902 ∩ cin 3904 ⊆ wss 3905 ∅c0 4286 𝒫 cpw 4553 {csn 4579 ⟨cop 4585 ∪ cuni 4861 ∪ ciun 4944 {copab 5157 ↦ cmpt 5176 × cxp 5621 ^◡ccnv 5622 ↾ cres 5625 “ cima 5626 ∘ ccom 5627 Rel wrel 5628 Fn wfn 6481 ⟶wf 6482 ‘cfv 6486 ℩crio 7309 (class class class)co 7353 ∈ cmpo 7355 0cc0 11028 1c1 11029 [,]cicc 13269 ↾_t crest 17342 Topctop 22796 TopOnctopon 22813 Clsdccld 22919 intcnt 22920 neicnei 23000 Cn ccn 23127 CnP ccnp 23128 Compccmp 23289 Conncconn 23314 ×_t ctx 23463 Homeochmeo 23656 IIcii 24784 CovMap ccvm 35227

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

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

This theorem is referenced by: cvmlift2lem13 35287

W3C validator