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

Theorem cvmlift2lem12 31624
Description: Lemma for cvmlift2 31626. (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.
StepHypRef 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) = (𝐻𝑥)))‘𝑦))
81, 2, 3, 4, 5, 6, 7cvmlift2lem5 31617 . 2 (𝜑𝐾:((0[,]1) × (0[,]1))⟶𝐵)
9 iunid 4774 . . . . . . 7 𝑎 ∈ (0[,]1){𝑎} = (0[,]1)
109xpeq2i 5344 . . . . . 6 ((0[,]1) × 𝑎 ∈ (0[,]1){𝑎}) = ((0[,]1) × (0[,]1))
11 xpiundi 5380 . . . . . 6 ((0[,]1) × 𝑎 ∈ (0[,]1){𝑎}) = 𝑎 ∈ (0[,]1)((0[,]1) × {𝑎})
1210, 11eqtr3i 2837 . . . . 5 ((0[,]1) × (0[,]1)) = 𝑎 ∈ (0[,]1)((0[,]1) × {𝑎})
13 cvmlift2.a . . . . . . . 8 𝐴 = {𝑎 ∈ (0[,]1) ∣ ((0[,]1) × {𝑎}) ⊆ 𝑀}
14 iiuni 22901 . . . . . . . . 9 (0[,]1) = II
15 iiconn 22907 . . . . . . . . . 10 II ∈ Conn
1615a1i 11 . . . . . . . . 9 (𝜑 → II ∈ Conn)
17 inss1 4036 . . . . . . . . . 10 (II ∩ (Clsd‘II)) ⊆ II
18 iicmp 22906 . . . . . . . . . . . . . . 15 II ∈ Comp
1918a1i 11 . . . . . . . . . . . . . 14 ((𝜑𝑎 ∈ (0[,]1)) → II ∈ Comp)
20 iitop 22900 . . . . . . . . . . . . . . 15 II ∈ Top
2120a1i 11 . . . . . . . . . . . . . 14 ((𝜑𝑎 ∈ (0[,]1)) → II ∈ Top)
2220, 20txtopi 21611 . . . . . . . . . . . . . . . 16 (II ×t II) ∈ Top
2314neiss2 21123 . . . . . . . . . . . . . . . . . . . . . . . 24 ((II ∈ Top ∧ 𝑢 ∈ ((nei‘II)‘{𝑟})) → {𝑟} ⊆ (0[,]1))
2420, 23mpan 673 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑢 ∈ ((nei‘II)‘{𝑟}) → {𝑟} ⊆ (0[,]1))
25 vex 3401 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑟 ∈ V
2625snss 4513 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑟 ∈ (0[,]1) ↔ {𝑟} ⊆ (0[,]1))
2724, 26sylibr 225 . . . . . . . . . . . . . . . . . . . . . 22 (𝑢 ∈ ((nei‘II)‘{𝑟}) → 𝑟 ∈ (0[,]1))
2827a1d 25 . . . . . . . . . . . . . . . . . . . . 21 (𝑢 ∈ ((nei‘II)‘{𝑟}) → (((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀) → 𝑟 ∈ (0[,]1)))
2928rexlimiv 3222 . . . . . . . . . . . . . . . . . . . 20 (∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀) → 𝑟 ∈ (0[,]1))
3029adantl 469 . . . . . . . . . . . . . . . . . . 19 ((𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀)) → 𝑟 ∈ (0[,]1))
31 simpl 470 . . . . . . . . . . . . . . . . . . 19 ((𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀)) → 𝑡 ∈ (0[,]1))
3230, 31jca 503 . . . . . . . . . . . . . . . . . 18 ((𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀)) → (𝑟 ∈ (0[,]1) ∧ 𝑡 ∈ (0[,]1)))
3332ssopab2i 5205 . . . . . . . . . . . . . . . . 17 {⟨𝑟, 𝑡⟩ ∣ (𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀))} ⊆ {⟨𝑟, 𝑡⟩ ∣ (𝑟 ∈ (0[,]1) ∧ 𝑡 ∈ (0[,]1))}
34 cvmlift2.s . . . . . . . . . . . . . . . . 17 𝑆 = {⟨𝑟, 𝑡⟩ ∣ (𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀))}
35 df-xp 5324 . . . . . . . . . . . . . . . . 17 ((0[,]1) × (0[,]1)) = {⟨𝑟, 𝑡⟩ ∣ (𝑟 ∈ (0[,]1) ∧ 𝑡 ∈ (0[,]1))}
3633, 34, 353sstr4i 3848 . . . . . . . . . . . . . . . 16 𝑆 ⊆ ((0[,]1) × (0[,]1))
3720, 20, 14, 14txunii 21614 . . . . . . . . . . . . . . . . 17 ((0[,]1) × (0[,]1)) = (II ×t II)
3837ntropn 21071 . . . . . . . . . . . . . . . 16 (((II ×t II) ∈ Top ∧ 𝑆 ⊆ ((0[,]1) × (0[,]1))) → ((int‘(II ×t II))‘𝑆) ∈ (II ×t II))
3922, 36, 38mp2an 675 . . . . . . . . . . . . . . 15 ((int‘(II ×t II))‘𝑆) ∈ (II ×t II)
4039a1i 11 . . . . . . . . . . . . . 14 ((𝜑𝑎 ∈ (0[,]1)) → ((int‘(II ×t II))‘𝑆) ∈ (II ×t II))
412adantr 468 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) → 𝐹 ∈ (𝐶 CovMap 𝐽))
423adantr 468 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) → 𝐺 ∈ ((II ×t II) Cn 𝐽))
434adantr 468 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) → 𝑃𝐵)
445adantr 468 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) → (𝐹𝑃) = (0𝐺0))
45 eqid 2813 . . . . . . . . . . . . . . . . . . . 20 (𝑘𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ ( 𝑠 = (𝐹𝑘) ∧ ∀𝑐𝑠 (∀𝑑 ∈ (𝑠 ∖ {𝑐})(𝑐𝑑) = ∅ ∧ (𝐹𝑐) ∈ ((𝐶t 𝑐)Homeo(𝐽t 𝑘))))}) = (𝑘𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ ( 𝑠 = (𝐹𝑘) ∧ ∀𝑐𝑠 (∀𝑑 ∈ (𝑠 ∖ {𝑐})(𝑐𝑑) = ∅ ∧ (𝐹𝑐) ∈ ((𝐶t 𝑐)Homeo(𝐽t 𝑘))))})
46 simprr 780 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) → 𝑏 ∈ (0[,]1))
47 simprl 778 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) → 𝑎 ∈ (0[,]1))
481, 41, 42, 43, 44, 6, 7, 45, 46, 47cvmlift2lem10 31622 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) → ∃𝑢 ∈ II ∃𝑣 ∈ II (𝑏𝑢𝑎𝑣 ∧ (∃𝑤𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II) ↾t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II) ↾t (𝑢 × 𝑣)) Cn 𝐶))))
4922a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏𝑢𝑎𝑣 ∧ (∃𝑤𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II) ↾t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II) ↾t (𝑢 × 𝑣)) Cn 𝐶)))) → (II ×t II) ∈ Top)
5036a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏𝑢𝑎𝑣 ∧ (∃𝑤𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II) ↾t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II) ↾t (𝑢 × 𝑣)) Cn 𝐶)))) → 𝑆 ⊆ ((0[,]1) × (0[,]1)))
5120a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏𝑢𝑎𝑣 ∧ (∃𝑤𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II) ↾t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II) ↾t (𝑢 × 𝑣)) Cn 𝐶)))) → II ∈ Top)
52 simplrl 786 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏𝑢𝑎𝑣 ∧ (∃𝑤𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II) ↾t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II) ↾t (𝑢 × 𝑣)) Cn 𝐶)))) → 𝑢 ∈ II)
53 simplrr 787 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏𝑢𝑎𝑣 ∧ (∃𝑤𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II) ↾t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II) ↾t (𝑢 × 𝑣)) Cn 𝐶)))) → 𝑣 ∈ II)
54 txopn 21623 . . . . . . . . . . . . . . . . . . . . . . . 24 (((II ∈ Top ∧ II ∈ Top) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) → (𝑢 × 𝑣) ∈ (II ×t II))
5551, 51, 52, 53, 54syl22anc 858 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏𝑢𝑎𝑣 ∧ (∃𝑤𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II) ↾t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II) ↾t (𝑢 × 𝑣)) Cn 𝐶)))) → (𝑢 × 𝑣) ∈ (II ×t II))
56 simpr 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑟𝑢𝑡𝑣) → 𝑡𝑣)
57 elunii 4642 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑡𝑣𝑣 ∈ II) → 𝑡 II)
5857, 14syl6eleqr 2903 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑡𝑣𝑣 ∈ II) → 𝑡 ∈ (0[,]1))
5956, 53, 58syl2anr 586 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏𝑢𝑎𝑣 ∧ (∃𝑤𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II) ↾t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II) ↾t (𝑢 × 𝑣)) Cn 𝐶)))) ∧ (𝑟𝑢𝑡𝑣)) → 𝑡 ∈ (0[,]1))
6020a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏𝑢𝑎𝑣 ∧ (∃𝑤𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II) ↾t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II) ↾t (𝑢 × 𝑣)) Cn 𝐶)))) ∧ (𝑟𝑢𝑡𝑣)) → II ∈ Top)
6152adantr 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏𝑢𝑎𝑣 ∧ (∃𝑤𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II) ↾t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II) ↾t (𝑢 × 𝑣)) Cn 𝐶)))) ∧ (𝑟𝑢𝑡𝑣)) → 𝑢 ∈ II)
62 simprl 778 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏𝑢𝑎𝑣 ∧ (∃𝑤𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II) ↾t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II) ↾t (𝑢 × 𝑣)) Cn 𝐶)))) ∧ (𝑟𝑢𝑡𝑣)) → 𝑟𝑢)
63 opnneip 21141 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((II ∈ Top ∧ 𝑢 ∈ II ∧ 𝑟𝑢) → 𝑢 ∈ ((nei‘II)‘{𝑟}))
6460, 61, 62, 63syl3anc 1483 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏𝑢𝑎𝑣 ∧ (∃𝑤𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II) ↾t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II) ↾t (𝑢 × 𝑣)) Cn 𝐶)))) ∧ (𝑟𝑢𝑡𝑣)) → 𝑢 ∈ ((nei‘II)‘{𝑟}))
6541ad3antrrr 712 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏𝑢𝑎𝑣 ∧ (∃𝑤𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II) ↾t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II) ↾t (𝑢 × 𝑣)) Cn 𝐶)))) ∧ (𝑟𝑢𝑡𝑣)) → 𝐹 ∈ (𝐶 CovMap 𝐽))
6642ad3antrrr 712 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏𝑢𝑎𝑣 ∧ (∃𝑤𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II) ↾t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II) ↾t (𝑢 × 𝑣)) Cn 𝐶)))) ∧ (𝑟𝑢𝑡𝑣)) → 𝐺 ∈ ((II ×t II) Cn 𝐽))
6743ad3antrrr 712 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏𝑢𝑎𝑣 ∧ (∃𝑤𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II) ↾t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II) ↾t (𝑢 × 𝑣)) Cn 𝐶)))) ∧ (𝑟𝑢𝑡𝑣)) → 𝑃𝐵)
6844ad3antrrr 712 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏𝑢𝑎𝑣 ∧ (∃𝑤𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II) ↾t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II) ↾t (𝑢 × 𝑣)) Cn 𝐶)))) ∧ (𝑟𝑢𝑡𝑣)) → (𝐹𝑃) = (0𝐺0))
69 cvmlift2.m . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 𝑀 = {𝑧 ∈ ((0[,]1) × (0[,]1)) ∣ 𝐾 ∈ (((II ×t II) CnP 𝐶)‘𝑧)}
7053adantr 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏𝑢𝑎𝑣 ∧ (∃𝑤𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II) ↾t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II) ↾t (𝑢 × 𝑣)) Cn 𝐶)))) ∧ (𝑟𝑢𝑡𝑣)) → 𝑣 ∈ II)
71 simplr2 1270 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏𝑢𝑎𝑣 ∧ (∃𝑤𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II) ↾t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II) ↾t (𝑢 × 𝑣)) Cn 𝐶)))) ∧ (𝑟𝑢𝑡𝑣)) → 𝑎𝑣)
72 simprr 780 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏𝑢𝑎𝑣 ∧ (∃𝑤𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II) ↾t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II) ↾t (𝑢 × 𝑣)) Cn 𝐶)))) ∧ (𝑟𝑢𝑡𝑣)) → 𝑡𝑣)
73 sneq 4387 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑐 = 𝑤 → {𝑐} = {𝑤})
7473xpeq2d 5347 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑐 = 𝑤 → (𝑢 × {𝑐}) = (𝑢 × {𝑤}))
7574reseq2d 5604 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑐 = 𝑤 → (𝐾 ↾ (𝑢 × {𝑐})) = (𝐾 ↾ (𝑢 × {𝑤})))
7674oveq2d 6893 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑐 = 𝑤 → ((II ×t II) ↾t (𝑢 × {𝑐})) = ((II ×t II) ↾t (𝑢 × {𝑤})))
7776oveq1d 6892 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑐 = 𝑤 → (((II ×t II) ↾t (𝑢 × {𝑐})) Cn 𝐶) = (((II ×t II) ↾t (𝑢 × {𝑤})) Cn 𝐶))
7875, 77eleq12d 2886 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑐 = 𝑤 → ((𝐾 ↾ (𝑢 × {𝑐})) ∈ (((II ×t II) ↾t (𝑢 × {𝑐})) Cn 𝐶) ↔ (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II) ↾t (𝑢 × {𝑤})) Cn 𝐶)))
7978cbvrexv 3368 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (∃𝑐𝑣 (𝐾 ↾ (𝑢 × {𝑐})) ∈ (((II ×t II) ↾t (𝑢 × {𝑐})) Cn 𝐶) ↔ ∃𝑤𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II) ↾t (𝑢 × {𝑤})) Cn 𝐶))
80 simplr3 1272 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 𝐶)))
8179, 80syl5bi 233 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 𝐶)))
821, 65, 66, 67, 68, 6, 7, 69, 61, 70, 71, 72, 81cvmlift2lem11 31623 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏𝑢𝑎𝑣 ∧ (∃𝑤𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II) ↾t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II) ↾t (𝑢 × 𝑣)) Cn 𝐶)))) ∧ (𝑟𝑢𝑡𝑣)) → ((𝑢 × {𝑎}) ⊆ 𝑀 → (𝑢 × {𝑡}) ⊆ 𝑀))
831, 65, 66, 67, 68, 6, 7, 69, 61, 70, 72, 71, 81cvmlift2lem11 31623 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏𝑢𝑎𝑣 ∧ (∃𝑤𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II) ↾t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II) ↾t (𝑢 × 𝑣)) Cn 𝐶)))) ∧ (𝑟𝑢𝑡𝑣)) → ((𝑢 × {𝑡}) ⊆ 𝑀 → (𝑢 × {𝑎}) ⊆ 𝑀))
8482, 83impbid 203 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏𝑢𝑎𝑣 ∧ (∃𝑤𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II) ↾t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II) ↾t (𝑢 × 𝑣)) Cn 𝐶)))) ∧ (𝑟𝑢𝑡𝑣)) → ((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀))
85 rspe 3197 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑢 ∈ ((nei‘II)‘{𝑟}) ∧ ((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀)) → ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀))
8664, 84, 85syl2anc 575 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏𝑢𝑎𝑣 ∧ (∃𝑤𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II) ↾t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II) ↾t (𝑢 × 𝑣)) Cn 𝐶)))) ∧ (𝑟𝑢𝑡𝑣)) → ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀))
8759, 86jca 503 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏𝑢𝑎𝑣 ∧ (∃𝑤𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II) ↾t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II) ↾t (𝑢 × 𝑣)) Cn 𝐶)))) ∧ (𝑟𝑢𝑡𝑣)) → (𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀)))
8887ex 399 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏𝑢𝑎𝑣 ∧ (∃𝑤𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II) ↾t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II) ↾t (𝑢 × 𝑣)) Cn 𝐶)))) → ((𝑟𝑢𝑡𝑣) → (𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀))))
8988alrimivv 2019 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏𝑢𝑎𝑣 ∧ (∃𝑤𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II) ↾t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II) ↾t (𝑢 × 𝑣)) Cn 𝐶)))) → ∀𝑟𝑡((𝑟𝑢𝑡𝑣) → (𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀))))
90 df-xp 5324 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑢 × 𝑣) = {⟨𝑟, 𝑡⟩ ∣ (𝑟𝑢𝑡𝑣)}
9190, 34sseq12i 3835 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑢 × 𝑣) ⊆ 𝑆 ↔ {⟨𝑟, 𝑡⟩ ∣ (𝑟𝑢𝑡𝑣)} ⊆ {⟨𝑟, 𝑡⟩ ∣ (𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀))})
92 ssopab2b 5204 . . . . . . . . . . . . . . . . . . . . . . . . 25 ({⟨𝑟, 𝑡⟩ ∣ (𝑟𝑢𝑡𝑣)} ⊆ {⟨𝑟, 𝑡⟩ ∣ (𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀))} ↔ ∀𝑟𝑡((𝑟𝑢𝑡𝑣) → (𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀))))
9391, 92bitri 266 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑢 × 𝑣) ⊆ 𝑆 ↔ ∀𝑟𝑡((𝑟𝑢𝑡𝑣) → (𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀))))
9489, 93sylibr 225 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏𝑢𝑎𝑣 ∧ (∃𝑤𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II) ↾t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II) ↾t (𝑢 × 𝑣)) Cn 𝐶)))) → (𝑢 × 𝑣) ⊆ 𝑆)
9537ssntr 21080 . . . . . . . . . . . . . . . . . . . . . . 23 ((((II ×t II) ∈ Top ∧ 𝑆 ⊆ ((0[,]1) × (0[,]1))) ∧ ((𝑢 × 𝑣) ∈ (II ×t II) ∧ (𝑢 × 𝑣) ⊆ 𝑆)) → (𝑢 × 𝑣) ⊆ ((int‘(II ×t II))‘𝑆))
9649, 50, 55, 94, 95syl22anc 858 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏𝑢𝑎𝑣 ∧ (∃𝑤𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II) ↾t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II) ↾t (𝑢 × 𝑣)) Cn 𝐶)))) → (𝑢 × 𝑣) ⊆ ((int‘(II ×t II))‘𝑆))
97 simpr1 1241 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏𝑢𝑎𝑣 ∧ (∃𝑤𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II) ↾t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II) ↾t (𝑢 × 𝑣)) Cn 𝐶)))) → 𝑏𝑢)
98 simpr2 1243 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏𝑢𝑎𝑣 ∧ (∃𝑤𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II) ↾t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II) ↾t (𝑢 × 𝑣)) Cn 𝐶)))) → 𝑎𝑣)
99 opelxpi 5355 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑏𝑢𝑎𝑣) → ⟨𝑏, 𝑎⟩ ∈ (𝑢 × 𝑣))
10097, 98, 99syl2anc 575 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏𝑢𝑎𝑣 ∧ (∃𝑤𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II) ↾t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II) ↾t (𝑢 × 𝑣)) Cn 𝐶)))) → ⟨𝑏, 𝑎⟩ ∈ (𝑢 × 𝑣))
10196, 100sseldd 3806 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏𝑢𝑎𝑣 ∧ (∃𝑤𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II) ↾t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II) ↾t (𝑢 × 𝑣)) Cn 𝐶)))) → ⟨𝑏, 𝑎⟩ ∈ ((int‘(II ×t II))‘𝑆))
102101ex 399 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) → ((𝑏𝑢𝑎𝑣 ∧ (∃𝑤𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II) ↾t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II) ↾t (𝑢 × 𝑣)) Cn 𝐶))) → ⟨𝑏, 𝑎⟩ ∈ ((int‘(II ×t II))‘𝑆)))
103102rexlimdvva 3233 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) → (∃𝑢 ∈ II ∃𝑣 ∈ II (𝑏𝑢𝑎𝑣 ∧ (∃𝑤𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II) ↾t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II) ↾t (𝑢 × 𝑣)) Cn 𝐶))) → ⟨𝑏, 𝑎⟩ ∈ ((int‘(II ×t II))‘𝑆)))
10448, 103mpd 15 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) → ⟨𝑏, 𝑎⟩ ∈ ((int‘(II ×t II))‘𝑆))
105 vex 3401 . . . . . . . . . . . . . . . . . . 19 𝑎 ∈ V
106 opeq2 4603 . . . . . . . . . . . . . . . . . . . 20 (𝑤 = 𝑎 → ⟨𝑏, 𝑤⟩ = ⟨𝑏, 𝑎⟩)
107106eleq1d 2877 . . . . . . . . . . . . . . . . . . 19 (𝑤 = 𝑎 → (⟨𝑏, 𝑤⟩ ∈ ((int‘(II ×t II))‘𝑆) ↔ ⟨𝑏, 𝑎⟩ ∈ ((int‘(II ×t II))‘𝑆)))
108105, 107ralsn 4422 . . . . . . . . . . . . . . . . . 18 (∀𝑤 ∈ {𝑎}⟨𝑏, 𝑤⟩ ∈ ((int‘(II ×t II))‘𝑆) ↔ ⟨𝑏, 𝑎⟩ ∈ ((int‘(II ×t II))‘𝑆))
109104, 108sylibr 225 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) → ∀𝑤 ∈ {𝑎}⟨𝑏, 𝑤⟩ ∈ ((int‘(II ×t II))‘𝑆))
110109anassrs 455 . . . . . . . . . . . . . . . 16 (((𝜑𝑎 ∈ (0[,]1)) ∧ 𝑏 ∈ (0[,]1)) → ∀𝑤 ∈ {𝑎}⟨𝑏, 𝑤⟩ ∈ ((int‘(II ×t II))‘𝑆))
111110ralrimiva 3161 . . . . . . . . . . . . . . 15 ((𝜑𝑎 ∈ (0[,]1)) → ∀𝑏 ∈ (0[,]1)∀𝑤 ∈ {𝑎}⟨𝑏, 𝑤⟩ ∈ ((int‘(II ×t II))‘𝑆))
112 dfss3 3794 . . . . . . . . . . . . . . . 16 (((0[,]1) × {𝑎}) ⊆ ((int‘(II ×t II))‘𝑆) ↔ ∀𝑢 ∈ ((0[,]1) × {𝑎})𝑢 ∈ ((int‘(II ×t II))‘𝑆))
113 eleq1 2880 . . . . . . . . . . . . . . . . 17 (𝑢 = ⟨𝑏, 𝑤⟩ → (𝑢 ∈ ((int‘(II ×t II))‘𝑆) ↔ ⟨𝑏, 𝑤⟩ ∈ ((int‘(II ×t II))‘𝑆)))
114113ralxp 5472 . . . . . . . . . . . . . . . 16 (∀𝑢 ∈ ((0[,]1) × {𝑎})𝑢 ∈ ((int‘(II ×t II))‘𝑆) ↔ ∀𝑏 ∈ (0[,]1)∀𝑤 ∈ {𝑎}⟨𝑏, 𝑤⟩ ∈ ((int‘(II ×t II))‘𝑆))
115112, 114bitri 266 . . . . . . . . . . . . . . 15 (((0[,]1) × {𝑎}) ⊆ ((int‘(II ×t II))‘𝑆) ↔ ∀𝑏 ∈ (0[,]1)∀𝑤 ∈ {𝑎}⟨𝑏, 𝑤⟩ ∈ ((int‘(II ×t II))‘𝑆))
116111, 115sylibr 225 . . . . . . . . . . . . . 14 ((𝜑𝑎 ∈ (0[,]1)) → ((0[,]1) × {𝑎}) ⊆ ((int‘(II ×t II))‘𝑆))
117 simpr 473 . . . . . . . . . . . . . 14 ((𝜑𝑎 ∈ (0[,]1)) → 𝑎 ∈ (0[,]1))
11814, 14, 19, 21, 40, 116, 117txtube 21661 . . . . . . . . . . . . 13 ((𝜑𝑎 ∈ (0[,]1)) → ∃𝑣 ∈ II (𝑎𝑣 ∧ ((0[,]1) × 𝑣) ⊆ ((int‘(II ×t II))‘𝑆)))
11937ntrss2 21079 . . . . . . . . . . . . . . . . . . 19 (((II ×t II) ∈ Top ∧ 𝑆 ⊆ ((0[,]1) × (0[,]1))) → ((int‘(II ×t II))‘𝑆) ⊆ 𝑆)
12022, 36, 119mp2an 675 . . . . . . . . . . . . . . . . . 18 ((int‘(II ×t II))‘𝑆) ⊆ 𝑆
121 sstr 3813 . . . . . . . . . . . . . . . . . 18 ((((0[,]1) × 𝑣) ⊆ ((int‘(II ×t II))‘𝑆) ∧ ((int‘(II ×t II))‘𝑆) ⊆ 𝑆) → ((0[,]1) × 𝑣) ⊆ 𝑆)
122120, 121mpan2 674 . . . . . . . . . . . . . . . . 17 (((0[,]1) × 𝑣) ⊆ ((int‘(II ×t II))‘𝑆) → ((0[,]1) × 𝑣) ⊆ 𝑆)
123 df-xp 5324 . . . . . . . . . . . . . . . . . . 19 ((0[,]1) × 𝑣) = {⟨𝑟, 𝑡⟩ ∣ (𝑟 ∈ (0[,]1) ∧ 𝑡𝑣)}
124123, 34sseq12i 3835 . . . . . . . . . . . . . . . . . 18 (((0[,]1) × 𝑣) ⊆ 𝑆 ↔ {⟨𝑟, 𝑡⟩ ∣ (𝑟 ∈ (0[,]1) ∧ 𝑡𝑣)} ⊆ {⟨𝑟, 𝑡⟩ ∣ (𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀))})
125 ssopab2b 5204 . . . . . . . . . . . . . . . . . . 19 ({⟨𝑟, 𝑡⟩ ∣ (𝑟 ∈ (0[,]1) ∧ 𝑡𝑣)} ⊆ {⟨𝑟, 𝑡⟩ ∣ (𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀))} ↔ ∀𝑟𝑡((𝑟 ∈ (0[,]1) ∧ 𝑡𝑣) → (𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀))))
126 r2al 3134 . . . . . . . . . . . . . . . . . . 19 (∀𝑟 ∈ (0[,]1)∀𝑡𝑣 (𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀)) ↔ ∀𝑟𝑡((𝑟 ∈ (0[,]1) ∧ 𝑡𝑣) → (𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀))))
127 ralcom 3293 . . . . . . . . . . . . . . . . . . 19 (∀𝑟 ∈ (0[,]1)∀𝑡𝑣 (𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀)) ↔ ∀𝑡𝑣𝑟 ∈ (0[,]1)(𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀)))
128125, 126, 1273bitr2i 290 . . . . . . . . . . . . . . . . . 18 ({⟨𝑟, 𝑡⟩ ∣ (𝑟 ∈ (0[,]1) ∧ 𝑡𝑣)} ⊆ {⟨𝑟, 𝑡⟩ ∣ (𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀))} ↔ ∀𝑡𝑣𝑟 ∈ (0[,]1)(𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀)))
129124, 128bitri 266 . . . . . . . . . . . . . . . . 17 (((0[,]1) × 𝑣) ⊆ 𝑆 ↔ ∀𝑡𝑣𝑟 ∈ (0[,]1)(𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀)))
130122, 129sylib 209 . . . . . . . . . . . . . . . 16 (((0[,]1) × 𝑣) ⊆ ((int‘(II ×t II))‘𝑆) → ∀𝑡𝑣𝑟 ∈ (0[,]1)(𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀)))
131 simpr 473 . . . . . . . . . . . . . . . . . . . 20 ((𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀)) → ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀))
132131ralimi 3147 . . . . . . . . . . . . . . . . . . 19 (∀𝑟 ∈ (0[,]1)(𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀)) → ∀𝑟 ∈ (0[,]1)∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀))
133 cvmlift2lem1 31612 . . . . . . . . . . . . . . . . . . . 20 (∀𝑟 ∈ (0[,]1)∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀) → (((0[,]1) × {𝑎}) ⊆ 𝑀 → ((0[,]1) × {𝑡}) ⊆ 𝑀))
134 bicom 213 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀) ↔ ((𝑢 × {𝑡}) ⊆ 𝑀 ↔ (𝑢 × {𝑎}) ⊆ 𝑀))
135134rexbii 3236 . . . . . . . . . . . . . . . . . . . . . 22 (∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀) ↔ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑡}) ⊆ 𝑀 ↔ (𝑢 × {𝑎}) ⊆ 𝑀))
136135ralbii 3175 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑟 ∈ (0[,]1)∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀) ↔ ∀𝑟 ∈ (0[,]1)∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑡}) ⊆ 𝑀 ↔ (𝑢 × {𝑎}) ⊆ 𝑀))
137 cvmlift2lem1 31612 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑟 ∈ (0[,]1)∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑡}) ⊆ 𝑀 ↔ (𝑢 × {𝑎}) ⊆ 𝑀) → (((0[,]1) × {𝑡}) ⊆ 𝑀 → ((0[,]1) × {𝑎}) ⊆ 𝑀))
138136, 137sylbi 208 . . . . . . . . . . . . . . . . . . . 20 (∀𝑟 ∈ (0[,]1)∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀) → (((0[,]1) × {𝑡}) ⊆ 𝑀 → ((0[,]1) × {𝑎}) ⊆ 𝑀))
139133, 138impbid 203 . . . . . . . . . . . . . . . . . . 19 (∀𝑟 ∈ (0[,]1)∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀) → (((0[,]1) × {𝑎}) ⊆ 𝑀 ↔ ((0[,]1) × {𝑡}) ⊆ 𝑀))
140132, 139syl 17 . . . . . . . . . . . . . . . . . 18 (∀𝑟 ∈ (0[,]1)(𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀)) → (((0[,]1) × {𝑎}) ⊆ 𝑀 ↔ ((0[,]1) × {𝑡}) ⊆ 𝑀))
14113rabeq2i 3394 . . . . . . . . . . . . . . . . . . . . 21 (𝑎𝐴 ↔ (𝑎 ∈ (0[,]1) ∧ ((0[,]1) × {𝑎}) ⊆ 𝑀))
142141baib 527 . . . . . . . . . . . . . . . . . . . 20 (𝑎 ∈ (0[,]1) → (𝑎𝐴 ↔ ((0[,]1) × {𝑎}) ⊆ 𝑀))
143142ad3antlr 713 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑎 ∈ (0[,]1)) ∧ 𝑣 ∈ II) ∧ 𝑡𝑣) → (𝑎𝐴 ↔ ((0[,]1) × {𝑎}) ⊆ 𝑀))
144 elssuni 4668 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑣 ∈ II → 𝑣 II)
145144, 14syl6sseqr 3856 . . . . . . . . . . . . . . . . . . . . . 22 (𝑣 ∈ II → 𝑣 ⊆ (0[,]1))
146145adantl 469 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑎 ∈ (0[,]1)) ∧ 𝑣 ∈ II) → 𝑣 ⊆ (0[,]1))
147146sselda 3805 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑎 ∈ (0[,]1)) ∧ 𝑣 ∈ II) ∧ 𝑡𝑣) → 𝑡 ∈ (0[,]1))
148 sneq 4387 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑎 = 𝑡 → {𝑎} = {𝑡})
149148xpeq2d 5347 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑎 = 𝑡 → ((0[,]1) × {𝑎}) = ((0[,]1) × {𝑡}))
150149sseq1d 3836 . . . . . . . . . . . . . . . . . . . . . 22 (𝑎 = 𝑡 → (((0[,]1) × {𝑎}) ⊆ 𝑀 ↔ ((0[,]1) × {𝑡}) ⊆ 𝑀))
151150, 13elrab2 3569 . . . . . . . . . . . . . . . . . . . . 21 (𝑡𝐴 ↔ (𝑡 ∈ (0[,]1) ∧ ((0[,]1) × {𝑡}) ⊆ 𝑀))
152151baib 527 . . . . . . . . . . . . . . . . . . . 20 (𝑡 ∈ (0[,]1) → (𝑡𝐴 ↔ ((0[,]1) × {𝑡}) ⊆ 𝑀))
153147, 152syl 17 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑎 ∈ (0[,]1)) ∧ 𝑣 ∈ II) ∧ 𝑡𝑣) → (𝑡𝐴 ↔ ((0[,]1) × {𝑡}) ⊆ 𝑀))
154143, 153bibi12d 336 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑎 ∈ (0[,]1)) ∧ 𝑣 ∈ II) ∧ 𝑡𝑣) → ((𝑎𝐴𝑡𝐴) ↔ (((0[,]1) × {𝑎}) ⊆ 𝑀 ↔ ((0[,]1) × {𝑡}) ⊆ 𝑀)))
155140, 154syl5ibr 237 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑎 ∈ (0[,]1)) ∧ 𝑣 ∈ II) ∧ 𝑡𝑣) → (∀𝑟 ∈ (0[,]1)(𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀)) → (𝑎𝐴𝑡𝐴)))
156155ralimdva 3157 . . . . . . . . . . . . . . . 16 (((𝜑𝑎 ∈ (0[,]1)) ∧ 𝑣 ∈ II) → (∀𝑡𝑣𝑟 ∈ (0[,]1)(𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀)) → ∀𝑡𝑣 (𝑎𝐴𝑡𝐴)))
157130, 156syl5 34 . . . . . . . . . . . . . . 15 (((𝜑𝑎 ∈ (0[,]1)) ∧ 𝑣 ∈ II) → (((0[,]1) × 𝑣) ⊆ ((int‘(II ×t II))‘𝑆) → ∀𝑡𝑣 (𝑎𝐴𝑡𝐴)))
158157anim2d 601 . . . . . . . . . . . . . 14 (((𝜑𝑎 ∈ (0[,]1)) ∧ 𝑣 ∈ II) → ((𝑎𝑣 ∧ ((0[,]1) × 𝑣) ⊆ ((int‘(II ×t II))‘𝑆)) → (𝑎𝑣 ∧ ∀𝑡𝑣 (𝑎𝐴𝑡𝐴))))
159158reximdva 3211 . . . . . . . . . . . . 13 ((𝜑𝑎 ∈ (0[,]1)) → (∃𝑣 ∈ II (𝑎𝑣 ∧ ((0[,]1) × 𝑣) ⊆ ((int‘(II ×t II))‘𝑆)) → ∃𝑣 ∈ II (𝑎𝑣 ∧ ∀𝑡𝑣 (𝑎𝐴𝑡𝐴))))
160118, 159mpd 15 . . . . . . . . . . . 12 ((𝜑𝑎 ∈ (0[,]1)) → ∃𝑣 ∈ II (𝑎𝑣 ∧ ∀𝑡𝑣 (𝑎𝐴𝑡𝐴)))
161160ralrimiva 3161 . . . . . . . . . . 11 (𝜑 → ∀𝑎 ∈ (0[,]1)∃𝑣 ∈ II (𝑎𝑣 ∧ ∀𝑡𝑣 (𝑎𝐴𝑡𝐴)))
162 ssrab2 3891 . . . . . . . . . . . . 13 {𝑎 ∈ (0[,]1) ∣ ((0[,]1) × {𝑎}) ⊆ 𝑀} ⊆ (0[,]1)
16313, 162eqsstri 3839 . . . . . . . . . . . 12 𝐴 ⊆ (0[,]1)
16414isclo 21109 . . . . . . . . . . . 12 ((II ∈ Top ∧ 𝐴 ⊆ (0[,]1)) → (𝐴 ∈ (II ∩ (Clsd‘II)) ↔ ∀𝑎 ∈ (0[,]1)∃𝑣 ∈ II (𝑎𝑣 ∧ ∀𝑡𝑣 (𝑎𝐴𝑡𝐴))))
16520, 163, 164mp2an 675 . . . . . . . . . . 11 (𝐴 ∈ (II ∩ (Clsd‘II)) ↔ ∀𝑎 ∈ (0[,]1)∃𝑣 ∈ II (𝑎𝑣 ∧ ∀𝑡𝑣 (𝑎𝐴𝑡𝐴)))
166161, 165sylibr 225 . . . . . . . . . 10 (𝜑𝐴 ∈ (II ∩ (Clsd‘II)))
16717, 166sseldi 3803 . . . . . . . . 9 (𝜑𝐴 ∈ II)
168 0elunit 12514 . . . . . . . . . . . 12 0 ∈ (0[,]1)
169168a1i 11 . . . . . . . . . . 11 (𝜑 → 0 ∈ (0[,]1))
170 relxp 5335 . . . . . . . . . . . . 13 Rel ((0[,]1) × {0})
171170a1i 11 . . . . . . . . . . . 12 (𝜑 → Rel ((0[,]1) × {0}))
172 opelxp 5353 . . . . . . . . . . . . 13 (⟨𝑟, 𝑎⟩ ∈ ((0[,]1) × {0}) ↔ (𝑟 ∈ (0[,]1) ∧ 𝑎 ∈ {0}))
173 id 22 . . . . . . . . . . . . . . . . 17 (𝑟 ∈ (0[,]1) → 𝑟 ∈ (0[,]1))
174 opelxpi 5355 . . . . . . . . . . . . . . . . 17 ((𝑟 ∈ (0[,]1) ∧ 0 ∈ (0[,]1)) → ⟨𝑟, 0⟩ ∈ ((0[,]1) × (0[,]1)))
175173, 169, 174syl2anr 586 . . . . . . . . . . . . . . . 16 ((𝜑𝑟 ∈ (0[,]1)) → ⟨𝑟, 0⟩ ∈ ((0[,]1) × (0[,]1)))
1762adantr 468 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑟 ∈ (0[,]1)) → 𝐹 ∈ (𝐶 CovMap 𝐽))
1773adantr 468 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑟 ∈ (0[,]1)) → 𝐺 ∈ ((II ×t II) Cn 𝐽))
1784adantr 468 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑟 ∈ (0[,]1)) → 𝑃𝐵)
1795adantr 468 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑟 ∈ (0[,]1)) → (𝐹𝑃) = (0𝐺0))
180 simpr 473 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑟 ∈ (0[,]1)) → 𝑟 ∈ (0[,]1))
181168a1i 11 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑟 ∈ (0[,]1)) → 0 ∈ (0[,]1))
1821, 176, 177, 178, 179, 6, 7, 45, 180, 181cvmlift2lem10 31622 . . . . . . . . . . . . . . . . 17 ((𝜑𝑟 ∈ (0[,]1)) → ∃𝑢 ∈ II ∃𝑣 ∈ II (𝑟𝑢 ∧ 0 ∈ 𝑣 ∧ (∃𝑤𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II) ↾t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II) ↾t (𝑢 × 𝑣)) Cn 𝐶))))
183 df-3an 1102 . . . . . . . . . . . . . . . . . . 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 780 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟𝑢 ∧ 0 ∈ 𝑣)) → 0 ∈ 𝑣)
1858ad3antrrr 712 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟𝑢 ∧ 0 ∈ 𝑣)) → 𝐾:((0[,]1) × (0[,]1))⟶𝐵)
186185ffnd 6260 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟𝑢 ∧ 0 ∈ 𝑣)) → 𝐾 Fn ((0[,]1) × (0[,]1)))
187 fnov 7001 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝐾 Fn ((0[,]1) × (0[,]1)) ↔ 𝐾 = (𝑏 ∈ (0[,]1), 𝑤 ∈ (0[,]1) ↦ (𝑏𝐾𝑤)))
188186, 187sylib 209 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟𝑢 ∧ 0 ∈ 𝑣)) → 𝐾 = (𝑏 ∈ (0[,]1), 𝑤 ∈ (0[,]1) ↦ (𝑏𝐾𝑤)))
189188reseq1d 5603 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟𝑢 ∧ 0 ∈ 𝑣)) → (𝐾 ↾ (𝑢 × {0})) = ((𝑏 ∈ (0[,]1), 𝑤 ∈ (0[,]1) ↦ (𝑏𝐾𝑤)) ↾ (𝑢 × {0})))
190 simplrl 786 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟𝑢 ∧ 0 ∈ 𝑣)) → 𝑢 ∈ II)
191 elssuni 4668 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑢 ∈ II → 𝑢 II)
192191, 14syl6sseqr 3856 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑢 ∈ II → 𝑢 ⊆ (0[,]1))
193190, 192syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟𝑢 ∧ 0 ∈ 𝑣)) → 𝑢 ⊆ (0[,]1))
194169snssd 4537 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → {0} ⊆ (0[,]1))
195194ad3antrrr 712 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟𝑢 ∧ 0 ∈ 𝑣)) → {0} ⊆ (0[,]1))
196 resmpt2 6991 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑢 ⊆ (0[,]1) ∧ {0} ⊆ (0[,]1)) → ((𝑏 ∈ (0[,]1), 𝑤 ∈ (0[,]1) ↦ (𝑏𝐾𝑤)) ↾ (𝑢 × {0})) = (𝑏𝑢, 𝑤 ∈ {0} ↦ (𝑏𝐾𝑤)))
197193, 195, 196syl2anc 575 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟𝑢 ∧ 0 ∈ 𝑣)) → ((𝑏 ∈ (0[,]1), 𝑤 ∈ (0[,]1) ↦ (𝑏𝐾𝑤)) ↾ (𝑢 × {0})) = (𝑏𝑢, 𝑤 ∈ {0} ↦ (𝑏𝐾𝑤)))
198193sselda 3805 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((𝜑𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟𝑢 ∧ 0 ∈ 𝑣)) ∧ 𝑏𝑢) → 𝑏 ∈ (0[,]1))
199 simplll 782 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟𝑢 ∧ 0 ∈ 𝑣)) → 𝜑)
2001, 2, 3, 4, 5, 6, 7cvmlift2lem8 31620 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑏 ∈ (0[,]1)) → (𝑏𝐾0) = (𝐻𝑏))
201199, 200sylan 571 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((𝜑𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟𝑢 ∧ 0 ∈ 𝑣)) ∧ 𝑏 ∈ (0[,]1)) → (𝑏𝐾0) = (𝐻𝑏))
202198, 201syldan 581 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝜑𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟𝑢 ∧ 0 ∈ 𝑣)) ∧ 𝑏𝑢) → (𝑏𝐾0) = (𝐻𝑏))
203 elsni 4394 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑤 ∈ {0} → 𝑤 = 0)
204203oveq2d 6893 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑤 ∈ {0} → (𝑏𝐾𝑤) = (𝑏𝐾0))
205204eqeq1d 2815 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑤 ∈ {0} → ((𝑏𝐾𝑤) = (𝐻𝑏) ↔ (𝑏𝐾0) = (𝐻𝑏)))
206202, 205syl5ibrcom 238 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝜑𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟𝑢 ∧ 0 ∈ 𝑣)) ∧ 𝑏𝑢) → (𝑤 ∈ {0} → (𝑏𝐾𝑤) = (𝐻𝑏)))
2072063impia 1138 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟𝑢 ∧ 0 ∈ 𝑣)) ∧ 𝑏𝑢𝑤 ∈ {0}) → (𝑏𝐾𝑤) = (𝐻𝑏))
208207mpt2eq3dva 6952 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟𝑢 ∧ 0 ∈ 𝑣)) → (𝑏𝑢, 𝑤 ∈ {0} ↦ (𝑏𝐾𝑤)) = (𝑏𝑢, 𝑤 ∈ {0} ↦ (𝐻𝑏)))
209189, 197, 2083eqtrd 2851 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟𝑢 ∧ 0 ∈ 𝑣)) → (𝐾 ↾ (𝑢 × {0})) = (𝑏𝑢, 𝑤 ∈ {0} ↦ (𝐻𝑏)))
210 eqid 2813 . . . . . . . . . . . . . . . . . . . . . . . . 25 (II ↾t 𝑢) = (II ↾t 𝑢)
211 iitopon 22899 . . . . . . . . . . . . . . . . . . . . . . . . . 26 II ∈ (TopOn‘(0[,]1))
212211a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟𝑢 ∧ 0 ∈ 𝑣)) → II ∈ (TopOn‘(0[,]1)))
213 eqid 2813 . . . . . . . . . . . . . . . . . . . . . . . . 25 (II ↾t {0}) = (II ↾t {0})
214212, 212cnmpt1st 21689 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟𝑢 ∧ 0 ∈ 𝑣)) → (𝑏 ∈ (0[,]1), 𝑤 ∈ (0[,]1) ↦ 𝑏) ∈ ((II ×t II) Cn II))
2151, 2, 3, 4, 5, 6cvmlift2lem2 31614 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → (𝐻 ∈ (II Cn 𝐶) ∧ (𝐹𝐻) = (𝑧 ∈ (0[,]1) ↦ (𝑧𝐺0)) ∧ (𝐻‘0) = 𝑃))
216215simp1d 1165 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑𝐻 ∈ (II Cn 𝐶))
217199, 216syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟𝑢 ∧ 0 ∈ 𝑣)) → 𝐻 ∈ (II Cn 𝐶))
218212, 212, 214, 217cnmpt21f 21693 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟𝑢 ∧ 0 ∈ 𝑣)) → (𝑏 ∈ (0[,]1), 𝑤 ∈ (0[,]1) ↦ (𝐻𝑏)) ∈ ((II ×t II) Cn 𝐶))
219210, 212, 193, 213, 212, 195, 218cnmpt2res 21698 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟𝑢 ∧ 0 ∈ 𝑣)) → (𝑏𝑢, 𝑤 ∈ {0} ↦ (𝐻𝑏)) ∈ (((II ↾t 𝑢) ×t (II ↾t {0})) Cn 𝐶))
220 vex 3401 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑢 ∈ V
221 snex 5105 . . . . . . . . . . . . . . . . . . . . . . . . . 26 {0} ∈ V
222 txrest 21652 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((II ∈ Top ∧ II ∈ Top) ∧ (𝑢 ∈ V ∧ {0} ∈ V)) → ((II ×t II) ↾t (𝑢 × {0})) = ((II ↾t 𝑢) ×t (II ↾t {0})))
22320, 20, 220, 221, 222mp4an 676 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((II ×t II) ↾t (𝑢 × {0})) = ((II ↾t 𝑢) ×t (II ↾t {0}))
224223oveq1i 6887 . . . . . . . . . . . . . . . . . . . . . . . 24 (((II ×t II) ↾t (𝑢 × {0})) Cn 𝐶) = (((II ↾t 𝑢) ×t (II ↾t {0})) Cn 𝐶)
225219, 224syl6eleqr 2903 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟𝑢 ∧ 0 ∈ 𝑣)) → (𝑏𝑢, 𝑤 ∈ {0} ↦ (𝐻𝑏)) ∈ (((II ×t II) ↾t (𝑢 × {0})) Cn 𝐶))
226209, 225eqeltrd 2892 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟𝑢 ∧ 0 ∈ 𝑣)) → (𝐾 ↾ (𝑢 × {0})) ∈ (((II ×t II) ↾t (𝑢 × {0})) Cn 𝐶))
227 sneq 4387 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑤 = 0 → {𝑤} = {0})
228227xpeq2d 5347 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑤 = 0 → (𝑢 × {𝑤}) = (𝑢 × {0}))
229228reseq2d 5604 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑤 = 0 → (𝐾 ↾ (𝑢 × {𝑤})) = (𝐾 ↾ (𝑢 × {0})))
230228oveq2d 6893 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑤 = 0 → ((II ×t II) ↾t (𝑢 × {𝑤})) = ((II ×t II) ↾t (𝑢 × {0})))
231230oveq1d 6892 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑤 = 0 → (((II ×t II) ↾t (𝑢 × {𝑤})) Cn 𝐶) = (((II ×t II) ↾t (𝑢 × {0})) Cn 𝐶))
232229, 231eleq12d 2886 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑤 = 0 → ((𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II) ↾t (𝑢 × {𝑤})) Cn 𝐶) ↔ (𝐾 ↾ (𝑢 × {0})) ∈ (((II ×t II) ↾t (𝑢 × {0})) Cn 𝐶)))
233232rspcev 3509 . . . . . . . . . . . . . . . . . . . . . 22 ((0 ∈ 𝑣 ∧ (𝐾 ↾ (𝑢 × {0})) ∈ (((II ×t II) ↾t (𝑢 × {0})) Cn 𝐶)) → ∃𝑤𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II) ↾t (𝑢 × {𝑤})) Cn 𝐶))
234184, 226, 233syl2anc 575 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟𝑢 ∧ 0 ∈ 𝑣)) → ∃𝑤𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II) ↾t (𝑢 × {𝑤})) Cn 𝐶))
235 opelxpi 5355 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑟𝑢 ∧ 0 ∈ 𝑣) → ⟨𝑟, 0⟩ ∈ (𝑢 × 𝑣))
236235adantl 469 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟𝑢 ∧ 0 ∈ 𝑣)) → ⟨𝑟, 0⟩ ∈ (𝑢 × 𝑣))
237 simplrr 787 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟𝑢 ∧ 0 ∈ 𝑣)) → 𝑣 ∈ II)
238237, 145syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟𝑢 ∧ 0 ∈ 𝑣)) → 𝑣 ⊆ (0[,]1))
239 xpss12 5333 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑢 ⊆ (0[,]1) ∧ 𝑣 ⊆ (0[,]1)) → (𝑢 × 𝑣) ⊆ ((0[,]1) × (0[,]1)))
240193, 238, 239syl2anc 575 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟𝑢 ∧ 0 ∈ 𝑣)) → (𝑢 × 𝑣) ⊆ ((0[,]1) × (0[,]1)))
24137restuni 21184 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((II ×t II) ∈ Top ∧ (𝑢 × 𝑣) ⊆ ((0[,]1) × (0[,]1))) → (𝑢 × 𝑣) = ((II ×t II) ↾t (𝑢 × 𝑣)))
24222, 240, 241sylancr 577 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟𝑢 ∧ 0 ∈ 𝑣)) → (𝑢 × 𝑣) = ((II ×t II) ↾t (𝑢 × 𝑣)))
243236, 242eleqtrd 2894 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟𝑢 ∧ 0 ∈ 𝑣)) → ⟨𝑟, 0⟩ ∈ ((II ×t II) ↾t (𝑢 × 𝑣)))
244 eqid 2813 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((II ×t II) ↾t (𝑢 × 𝑣)) = ((II ×t II) ↾t (𝑢 × 𝑣))
245244cncnpi 21300 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II) ↾t (𝑢 × 𝑣)) Cn 𝐶) ∧ ⟨𝑟, 0⟩ ∈ ((II ×t II) ↾t (𝑢 × 𝑣))) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ ((((II ×t II) ↾t (𝑢 × 𝑣)) CnP 𝐶)‘⟨𝑟, 0⟩))
246245expcom 400 . . . . . . . . . . . . . . . . . . . . . . 23 (⟨𝑟, 0⟩ ∈ ((II ×t II) ↾t (𝑢 × 𝑣)) → ((𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II) ↾t (𝑢 × 𝑣)) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ ((((II ×t II) ↾t (𝑢 × 𝑣)) CnP 𝐶)‘⟨𝑟, 0⟩)))
247243, 246syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟𝑢 ∧ 0 ∈ 𝑣)) → ((𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II) ↾t (𝑢 × 𝑣)) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ ((((II ×t II) ↾t (𝑢 × 𝑣)) CnP 𝐶)‘⟨𝑟, 0⟩)))
24822a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟𝑢 ∧ 0 ∈ 𝑣)) → (II ×t II) ∈ Top)
24920a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟𝑢 ∧ 0 ∈ 𝑣)) → II ∈ Top)
250249, 249, 190, 237, 54syl22anc 858 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟𝑢 ∧ 0 ∈ 𝑣)) → (𝑢 × 𝑣) ∈ (II ×t II))
251 isopn3i 21104 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((II ×t II) ∈ Top ∧ (𝑢 × 𝑣) ∈ (II ×t II)) → ((int‘(II ×t II))‘(𝑢 × 𝑣)) = (𝑢 × 𝑣))
25222, 250, 251sylancr 577 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟𝑢 ∧ 0 ∈ 𝑣)) → ((int‘(II ×t II))‘(𝑢 × 𝑣)) = (𝑢 × 𝑣))
253236, 252eleqtrrd 2895 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟𝑢 ∧ 0 ∈ 𝑣)) → ⟨𝑟, 0⟩ ∈ ((int‘(II ×t II))‘(𝑢 × 𝑣)))
25437, 1cnprest 21311 . . . . . . . . . . . . . . . . . . . . . . 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⟩)))
255248, 240, 253, 185, 254syl22anc 858 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟𝑢 ∧ 0 ∈ 𝑣)) → (𝐾 ∈ (((II ×t II) CnP 𝐶)‘⟨𝑟, 0⟩) ↔ (𝐾 ↾ (𝑢 × 𝑣)) ∈ ((((II ×t II) ↾t (𝑢 × 𝑣)) CnP 𝐶)‘⟨𝑟, 0⟩)))
256247, 255sylibrd 250 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟𝑢 ∧ 0 ∈ 𝑣)) → ((𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II) ↾t (𝑢 × 𝑣)) Cn 𝐶) → 𝐾 ∈ (((II ×t II) CnP 𝐶)‘⟨𝑟, 0⟩)))
257234, 256embantd 59 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟𝑢 ∧ 0 ∈ 𝑣)) → ((∃𝑤𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II) ↾t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II) ↾t (𝑢 × 𝑣)) Cn 𝐶)) → 𝐾 ∈ (((II ×t II) CnP 𝐶)‘⟨𝑟, 0⟩)))
258257expimpd 443 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) → (((𝑟𝑢 ∧ 0 ∈ 𝑣) ∧ (∃𝑤𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II) ↾t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II) ↾t (𝑢 × 𝑣)) Cn 𝐶))) → 𝐾 ∈ (((II ×t II) CnP 𝐶)‘⟨𝑟, 0⟩)))
259183, 258syl5bi 233 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) → ((𝑟𝑢 ∧ 0 ∈ 𝑣 ∧ (∃𝑤𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II) ↾t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II) ↾t (𝑢 × 𝑣)) Cn 𝐶))) → 𝐾 ∈ (((II ×t II) CnP 𝐶)‘⟨𝑟, 0⟩)))
260259rexlimdvva 3233 . . . . . . . . . . . . . . . . 17 ((𝜑𝑟 ∈ (0[,]1)) → (∃𝑢 ∈ II ∃𝑣 ∈ II (𝑟𝑢 ∧ 0 ∈ 𝑣 ∧ (∃𝑤𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II) ↾t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II) ↾t (𝑢 × 𝑣)) Cn 𝐶))) → 𝐾 ∈ (((II ×t II) CnP 𝐶)‘⟨𝑟, 0⟩)))
261182, 260mpd 15 . . . . . . . . . . . . . . . 16 ((𝜑𝑟 ∈ (0[,]1)) → 𝐾 ∈ (((II ×t II) CnP 𝐶)‘⟨𝑟, 0⟩))
262 fveq2 6411 . . . . . . . . . . . . . . . . . 18 (𝑧 = ⟨𝑟, 0⟩ → (((II ×t II) CnP 𝐶)‘𝑧) = (((II ×t II) CnP 𝐶)‘⟨𝑟, 0⟩))
263262eleq2d 2878 . . . . . . . . . . . . . . . . 17 (𝑧 = ⟨𝑟, 0⟩ → (𝐾 ∈ (((II ×t II) CnP 𝐶)‘𝑧) ↔ 𝐾 ∈ (((II ×t II) CnP 𝐶)‘⟨𝑟, 0⟩)))
264263, 69elrab2 3569 . . . . . . . . . . . . . . . 16 (⟨𝑟, 0⟩ ∈ 𝑀 ↔ (⟨𝑟, 0⟩ ∈ ((0[,]1) × (0[,]1)) ∧ 𝐾 ∈ (((II ×t II) CnP 𝐶)‘⟨𝑟, 0⟩)))
265175, 261, 264sylanbrc 574 . . . . . . . . . . . . . . 15 ((𝜑𝑟 ∈ (0[,]1)) → ⟨𝑟, 0⟩ ∈ 𝑀)
266 elsni 4394 . . . . . . . . . . . . . . . . 17 (𝑎 ∈ {0} → 𝑎 = 0)
267266opeq2d 4609 . . . . . . . . . . . . . . . 16 (𝑎 ∈ {0} → ⟨𝑟, 𝑎⟩ = ⟨𝑟, 0⟩)
268267eleq1d 2877 . . . . . . . . . . . . . . 15 (𝑎 ∈ {0} → (⟨𝑟, 𝑎⟩ ∈ 𝑀 ↔ ⟨𝑟, 0⟩ ∈ 𝑀))
269265, 268syl5ibrcom 238 . . . . . . . . . . . . . 14 ((𝜑𝑟 ∈ (0[,]1)) → (𝑎 ∈ {0} → ⟨𝑟, 𝑎⟩ ∈ 𝑀))
270269expimpd 443 . . . . . . . . . . . . 13 (𝜑 → ((𝑟 ∈ (0[,]1) ∧ 𝑎 ∈ {0}) → ⟨𝑟, 𝑎⟩ ∈ 𝑀))
271172, 270syl5bi 233 . . . . . . . . . . . 12 (𝜑 → (⟨𝑟, 𝑎⟩ ∈ ((0[,]1) × {0}) → ⟨𝑟, 𝑎⟩ ∈ 𝑀))
272171, 271relssdv 5421 . . . . . . . . . . 11 (𝜑 → ((0[,]1) × {0}) ⊆ 𝑀)
273 sneq 4387 . . . . . . . . . . . . . 14 (𝑎 = 0 → {𝑎} = {0})
274273xpeq2d 5347 . . . . . . . . . . . . 13 (𝑎 = 0 → ((0[,]1) × {𝑎}) = ((0[,]1) × {0}))
275274sseq1d 3836 . . . . . . . . . . . 12 (𝑎 = 0 → (((0[,]1) × {𝑎}) ⊆ 𝑀 ↔ ((0[,]1) × {0}) ⊆ 𝑀))
276275, 13elrab2 3569 . . . . . . . . . . 11 (0 ∈ 𝐴 ↔ (0 ∈ (0[,]1) ∧ ((0[,]1) × {0}) ⊆ 𝑀))
277169, 272, 276sylanbrc 574 . . . . . . . . . 10 (𝜑 → 0 ∈ 𝐴)
278277ne0d 4130 . . . . . . . . 9 (𝜑𝐴 ≠ ∅)
279 inss2 4037 . . . . . . . . . 10 (II ∩ (Clsd‘II)) ⊆ (Clsd‘II)
280279, 166sseldi 3803 . . . . . . . . 9 (𝜑𝐴 ∈ (Clsd‘II))
28114, 16, 167, 278, 280connclo 21436 . . . . . . . 8 (𝜑𝐴 = (0[,]1))
28213, 281syl5reqr 2862 . . . . . . 7 (𝜑 → (0[,]1) = {𝑎 ∈ (0[,]1) ∣ ((0[,]1) × {𝑎}) ⊆ 𝑀})
283 rabid2 3314 . . . . . . 7 ((0[,]1) = {𝑎 ∈ (0[,]1) ∣ ((0[,]1) × {𝑎}) ⊆ 𝑀} ↔ ∀𝑎 ∈ (0[,]1)((0[,]1) × {𝑎}) ⊆ 𝑀)
284282, 283sylib 209 . . . . . 6 (𝜑 → ∀𝑎 ∈ (0[,]1)((0[,]1) × {𝑎}) ⊆ 𝑀)
285 iunss 4760 . . . . . 6 ( 𝑎 ∈ (0[,]1)((0[,]1) × {𝑎}) ⊆ 𝑀 ↔ ∀𝑎 ∈ (0[,]1)((0[,]1) × {𝑎}) ⊆ 𝑀)
286284, 285sylibr 225 . . . . 5 (𝜑 𝑎 ∈ (0[,]1)((0[,]1) × {𝑎}) ⊆ 𝑀)
28712, 286syl5eqss 3853 . . . 4 (𝜑 → ((0[,]1) × (0[,]1)) ⊆ 𝑀)
288287, 69syl6sseq 3855 . . 3 (𝜑 → ((0[,]1) × (0[,]1)) ⊆ {𝑧 ∈ ((0[,]1) × (0[,]1)) ∣ 𝐾 ∈ (((II ×t II) CnP 𝐶)‘𝑧)})
289 ssrab 3884 . . . 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 𝐶)‘𝑧)))
290289simprbi 486 . . 3 (((0[,]1) × (0[,]1)) ⊆ {𝑧 ∈ ((0[,]1) × (0[,]1)) ∣ 𝐾 ∈ (((II ×t II) CnP 𝐶)‘𝑧)} → ∀𝑧 ∈ ((0[,]1) × (0[,]1))𝐾 ∈ (((II ×t II) CnP 𝐶)‘𝑧))
291288, 290syl 17 . 2 (𝜑 → ∀𝑧 ∈ ((0[,]1) × (0[,]1))𝐾 ∈ (((II ×t II) CnP 𝐶)‘𝑧))
292 txtopon 21612 . . . 4 ((II ∈ (TopOn‘(0[,]1)) ∧ II ∈ (TopOn‘(0[,]1))) → (II ×t II) ∈ (TopOn‘((0[,]1) × (0[,]1))))
293211, 211, 292mp2an 675 . . 3 (II ×t II) ∈ (TopOn‘((0[,]1) × (0[,]1)))
294 cvmtop1 31570 . . . . 5 (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐶 ∈ Top)
2952, 294syl 17 . . . 4 (𝜑𝐶 ∈ Top)
2961toptopon 20939 . . . 4 (𝐶 ∈ Top ↔ 𝐶 ∈ (TopOn‘𝐵))
297295, 296sylib 209 . . 3 (𝜑𝐶 ∈ (TopOn‘𝐵))
298 cncnp 21302 . . 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 𝐶)‘𝑧))))
299293, 297, 298sylancr 577 . 2 (𝜑 → (𝐾 ∈ ((II ×t II) Cn 𝐶) ↔ (𝐾:((0[,]1) × (0[,]1))⟶𝐵 ∧ ∀𝑧 ∈ ((0[,]1) × (0[,]1))𝐾 ∈ (((II ×t II) CnP 𝐶)‘𝑧))))
3008, 291, 299mpbir2and 695 1 (𝜑𝐾 ∈ ((II ×t II) Cn 𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384  w3a 1100  wal 1635   = wceq 1637  wcel 2157  wral 3103  wrex 3104  {crab 3107  Vcvv 3398  cdif 3773  cin 3775  wss 3776  c0 4123  𝒫 cpw 4358  {csn 4377  cop 4383   cuni 4637   ciun 4719  {copab 4913  cmpt 4930   × cxp 5316  ccnv 5317  cres 5320  cima 5321  ccom 5322  Rel wrel 5323   Fn wfn 6099  wf 6100  cfv 6104  crio 6837  (class class class)co 6877  cmpt2 6879  0cc0 10224  1c1 10225  [,]cicc 12399  t crest 16289  Topctop 20915  TopOnctopon 20932  Clsdccld 21038  intcnt 21039  neicnei 21119   Cn ccn 21246   CnP ccnp 21247  Compccmp 21407  Conncconn 21432   ×t ctx 21581  Homeochmeo 21774  IIcii 22895   CovMap ccvm 31565
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-8 2159  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2791  ax-rep 4971  ax-sep 4982  ax-nul 4990  ax-pow 5042  ax-pr 5103  ax-un 7182  ax-inf2 8788  ax-cnex 10280  ax-resscn 10281  ax-1cn 10282  ax-icn 10283  ax-addcl 10284  ax-addrcl 10285  ax-mulcl 10286  ax-mulrcl 10287  ax-mulcom 10288  ax-addass 10289  ax-mulass 10290  ax-distr 10291  ax-i2m1 10292  ax-1ne0 10293  ax-1rid 10294  ax-rnegex 10295  ax-rrecex 10296  ax-cnre 10297  ax-pre-lttri 10298  ax-pre-lttrn 10299  ax-pre-ltadd 10300  ax-pre-mulgt0 10301  ax-pre-sup 10302  ax-addf 10303  ax-mulf 10304
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-fal 1651  df-ex 1860  df-nf 1864  df-sb 2062  df-mo 2635  df-eu 2638  df-clab 2800  df-cleq 2806  df-clel 2809  df-nfc 2944  df-ne 2986  df-nel 3089  df-ral 3108  df-rex 3109  df-reu 3110  df-rmo 3111  df-rab 3112  df-v 3400  df-sbc 3641  df-csb 3736  df-dif 3779  df-un 3781  df-in 3783  df-ss 3790  df-pss 3792  df-nul 4124  df-if 4287  df-pw 4360  df-sn 4378  df-pr 4380  df-tp 4382  df-op 4384  df-uni 4638  df-int 4677  df-iun 4721  df-iin 4722  df-br 4852  df-opab 4914  df-mpt 4931  df-tr 4954  df-id 5226  df-eprel 5231  df-po 5239  df-so 5240  df-fr 5277  df-se 5278  df-we 5279  df-xp 5324  df-rel 5325  df-cnv 5326  df-co 5327  df-dm 5328  df-rn 5329  df-res 5330  df-ima 5331  df-pred 5900  df-ord 5946  df-on 5947  df-lim 5948  df-suc 5949  df-iota 6067  df-fun 6106  df-fn 6107  df-f 6108  df-f1 6109  df-fo 6110  df-f1o 6111  df-fv 6112  df-isom 6113  df-riota 6838  df-ov 6880  df-oprab 6881  df-mpt2 6882  df-of 7130  df-om 7299  df-1st 7401  df-2nd 7402  df-supp 7533  df-wrecs 7645  df-recs 7707  df-rdg 7745  df-1o 7799  df-2o 7800  df-oadd 7803  df-er 7982  df-ec 7984  df-map 8097  df-ixp 8149  df-en 8196  df-dom 8197  df-sdom 8198  df-fin 8199  df-fsupp 8518  df-fi 8559  df-sup 8590  df-inf 8591  df-oi 8657  df-card 9051  df-cda 9278  df-pnf 10364  df-mnf 10365  df-xr 10366  df-ltxr 10367  df-le 10368  df-sub 10556  df-neg 10557  df-div 10973  df-nn 11309  df-2 11367  df-3 11368  df-4 11369  df-5 11370  df-6 11371  df-7 11372  df-8 11373  df-9 11374  df-n0 11563  df-z 11647  df-dec 11763  df-uz 11908  df-q 12011  df-rp 12050  df-xneg 12165  df-xadd 12166  df-xmul 12167  df-ioo 12400  df-ico 12402  df-icc 12403  df-fz 12553  df-fzo 12693  df-fl 12820  df-seq 13028  df-exp 13087  df-hash 13341  df-cj 14065  df-re 14066  df-im 14067  df-sqrt 14201  df-abs 14202  df-clim 14445  df-sum 14643  df-struct 16073  df-ndx 16074  df-slot 16075  df-base 16077  df-sets 16078  df-ress 16079  df-plusg 16169  df-mulr 16170  df-starv 16171  df-sca 16172  df-vsca 16173  df-ip 16174  df-tset 16175  df-ple 16176  df-ds 16178  df-unif 16179  df-hom 16180  df-cco 16181  df-rest 16291  df-topn 16292  df-0g 16310  df-gsum 16311  df-topgen 16312  df-pt 16313  df-prds 16316  df-xrs 16370  df-qtop 16375  df-imas 16376  df-xps 16378  df-mre 16454  df-mrc 16455  df-acs 16457  df-mgm 17450  df-sgrp 17492  df-mnd 17503  df-submnd 17544  df-mulg 17749  df-cntz 17954  df-cmn 18399  df-psmet 19949  df-xmet 19950  df-met 19951  df-bl 19952  df-mopn 19953  df-cnfld 19958  df-top 20916  df-topon 20933  df-topsp 20955  df-bases 20968  df-cld 21041  df-ntr 21042  df-cls 21043  df-nei 21120  df-cn 21249  df-cnp 21250  df-cmp 21408  df-conn 21433  df-lly 21487  df-nlly 21488  df-tx 21583  df-hmeo 21776  df-xms 22342  df-ms 22343  df-tms 22344  df-ii 22897  df-htpy 22986  df-phtpy 22987  df-phtpc 23008  df-pconn 31531  df-sconn 31532  df-cvm 31566
This theorem is referenced by:  cvmlift2lem13  31625
  Copyright terms: Public domain W3C validator