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 33908
Description: Lemma for cvmlift2 33910. (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 33901 . 2 (𝜑𝐾:((0[,]1) × (0[,]1))⟶𝐵)
9 iunid 5020 . . . . . . 7 𝑎 ∈ (0[,]1){𝑎} = (0[,]1)
109xpeq2i 5660 . . . . . 6 ((0[,]1) × 𝑎 ∈ (0[,]1){𝑎}) = ((0[,]1) × (0[,]1))
11 xpiundi 5702 . . . . . 6 ((0[,]1) × 𝑎 ∈ (0[,]1){𝑎}) = 𝑎 ∈ (0[,]1)((0[,]1) × {𝑎})
1210, 11eqtr3i 2766 . . . . 5 ((0[,]1) × (0[,]1)) = 𝑎 ∈ (0[,]1)((0[,]1) × {𝑎})
13 iiuni 24244 . . . . . . . . 9 (0[,]1) = II
14 iiconn 24250 . . . . . . . . . 10 II ∈ Conn
1514a1i 11 . . . . . . . . 9 (𝜑 → II ∈ Conn)
16 inss1 4188 . . . . . . . . . 10 (II ∩ (Clsd‘II)) ⊆ II
17 iicmp 24249 . . . . . . . . . . . . . . 15 II ∈ Comp
1817a1i 11 . . . . . . . . . . . . . 14 ((𝜑𝑎 ∈ (0[,]1)) → II ∈ Comp)
19 iitop 24243 . . . . . . . . . . . . . . 15 II ∈ Top
2019a1i 11 . . . . . . . . . . . . . 14 ((𝜑𝑎 ∈ (0[,]1)) → II ∈ Top)
2119, 19txtopi 22941 . . . . . . . . . . . . . . . 16 (II ×t II) ∈ Top
2213neiss2 22452 . . . . . . . . . . . . . . . . . . . . . . . 24 ((II ∈ Top ∧ 𝑢 ∈ ((nei‘II)‘{𝑟})) → {𝑟} ⊆ (0[,]1))
2319, 22mpan 688 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑢 ∈ ((nei‘II)‘{𝑟}) → {𝑟} ⊆ (0[,]1))
24 vex 3449 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑟 ∈ V
2524snss 4746 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑟 ∈ (0[,]1) ↔ {𝑟} ⊆ (0[,]1))
2623, 25sylibr 233 . . . . . . . . . . . . . . . . . . . . . 22 (𝑢 ∈ ((nei‘II)‘{𝑟}) → 𝑟 ∈ (0[,]1))
2726a1d 25 . . . . . . . . . . . . . . . . . . . . 21 (𝑢 ∈ ((nei‘II)‘{𝑟}) → (((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀) → 𝑟 ∈ (0[,]1)))
2827rexlimiv 3145 . . . . . . . . . . . . . . . . . . . 20 (∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀) → 𝑟 ∈ (0[,]1))
2928adantl 482 . . . . . . . . . . . . . . . . . . 19 ((𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀)) → 𝑟 ∈ (0[,]1))
30 simpl 483 . . . . . . . . . . . . . . . . . . 19 ((𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀)) → 𝑡 ∈ (0[,]1))
3129, 30jca 512 . . . . . . . . . . . . . . . . . 18 ((𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀)) → (𝑟 ∈ (0[,]1) ∧ 𝑡 ∈ (0[,]1)))
3231ssopab2i 5507 . . . . . . . . . . . . . . . . 17 {⟨𝑟, 𝑡⟩ ∣ (𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀))} ⊆ {⟨𝑟, 𝑡⟩ ∣ (𝑟 ∈ (0[,]1) ∧ 𝑡 ∈ (0[,]1))}
33 cvmlift2.s . . . . . . . . . . . . . . . . 17 𝑆 = {⟨𝑟, 𝑡⟩ ∣ (𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀))}
34 df-xp 5639 . . . . . . . . . . . . . . . . 17 ((0[,]1) × (0[,]1)) = {⟨𝑟, 𝑡⟩ ∣ (𝑟 ∈ (0[,]1) ∧ 𝑡 ∈ (0[,]1))}
3532, 33, 343sstr4i 3987 . . . . . . . . . . . . . . . 16 𝑆 ⊆ ((0[,]1) × (0[,]1))
3619, 19, 13, 13txunii 22944 . . . . . . . . . . . . . . . . 17 ((0[,]1) × (0[,]1)) = (II ×t II)
3736ntropn 22400 . . . . . . . . . . . . . . . 16 (((II ×t II) ∈ Top ∧ 𝑆 ⊆ ((0[,]1) × (0[,]1))) → ((int‘(II ×t II))‘𝑆) ∈ (II ×t II))
3821, 35, 37mp2an 690 . . . . . . . . . . . . . . 15 ((int‘(II ×t II))‘𝑆) ∈ (II ×t II)
3938a1i 11 . . . . . . . . . . . . . 14 ((𝜑𝑎 ∈ (0[,]1)) → ((int‘(II ×t II))‘𝑆) ∈ (II ×t II))
402adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) → 𝐹 ∈ (𝐶 CovMap 𝐽))
413adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) → 𝐺 ∈ ((II ×t II) Cn 𝐽))
424adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) → 𝑃𝐵)
435adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) → (𝐹𝑃) = (0𝐺0))
44 eqid 2736 . . . . . . . . . . . . . . . . . . . 20 (𝑘𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ ( 𝑠 = (𝐹𝑘) ∧ ∀𝑐𝑠 (∀𝑑 ∈ (𝑠 ∖ {𝑐})(𝑐𝑑) = ∅ ∧ (𝐹𝑐) ∈ ((𝐶t 𝑐)Homeo(𝐽t 𝑘))))}) = (𝑘𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ ( 𝑠 = (𝐹𝑘) ∧ ∀𝑐𝑠 (∀𝑑 ∈ (𝑠 ∖ {𝑐})(𝑐𝑑) = ∅ ∧ (𝐹𝑐) ∈ ((𝐶t 𝑐)Homeo(𝐽t 𝑘))))})
45 simprr 771 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) → 𝑏 ∈ (0[,]1))
46 simprl 769 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) → 𝑎 ∈ (0[,]1))
471, 40, 41, 42, 43, 6, 7, 44, 45, 46cvmlift2lem10 33906 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) → ∃𝑢 ∈ II ∃𝑣 ∈ II (𝑏𝑢𝑎𝑣 ∧ (∃𝑤𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II) ↾t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II) ↾t (𝑢 × 𝑣)) Cn 𝐶))))
4821a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏𝑢𝑎𝑣 ∧ (∃𝑤𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II) ↾t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II) ↾t (𝑢 × 𝑣)) Cn 𝐶)))) → (II ×t II) ∈ Top)
4935a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏𝑢𝑎𝑣 ∧ (∃𝑤𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II) ↾t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II) ↾t (𝑢 × 𝑣)) Cn 𝐶)))) → 𝑆 ⊆ ((0[,]1) × (0[,]1)))
5019a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏𝑢𝑎𝑣 ∧ (∃𝑤𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II) ↾t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II) ↾t (𝑢 × 𝑣)) Cn 𝐶)))) → II ∈ Top)
51 simplrl 775 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏𝑢𝑎𝑣 ∧ (∃𝑤𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II) ↾t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II) ↾t (𝑢 × 𝑣)) Cn 𝐶)))) → 𝑢 ∈ II)
52 simplrr 776 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏𝑢𝑎𝑣 ∧ (∃𝑤𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II) ↾t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II) ↾t (𝑢 × 𝑣)) Cn 𝐶)))) → 𝑣 ∈ II)
53 txopn 22953 . . . . . . . . . . . . . . . . . . . . . . . 24 (((II ∈ Top ∧ II ∈ Top) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) → (𝑢 × 𝑣) ∈ (II ×t II))
5450, 50, 51, 52, 53syl22anc 837 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏𝑢𝑎𝑣 ∧ (∃𝑤𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II) ↾t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II) ↾t (𝑢 × 𝑣)) Cn 𝐶)))) → (𝑢 × 𝑣) ∈ (II ×t II))
55 simpr 485 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑟𝑢𝑡𝑣) → 𝑡𝑣)
56 elunii 4870 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑡𝑣𝑣 ∈ II) → 𝑡 II)
5756, 13eleqtrrdi 2849 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑡𝑣𝑣 ∈ II) → 𝑡 ∈ (0[,]1))
5855, 52, 57syl2anr 597 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏𝑢𝑎𝑣 ∧ (∃𝑤𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II) ↾t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II) ↾t (𝑢 × 𝑣)) Cn 𝐶)))) ∧ (𝑟𝑢𝑡𝑣)) → 𝑡 ∈ (0[,]1))
5919a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏𝑢𝑎𝑣 ∧ (∃𝑤𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II) ↾t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II) ↾t (𝑢 × 𝑣)) Cn 𝐶)))) ∧ (𝑟𝑢𝑡𝑣)) → II ∈ Top)
6051adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏𝑢𝑎𝑣 ∧ (∃𝑤𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II) ↾t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II) ↾t (𝑢 × 𝑣)) Cn 𝐶)))) ∧ (𝑟𝑢𝑡𝑣)) → 𝑢 ∈ II)
61 simprl 769 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏𝑢𝑎𝑣 ∧ (∃𝑤𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II) ↾t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II) ↾t (𝑢 × 𝑣)) Cn 𝐶)))) ∧ (𝑟𝑢𝑡𝑣)) → 𝑟𝑢)
62 opnneip 22470 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((II ∈ Top ∧ 𝑢 ∈ II ∧ 𝑟𝑢) → 𝑢 ∈ ((nei‘II)‘{𝑟}))
6359, 60, 61, 62syl3anc 1371 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏𝑢𝑎𝑣 ∧ (∃𝑤𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II) ↾t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II) ↾t (𝑢 × 𝑣)) Cn 𝐶)))) ∧ (𝑟𝑢𝑡𝑣)) → 𝑢 ∈ ((nei‘II)‘{𝑟}))
6440ad3antrrr 728 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏𝑢𝑎𝑣 ∧ (∃𝑤𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II) ↾t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II) ↾t (𝑢 × 𝑣)) Cn 𝐶)))) ∧ (𝑟𝑢𝑡𝑣)) → 𝐹 ∈ (𝐶 CovMap 𝐽))
6541ad3antrrr 728 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏𝑢𝑎𝑣 ∧ (∃𝑤𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II) ↾t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II) ↾t (𝑢 × 𝑣)) Cn 𝐶)))) ∧ (𝑟𝑢𝑡𝑣)) → 𝐺 ∈ ((II ×t II) Cn 𝐽))
6642ad3antrrr 728 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏𝑢𝑎𝑣 ∧ (∃𝑤𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II) ↾t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II) ↾t (𝑢 × 𝑣)) Cn 𝐶)))) ∧ (𝑟𝑢𝑡𝑣)) → 𝑃𝐵)
6743ad3antrrr 728 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 𝐶)‘𝑧)}
6952adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏𝑢𝑎𝑣 ∧ (∃𝑤𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II) ↾t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II) ↾t (𝑢 × 𝑣)) Cn 𝐶)))) ∧ (𝑟𝑢𝑡𝑣)) → 𝑣 ∈ II)
70 simplr2 1216 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏𝑢𝑎𝑣 ∧ (∃𝑤𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II) ↾t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II) ↾t (𝑢 × 𝑣)) Cn 𝐶)))) ∧ (𝑟𝑢𝑡𝑣)) → 𝑎𝑣)
71 simprr 771 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏𝑢𝑎𝑣 ∧ (∃𝑤𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II) ↾t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II) ↾t (𝑢 × 𝑣)) Cn 𝐶)))) ∧ (𝑟𝑢𝑡𝑣)) → 𝑡𝑣)
72 sneq 4596 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑐 = 𝑤 → {𝑐} = {𝑤})
7372xpeq2d 5663 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑐 = 𝑤 → (𝑢 × {𝑐}) = (𝑢 × {𝑤}))
7473reseq2d 5937 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑐 = 𝑤 → (𝐾 ↾ (𝑢 × {𝑐})) = (𝐾 ↾ (𝑢 × {𝑤})))
7573oveq2d 7373 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑐 = 𝑤 → ((II ×t II) ↾t (𝑢 × {𝑐})) = ((II ×t II) ↾t (𝑢 × {𝑤})))
7675oveq1d 7372 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑐 = 𝑤 → (((II ×t II) ↾t (𝑢 × {𝑐})) Cn 𝐶) = (((II ×t II) ↾t (𝑢 × {𝑤})) Cn 𝐶))
7774, 76eleq12d 2832 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑐 = 𝑤 → ((𝐾 ↾ (𝑢 × {𝑐})) ∈ (((II ×t II) ↾t (𝑢 × {𝑐})) Cn 𝐶) ↔ (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II) ↾t (𝑢 × {𝑤})) Cn 𝐶)))
7877cbvrexvw 3226 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (∃𝑐𝑣 (𝐾 ↾ (𝑢 × {𝑐})) ∈ (((II ×t II) ↾t (𝑢 × {𝑐})) Cn 𝐶) ↔ ∃𝑤𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II) ↾t (𝑢 × {𝑤})) Cn 𝐶))
79 simplr3 1217 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 𝐶)))
8078, 79biimtrid 241 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 𝐶)))
811, 64, 65, 66, 67, 6, 7, 68, 60, 69, 70, 71, 80cvmlift2lem11 33907 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏𝑢𝑎𝑣 ∧ (∃𝑤𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II) ↾t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II) ↾t (𝑢 × 𝑣)) Cn 𝐶)))) ∧ (𝑟𝑢𝑡𝑣)) → ((𝑢 × {𝑎}) ⊆ 𝑀 → (𝑢 × {𝑡}) ⊆ 𝑀))
821, 64, 65, 66, 67, 6, 7, 68, 60, 69, 71, 70, 80cvmlift2lem11 33907 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏𝑢𝑎𝑣 ∧ (∃𝑤𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II) ↾t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II) ↾t (𝑢 × 𝑣)) Cn 𝐶)))) ∧ (𝑟𝑢𝑡𝑣)) → ((𝑢 × {𝑡}) ⊆ 𝑀 → (𝑢 × {𝑎}) ⊆ 𝑀))
8381, 82impbid 211 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏𝑢𝑎𝑣 ∧ (∃𝑤𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II) ↾t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II) ↾t (𝑢 × 𝑣)) Cn 𝐶)))) ∧ (𝑟𝑢𝑡𝑣)) → ((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀))
84 rspe 3232 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑢 ∈ ((nei‘II)‘{𝑟}) ∧ ((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀)) → ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀))
8563, 83, 84syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏𝑢𝑎𝑣 ∧ (∃𝑤𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II) ↾t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II) ↾t (𝑢 × 𝑣)) Cn 𝐶)))) ∧ (𝑟𝑢𝑡𝑣)) → ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀))
8658, 85jca 512 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏𝑢𝑎𝑣 ∧ (∃𝑤𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II) ↾t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II) ↾t (𝑢 × 𝑣)) Cn 𝐶)))) ∧ (𝑟𝑢𝑡𝑣)) → (𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀)))
8786ex 413 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏𝑢𝑎𝑣 ∧ (∃𝑤𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II) ↾t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II) ↾t (𝑢 × 𝑣)) Cn 𝐶)))) → ((𝑟𝑢𝑡𝑣) → (𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀))))
8887alrimivv 1931 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏𝑢𝑎𝑣 ∧ (∃𝑤𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II) ↾t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II) ↾t (𝑢 × 𝑣)) Cn 𝐶)))) → ∀𝑟𝑡((𝑟𝑢𝑡𝑣) → (𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀))))
89 df-xp 5639 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑢 × 𝑣) = {⟨𝑟, 𝑡⟩ ∣ (𝑟𝑢𝑡𝑣)}
9089, 33sseq12i 3974 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑢 × 𝑣) ⊆ 𝑆 ↔ {⟨𝑟, 𝑡⟩ ∣ (𝑟𝑢𝑡𝑣)} ⊆ {⟨𝑟, 𝑡⟩ ∣ (𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀))})
91 ssopab2bw 5504 . . . . . . . . . . . . . . . . . . . . . . . . 25 ({⟨𝑟, 𝑡⟩ ∣ (𝑟𝑢𝑡𝑣)} ⊆ {⟨𝑟, 𝑡⟩ ∣ (𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀))} ↔ ∀𝑟𝑡((𝑟𝑢𝑡𝑣) → (𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀))))
9290, 91bitri 274 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑢 × 𝑣) ⊆ 𝑆 ↔ ∀𝑟𝑡((𝑟𝑢𝑡𝑣) → (𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀))))
9388, 92sylibr 233 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏𝑢𝑎𝑣 ∧ (∃𝑤𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II) ↾t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II) ↾t (𝑢 × 𝑣)) Cn 𝐶)))) → (𝑢 × 𝑣) ⊆ 𝑆)
9436ssntr 22409 . . . . . . . . . . . . . . . . . . . . . . 23 ((((II ×t II) ∈ Top ∧ 𝑆 ⊆ ((0[,]1) × (0[,]1))) ∧ ((𝑢 × 𝑣) ∈ (II ×t II) ∧ (𝑢 × 𝑣) ⊆ 𝑆)) → (𝑢 × 𝑣) ⊆ ((int‘(II ×t II))‘𝑆))
9548, 49, 54, 93, 94syl22anc 837 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏𝑢𝑎𝑣 ∧ (∃𝑤𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II) ↾t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II) ↾t (𝑢 × 𝑣)) Cn 𝐶)))) → (𝑢 × 𝑣) ⊆ ((int‘(II ×t II))‘𝑆))
96 simpr1 1194 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏𝑢𝑎𝑣 ∧ (∃𝑤𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II) ↾t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II) ↾t (𝑢 × 𝑣)) Cn 𝐶)))) → 𝑏𝑢)
97 simpr2 1195 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏𝑢𝑎𝑣 ∧ (∃𝑤𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II) ↾t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II) ↾t (𝑢 × 𝑣)) Cn 𝐶)))) → 𝑎𝑣)
98 opelxpi 5670 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑏𝑢𝑎𝑣) → ⟨𝑏, 𝑎⟩ ∈ (𝑢 × 𝑣))
9996, 97, 98syl2anc 584 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏𝑢𝑎𝑣 ∧ (∃𝑤𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II) ↾t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II) ↾t (𝑢 × 𝑣)) Cn 𝐶)))) → ⟨𝑏, 𝑎⟩ ∈ (𝑢 × 𝑣))
10095, 99sseldd 3945 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑏𝑢𝑎𝑣 ∧ (∃𝑤𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II) ↾t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II) ↾t (𝑢 × 𝑣)) Cn 𝐶)))) → ⟨𝑏, 𝑎⟩ ∈ ((int‘(II ×t II))‘𝑆))
101100ex 413 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) → ((𝑏𝑢𝑎𝑣 ∧ (∃𝑤𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II) ↾t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II) ↾t (𝑢 × 𝑣)) Cn 𝐶))) → ⟨𝑏, 𝑎⟩ ∈ ((int‘(II ×t II))‘𝑆)))
102101rexlimdvva 3205 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) → (∃𝑢 ∈ II ∃𝑣 ∈ II (𝑏𝑢𝑎𝑣 ∧ (∃𝑤𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II) ↾t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II) ↾t (𝑢 × 𝑣)) Cn 𝐶))) → ⟨𝑏, 𝑎⟩ ∈ ((int‘(II ×t II))‘𝑆)))
10347, 102mpd 15 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) → ⟨𝑏, 𝑎⟩ ∈ ((int‘(II ×t II))‘𝑆))
104 vex 3449 . . . . . . . . . . . . . . . . . . 19 𝑎 ∈ V
105 opeq2 4831 . . . . . . . . . . . . . . . . . . . 20 (𝑤 = 𝑎 → ⟨𝑏, 𝑤⟩ = ⟨𝑏, 𝑎⟩)
106105eleq1d 2822 . . . . . . . . . . . . . . . . . . 19 (𝑤 = 𝑎 → (⟨𝑏, 𝑤⟩ ∈ ((int‘(II ×t II))‘𝑆) ↔ ⟨𝑏, 𝑎⟩ ∈ ((int‘(II ×t II))‘𝑆)))
107104, 106ralsn 4642 . . . . . . . . . . . . . . . . . 18 (∀𝑤 ∈ {𝑎}⟨𝑏, 𝑤⟩ ∈ ((int‘(II ×t II))‘𝑆) ↔ ⟨𝑏, 𝑎⟩ ∈ ((int‘(II ×t II))‘𝑆))
108103, 107sylibr 233 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1))) → ∀𝑤 ∈ {𝑎}⟨𝑏, 𝑤⟩ ∈ ((int‘(II ×t II))‘𝑆))
109108anassrs 468 . . . . . . . . . . . . . . . 16 (((𝜑𝑎 ∈ (0[,]1)) ∧ 𝑏 ∈ (0[,]1)) → ∀𝑤 ∈ {𝑎}⟨𝑏, 𝑤⟩ ∈ ((int‘(II ×t II))‘𝑆))
110109ralrimiva 3143 . . . . . . . . . . . . . . 15 ((𝜑𝑎 ∈ (0[,]1)) → ∀𝑏 ∈ (0[,]1)∀𝑤 ∈ {𝑎}⟨𝑏, 𝑤⟩ ∈ ((int‘(II ×t II))‘𝑆))
111 dfss3 3932 . . . . . . . . . . . . . . . 16 (((0[,]1) × {𝑎}) ⊆ ((int‘(II ×t II))‘𝑆) ↔ ∀𝑢 ∈ ((0[,]1) × {𝑎})𝑢 ∈ ((int‘(II ×t II))‘𝑆))
112 eleq1 2825 . . . . . . . . . . . . . . . . 17 (𝑢 = ⟨𝑏, 𝑤⟩ → (𝑢 ∈ ((int‘(II ×t II))‘𝑆) ↔ ⟨𝑏, 𝑤⟩ ∈ ((int‘(II ×t II))‘𝑆)))
113112ralxp 5797 . . . . . . . . . . . . . . . 16 (∀𝑢 ∈ ((0[,]1) × {𝑎})𝑢 ∈ ((int‘(II ×t II))‘𝑆) ↔ ∀𝑏 ∈ (0[,]1)∀𝑤 ∈ {𝑎}⟨𝑏, 𝑤⟩ ∈ ((int‘(II ×t II))‘𝑆))
114111, 113bitri 274 . . . . . . . . . . . . . . 15 (((0[,]1) × {𝑎}) ⊆ ((int‘(II ×t II))‘𝑆) ↔ ∀𝑏 ∈ (0[,]1)∀𝑤 ∈ {𝑎}⟨𝑏, 𝑤⟩ ∈ ((int‘(II ×t II))‘𝑆))
115110, 114sylibr 233 . . . . . . . . . . . . . 14 ((𝜑𝑎 ∈ (0[,]1)) → ((0[,]1) × {𝑎}) ⊆ ((int‘(II ×t II))‘𝑆))
116 simpr 485 . . . . . . . . . . . . . 14 ((𝜑𝑎 ∈ (0[,]1)) → 𝑎 ∈ (0[,]1))
11713, 13, 18, 20, 39, 115, 116txtube 22991 . . . . . . . . . . . . 13 ((𝜑𝑎 ∈ (0[,]1)) → ∃𝑣 ∈ II (𝑎𝑣 ∧ ((0[,]1) × 𝑣) ⊆ ((int‘(II ×t II))‘𝑆)))
11836ntrss2 22408 . . . . . . . . . . . . . . . . . . 19 (((II ×t II) ∈ Top ∧ 𝑆 ⊆ ((0[,]1) × (0[,]1))) → ((int‘(II ×t II))‘𝑆) ⊆ 𝑆)
11921, 35, 118mp2an 690 . . . . . . . . . . . . . . . . . 18 ((int‘(II ×t II))‘𝑆) ⊆ 𝑆
120 sstr 3952 . . . . . . . . . . . . . . . . . 18 ((((0[,]1) × 𝑣) ⊆ ((int‘(II ×t II))‘𝑆) ∧ ((int‘(II ×t II))‘𝑆) ⊆ 𝑆) → ((0[,]1) × 𝑣) ⊆ 𝑆)
121119, 120mpan2 689 . . . . . . . . . . . . . . . . 17 (((0[,]1) × 𝑣) ⊆ ((int‘(II ×t II))‘𝑆) → ((0[,]1) × 𝑣) ⊆ 𝑆)
122 df-xp 5639 . . . . . . . . . . . . . . . . . . 19 ((0[,]1) × 𝑣) = {⟨𝑟, 𝑡⟩ ∣ (𝑟 ∈ (0[,]1) ∧ 𝑡𝑣)}
123122, 33sseq12i 3974 . . . . . . . . . . . . . . . . . 18 (((0[,]1) × 𝑣) ⊆ 𝑆 ↔ {⟨𝑟, 𝑡⟩ ∣ (𝑟 ∈ (0[,]1) ∧ 𝑡𝑣)} ⊆ {⟨𝑟, 𝑡⟩ ∣ (𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀))})
124 ssopab2bw 5504 . . . . . . . . . . . . . . . . . . 19 ({⟨𝑟, 𝑡⟩ ∣ (𝑟 ∈ (0[,]1) ∧ 𝑡𝑣)} ⊆ {⟨𝑟, 𝑡⟩ ∣ (𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀))} ↔ ∀𝑟𝑡((𝑟 ∈ (0[,]1) ∧ 𝑡𝑣) → (𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀))))
125 r2al 3191 . . . . . . . . . . . . . . . . . . 19 (∀𝑟 ∈ (0[,]1)∀𝑡𝑣 (𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀)) ↔ ∀𝑟𝑡((𝑟 ∈ (0[,]1) ∧ 𝑡𝑣) → (𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀))))
126 ralcom 3272 . . . . . . . . . . . . . . . . . . 19 (∀𝑟 ∈ (0[,]1)∀𝑡𝑣 (𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀)) ↔ ∀𝑡𝑣𝑟 ∈ (0[,]1)(𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀)))
127124, 125, 1263bitr2i 298 . . . . . . . . . . . . . . . . . 18 ({⟨𝑟, 𝑡⟩ ∣ (𝑟 ∈ (0[,]1) ∧ 𝑡𝑣)} ⊆ {⟨𝑟, 𝑡⟩ ∣ (𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀))} ↔ ∀𝑡𝑣𝑟 ∈ (0[,]1)(𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀)))
128123, 127bitri 274 . . . . . . . . . . . . . . . . 17 (((0[,]1) × 𝑣) ⊆ 𝑆 ↔ ∀𝑡𝑣𝑟 ∈ (0[,]1)(𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀)))
129121, 128sylib 217 . . . . . . . . . . . . . . . 16 (((0[,]1) × 𝑣) ⊆ ((int‘(II ×t II))‘𝑆) → ∀𝑡𝑣𝑟 ∈ (0[,]1)(𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀)))
130 simpr 485 . . . . . . . . . . . . . . . . . . . 20 ((𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀)) → ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀))
131130ralimi 3086 . . . . . . . . . . . . . . . . . . 19 (∀𝑟 ∈ (0[,]1)(𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀)) → ∀𝑟 ∈ (0[,]1)∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀))
132 cvmlift2lem1 33896 . . . . . . . . . . . . . . . . . . . 20 (∀𝑟 ∈ (0[,]1)∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀) → (((0[,]1) × {𝑎}) ⊆ 𝑀 → ((0[,]1) × {𝑡}) ⊆ 𝑀))
133 bicom 221 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀) ↔ ((𝑢 × {𝑡}) ⊆ 𝑀 ↔ (𝑢 × {𝑎}) ⊆ 𝑀))
134133rexbii 3097 . . . . . . . . . . . . . . . . . . . . . 22 (∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀) ↔ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑡}) ⊆ 𝑀 ↔ (𝑢 × {𝑎}) ⊆ 𝑀))
135134ralbii 3096 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑟 ∈ (0[,]1)∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀) ↔ ∀𝑟 ∈ (0[,]1)∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑡}) ⊆ 𝑀 ↔ (𝑢 × {𝑎}) ⊆ 𝑀))
136 cvmlift2lem1 33896 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑟 ∈ (0[,]1)∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑡}) ⊆ 𝑀 ↔ (𝑢 × {𝑎}) ⊆ 𝑀) → (((0[,]1) × {𝑡}) ⊆ 𝑀 → ((0[,]1) × {𝑎}) ⊆ 𝑀))
137135, 136sylbi 216 . . . . . . . . . . . . . . . . . . . 20 (∀𝑟 ∈ (0[,]1)∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀) → (((0[,]1) × {𝑡}) ⊆ 𝑀 → ((0[,]1) × {𝑎}) ⊆ 𝑀))
138132, 137impbid 211 . . . . . . . . . . . . . . . . . . 19 (∀𝑟 ∈ (0[,]1)∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀) → (((0[,]1) × {𝑎}) ⊆ 𝑀 ↔ ((0[,]1) × {𝑡}) ⊆ 𝑀))
139131, 138syl 17 . . . . . . . . . . . . . . . . . 18 (∀𝑟 ∈ (0[,]1)(𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀)) → (((0[,]1) × {𝑎}) ⊆ 𝑀 ↔ ((0[,]1) × {𝑡}) ⊆ 𝑀))
140 cvmlift2.a . . . . . . . . . . . . . . . . . . . . . 22 𝐴 = {𝑎 ∈ (0[,]1) ∣ ((0[,]1) × {𝑎}) ⊆ 𝑀}
141140reqabi 3429 . . . . . . . . . . . . . . . . . . . . 21 (𝑎𝐴 ↔ (𝑎 ∈ (0[,]1) ∧ ((0[,]1) × {𝑎}) ⊆ 𝑀))
142141baib 536 . . . . . . . . . . . . . . . . . . . 20 (𝑎 ∈ (0[,]1) → (𝑎𝐴 ↔ ((0[,]1) × {𝑎}) ⊆ 𝑀))
143142ad3antlr 729 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑎 ∈ (0[,]1)) ∧ 𝑣 ∈ II) ∧ 𝑡𝑣) → (𝑎𝐴 ↔ ((0[,]1) × {𝑎}) ⊆ 𝑀))
144 elssuni 4898 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑣 ∈ II → 𝑣 II)
145144, 13sseqtrrdi 3995 . . . . . . . . . . . . . . . . . . . . . 22 (𝑣 ∈ II → 𝑣 ⊆ (0[,]1))
146145adantl 482 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑎 ∈ (0[,]1)) ∧ 𝑣 ∈ II) → 𝑣 ⊆ (0[,]1))
147146sselda 3944 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑎 ∈ (0[,]1)) ∧ 𝑣 ∈ II) ∧ 𝑡𝑣) → 𝑡 ∈ (0[,]1))
148 sneq 4596 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑎 = 𝑡 → {𝑎} = {𝑡})
149148xpeq2d 5663 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑎 = 𝑡 → ((0[,]1) × {𝑎}) = ((0[,]1) × {𝑡}))
150149sseq1d 3975 . . . . . . . . . . . . . . . . . . . . . 22 (𝑎 = 𝑡 → (((0[,]1) × {𝑎}) ⊆ 𝑀 ↔ ((0[,]1) × {𝑡}) ⊆ 𝑀))
151150, 140elrab2 3648 . . . . . . . . . . . . . . . . . . . . 21 (𝑡𝐴 ↔ (𝑡 ∈ (0[,]1) ∧ ((0[,]1) × {𝑡}) ⊆ 𝑀))
152151baib 536 . . . . . . . . . . . . . . . . . . . 20 (𝑡 ∈ (0[,]1) → (𝑡𝐴 ↔ ((0[,]1) × {𝑡}) ⊆ 𝑀))
153147, 152syl 17 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑎 ∈ (0[,]1)) ∧ 𝑣 ∈ II) ∧ 𝑡𝑣) → (𝑡𝐴 ↔ ((0[,]1) × {𝑡}) ⊆ 𝑀))
154143, 153bibi12d 345 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑎 ∈ (0[,]1)) ∧ 𝑣 ∈ II) ∧ 𝑡𝑣) → ((𝑎𝐴𝑡𝐴) ↔ (((0[,]1) × {𝑎}) ⊆ 𝑀 ↔ ((0[,]1) × {𝑡}) ⊆ 𝑀)))
155139, 154syl5ibr 245 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑎 ∈ (0[,]1)) ∧ 𝑣 ∈ II) ∧ 𝑡𝑣) → (∀𝑟 ∈ (0[,]1)(𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀)) → (𝑎𝐴𝑡𝐴)))
156155ralimdva 3164 . . . . . . . . . . . . . . . 16 (((𝜑𝑎 ∈ (0[,]1)) ∧ 𝑣 ∈ II) → (∀𝑡𝑣𝑟 ∈ (0[,]1)(𝑡 ∈ (0[,]1) ∧ ∃𝑢 ∈ ((nei‘II)‘{𝑟})((𝑢 × {𝑎}) ⊆ 𝑀 ↔ (𝑢 × {𝑡}) ⊆ 𝑀)) → ∀𝑡𝑣 (𝑎𝐴𝑡𝐴)))
157129, 156syl5 34 . . . . . . . . . . . . . . 15 (((𝜑𝑎 ∈ (0[,]1)) ∧ 𝑣 ∈ II) → (((0[,]1) × 𝑣) ⊆ ((int‘(II ×t II))‘𝑆) → ∀𝑡𝑣 (𝑎𝐴𝑡𝐴)))
158157anim2d 612 . . . . . . . . . . . . . 14 (((𝜑𝑎 ∈ (0[,]1)) ∧ 𝑣 ∈ II) → ((𝑎𝑣 ∧ ((0[,]1) × 𝑣) ⊆ ((int‘(II ×t II))‘𝑆)) → (𝑎𝑣 ∧ ∀𝑡𝑣 (𝑎𝐴𝑡𝐴))))
159158reximdva 3165 . . . . . . . . . . . . 13 ((𝜑𝑎 ∈ (0[,]1)) → (∃𝑣 ∈ II (𝑎𝑣 ∧ ((0[,]1) × 𝑣) ⊆ ((int‘(II ×t II))‘𝑆)) → ∃𝑣 ∈ II (𝑎𝑣 ∧ ∀𝑡𝑣 (𝑎𝐴𝑡𝐴))))
160117, 159mpd 15 . . . . . . . . . . . 12 ((𝜑𝑎 ∈ (0[,]1)) → ∃𝑣 ∈ II (𝑎𝑣 ∧ ∀𝑡𝑣 (𝑎𝐴𝑡𝐴)))
161160ralrimiva 3143 . . . . . . . . . . 11 (𝜑 → ∀𝑎 ∈ (0[,]1)∃𝑣 ∈ II (𝑎𝑣 ∧ ∀𝑡𝑣 (𝑎𝐴𝑡𝐴)))
162 ssrab2 4037 . . . . . . . . . . . . 13 {𝑎 ∈ (0[,]1) ∣ ((0[,]1) × {𝑎}) ⊆ 𝑀} ⊆ (0[,]1)
163140, 162eqsstri 3978 . . . . . . . . . . . 12 𝐴 ⊆ (0[,]1)
16413isclo 22438 . . . . . . . . . . . 12 ((II ∈ Top ∧ 𝐴 ⊆ (0[,]1)) → (𝐴 ∈ (II ∩ (Clsd‘II)) ↔ ∀𝑎 ∈ (0[,]1)∃𝑣 ∈ II (𝑎𝑣 ∧ ∀𝑡𝑣 (𝑎𝐴𝑡𝐴))))
16519, 163, 164mp2an 690 . . . . . . . . . . 11 (𝐴 ∈ (II ∩ (Clsd‘II)) ↔ ∀𝑎 ∈ (0[,]1)∃𝑣 ∈ II (𝑎𝑣 ∧ ∀𝑡𝑣 (𝑎𝐴𝑡𝐴)))
166161, 165sylibr 233 . . . . . . . . . 10 (𝜑𝐴 ∈ (II ∩ (Clsd‘II)))
16716, 166sselid 3942 . . . . . . . . 9 (𝜑𝐴 ∈ II)
168 0elunit 13386 . . . . . . . . . . . 12 0 ∈ (0[,]1)
169168a1i 11 . . . . . . . . . . 11 (𝜑 → 0 ∈ (0[,]1))
170 relxp 5651 . . . . . . . . . . . . 13 Rel ((0[,]1) × {0})
171170a1i 11 . . . . . . . . . . . 12 (𝜑 → Rel ((0[,]1) × {0}))
172 opelxp 5669 . . . . . . . . . . . . 13 (⟨𝑟, 𝑎⟩ ∈ ((0[,]1) × {0}) ↔ (𝑟 ∈ (0[,]1) ∧ 𝑎 ∈ {0}))
173 id 22 . . . . . . . . . . . . . . . . 17 (𝑟 ∈ (0[,]1) → 𝑟 ∈ (0[,]1))
174 opelxpi 5670 . . . . . . . . . . . . . . . . 17 ((𝑟 ∈ (0[,]1) ∧ 0 ∈ (0[,]1)) → ⟨𝑟, 0⟩ ∈ ((0[,]1) × (0[,]1)))
175173, 169, 174syl2anr 597 . . . . . . . . . . . . . . . 16 ((𝜑𝑟 ∈ (0[,]1)) → ⟨𝑟, 0⟩ ∈ ((0[,]1) × (0[,]1)))
1762adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑟 ∈ (0[,]1)) → 𝐹 ∈ (𝐶 CovMap 𝐽))
1773adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑟 ∈ (0[,]1)) → 𝐺 ∈ ((II ×t II) Cn 𝐽))
1784adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑟 ∈ (0[,]1)) → 𝑃𝐵)
1795adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑟 ∈ (0[,]1)) → (𝐹𝑃) = (0𝐺0))
180 simpr 485 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑟 ∈ (0[,]1)) → 𝑟 ∈ (0[,]1))
181168a1i 11 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑟 ∈ (0[,]1)) → 0 ∈ (0[,]1))
1821, 176, 177, 178, 179, 6, 7, 44, 180, 181cvmlift2lem10 33906 . . . . . . . . . . . . . . . . 17 ((𝜑𝑟 ∈ (0[,]1)) → ∃𝑢 ∈ II ∃𝑣 ∈ II (𝑟𝑢 ∧ 0 ∈ 𝑣 ∧ (∃𝑤𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II) ↾t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II) ↾t (𝑢 × 𝑣)) Cn 𝐶))))
183 df-3an 1089 . . . . . . . . . . . . . . . . . . 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 771 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟𝑢 ∧ 0 ∈ 𝑣)) → 0 ∈ 𝑣)
1858ad3antrrr 728 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟𝑢 ∧ 0 ∈ 𝑣)) → 𝐾:((0[,]1) × (0[,]1))⟶𝐵)
186185ffnd 6669 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟𝑢 ∧ 0 ∈ 𝑣)) → 𝐾 Fn ((0[,]1) × (0[,]1)))
187 fnov 7487 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝐾 Fn ((0[,]1) × (0[,]1)) ↔ 𝐾 = (𝑏 ∈ (0[,]1), 𝑤 ∈ (0[,]1) ↦ (𝑏𝐾𝑤)))
188186, 187sylib 217 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟𝑢 ∧ 0 ∈ 𝑣)) → 𝐾 = (𝑏 ∈ (0[,]1), 𝑤 ∈ (0[,]1) ↦ (𝑏𝐾𝑤)))
189188reseq1d 5936 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟𝑢 ∧ 0 ∈ 𝑣)) → (𝐾 ↾ (𝑢 × {0})) = ((𝑏 ∈ (0[,]1), 𝑤 ∈ (0[,]1) ↦ (𝑏𝐾𝑤)) ↾ (𝑢 × {0})))
190 simplrl 775 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟𝑢 ∧ 0 ∈ 𝑣)) → 𝑢 ∈ II)
191 elssuni 4898 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑢 ∈ II → 𝑢 II)
192191, 13sseqtrrdi 3995 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑢 ∈ II → 𝑢 ⊆ (0[,]1))
193190, 192syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟𝑢 ∧ 0 ∈ 𝑣)) → 𝑢 ⊆ (0[,]1))
194169snssd 4769 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → {0} ⊆ (0[,]1))
195194ad3antrrr 728 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟𝑢 ∧ 0 ∈ 𝑣)) → {0} ⊆ (0[,]1))
196 resmpo 7476 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑢 ⊆ (0[,]1) ∧ {0} ⊆ (0[,]1)) → ((𝑏 ∈ (0[,]1), 𝑤 ∈ (0[,]1) ↦ (𝑏𝐾𝑤)) ↾ (𝑢 × {0})) = (𝑏𝑢, 𝑤 ∈ {0} ↦ (𝑏𝐾𝑤)))
197193, 195, 196syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟𝑢 ∧ 0 ∈ 𝑣)) → ((𝑏 ∈ (0[,]1), 𝑤 ∈ (0[,]1) ↦ (𝑏𝐾𝑤)) ↾ (𝑢 × {0})) = (𝑏𝑢, 𝑤 ∈ {0} ↦ (𝑏𝐾𝑤)))
198193sselda 3944 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((𝜑𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟𝑢 ∧ 0 ∈ 𝑣)) ∧ 𝑏𝑢) → 𝑏 ∈ (0[,]1))
199 simplll 773 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟𝑢 ∧ 0 ∈ 𝑣)) → 𝜑)
2001, 2, 3, 4, 5, 6, 7cvmlift2lem8 33904 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑏 ∈ (0[,]1)) → (𝑏𝐾0) = (𝐻𝑏))
201199, 200sylan 580 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((𝜑𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟𝑢 ∧ 0 ∈ 𝑣)) ∧ 𝑏 ∈ (0[,]1)) → (𝑏𝐾0) = (𝐻𝑏))
202198, 201syldan 591 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝜑𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟𝑢 ∧ 0 ∈ 𝑣)) ∧ 𝑏𝑢) → (𝑏𝐾0) = (𝐻𝑏))
203 elsni 4603 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑤 ∈ {0} → 𝑤 = 0)
204203oveq2d 7373 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑤 ∈ {0} → (𝑏𝐾𝑤) = (𝑏𝐾0))
205204eqeq1d 2738 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑤 ∈ {0} → ((𝑏𝐾𝑤) = (𝐻𝑏) ↔ (𝑏𝐾0) = (𝐻𝑏)))
206202, 205syl5ibrcom 246 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝜑𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟𝑢 ∧ 0 ∈ 𝑣)) ∧ 𝑏𝑢) → (𝑤 ∈ {0} → (𝑏𝐾𝑤) = (𝐻𝑏)))
2072063impia 1117 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟𝑢 ∧ 0 ∈ 𝑣)) ∧ 𝑏𝑢𝑤 ∈ {0}) → (𝑏𝐾𝑤) = (𝐻𝑏))
208207mpoeq3dva 7434 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟𝑢 ∧ 0 ∈ 𝑣)) → (𝑏𝑢, 𝑤 ∈ {0} ↦ (𝑏𝐾𝑤)) = (𝑏𝑢, 𝑤 ∈ {0} ↦ (𝐻𝑏)))
209189, 197, 2083eqtrd 2780 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟𝑢 ∧ 0 ∈ 𝑣)) → (𝐾 ↾ (𝑢 × {0})) = (𝑏𝑢, 𝑤 ∈ {0} ↦ (𝐻𝑏)))
210 eqid 2736 . . . . . . . . . . . . . . . . . . . . . . . . 25 (II ↾t 𝑢) = (II ↾t 𝑢)
211 iitopon 24242 . . . . . . . . . . . . . . . . . . . . . . . . . 26 II ∈ (TopOn‘(0[,]1))
212211a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟𝑢 ∧ 0 ∈ 𝑣)) → II ∈ (TopOn‘(0[,]1)))
213 eqid 2736 . . . . . . . . . . . . . . . . . . . . . . . . 25 (II ↾t {0}) = (II ↾t {0})
214212, 212cnmpt1st 23019 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟𝑢 ∧ 0 ∈ 𝑣)) → (𝑏 ∈ (0[,]1), 𝑤 ∈ (0[,]1) ↦ 𝑏) ∈ ((II ×t II) Cn II))
2151, 2, 3, 4, 5, 6cvmlift2lem2 33898 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → (𝐻 ∈ (II Cn 𝐶) ∧ (𝐹𝐻) = (𝑧 ∈ (0[,]1) ↦ (𝑧𝐺0)) ∧ (𝐻‘0) = 𝑃))
216215simp1d 1142 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑𝐻 ∈ (II Cn 𝐶))
217199, 216syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟𝑢 ∧ 0 ∈ 𝑣)) → 𝐻 ∈ (II Cn 𝐶))
218212, 212, 214, 217cnmpt21f 23023 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟𝑢 ∧ 0 ∈ 𝑣)) → (𝑏 ∈ (0[,]1), 𝑤 ∈ (0[,]1) ↦ (𝐻𝑏)) ∈ ((II ×t II) Cn 𝐶))
219210, 212, 193, 213, 212, 195, 218cnmpt2res 23028 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟𝑢 ∧ 0 ∈ 𝑣)) → (𝑏𝑢, 𝑤 ∈ {0} ↦ (𝐻𝑏)) ∈ (((II ↾t 𝑢) ×t (II ↾t {0})) Cn 𝐶))
220 vex 3449 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑢 ∈ V
221 snex 5388 . . . . . . . . . . . . . . . . . . . . . . . . . 26 {0} ∈ V
222 txrest 22982 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((II ∈ Top ∧ II ∈ Top) ∧ (𝑢 ∈ V ∧ {0} ∈ V)) → ((II ×t II) ↾t (𝑢 × {0})) = ((II ↾t 𝑢) ×t (II ↾t {0})))
22319, 19, 220, 221, 222mp4an 691 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((II ×t II) ↾t (𝑢 × {0})) = ((II ↾t 𝑢) ×t (II ↾t {0}))
224223oveq1i 7367 . . . . . . . . . . . . . . . . . . . . . . . 24 (((II ×t II) ↾t (𝑢 × {0})) Cn 𝐶) = (((II ↾t 𝑢) ×t (II ↾t {0})) Cn 𝐶)
225219, 224eleqtrrdi 2849 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟𝑢 ∧ 0 ∈ 𝑣)) → (𝑏𝑢, 𝑤 ∈ {0} ↦ (𝐻𝑏)) ∈ (((II ×t II) ↾t (𝑢 × {0})) Cn 𝐶))
226209, 225eqeltrd 2838 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟𝑢 ∧ 0 ∈ 𝑣)) → (𝐾 ↾ (𝑢 × {0})) ∈ (((II ×t II) ↾t (𝑢 × {0})) Cn 𝐶))
227 sneq 4596 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑤 = 0 → {𝑤} = {0})
228227xpeq2d 5663 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑤 = 0 → (𝑢 × {𝑤}) = (𝑢 × {0}))
229228reseq2d 5937 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑤 = 0 → (𝐾 ↾ (𝑢 × {𝑤})) = (𝐾 ↾ (𝑢 × {0})))
230228oveq2d 7373 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑤 = 0 → ((II ×t II) ↾t (𝑢 × {𝑤})) = ((II ×t II) ↾t (𝑢 × {0})))
231230oveq1d 7372 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑤 = 0 → (((II ×t II) ↾t (𝑢 × {𝑤})) Cn 𝐶) = (((II ×t II) ↾t (𝑢 × {0})) Cn 𝐶))
232229, 231eleq12d 2832 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑤 = 0 → ((𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II) ↾t (𝑢 × {𝑤})) Cn 𝐶) ↔ (𝐾 ↾ (𝑢 × {0})) ∈ (((II ×t II) ↾t (𝑢 × {0})) Cn 𝐶)))
233232rspcev 3581 . . . . . . . . . . . . . . . . . . . . . 22 ((0 ∈ 𝑣 ∧ (𝐾 ↾ (𝑢 × {0})) ∈ (((II ×t II) ↾t (𝑢 × {0})) Cn 𝐶)) → ∃𝑤𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II) ↾t (𝑢 × {𝑤})) Cn 𝐶))
234184, 226, 233syl2anc 584 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟𝑢 ∧ 0 ∈ 𝑣)) → ∃𝑤𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II) ↾t (𝑢 × {𝑤})) Cn 𝐶))
235 opelxpi 5670 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑟𝑢 ∧ 0 ∈ 𝑣) → ⟨𝑟, 0⟩ ∈ (𝑢 × 𝑣))
236235adantl 482 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟𝑢 ∧ 0 ∈ 𝑣)) → ⟨𝑟, 0⟩ ∈ (𝑢 × 𝑣))
237 simplrr 776 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟𝑢 ∧ 0 ∈ 𝑣)) → 𝑣 ∈ II)
238237, 145syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟𝑢 ∧ 0 ∈ 𝑣)) → 𝑣 ⊆ (0[,]1))
239 xpss12 5648 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑢 ⊆ (0[,]1) ∧ 𝑣 ⊆ (0[,]1)) → (𝑢 × 𝑣) ⊆ ((0[,]1) × (0[,]1)))
240193, 238, 239syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟𝑢 ∧ 0 ∈ 𝑣)) → (𝑢 × 𝑣) ⊆ ((0[,]1) × (0[,]1)))
24136restuni 22513 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((II ×t II) ∈ Top ∧ (𝑢 × 𝑣) ⊆ ((0[,]1) × (0[,]1))) → (𝑢 × 𝑣) = ((II ×t II) ↾t (𝑢 × 𝑣)))
24221, 240, 241sylancr 587 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟𝑢 ∧ 0 ∈ 𝑣)) → (𝑢 × 𝑣) = ((II ×t II) ↾t (𝑢 × 𝑣)))
243236, 242eleqtrd 2840 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟𝑢 ∧ 0 ∈ 𝑣)) → ⟨𝑟, 0⟩ ∈ ((II ×t II) ↾t (𝑢 × 𝑣)))
244 eqid 2736 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((II ×t II) ↾t (𝑢 × 𝑣)) = ((II ×t II) ↾t (𝑢 × 𝑣))
245244cncnpi 22629 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II) ↾t (𝑢 × 𝑣)) Cn 𝐶) ∧ ⟨𝑟, 0⟩ ∈ ((II ×t II) ↾t (𝑢 × 𝑣))) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ ((((II ×t II) ↾t (𝑢 × 𝑣)) CnP 𝐶)‘⟨𝑟, 0⟩))
246245expcom 414 . . . . . . . . . . . . . . . . . . . . . . 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⟩)))
24821a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟𝑢 ∧ 0 ∈ 𝑣)) → (II ×t II) ∈ Top)
24919a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟𝑢 ∧ 0 ∈ 𝑣)) → II ∈ Top)
250249, 249, 190, 237, 53syl22anc 837 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟𝑢 ∧ 0 ∈ 𝑣)) → (𝑢 × 𝑣) ∈ (II ×t II))
251 isopn3i 22433 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((II ×t II) ∈ Top ∧ (𝑢 × 𝑣) ∈ (II ×t II)) → ((int‘(II ×t II))‘(𝑢 × 𝑣)) = (𝑢 × 𝑣))
25221, 250, 251sylancr 587 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟𝑢 ∧ 0 ∈ 𝑣)) → ((int‘(II ×t II))‘(𝑢 × 𝑣)) = (𝑢 × 𝑣))
253236, 252eleqtrrd 2841 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟𝑢 ∧ 0 ∈ 𝑣)) → ⟨𝑟, 0⟩ ∈ ((int‘(II ×t II))‘(𝑢 × 𝑣)))
25436, 1cnprest 22640 . . . . . . . . . . . . . . . . . . . . . . 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 837 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) ∧ (𝑟𝑢 ∧ 0 ∈ 𝑣)) → (𝐾 ∈ (((II ×t II) CnP 𝐶)‘⟨𝑟, 0⟩) ↔ (𝐾 ↾ (𝑢 × 𝑣)) ∈ ((((II ×t II) ↾t (𝑢 × 𝑣)) CnP 𝐶)‘⟨𝑟, 0⟩)))
256247, 255sylibrd 258 . . . . . . . . . . . . . . . . . . . . 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 454 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) → (((𝑟𝑢 ∧ 0 ∈ 𝑣) ∧ (∃𝑤𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II) ↾t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II) ↾t (𝑢 × 𝑣)) Cn 𝐶))) → 𝐾 ∈ (((II ×t II) CnP 𝐶)‘⟨𝑟, 0⟩)))
259183, 258biimtrid 241 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑟 ∈ (0[,]1)) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) → ((𝑟𝑢 ∧ 0 ∈ 𝑣 ∧ (∃𝑤𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II) ↾t (𝑢 × {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II) ↾t (𝑢 × 𝑣)) Cn 𝐶))) → 𝐾 ∈ (((II ×t II) CnP 𝐶)‘⟨𝑟, 0⟩)))
260259rexlimdvva 3205 . . . . . . . . . . . . . . . . 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 6842 . . . . . . . . . . . . . . . . . 18 (𝑧 = ⟨𝑟, 0⟩ → (((II ×t II) CnP 𝐶)‘𝑧) = (((II ×t II) CnP 𝐶)‘⟨𝑟, 0⟩))
263262eleq2d 2823 . . . . . . . . . . . . . . . . 17 (𝑧 = ⟨𝑟, 0⟩ → (𝐾 ∈ (((II ×t II) CnP 𝐶)‘𝑧) ↔ 𝐾 ∈ (((II ×t II) CnP 𝐶)‘⟨𝑟, 0⟩)))
264263, 68elrab2 3648 . . . . . . . . . . . . . . . 16 (⟨𝑟, 0⟩ ∈ 𝑀 ↔ (⟨𝑟, 0⟩ ∈ ((0[,]1) × (0[,]1)) ∧ 𝐾 ∈ (((II ×t II) CnP 𝐶)‘⟨𝑟, 0⟩)))
265175, 261, 264sylanbrc 583 . . . . . . . . . . . . . . 15 ((𝜑𝑟 ∈ (0[,]1)) → ⟨𝑟, 0⟩ ∈ 𝑀)
266 elsni 4603 . . . . . . . . . . . . . . . . 17 (𝑎 ∈ {0} → 𝑎 = 0)
267266opeq2d 4837 . . . . . . . . . . . . . . . 16 (𝑎 ∈ {0} → ⟨𝑟, 𝑎⟩ = ⟨𝑟, 0⟩)
268267eleq1d 2822 . . . . . . . . . . . . . . 15 (𝑎 ∈ {0} → (⟨𝑟, 𝑎⟩ ∈ 𝑀 ↔ ⟨𝑟, 0⟩ ∈ 𝑀))
269265, 268syl5ibrcom 246 . . . . . . . . . . . . . 14 ((𝜑𝑟 ∈ (0[,]1)) → (𝑎 ∈ {0} → ⟨𝑟, 𝑎⟩ ∈ 𝑀))
270269expimpd 454 . . . . . . . . . . . . 13 (𝜑 → ((𝑟 ∈ (0[,]1) ∧ 𝑎 ∈ {0}) → ⟨𝑟, 𝑎⟩ ∈ 𝑀))
271172, 270biimtrid 241 . . . . . . . . . . . 12 (𝜑 → (⟨𝑟, 𝑎⟩ ∈ ((0[,]1) × {0}) → ⟨𝑟, 𝑎⟩ ∈ 𝑀))
272171, 271relssdv 5744 . . . . . . . . . . 11 (𝜑 → ((0[,]1) × {0}) ⊆ 𝑀)
273 sneq 4596 . . . . . . . . . . . . . 14 (𝑎 = 0 → {𝑎} = {0})
274273xpeq2d 5663 . . . . . . . . . . . . 13 (𝑎 = 0 → ((0[,]1) × {𝑎}) = ((0[,]1) × {0}))
275274sseq1d 3975 . . . . . . . . . . . 12 (𝑎 = 0 → (((0[,]1) × {𝑎}) ⊆ 𝑀 ↔ ((0[,]1) × {0}) ⊆ 𝑀))
276275, 140elrab2 3648 . . . . . . . . . . 11 (0 ∈ 𝐴 ↔ (0 ∈ (0[,]1) ∧ ((0[,]1) × {0}) ⊆ 𝑀))
277169, 272, 276sylanbrc 583 . . . . . . . . . 10 (𝜑 → 0 ∈ 𝐴)
278277ne0d 4295 . . . . . . . . 9 (𝜑𝐴 ≠ ∅)
279 inss2 4189 . . . . . . . . . 10 (II ∩ (Clsd‘II)) ⊆ (Clsd‘II)
280279, 166sselid 3942 . . . . . . . . 9 (𝜑𝐴 ∈ (Clsd‘II))
28113, 15, 167, 278, 280connclo 22766 . . . . . . . 8 (𝜑𝐴 = (0[,]1))
282281, 140eqtr3di 2791 . . . . . . 7 (𝜑 → (0[,]1) = {𝑎 ∈ (0[,]1) ∣ ((0[,]1) × {𝑎}) ⊆ 𝑀})
283 rabid2 3436 . . . . . . 7 ((0[,]1) = {𝑎 ∈ (0[,]1) ∣ ((0[,]1) × {𝑎}) ⊆ 𝑀} ↔ ∀𝑎 ∈ (0[,]1)((0[,]1) × {𝑎}) ⊆ 𝑀)
284282, 283sylib 217 . . . . . 6 (𝜑 → ∀𝑎 ∈ (0[,]1)((0[,]1) × {𝑎}) ⊆ 𝑀)
285 iunss 5005 . . . . . 6 ( 𝑎 ∈ (0[,]1)((0[,]1) × {𝑎}) ⊆ 𝑀 ↔ ∀𝑎 ∈ (0[,]1)((0[,]1) × {𝑎}) ⊆ 𝑀)
286284, 285sylibr 233 . . . . 5 (𝜑 𝑎 ∈ (0[,]1)((0[,]1) × {𝑎}) ⊆ 𝑀)
28712, 286eqsstrid 3992 . . . 4 (𝜑 → ((0[,]1) × (0[,]1)) ⊆ 𝑀)
288287, 68sseqtrdi 3994 . . 3 (𝜑 → ((0[,]1) × (0[,]1)) ⊆ {𝑧 ∈ ((0[,]1) × (0[,]1)) ∣ 𝐾 ∈ (((II ×t II) CnP 𝐶)‘𝑧)})
289 ssrab 4030 . . . 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 497 . . 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 22942 . . . 4 ((II ∈ (TopOn‘(0[,]1)) ∧ II ∈ (TopOn‘(0[,]1))) → (II ×t II) ∈ (TopOn‘((0[,]1) × (0[,]1))))
293211, 211, 292mp2an 690 . . 3 (II ×t II) ∈ (TopOn‘((0[,]1) × (0[,]1)))
294 cvmtop1 33854 . . . . 5 (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐶 ∈ Top)
2952, 294syl 17 . . . 4 (𝜑𝐶 ∈ Top)
2961toptopon 22266 . . . 4 (𝐶 ∈ Top ↔ 𝐶 ∈ (TopOn‘𝐵))
297295, 296sylib 217 . . 3 (𝜑𝐶 ∈ (TopOn‘𝐵))
298 cncnp 22631 . . 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 587 . 2 (𝜑 → (𝐾 ∈ ((II ×t II) Cn 𝐶) ↔ (𝐾:((0[,]1) × (0[,]1))⟶𝐵 ∧ ∀𝑧 ∈ ((0[,]1) × (0[,]1))𝐾 ∈ (((II ×t II) CnP 𝐶)‘𝑧))))
3008, 291, 299mpbir2and 711 1 (𝜑𝐾 ∈ ((II ×t II) Cn 𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396  w3a 1087  wal 1539   = wceq 1541  wcel 2106  wral 3064  wrex 3073  {crab 3407  Vcvv 3445  cdif 3907  cin 3909  wss 3910  c0 4282  𝒫 cpw 4560  {csn 4586  cop 4592   cuni 4865   ciun 4954  {copab 5167  cmpt 5188   × cxp 5631  ccnv 5632  cres 5635  cima 5636  ccom 5637  Rel wrel 5638   Fn wfn 6491  wf 6492  cfv 6496  crio 7312  (class class class)co 7357  cmpo 7359  0cc0 11051  1c1 11052  [,]cicc 13267  t crest 17302  Topctop 22242  TopOnctopon 22259  Clsdccld 22367  intcnt 22368  neicnei 22448   Cn ccn 22575   CnP ccnp 22576  Compccmp 22737  Conncconn 22762   ×t ctx 22911  Homeochmeo 23104  IIcii 24238   CovMap ccvm 33849
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672  ax-inf2 9577  ax-cnex 11107  ax-resscn 11108  ax-1cn 11109  ax-icn 11110  ax-addcl 11111  ax-addrcl 11112  ax-mulcl 11113  ax-mulrcl 11114  ax-mulcom 11115  ax-addass 11116  ax-mulass 11117  ax-distr 11118  ax-i2m1 11119  ax-1ne0 11120  ax-1rid 11121  ax-rnegex 11122  ax-rrecex 11123  ax-cnre 11124  ax-pre-lttri 11125  ax-pre-lttrn 11126  ax-pre-ltadd 11127  ax-pre-mulgt0 11128  ax-pre-sup 11129  ax-addf 11130  ax-mulf 11131
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3065  df-rex 3074  df-rmo 3353  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-tp 4591  df-op 4593  df-uni 4866  df-int 4908  df-iun 4956  df-iin 4957  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-se 5589  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-isom 6505  df-riota 7313  df-ov 7360  df-oprab 7361  df-mpo 7362  df-of 7617  df-om 7803  df-1st 7921  df-2nd 7922  df-supp 8093  df-frecs 8212  df-wrecs 8243  df-recs 8317  df-rdg 8356  df-1o 8412  df-2o 8413  df-er 8648  df-ec 8650  df-map 8767  df-ixp 8836  df-en 8884  df-dom 8885  df-sdom 8886  df-fin 8887  df-fsupp 9306  df-fi 9347  df-sup 9378  df-inf 9379  df-oi 9446  df-card 9875  df-pnf 11191  df-mnf 11192  df-xr 11193  df-ltxr 11194  df-le 11195  df-sub 11387  df-neg 11388  df-div 11813  df-nn 12154  df-2 12216  df-3 12217  df-4 12218  df-5 12219  df-6 12220  df-7 12221  df-8 12222  df-9 12223  df-n0 12414  df-z 12500  df-dec 12619  df-uz 12764  df-q 12874  df-rp 12916  df-xneg 13033  df-xadd 13034  df-xmul 13035  df-ioo 13268  df-ico 13270  df-icc 13271  df-fz 13425  df-fzo 13568  df-fl 13697  df-seq 13907  df-exp 13968  df-hash 14231  df-cj 14984  df-re 14985  df-im 14986  df-sqrt 15120  df-abs 15121  df-clim 15370  df-sum 15571  df-struct 17019  df-sets 17036  df-slot 17054  df-ndx 17066  df-base 17084  df-ress 17113  df-plusg 17146  df-mulr 17147  df-starv 17148  df-sca 17149  df-vsca 17150  df-ip 17151  df-tset 17152  df-ple 17153  df-ds 17155  df-unif 17156  df-hom 17157  df-cco 17158  df-rest 17304  df-topn 17305  df-0g 17323  df-gsum 17324  df-topgen 17325  df-pt 17326  df-prds 17329  df-xrs 17384  df-qtop 17389  df-imas 17390  df-xps 17392  df-mre 17466  df-mrc 17467  df-acs 17469  df-mgm 18497  df-sgrp 18546  df-mnd 18557  df-submnd 18602  df-mulg 18873  df-cntz 19097  df-cmn 19564  df-psmet 20788  df-xmet 20789  df-met 20790  df-bl 20791  df-mopn 20792  df-cnfld 20797  df-top 22243  df-topon 22260  df-topsp 22282  df-bases 22296  df-cld 22370  df-ntr 22371  df-cls 22372  df-nei 22449  df-cn 22578  df-cnp 22579  df-cmp 22738  df-conn 22763  df-lly 22817  df-nlly 22818  df-tx 22913  df-hmeo 23106  df-xms 23673  df-ms 23674  df-tms 23675  df-ii 24240  df-htpy 24333  df-phtpy 24334  df-phtpc 24355  df-pconn 33815  df-sconn 33816  df-cvm 33850
This theorem is referenced by:  cvmlift2lem13  33909
  Copyright terms: Public domain W3C validator