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 35298

Description: Lemma for cvmlift2 35300. (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 35291	. 2 ⊢ (𝜑 → 𝐾:((0[,]1) × (0[,]1))⟶𝐵)
9		iunid 5064	. . . . . . 7 ⊢ ∪ 𝑎 ∈ (0[,]1){𝑎} = (0[,]1)
10	9	xpeq2i 5715	. . . . . 6 ⊢ ((0[,]1) × ∪ 𝑎 ∈ (0[,]1){𝑎}) = ((0[,]1) × (0[,]1))
11		xpiundi 5758	. . . . . 6 ⊢ ((0[,]1) × ∪ 𝑎 ∈ (0[,]1){𝑎}) = ∪ 𝑎 ∈ (0[,]1)((0[,]1) × {𝑎})
12	10, 11	eqtr3i 2764	. . . . 5 ⊢ ((0[,]1) × (0[,]1)) = ∪ 𝑎 ∈ (0[,]1)((0[,]1) × {𝑎})
13		iiuni 24920	. . . . . . . . 9 ⊢ (0[,]1) = ∪ II
14		iiconn 24926	. . . . . . . . . 10 ⊢ II ∈ Conn
15	14	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → II ∈ Conn)
16		inss1 4244	. . . . . . . . . 10 ⊢ (II ∩ (Clsd‘II)) ⊆ II
17		iicmp 24925	. . . . . . . . . . . . . . 15 ⊢ II ∈ Comp
18	17	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑎 ∈ (0[,]1)) → II ∈ Comp)
19		iitop 24919	. . . . . . . . . . . . . . 15 ⊢ II ∈ Top
20	19	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑎 ∈ (0[,]1)) → II ∈ Top)
21	19, 19	txtopi 23613	. . . . . . . . . . . . . . . 16 ⊢ (II ×_t II) ∈ Top
22	13	neiss2 23124	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((II ∈ Top ∧ 𝑢 ∈ ((nei‘II)‘{𝑟})) → {𝑟} ⊆ (0[,]1))
23	19, 22	mpan 690	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑢 ∈ ((nei‘II)‘{𝑟}) → {𝑟} ⊆ (0[,]1))
24		vex 3481	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 𝑟 ∈ V
25	24	snss 4789	. . . . . . . . . . . . . . . . . . . . . . 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 3145	. . . . . . . . . . . . . . . . . . . 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 5559	. . . . . . . . . . . . . . . . 17 ⊢ {⟨𝑟, 𝑡⟩ ∣ (𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀))} ⊆ {⟨𝑟, 𝑡⟩ ∣ (𝑟 ∈ (0[,]1) ∧ 𝑡 ∈ (0[,]1))}
33		cvmlift2.s	. . . . . . . . . . . . . . . . 17 ⊢ 𝑆 = {⟨𝑟, 𝑡⟩ ∣ (𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀))}
34		df-xp 5694	. . . . . . . . . . . . . . . . 17 ⊢ ((0[,]1) × (0[,]1)) = {⟨𝑟, 𝑡⟩ ∣ (𝑟 ∈ (0[,]1) ∧ 𝑡 ∈ (0[,]1))}
35	32, 33, 34	3sstr4i 4038	. . . . . . . . . . . . . . . 16 ⊢ 𝑆 ⊆ ((0[,]1) × (0[,]1))
36	19, 19, 13, 13	txunii 23616	. . . . . . . . . . . . . . . . 17 ⊢ ((0[,]1) × (0[,]1)) = ∪ (II ×_t II)
37	36	ntropn 23072	. . . . . . . . . . . . . . . 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 2734	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (^◡𝐹 “ 𝑘) ∧ ∀𝑐 ∈ 𝑠 (∀𝑑 ∈ (𝑠 ∖ {𝑐})(𝑐 ∩ 𝑑) = ∅ ∧ (𝐹 ↾ 𝑐) ∈ ((𝐶 ↾_t 𝑐)Homeo(𝐽 ↾_t 𝑘))))}) = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (^◡𝐹 “ 𝑘) ∧ ∀𝑐 ∈ 𝑠 (∀𝑑 ∈ (𝑠 ∖ {𝑐})(𝑐 ∩ 𝑑) = ∅ ∧ (𝐹 ↾ 𝑐) ∈ ((𝐶 ↾_t 𝑐)Homeo(𝐽 ↾_t 𝑘))))})
45		simprr 773	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) → 𝑏 ∈ (0[,]1))
46		simprl 771	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) → 𝑎 ∈ (0[,]1))
47	1, 40, 41, 42, 43, 6, 7, 44, 45, 46	cvmlift2lem10 35296	. . . . . . . . . . . . . . . . . . 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 777	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×_t II) ↾_t (𝑢 × 𝑣)) Cn 𝐶)))) → 𝑢 ∈ II)
52		simplrr 778	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×_t II) ↾_t (𝑢 × 𝑣)) Cn 𝐶)))) → 𝑣 ∈ II)
53		txopn 23625	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((II ∈ Top ∧ II ∈ Top) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) → (𝑢 × 𝑣) ∈ (II ×_t II))
54	50, 50, 51, 52, 53	syl22anc 839	. . . . . . . . . . . . . . . . . . . . . . 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 4916	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑡 ∈ 𝑣 ∧ 𝑣 ∈ II) → 𝑡 ∈ ∪ II)
57	56, 13	eleqtrrdi 2849	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 771	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×_t II) ↾_t (𝑢 × 𝑣)) Cn 𝐶)))) ∧ (𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣)) → 𝑟 ∈ 𝑢)
62		opnneip 23142	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((II ∈ Top ∧ 𝑢 ∈ II ∧ 𝑟 ∈ 𝑢) → 𝑢 ∈ ((nei‘II)‘{𝑟}))
63	59, 60, 61, 62	syl3anc 1370	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1215	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×_t II) ↾_t (𝑢 × 𝑣)) Cn 𝐶)))) ∧ (𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣)) → 𝑎 ∈ 𝑣)
71		simprr 773	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×_t II) ↾_t (𝑢 × 𝑣)) Cn 𝐶)))) ∧ (𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣)) → 𝑡 ∈ 𝑣)
72		sneq 4640	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑐 = 𝑤 → {𝑐} = {𝑤})
73	72	xpeq2d 5718	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑐 = 𝑤 → (𝑢 × {𝑐}) = (𝑢 × {𝑤}))
74	73	reseq2d 5999	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑐 = 𝑤 → (𝐾 ↾ (𝑢 × {𝑐})) = (𝐾 ↾ (𝑢 × {𝑤})))
75	73	oveq2d 7446	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑐 = 𝑤 → ((II ×_t II) ↾_t (𝑢 × {𝑐})) = ((II ×_t II) ↾_t (𝑢 × {𝑤})))
76	75	oveq1d 7445	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑐 = 𝑤 → (((II ×_t II) ↾_t (𝑢 × {𝑐})) Cn 𝐶) = (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶))
77	74, 76	eleq12d 2832	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑐 = 𝑤 → ((𝐾 ↾ (𝑢 × {𝑐})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑐})) Cn 𝐶) ↔ (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶)))
78	77	cbvrexvw 3235	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (∃𝑐 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑐})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑐})) Cn 𝐶) ↔ ∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶))
79		simplr3 1216	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 35297	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 35297	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3246	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1925	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×_t II) ↾_t (𝑢 × 𝑣)) Cn 𝐶)))) → ∀𝑟∀𝑡((𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣) → (𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀))))
89		df-xp 5694	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑢 × 𝑣) = {⟨𝑟, 𝑡⟩ ∣ (𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣)}
90	89, 33	sseq12i 4025	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑢 × 𝑣) ⊆ 𝑆 ↔ {⟨𝑟, 𝑡⟩ ∣ (𝑟 ∈ 𝑢 ∧ 𝑡 ∈ 𝑣)} ⊆ {⟨𝑟, 𝑡⟩ ∣ (𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀))})
91		ssopab2bw 5556	. . . . . . . . . . . . . . . . . . . . . . . . 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 23081	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((II ×_t II) ∈ Top ∧ 𝑆 ⊆ ((0[,]1) × (0[,]1))) ∧ ((𝑢 × 𝑣) ∈ (II ×_t II) ∧ (𝑢 × 𝑣) ⊆ 𝑆)) → (𝑢 × 𝑣) ⊆ ((int‘(II ×_t II))‘𝑆))
95	48, 49, 54, 93, 94	syl22anc 839	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×_t II) ↾_t (𝑢 × 𝑣)) Cn 𝐶)))) → (𝑢 × 𝑣) ⊆ ((int‘(II ×_t II))‘𝑆))
96		simpr1 1193	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×_t II) ↾_t (𝑢 × 𝑣)) Cn 𝐶)))) → 𝑏 ∈ 𝑢)
97		simpr2 1194	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏 ∈ 𝑢 ∧ 𝑎 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×_t II) ↾_t (𝑢 × 𝑣)) Cn 𝐶)))) → 𝑎 ∈ 𝑣)
98		opelxpi 5725	. . . . . . . . . . . . . . . . . . . . . . 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 3995	. . . . . . . . . . . . . . . . . . . . 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 3210	. . . . . . . . . . . . . . . . . . 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 3481	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑎 ∈ V
105		opeq2 4878	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 = 𝑎 → ⟨𝑏, 𝑤⟩ = ⟨𝑏, 𝑎⟩)
106	105	eleq1d 2823	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 = 𝑎 → (⟨𝑏, 𝑤⟩ ∈ ((int‘(II ×_t II))‘𝑆) ↔ ⟨𝑏, 𝑎⟩ ∈ ((int‘(II ×_t II))‘𝑆)))
107	104, 106	ralsn 4685	. . . . . . . . . . . . . . . . . 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 3143	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑎 ∈ (0[,]1)) → ∀𝑏 ∈ (0[,]1)∀𝑤 ∈ {𝑎}⟨𝑏, 𝑤⟩ ∈ ((int‘(II ×_t II))‘𝑆))
111		dfss3 3983	. . . . . . . . . . . . . . . 16 ⊢ (((0[,]1) × {𝑎}) ⊆ ((int‘(II ×_t II))‘𝑆) ↔ ∀𝑢 ∈ ((0[,]1) × {𝑎})𝑢 ∈ ((int‘(II ×_t II))‘𝑆))
112		eleq1 2826	. . . . . . . . . . . . . . . . 17 ⊢ (𝑢 = ⟨𝑏, 𝑤⟩ → (𝑢 ∈ ((int‘(II ×_t II))‘𝑆) ↔ ⟨𝑏, 𝑤⟩ ∈ ((int‘(II ×_t II))‘𝑆)))
113	112	ralxp 5854	. . . . . . . . . . . . . . . 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 23663	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑎 ∈ (0[,]1)) → ∃𝑣 ∈ II (𝑎 ∈ 𝑣 ∧ ((0[,]1) × 𝑣) ⊆ ((int‘(II ×_t II))‘𝑆)))
118	36	ntrss2 23080	. . . . . . . . . . . . . . . . . . 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 4003	. . . . . . . . . . . . . . . . . 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 5694	. . . . . . . . . . . . . . . . . . 19 ⊢ ((0[,]1) × 𝑣) = {⟨𝑟, 𝑡⟩ ∣ (𝑟 ∈ (0[,]1) ∧ 𝑡 ∈ 𝑣)}
123	122, 33	sseq12i 4025	. . . . . . . . . . . . . . . . . 18 ⊢ (((0[,]1) × 𝑣) ⊆ 𝑆 ↔ {⟨𝑟, 𝑡⟩ ∣ (𝑟 ∈ (0[,]1) ∧ 𝑡 ∈ 𝑣)} ⊆ {⟨𝑟, 𝑡⟩ ∣ (𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀))})
124		ssopab2bw 5556	. . . . . . . . . . . . . . . . . . 19 ⊢ ({⟨𝑟, 𝑡⟩ ∣ (𝑟 ∈ (0[,]1) ∧ 𝑡 ∈ 𝑣)} ⊆ {⟨𝑟, 𝑡⟩ ∣ (𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀))} ↔ ∀𝑟∀𝑡((𝑟 ∈ (0[,]1) ∧ 𝑡 ∈ 𝑣) → (𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀))))
125		r2al 3192	. . . . . . . . . . . . . . . . . . 19 ⊢ (∀𝑟 ∈ (0[,]1)∀𝑡 ∈ 𝑣 (𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀)) ↔ ∀𝑟∀𝑡((𝑟 ∈ (0[,]1) ∧ 𝑡 ∈ 𝑣) → (𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀))))
126		ralcom 3286	. . . . . . . . . . . . . . . . . . 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 3080	. . . . . . . . . . . . . . . . . . 19 ⊢ (∀𝑟 ∈ (0[,]1)(𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀)) → ∀𝑟 ∈ (0[,]1)∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀))
132		cvmlift2lem1 35286	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∀𝑟 ∈ (0[,]1)∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀) → (((0[,]1) × {𝑎}) ⊆ 𝑀 → ((0[,]1) × {𝑡}) ⊆ 𝑀))
133		bicom 222	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀) ↔ ((𝑢 × {𝑡}) ⊆ 𝑀 ↔ (𝑢 × {𝑎}) ⊆ 𝑀))
134	133	rexbii 3091	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀) ↔ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑡}) ⊆ 𝑀 ↔ (𝑢 × {𝑎}) ⊆ 𝑀))
135	134	ralbii 3090	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∀𝑟 ∈ (0[,]1)∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀) ↔ ∀𝑟 ∈ (0[,]1)∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑡}) ⊆ 𝑀 ↔ (𝑢 × {𝑎}) ⊆ 𝑀))
136		cvmlift2lem1 35286	. . . . . . . . . . . . . . . . . . . . 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 3456	. . . . . . . . . . . . . . . . . . . . 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 4941	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑣 ∈ II → 𝑣 ⊆ ∪ II)
145	144, 13	sseqtrrdi 4046	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑣 ∈ II → 𝑣 ⊆ (0[,]1))
146	145	adantl 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑎 ∈ (0[,]1)) ∧ 𝑣 ∈ II) → 𝑣 ⊆ (0[,]1))
147	146	sselda 3994	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑎 ∈ (0[,]1)) ∧ 𝑣 ∈ II) ∧ 𝑡 ∈ 𝑣) → 𝑡 ∈ (0[,]1))
148		sneq 4640	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑎 = 𝑡 → {𝑎} = {𝑡})
149	148	xpeq2d 5718	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑎 = 𝑡 → ((0[,]1) × {𝑎}) = ((0[,]1) × {𝑡}))
150	149	sseq1d 4026	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑎 = 𝑡 → (((0[,]1) × {𝑎}) ⊆ 𝑀 ↔ ((0[,]1) × {𝑡}) ⊆ 𝑀))
151	150, 140	elrab2 3697	. . . . . . . . . . . . . . . . . . . . 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 3164	. . . . . . . . . . . . . . . 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 3165	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑎 ∈ (0[,]1)) → (∃𝑣 ∈ II (𝑎 ∈ 𝑣 ∧ ((0[,]1) × 𝑣) ⊆ ((int‘(II ×_t II))‘𝑆)) → ∃𝑣 ∈ II (𝑎 ∈ 𝑣 ∧ ∀𝑡 ∈ 𝑣 (𝑎 ∈ 𝐴 ↔ 𝑡 ∈ 𝐴))))
160	117, 159	mpd 15	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑎 ∈ (0[,]1)) → ∃𝑣 ∈ II (𝑎 ∈ 𝑣 ∧ ∀𝑡 ∈ 𝑣 (𝑎 ∈ 𝐴 ↔ 𝑡 ∈ 𝐴)))
161	160	ralrimiva 3143	. . . . . . . . . . 11 ⊢ (𝜑 → ∀𝑎 ∈ (0[,]1)∃𝑣 ∈ II (𝑎 ∈ 𝑣 ∧ ∀𝑡 ∈ 𝑣 (𝑎 ∈ 𝐴 ↔ 𝑡 ∈ 𝐴)))
162		ssrab2 4089	. . . . . . . . . . . . 13 ⊢ {𝑎 ∈ (0[,]1) ∣ ((0[,]1) × {𝑎}) ⊆ 𝑀} ⊆ (0[,]1)
163	140, 162	eqsstri 4029	. . . . . . . . . . . 12 ⊢ 𝐴 ⊆ (0[,]1)
164	13	isclo 23110	. . . . . . . . . . . 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 3992	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 ∈ II)
168		0elunit 13505	. . . . . . . . . . . 12 ⊢ 0 ∈ (0[,]1)
169	168	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → 0 ∈ (0[,]1))
170		relxp 5706	. . . . . . . . . . . . 13 ⊢ Rel ((0[,]1) × {0})
171	170	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → Rel ((0[,]1) × {0}))
172		opelxp 5724	. . . . . . . . . . . . 13 ⊢ (⟨𝑟, 𝑎⟩ ∈ ((0[,]1) × {0}) ↔ (𝑟 ∈ (0[,]1) ∧ 𝑎 ∈ {0}))
173		id 22	. . . . . . . . . . . . . . . . 17 ⊢ (𝑟 ∈ (0[,]1) → 𝑟 ∈ (0[,]1))
174		opelxpi 5725	. . . . . . . . . . . . . . . . 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 35296	. . . . . . . . . . . . . . . . 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 773	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → 0 ∈ 𝑣)
185	8	ad3antrrr 730	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → 𝐾:((0[,]1) × (0[,]1))⟶𝐵)
186	185	ffnd 6737	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → 𝐾 Fn ((0[,]1) × (0[,]1)))
187		fnov 7563	. . . . . . . . . . . . . . . . . . . . . . . . . 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 5998	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → (𝐾 ↾ (𝑢 × {0})) = ((𝑏 ∈ (0[,]1), 𝑤 ∈ (0[,]1) ↦ (𝑏𝐾𝑤)) ↾ (𝑢 × {0})))
190		simplrl 777	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → 𝑢 ∈ II)
191		elssuni 4941	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑢 ∈ II → 𝑢 ⊆ ∪ II)
192	191, 13	sseqtrrdi 4046	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑢 ∈ II → 𝑢 ⊆ (0[,]1))
193	190, 192	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → 𝑢 ⊆ (0[,]1))
194	169	snssd 4813	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → {0} ⊆ (0[,]1))
195	194	ad3antrrr 730	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → {0} ⊆ (0[,]1))
196		resmpo 7552	. . . . . . . . . . . . . . . . . . . . . . . . 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 3994	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) ∧ 𝑏 ∈ 𝑢) → 𝑏 ∈ (0[,]1))
199		simplll 775	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → 𝜑)
200	1, 2, 3, 4, 5, 6, 7	cvmlift2lem8 35294	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4647	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑤 ∈ {0} → 𝑤 = 0)
204	203	oveq2d 7446	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑤 ∈ {0} → (𝑏𝐾𝑤) = (𝑏𝐾0))
205	204	eqeq1d 2736	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑤 ∈ {0} → ((𝑏𝐾𝑤) = (𝐻‘𝑏) ↔ (𝑏𝐾0) = (𝐻‘𝑏)))
206	202, 205	syl5ibrcom 247	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) ∧ 𝑏 ∈ 𝑢) → (𝑤 ∈ {0} → (𝑏𝐾𝑤) = (𝐻‘𝑏)))
207	206	3impia 1116	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) ∧ 𝑏 ∈ 𝑢 ∧ 𝑤 ∈ {0}) → (𝑏𝐾𝑤) = (𝐻‘𝑏))
208	207	mpoeq3dva 7509	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → (𝑏 ∈ 𝑢, 𝑤 ∈ {0} ↦ (𝑏𝐾𝑤)) = (𝑏 ∈ 𝑢, 𝑤 ∈ {0} ↦ (𝐻‘𝑏)))
209	189, 197, 208	3eqtrd 2778	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → (𝐾 ↾ (𝑢 × {0})) = (𝑏 ∈ 𝑢, 𝑤 ∈ {0} ↦ (𝐻‘𝑏)))
210		eqid 2734	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (II ↾_t 𝑢) = (II ↾_t 𝑢)
211		iitopon 24918	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ II ∈ (TopOn‘(0[,]1))
212	211	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → II ∈ (TopOn‘(0[,]1)))
213		eqid 2734	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (II ↾_t {0}) = (II ↾_t {0})
214	212, 212	cnmpt1st 23691	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → (𝑏 ∈ (0[,]1), 𝑤 ∈ (0[,]1) ↦ 𝑏) ∈ ((II ×_t II) Cn II))
215	1, 2, 3, 4, 5, 6	cvmlift2lem2 35288	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → (𝐻 ∈ (II Cn 𝐶) ∧ (𝐹 ∘ 𝐻) = (𝑧 ∈ (0[,]1) ↦ (𝑧𝐺0)) ∧ (𝐻‘0) = 𝑃))
216	215	simp1d 1141	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → 𝐻 ∈ (II Cn 𝐶))
217	199, 216	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → 𝐻 ∈ (II Cn 𝐶))
218	212, 212, 214, 217	cnmpt21f 23695	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → (𝑏 ∈ (0[,]1), 𝑤 ∈ (0[,]1) ↦ (𝐻‘𝑏)) ∈ ((II ×_t II) Cn 𝐶))
219	210, 212, 193, 213, 212, 195, 218	cnmpt2res 23700	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → (𝑏 ∈ 𝑢, 𝑤 ∈ {0} ↦ (𝐻‘𝑏)) ∈ (((II ↾_t 𝑢) ×_t (II ↾_t {0})) Cn 𝐶))
220		vex 3481	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ 𝑢 ∈ V
221		snex 5441	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ {0} ∈ V
222		txrest 23654	. . . . . . . . . . . . . . . . . . . . . . . . . 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 7440	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((II ×_t II) ↾_t (𝑢 × {0})) Cn 𝐶) = (((II ↾_t 𝑢) ×_t (II ↾_t {0})) Cn 𝐶)
225	219, 224	eleqtrrdi 2849	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → (𝑏 ∈ 𝑢, 𝑤 ∈ {0} ↦ (𝐻‘𝑏)) ∈ (((II ×_t II) ↾_t (𝑢 × {0})) Cn 𝐶))
226	209, 225	eqeltrd 2838	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → (𝐾 ↾ (𝑢 × {0})) ∈ (((II ×_t II) ↾_t (𝑢 × {0})) Cn 𝐶))
227		sneq 4640	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑤 = 0 → {𝑤} = {0})
228	227	xpeq2d 5718	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑤 = 0 → (𝑢 × {𝑤}) = (𝑢 × {0}))
229	228	reseq2d 5999	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑤 = 0 → (𝐾 ↾ (𝑢 × {𝑤})) = (𝐾 ↾ (𝑢 × {0})))
230	228	oveq2d 7446	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑤 = 0 → ((II ×_t II) ↾_t (𝑢 × {𝑤})) = ((II ×_t II) ↾_t (𝑢 × {0})))
231	230	oveq1d 7445	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑤 = 0 → (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶) = (((II ×_t II) ↾_t (𝑢 × {0})) Cn 𝐶))
232	229, 231	eleq12d 2832	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 = 0 → ((𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×_t II) ↾_t (𝑢 × {𝑤})) Cn 𝐶) ↔ (𝐾 ↾ (𝑢 × {0})) ∈ (((II ×_t II) ↾_t (𝑢 × {0})) Cn 𝐶)))
233	232	rspcev 3621	. . . . . . . . . . . . . . . . . . . . . 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 5725	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣) → ⟨𝑟, 0⟩ ∈ (𝑢 × 𝑣))
236	235	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → ⟨𝑟, 0⟩ ∈ (𝑢 × 𝑣))
237		simplrr 778	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → 𝑣 ∈ II)
238	237, 145	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → 𝑣 ⊆ (0[,]1))
239		xpss12 5703	. . . . . . . . . . . . . . . . . . . . . . . . . 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 23185	. . . . . . . . . . . . . . . . . . . . . . . . 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 2840	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → ⟨𝑟, 0⟩ ∈ ∪ ((II ×_t II) ↾_t (𝑢 × 𝑣)))
244		eqid 2734	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ∪ ((II ×_t II) ↾_t (𝑢 × 𝑣)) = ∪ ((II ×_t II) ↾_t (𝑢 × 𝑣))
245	244	cncnpi 23301	. . . . . . . . . . . . . . . . . . . . . . . 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 839	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → (𝑢 × 𝑣) ∈ (II ×_t II))
251		isopn3i 23105	. . . . . . . . . . . . . . . . . . . . . . . . 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 2841	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟 ∈ 𝑢 ∧ 0 ∈ 𝑣)) → ⟨𝑟, 0⟩ ∈ ((int‘(II ×_t II))‘(𝑢 × 𝑣)))
254	36, 1	cnprest 23312	. . . . . . . . . . . . . . . . . . . . . . 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 839	. . . . . . . . . . . . . . . . . . . . . 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 3210	. . . . . . . . . . . . . . . . 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 6906	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = ⟨𝑟, 0⟩ → (((II ×_t II) CnP 𝐶)‘𝑧) = (((II ×_t II) CnP 𝐶)‘⟨𝑟, 0⟩))
263	262	eleq2d 2824	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = ⟨𝑟, 0⟩ → (𝐾 ∈ (((II ×_t II) CnP 𝐶)‘𝑧) ↔ 𝐾 ∈ (((II ×_t II) CnP 𝐶)‘⟨𝑟, 0⟩)))
264	263, 68	elrab2 3697	. . . . . . . . . . . . . . . 16 ⊢ (⟨𝑟, 0⟩ ∈ 𝑀 ↔ (⟨𝑟, 0⟩ ∈ ((0[,]1) × (0[,]1)) ∧ 𝐾 ∈ (((II ×_t II) CnP 𝐶)‘⟨𝑟, 0⟩)))
265	175, 261, 264	sylanbrc 583	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑟 ∈ (0[,]1)) → ⟨𝑟, 0⟩ ∈ 𝑀)
266		elsni 4647	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 ∈ {0} → 𝑎 = 0)
267	266	opeq2d 4884	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 ∈ {0} → ⟨𝑟, 𝑎⟩ = ⟨𝑟, 0⟩)
268	267	eleq1d 2823	. . . . . . . . . . . . . . 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 5800	. . . . . . . . . . 11 ⊢ (𝜑 → ((0[,]1) × {0}) ⊆ 𝑀)
273		sneq 4640	. . . . . . . . . . . . . 14 ⊢ (𝑎 = 0 → {𝑎} = {0})
274	273	xpeq2d 5718	. . . . . . . . . . . . 13 ⊢ (𝑎 = 0 → ((0[,]1) × {𝑎}) = ((0[,]1) × {0}))
275	274	sseq1d 4026	. . . . . . . . . . . 12 ⊢ (𝑎 = 0 → (((0[,]1) × {𝑎}) ⊆ 𝑀 ↔ ((0[,]1) × {0}) ⊆ 𝑀))
276	275, 140	elrab2 3697	. . . . . . . . . . 11 ⊢ (0 ∈ 𝐴 ↔ (0 ∈ (0[,]1) ∧ ((0[,]1) × {0}) ⊆ 𝑀))
277	169, 272, 276	sylanbrc 583	. . . . . . . . . 10 ⊢ (𝜑 → 0 ∈ 𝐴)
278	277	ne0d 4347	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 ≠ ∅)
279		inss2 4245	. . . . . . . . . 10 ⊢ (II ∩ (Clsd‘II)) ⊆ (Clsd‘II)
280	279, 166	sselid 3992	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 ∈ (Clsd‘II))
281	13, 15, 167, 278, 280	connclo 23438	. . . . . . . 8 ⊢ (𝜑 → 𝐴 = (0[,]1))
282	281, 140	eqtr3di 2789	. . . . . . 7 ⊢ (𝜑 → (0[,]1) = {𝑎 ∈ (0[,]1) ∣ ((0[,]1) × {𝑎}) ⊆ 𝑀})
283		rabid2 3467	. . . . . . 7 ⊢ ((0[,]1) = {𝑎 ∈ (0[,]1) ∣ ((0[,]1) × {𝑎}) ⊆ 𝑀} ↔ ∀𝑎 ∈ (0[,]1)((0[,]1) × {𝑎}) ⊆ 𝑀)
284	282, 283	sylib 218	. . . . . 6 ⊢ (𝜑 → ∀𝑎 ∈ (0[,]1)((0[,]1) × {𝑎}) ⊆ 𝑀)
285		iunss 5049	. . . . . 6 ⊢ (∪ 𝑎 ∈ (0[,]1)((0[,]1) × {𝑎}) ⊆ 𝑀 ↔ ∀𝑎 ∈ (0[,]1)((0[,]1) × {𝑎}) ⊆ 𝑀)
286	284, 285	sylibr 234	. . . . 5 ⊢ (𝜑 → ∪ 𝑎 ∈ (0[,]1)((0[,]1) × {𝑎}) ⊆ 𝑀)
287	12, 286	eqsstrid 4043	. . . 4 ⊢ (𝜑 → ((0[,]1) × (0[,]1)) ⊆ 𝑀)
288	287, 68	sseqtrdi 4045	. . 3 ⊢ (𝜑 → ((0[,]1) × (0[,]1)) ⊆ {𝑧 ∈ ((0[,]1) × (0[,]1)) ∣ 𝐾 ∈ (((II ×_t II) CnP 𝐶)‘𝑧)})
289		ssrab 4082	. . . 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 23614	. . . 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 35244	. . . . 5 ⊢ (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐶 ∈ Top)
295	2, 294	syl 17	. . . 4 ⊢ (𝜑 → 𝐶 ∈ Top)
296	1	toptopon 22938	. . . 4 ⊢ (𝐶 ∈ Top ↔ 𝐶 ∈ (TopOn‘𝐵))
297	295, 296	sylib 218	. . 3 ⊢ (𝜑 → 𝐶 ∈ (TopOn‘𝐵))
298		cncnp 23303	. . 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 1534 = wceq 1536 ∈ wcel 2105 ∀wral 3058 ∃wrex 3067 {crab 3432 Vcvv 3477 ∖ cdif 3959 ∩ cin 3961 ⊆ wss 3962 ∅c0 4338 𝒫 cpw 4604 {csn 4630 ⟨cop 4636 ∪ cuni 4911 ∪ ciun 4995 {copab 5209 ↦ cmpt 5230 × cxp 5686 ^◡ccnv 5687 ↾ cres 5690 “ cima 5691 ∘ ccom 5692 Rel wrel 5693 Fn wfn 6557 ⟶wf 6558 ‘cfv 6562 ℩crio 7386 (class class class)co 7430 ∈ cmpo 7432 0cc0 11152 1c1 11153 [,]cicc 13386 ↾_t crest 17466 Topctop 22914 TopOnctopon 22931 Clsdccld 23039 intcnt 23040 neicnei 23120 Cn ccn 23247 CnP ccnp 23248 Compccmp 23409 Conncconn 23434 ×_t ctx 23583 Homeochmeo 23776 IIcii 24914 CovMap ccvm 35239

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1791 ax-4 1805 ax-5 1907 ax-6 1964 ax-7 2004 ax-8 2107 ax-9 2115 ax-10 2138 ax-11 2154 ax-12 2174 ax-ext 2705 ax-rep 5284 ax-sep 5301 ax-nul 5311 ax-pow 5370 ax-pr 5437 ax-un 7753 ax-inf2 9678 ax-cnex 11208 ax-resscn 11209 ax-1cn 11210 ax-icn 11211 ax-addcl 11212 ax-addrcl 11213 ax-mulcl 11214 ax-mulrcl 11215 ax-mulcom 11216 ax-addass 11217 ax-mulass 11218 ax-distr 11219 ax-i2m1 11220 ax-1ne0 11221 ax-1rid 11222 ax-rnegex 11223 ax-rrecex 11224 ax-cnre 11225 ax-pre-lttri 11226 ax-pre-lttrn 11227 ax-pre-ltadd 11228 ax-pre-mulgt0 11229 ax-pre-sup 11230 ax-addf 11231

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1539 df-fal 1549 df-ex 1776 df-nf 1780 df-sb 2062 df-mo 2537 df-eu 2566 df-clab 2712 df-cleq 2726 df-clel 2813 df-nfc 2889 df-ne 2938 df-nel 3044 df-ral 3059 df-rex 3068 df-rmo 3377 df-reu 3378 df-rab 3433 df-v 3479 df-sbc 3791 df-csb 3908 df-dif 3965 df-un 3967 df-in 3969 df-ss 3979 df-pss 3982 df-nul 4339 df-if 4531 df-pw 4606 df-sn 4631 df-pr 4633 df-tp 4635 df-op 4637 df-uni 4912 df-int 4951 df-iun 4997 df-iin 4998 df-br 5148 df-opab 5210 df-mpt 5231 df-tr 5265 df-id 5582 df-eprel 5588 df-po 5596 df-so 5597 df-fr 5640 df-se 5641 df-we 5642 df-xp 5694 df-rel 5695 df-cnv 5696 df-co 5697 df-dm 5698 df-rn 5699 df-res 5700 df-ima 5701 df-pred 6322 df-ord 6388 df-on 6389 df-lim 6390 df-suc 6391 df-iota 6515 df-fun 6564 df-fn 6565 df-f 6566 df-f1 6567 df-fo 6568 df-f1o 6569 df-fv 6570 df-isom 6571 df-riota 7387 df-ov 7433 df-oprab 7434 df-mpo 7435 df-of 7696 df-om 7887 df-1st 8012 df-2nd 8013 df-supp 8184 df-frecs 8304 df-wrecs 8335 df-recs 8409 df-rdg 8448 df-1o 8504 df-2o 8505 df-er 8743 df-ec 8745 df-map 8866 df-ixp 8936 df-en 8984 df-dom 8985 df-sdom 8986 df-fin 8987 df-fsupp 9399 df-fi 9448 df-sup 9479 df-inf 9480 df-oi 9547 df-card 9976 df-pnf 11294 df-mnf 11295 df-xr 11296 df-ltxr 11297 df-le 11298 df-sub 11491 df-neg 11492 df-div 11918 df-nn 12264 df-2 12326 df-3 12327 df-4 12328 df-5 12329 df-6 12330 df-7 12331 df-8 12332 df-9 12333 df-n0 12524 df-z 12611 df-dec 12731 df-uz 12876 df-q 12988 df-rp 13032 df-xneg 13151 df-xadd 13152 df-xmul 13153 df-ioo 13387 df-ico 13389 df-icc 13390 df-fz 13544 df-fzo 13691 df-fl 13828 df-seq 14039 df-exp 14099 df-hash 14366 df-cj 15134 df-re 15135 df-im 15136 df-sqrt 15270 df-abs 15271 df-clim 15520 df-sum 15719 df-struct 17180 df-sets 17197 df-slot 17215 df-ndx 17227 df-base 17245 df-ress 17274 df-plusg 17310 df-mulr 17311 df-starv 17312 df-sca 17313 df-vsca 17314 df-ip 17315 df-tset 17316 df-ple 17317 df-ds 17319 df-unif 17320 df-hom 17321 df-cco 17322 df-rest 17468 df-topn 17469 df-0g 17487 df-gsum 17488 df-topgen 17489 df-pt 17490 df-prds 17493 df-xrs 17548 df-qtop 17553 df-imas 17554 df-xps 17556 df-mre 17630 df-mrc 17631 df-acs 17633 df-mgm 18665 df-sgrp 18744 df-mnd 18760 df-submnd 18809 df-mulg 19098 df-cntz 19347 df-cmn 19814 df-psmet 21373 df-xmet 21374 df-met 21375 df-bl 21376 df-mopn 21377 df-cnfld 21382 df-top 22915 df-topon 22932 df-topsp 22954 df-bases 22968 df-cld 23042 df-ntr 23043 df-cls 23044 df-nei 23121 df-cn 23250 df-cnp 23251 df-cmp 23410 df-conn 23435 df-lly 23489 df-nlly 23490 df-tx 23585 df-hmeo 23778 df-xms 24345 df-ms 24346 df-tms 24347 df-ii 24916 df-cncf 24917 df-htpy 25015 df-phtpy 25016 df-phtpc 25037 df-pconn 35205 df-sconn 35206 df-cvm 35240

This theorem is referenced by: cvmlift2lem13 35299

W3C validator