MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  lmss Structured version   Visualization version   GIF version

Theorem lmss 21903
Description: Limit on a subspace. (Contributed by NM, 30-Jan-2008.) (Revised by Mario Carneiro, 30-Dec-2013.)
Hypotheses
Ref Expression
lmss.1 𝐾 = (𝐽t 𝑌)
lmss.2 𝑍 = (ℤ𝑀)
lmss.3 (𝜑𝑌𝑉)
lmss.4 (𝜑𝐽 ∈ Top)
lmss.5 (𝜑𝑃𝑌)
lmss.6 (𝜑𝑀 ∈ ℤ)
lmss.7 (𝜑𝐹:𝑍𝑌)
Assertion
Ref Expression
lmss (𝜑 → (𝐹(⇝𝑡𝐽)𝑃𝐹(⇝𝑡𝐾)𝑃))

Proof of Theorem lmss
Dummy variables 𝑗 𝑘 𝑢 𝑣 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 lmss.4 . . . . . 6 (𝜑𝐽 ∈ Top)
2 toptopon2 21523 . . . . . 6 (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘ 𝐽))
31, 2sylib 221 . . . . 5 (𝜑𝐽 ∈ (TopOn‘ 𝐽))
4 lmcl 21902 . . . . 5 ((𝐽 ∈ (TopOn‘ 𝐽) ∧ 𝐹(⇝𝑡𝐽)𝑃) → 𝑃 𝐽)
53, 4sylan 583 . . . 4 ((𝜑𝐹(⇝𝑡𝐽)𝑃) → 𝑃 𝐽)
6 lmfss 21901 . . . . . . 7 ((𝐽 ∈ (TopOn‘ 𝐽) ∧ 𝐹(⇝𝑡𝐽)𝑃) → 𝐹 ⊆ (ℂ × 𝐽))
73, 6sylan 583 . . . . . 6 ((𝜑𝐹(⇝𝑡𝐽)𝑃) → 𝐹 ⊆ (ℂ × 𝐽))
8 rnss 5773 . . . . . 6 (𝐹 ⊆ (ℂ × 𝐽) → ran 𝐹 ⊆ ran (ℂ × 𝐽))
97, 8syl 17 . . . . 5 ((𝜑𝐹(⇝𝑡𝐽)𝑃) → ran 𝐹 ⊆ ran (ℂ × 𝐽))
10 rnxpss 5996 . . . . 5 ran (ℂ × 𝐽) ⊆ 𝐽
119, 10sstrdi 3927 . . . 4 ((𝜑𝐹(⇝𝑡𝐽)𝑃) → ran 𝐹 𝐽)
125, 11jca 515 . . 3 ((𝜑𝐹(⇝𝑡𝐽)𝑃) → (𝑃 𝐽 ∧ ran 𝐹 𝐽))
1312ex 416 . 2 (𝜑 → (𝐹(⇝𝑡𝐽)𝑃 → (𝑃 𝐽 ∧ ran 𝐹 𝐽)))
14 lmss.1 . . . . . . 7 𝐾 = (𝐽t 𝑌)
15 lmss.3 . . . . . . . 8 (𝜑𝑌𝑉)
16 resttopon2 21773 . . . . . . . 8 ((𝐽 ∈ (TopOn‘ 𝐽) ∧ 𝑌𝑉) → (𝐽t 𝑌) ∈ (TopOn‘(𝑌 𝐽)))
173, 15, 16syl2anc 587 . . . . . . 7 (𝜑 → (𝐽t 𝑌) ∈ (TopOn‘(𝑌 𝐽)))
1814, 17eqeltrid 2894 . . . . . 6 (𝜑𝐾 ∈ (TopOn‘(𝑌 𝐽)))
19 lmcl 21902 . . . . . 6 ((𝐾 ∈ (TopOn‘(𝑌 𝐽)) ∧ 𝐹(⇝𝑡𝐾)𝑃) → 𝑃 ∈ (𝑌 𝐽))
2018, 19sylan 583 . . . . 5 ((𝜑𝐹(⇝𝑡𝐾)𝑃) → 𝑃 ∈ (𝑌 𝐽))
2120elin2d 4126 . . . 4 ((𝜑𝐹(⇝𝑡𝐾)𝑃) → 𝑃 𝐽)
22 lmfss 21901 . . . . . . . 8 ((𝐾 ∈ (TopOn‘(𝑌 𝐽)) ∧ 𝐹(⇝𝑡𝐾)𝑃) → 𝐹 ⊆ (ℂ × (𝑌 𝐽)))
2318, 22sylan 583 . . . . . . 7 ((𝜑𝐹(⇝𝑡𝐾)𝑃) → 𝐹 ⊆ (ℂ × (𝑌 𝐽)))
24 rnss 5773 . . . . . . 7 (𝐹 ⊆ (ℂ × (𝑌 𝐽)) → ran 𝐹 ⊆ ran (ℂ × (𝑌 𝐽)))
2523, 24syl 17 . . . . . 6 ((𝜑𝐹(⇝𝑡𝐾)𝑃) → ran 𝐹 ⊆ ran (ℂ × (𝑌 𝐽)))
26 rnxpss 5996 . . . . . 6 ran (ℂ × (𝑌 𝐽)) ⊆ (𝑌 𝐽)
2725, 26sstrdi 3927 . . . . 5 ((𝜑𝐹(⇝𝑡𝐾)𝑃) → ran 𝐹 ⊆ (𝑌 𝐽))
28 inss2 4156 . . . . 5 (𝑌 𝐽) ⊆ 𝐽
2927, 28sstrdi 3927 . . . 4 ((𝜑𝐹(⇝𝑡𝐾)𝑃) → ran 𝐹 𝐽)
3021, 29jca 515 . . 3 ((𝜑𝐹(⇝𝑡𝐾)𝑃) → (𝑃 𝐽 ∧ ran 𝐹 𝐽))
3130ex 416 . 2 (𝜑 → (𝐹(⇝𝑡𝐾)𝑃 → (𝑃 𝐽 ∧ ran 𝐹 𝐽)))
32 simprl 770 . . . . . 6 ((𝜑 ∧ (𝑃 𝐽 ∧ ran 𝐹 𝐽)) → 𝑃 𝐽)
33 lmss.5 . . . . . . . 8 (𝜑𝑃𝑌)
3433adantr 484 . . . . . . 7 ((𝜑 ∧ (𝑃 𝐽 ∧ ran 𝐹 𝐽)) → 𝑃𝑌)
3534, 32elind 4121 . . . . . 6 ((𝜑 ∧ (𝑃 𝐽 ∧ ran 𝐹 𝐽)) → 𝑃 ∈ (𝑌 𝐽))
3632, 352thd 268 . . . . 5 ((𝜑 ∧ (𝑃 𝐽 ∧ ran 𝐹 𝐽)) → (𝑃 𝐽𝑃 ∈ (𝑌 𝐽)))
3714eleq2i 2881 . . . . . . . . 9 (𝑣𝐾𝑣 ∈ (𝐽t 𝑌))
381adantr 484 . . . . . . . . . . 11 ((𝜑 ∧ (𝑃 𝐽 ∧ ran 𝐹 𝐽)) → 𝐽 ∈ Top)
3915adantr 484 . . . . . . . . . . 11 ((𝜑 ∧ (𝑃 𝐽 ∧ ran 𝐹 𝐽)) → 𝑌𝑉)
40 elrest 16693 . . . . . . . . . . 11 ((𝐽 ∈ Top ∧ 𝑌𝑉) → (𝑣 ∈ (𝐽t 𝑌) ↔ ∃𝑢𝐽 𝑣 = (𝑢𝑌)))
4138, 39, 40syl2anc 587 . . . . . . . . . 10 ((𝜑 ∧ (𝑃 𝐽 ∧ ran 𝐹 𝐽)) → (𝑣 ∈ (𝐽t 𝑌) ↔ ∃𝑢𝐽 𝑣 = (𝑢𝑌)))
4241biimpa 480 . . . . . . . . 9 (((𝜑 ∧ (𝑃 𝐽 ∧ ran 𝐹 𝐽)) ∧ 𝑣 ∈ (𝐽t 𝑌)) → ∃𝑢𝐽 𝑣 = (𝑢𝑌))
4337, 42sylan2b 596 . . . . . . . 8 (((𝜑 ∧ (𝑃 𝐽 ∧ ran 𝐹 𝐽)) ∧ 𝑣𝐾) → ∃𝑢𝐽 𝑣 = (𝑢𝑌))
44 r19.29r 3217 . . . . . . . . . 10 ((∃𝑢𝐽 𝑣 = (𝑢𝑌) ∧ ∀𝑢𝐽 (𝑃𝑢 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ 𝑢)) → ∃𝑢𝐽 (𝑣 = (𝑢𝑌) ∧ (𝑃𝑢 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ 𝑢)))
4534biantrud 535 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑃 𝐽 ∧ ran 𝐹 𝐽)) → (𝑃𝑢 ↔ (𝑃𝑢𝑃𝑌)))
46 elin 3897 . . . . . . . . . . . . . . . . 17 (𝑃 ∈ (𝑢𝑌) ↔ (𝑃𝑢𝑃𝑌))
4745, 46syl6bbr 292 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑃 𝐽 ∧ ran 𝐹 𝐽)) → (𝑃𝑢𝑃 ∈ (𝑢𝑌)))
48 lmss.2 . . . . . . . . . . . . . . . . . . . . 21 𝑍 = (ℤ𝑀)
4948uztrn2 12250 . . . . . . . . . . . . . . . . . . . 20 ((𝑗𝑍𝑘 ∈ (ℤ𝑗)) → 𝑘𝑍)
50 lmss.7 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝐹:𝑍𝑌)
5150adantr 484 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑃 𝐽 ∧ ran 𝐹 𝐽)) → 𝐹:𝑍𝑌)
5251ffvelrnda 6828 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ (𝑃 𝐽 ∧ ran 𝐹 𝐽)) ∧ 𝑘𝑍) → (𝐹𝑘) ∈ 𝑌)
5352biantrud 535 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑃 𝐽 ∧ ran 𝐹 𝐽)) ∧ 𝑘𝑍) → ((𝐹𝑘) ∈ 𝑢 ↔ ((𝐹𝑘) ∈ 𝑢 ∧ (𝐹𝑘) ∈ 𝑌)))
54 elin 3897 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹𝑘) ∈ (𝑢𝑌) ↔ ((𝐹𝑘) ∈ 𝑢 ∧ (𝐹𝑘) ∈ 𝑌))
5553, 54syl6bbr 292 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑃 𝐽 ∧ ran 𝐹 𝐽)) ∧ 𝑘𝑍) → ((𝐹𝑘) ∈ 𝑢 ↔ (𝐹𝑘) ∈ (𝑢𝑌)))
5649, 55sylan2 595 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑃 𝐽 ∧ ran 𝐹 𝐽)) ∧ (𝑗𝑍𝑘 ∈ (ℤ𝑗))) → ((𝐹𝑘) ∈ 𝑢 ↔ (𝐹𝑘) ∈ (𝑢𝑌)))
5756anassrs 471 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝑃 𝐽 ∧ ran 𝐹 𝐽)) ∧ 𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) → ((𝐹𝑘) ∈ 𝑢 ↔ (𝐹𝑘) ∈ (𝑢𝑌)))
5857ralbidva 3161 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑃 𝐽 ∧ ran 𝐹 𝐽)) ∧ 𝑗𝑍) → (∀𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ 𝑢 ↔ ∀𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ (𝑢𝑌)))
5958rexbidva 3255 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑃 𝐽 ∧ ran 𝐹 𝐽)) → (∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ 𝑢 ↔ ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ (𝑢𝑌)))
6047, 59imbi12d 348 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑃 𝐽 ∧ ran 𝐹 𝐽)) → ((𝑃𝑢 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ 𝑢) ↔ (𝑃 ∈ (𝑢𝑌) → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ (𝑢𝑌))))
6160adantr 484 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑃 𝐽 ∧ ran 𝐹 𝐽)) ∧ 𝑢𝐽) → ((𝑃𝑢 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ 𝑢) ↔ (𝑃 ∈ (𝑢𝑌) → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ (𝑢𝑌))))
6261biimpd 232 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑃 𝐽 ∧ ran 𝐹 𝐽)) ∧ 𝑢𝐽) → ((𝑃𝑢 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ 𝑢) → (𝑃 ∈ (𝑢𝑌) → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ (𝑢𝑌))))
63 eleq2 2878 . . . . . . . . . . . . . . 15 (𝑣 = (𝑢𝑌) → (𝑃𝑣𝑃 ∈ (𝑢𝑌)))
64 eleq2 2878 . . . . . . . . . . . . . . . 16 (𝑣 = (𝑢𝑌) → ((𝐹𝑘) ∈ 𝑣 ↔ (𝐹𝑘) ∈ (𝑢𝑌)))
6564rexralbidv 3260 . . . . . . . . . . . . . . 15 (𝑣 = (𝑢𝑌) → (∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ 𝑣 ↔ ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ (𝑢𝑌)))
6663, 65imbi12d 348 . . . . . . . . . . . . . 14 (𝑣 = (𝑢𝑌) → ((𝑃𝑣 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ 𝑣) ↔ (𝑃 ∈ (𝑢𝑌) → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ (𝑢𝑌))))
6766imbi2d 344 . . . . . . . . . . . . 13 (𝑣 = (𝑢𝑌) → (((𝑃𝑢 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ 𝑢) → (𝑃𝑣 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ 𝑣)) ↔ ((𝑃𝑢 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ 𝑢) → (𝑃 ∈ (𝑢𝑌) → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ (𝑢𝑌)))))
6862, 67syl5ibrcom 250 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑃 𝐽 ∧ ran 𝐹 𝐽)) ∧ 𝑢𝐽) → (𝑣 = (𝑢𝑌) → ((𝑃𝑢 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ 𝑢) → (𝑃𝑣 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ 𝑣))))
6968impd 414 . . . . . . . . . . 11 (((𝜑 ∧ (𝑃 𝐽 ∧ ran 𝐹 𝐽)) ∧ 𝑢𝐽) → ((𝑣 = (𝑢𝑌) ∧ (𝑃𝑢 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ 𝑢)) → (𝑃𝑣 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ 𝑣)))
7069rexlimdva 3243 . . . . . . . . . 10 ((𝜑 ∧ (𝑃 𝐽 ∧ ran 𝐹 𝐽)) → (∃𝑢𝐽 (𝑣 = (𝑢𝑌) ∧ (𝑃𝑢 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ 𝑢)) → (𝑃𝑣 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ 𝑣)))
7144, 70syl5 34 . . . . . . . . 9 ((𝜑 ∧ (𝑃 𝐽 ∧ ran 𝐹 𝐽)) → ((∃𝑢𝐽 𝑣 = (𝑢𝑌) ∧ ∀𝑢𝐽 (𝑃𝑢 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ 𝑢)) → (𝑃𝑣 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ 𝑣)))
7271expdimp 456 . . . . . . . 8 (((𝜑 ∧ (𝑃 𝐽 ∧ ran 𝐹 𝐽)) ∧ ∃𝑢𝐽 𝑣 = (𝑢𝑌)) → (∀𝑢𝐽 (𝑃𝑢 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ 𝑢) → (𝑃𝑣 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ 𝑣)))
7343, 72syldan 594 . . . . . . 7 (((𝜑 ∧ (𝑃 𝐽 ∧ ran 𝐹 𝐽)) ∧ 𝑣𝐾) → (∀𝑢𝐽 (𝑃𝑢 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ 𝑢) → (𝑃𝑣 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ 𝑣)))
7473ralrimdva 3154 . . . . . 6 ((𝜑 ∧ (𝑃 𝐽 ∧ ran 𝐹 𝐽)) → (∀𝑢𝐽 (𝑃𝑢 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ 𝑢) → ∀𝑣𝐾 (𝑃𝑣 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ 𝑣)))
7538adantr 484 . . . . . . . . . . 11 (((𝜑 ∧ (𝑃 𝐽 ∧ ran 𝐹 𝐽)) ∧ 𝑢𝐽) → 𝐽 ∈ Top)
7639adantr 484 . . . . . . . . . . 11 (((𝜑 ∧ (𝑃 𝐽 ∧ ran 𝐹 𝐽)) ∧ 𝑢𝐽) → 𝑌𝑉)
77 simpr 488 . . . . . . . . . . 11 (((𝜑 ∧ (𝑃 𝐽 ∧ ran 𝐹 𝐽)) ∧ 𝑢𝐽) → 𝑢𝐽)
78 elrestr 16694 . . . . . . . . . . 11 ((𝐽 ∈ Top ∧ 𝑌𝑉𝑢𝐽) → (𝑢𝑌) ∈ (𝐽t 𝑌))
7975, 76, 77, 78syl3anc 1368 . . . . . . . . . 10 (((𝜑 ∧ (𝑃 𝐽 ∧ ran 𝐹 𝐽)) ∧ 𝑢𝐽) → (𝑢𝑌) ∈ (𝐽t 𝑌))
8079, 14eleqtrrdi 2901 . . . . . . . . 9 (((𝜑 ∧ (𝑃 𝐽 ∧ ran 𝐹 𝐽)) ∧ 𝑢𝐽) → (𝑢𝑌) ∈ 𝐾)
8166rspcv 3566 . . . . . . . . 9 ((𝑢𝑌) ∈ 𝐾 → (∀𝑣𝐾 (𝑃𝑣 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ 𝑣) → (𝑃 ∈ (𝑢𝑌) → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ (𝑢𝑌))))
8280, 81syl 17 . . . . . . . 8 (((𝜑 ∧ (𝑃 𝐽 ∧ ran 𝐹 𝐽)) ∧ 𝑢𝐽) → (∀𝑣𝐾 (𝑃𝑣 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ 𝑣) → (𝑃 ∈ (𝑢𝑌) → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ (𝑢𝑌))))
8382, 61sylibrd 262 . . . . . . 7 (((𝜑 ∧ (𝑃 𝐽 ∧ ran 𝐹 𝐽)) ∧ 𝑢𝐽) → (∀𝑣𝐾 (𝑃𝑣 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ 𝑣) → (𝑃𝑢 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ 𝑢)))
8483ralrimdva 3154 . . . . . 6 ((𝜑 ∧ (𝑃 𝐽 ∧ ran 𝐹 𝐽)) → (∀𝑣𝐾 (𝑃𝑣 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ 𝑣) → ∀𝑢𝐽 (𝑃𝑢 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ 𝑢)))
8574, 84impbid 215 . . . . 5 ((𝜑 ∧ (𝑃 𝐽 ∧ ran 𝐹 𝐽)) → (∀𝑢𝐽 (𝑃𝑢 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ 𝑢) ↔ ∀𝑣𝐾 (𝑃𝑣 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ 𝑣)))
8636, 85anbi12d 633 . . . 4 ((𝜑 ∧ (𝑃 𝐽 ∧ ran 𝐹 𝐽)) → ((𝑃 𝐽 ∧ ∀𝑢𝐽 (𝑃𝑢 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ 𝑢)) ↔ (𝑃 ∈ (𝑌 𝐽) ∧ ∀𝑣𝐾 (𝑃𝑣 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ 𝑣))))
8738, 2sylib 221 . . . . 5 ((𝜑 ∧ (𝑃 𝐽 ∧ ran 𝐹 𝐽)) → 𝐽 ∈ (TopOn‘ 𝐽))
88 lmss.6 . . . . . 6 (𝜑𝑀 ∈ ℤ)
8988adantr 484 . . . . 5 ((𝜑 ∧ (𝑃 𝐽 ∧ ran 𝐹 𝐽)) → 𝑀 ∈ ℤ)
9051ffnd 6488 . . . . . 6 ((𝜑 ∧ (𝑃 𝐽 ∧ ran 𝐹 𝐽)) → 𝐹 Fn 𝑍)
91 simprr 772 . . . . . 6 ((𝜑 ∧ (𝑃 𝐽 ∧ ran 𝐹 𝐽)) → ran 𝐹 𝐽)
92 df-f 6328 . . . . . 6 (𝐹:𝑍 𝐽 ↔ (𝐹 Fn 𝑍 ∧ ran 𝐹 𝐽))
9390, 91, 92sylanbrc 586 . . . . 5 ((𝜑 ∧ (𝑃 𝐽 ∧ ran 𝐹 𝐽)) → 𝐹:𝑍 𝐽)
94 eqidd 2799 . . . . 5 (((𝜑 ∧ (𝑃 𝐽 ∧ ran 𝐹 𝐽)) ∧ 𝑘𝑍) → (𝐹𝑘) = (𝐹𝑘))
9587, 48, 89, 93, 94lmbrf 21865 . . . 4 ((𝜑 ∧ (𝑃 𝐽 ∧ ran 𝐹 𝐽)) → (𝐹(⇝𝑡𝐽)𝑃 ↔ (𝑃 𝐽 ∧ ∀𝑢𝐽 (𝑃𝑢 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ 𝑢))))
9618adantr 484 . . . . 5 ((𝜑 ∧ (𝑃 𝐽 ∧ ran 𝐹 𝐽)) → 𝐾 ∈ (TopOn‘(𝑌 𝐽)))
9751frnd 6494 . . . . . . 7 ((𝜑 ∧ (𝑃 𝐽 ∧ ran 𝐹 𝐽)) → ran 𝐹𝑌)
9897, 91ssind 4159 . . . . . 6 ((𝜑 ∧ (𝑃 𝐽 ∧ ran 𝐹 𝐽)) → ran 𝐹 ⊆ (𝑌 𝐽))
99 df-f 6328 . . . . . 6 (𝐹:𝑍⟶(𝑌 𝐽) ↔ (𝐹 Fn 𝑍 ∧ ran 𝐹 ⊆ (𝑌 𝐽)))
10090, 98, 99sylanbrc 586 . . . . 5 ((𝜑 ∧ (𝑃 𝐽 ∧ ran 𝐹 𝐽)) → 𝐹:𝑍⟶(𝑌 𝐽))
10196, 48, 89, 100, 94lmbrf 21865 . . . 4 ((𝜑 ∧ (𝑃 𝐽 ∧ ran 𝐹 𝐽)) → (𝐹(⇝𝑡𝐾)𝑃 ↔ (𝑃 ∈ (𝑌 𝐽) ∧ ∀𝑣𝐾 (𝑃𝑣 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ 𝑣))))
10286, 95, 1013bitr4d 314 . . 3 ((𝜑 ∧ (𝑃 𝐽 ∧ ran 𝐹 𝐽)) → (𝐹(⇝𝑡𝐽)𝑃𝐹(⇝𝑡𝐾)𝑃))
103102ex 416 . 2 (𝜑 → ((𝑃 𝐽 ∧ ran 𝐹 𝐽) → (𝐹(⇝𝑡𝐽)𝑃𝐹(⇝𝑡𝐾)𝑃)))
10413, 31, 103pm5.21ndd 384 1 (𝜑 → (𝐹(⇝𝑡𝐽)𝑃𝐹(⇝𝑡𝐾)𝑃))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399   = wceq 1538  wcel 2111  wral 3106  wrex 3107  cin 3880  wss 3881   cuni 4800   class class class wbr 5030   × cxp 5517  ran crn 5520   Fn wfn 6319  wf 6320  cfv 6324  (class class class)co 7135  cc 10524  cz 11969  cuz 12231  t crest 16686  Topctop 21498  TopOnctopon 21515  𝑡clm 21831
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-rep 5154  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295  ax-un 7441  ax-cnex 10582  ax-resscn 10583  ax-pre-lttri 10600  ax-pre-lttrn 10601
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-nel 3092  df-ral 3111  df-rex 3112  df-reu 3113  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-pss 3900  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-uni 4801  df-int 4839  df-iun 4883  df-br 5031  df-opab 5093  df-mpt 5111  df-tr 5137  df-id 5425  df-eprel 5430  df-po 5438  df-so 5439  df-fr 5478  df-we 5480  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-pred 6116  df-ord 6162  df-on 6163  df-lim 6164  df-suc 6165  df-iota 6283  df-fun 6326  df-fn 6327  df-f 6328  df-f1 6329  df-fo 6330  df-f1o 6331  df-fv 6332  df-ov 7138  df-oprab 7139  df-mpo 7140  df-om 7561  df-1st 7671  df-2nd 7672  df-wrecs 7930  df-recs 7991  df-rdg 8029  df-oadd 8089  df-er 8272  df-pm 8392  df-en 8493  df-dom 8494  df-sdom 8495  df-fin 8496  df-fi 8859  df-pnf 10666  df-mnf 10667  df-xr 10668  df-ltxr 10669  df-le 10670  df-neg 10862  df-z 11970  df-uz 12232  df-rest 16688  df-topgen 16709  df-top 21499  df-topon 21516  df-bases 21551  df-lm 21834
This theorem is referenced by:  1stckgen  22159  minvecolem4b  28661  minvecolem4  28663  hhsscms  29061  lmlim  31300  climreeq  42253  xlimclim  42464
  Copyright terms: Public domain W3C validator