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

Theorem lmss 23306
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 22924 . . . . . 6 (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘ 𝐽))
31, 2sylib 218 . . . . 5 (𝜑𝐽 ∈ (TopOn‘ 𝐽))
4 lmcl 23305 . . . . 5 ((𝐽 ∈ (TopOn‘ 𝐽) ∧ 𝐹(⇝𝑡𝐽)𝑃) → 𝑃 𝐽)
53, 4sylan 580 . . . 4 ((𝜑𝐹(⇝𝑡𝐽)𝑃) → 𝑃 𝐽)
6 lmfss 23304 . . . . . . 7 ((𝐽 ∈ (TopOn‘ 𝐽) ∧ 𝐹(⇝𝑡𝐽)𝑃) → 𝐹 ⊆ (ℂ × 𝐽))
73, 6sylan 580 . . . . . 6 ((𝜑𝐹(⇝𝑡𝐽)𝑃) → 𝐹 ⊆ (ℂ × 𝐽))
8 rnss 5950 . . . . . 6 (𝐹 ⊆ (ℂ × 𝐽) → ran 𝐹 ⊆ ran (ℂ × 𝐽))
97, 8syl 17 . . . . 5 ((𝜑𝐹(⇝𝑡𝐽)𝑃) → ran 𝐹 ⊆ ran (ℂ × 𝐽))
10 rnxpss 6192 . . . . 5 ran (ℂ × 𝐽) ⊆ 𝐽
119, 10sstrdi 3996 . . . 4 ((𝜑𝐹(⇝𝑡𝐽)𝑃) → ran 𝐹 𝐽)
125, 11jca 511 . . 3 ((𝜑𝐹(⇝𝑡𝐽)𝑃) → (𝑃 𝐽 ∧ ran 𝐹 𝐽))
1312ex 412 . 2 (𝜑 → (𝐹(⇝𝑡𝐽)𝑃 → (𝑃 𝐽 ∧ ran 𝐹 𝐽)))
14 lmss.1 . . . . . . 7 𝐾 = (𝐽t 𝑌)
15 lmss.3 . . . . . . . 8 (𝜑𝑌𝑉)
16 resttopon2 23176 . . . . . . . 8 ((𝐽 ∈ (TopOn‘ 𝐽) ∧ 𝑌𝑉) → (𝐽t 𝑌) ∈ (TopOn‘(𝑌 𝐽)))
173, 15, 16syl2anc 584 . . . . . . 7 (𝜑 → (𝐽t 𝑌) ∈ (TopOn‘(𝑌 𝐽)))
1814, 17eqeltrid 2845 . . . . . 6 (𝜑𝐾 ∈ (TopOn‘(𝑌 𝐽)))
19 lmcl 23305 . . . . . 6 ((𝐾 ∈ (TopOn‘(𝑌 𝐽)) ∧ 𝐹(⇝𝑡𝐾)𝑃) → 𝑃 ∈ (𝑌 𝐽))
2018, 19sylan 580 . . . . 5 ((𝜑𝐹(⇝𝑡𝐾)𝑃) → 𝑃 ∈ (𝑌 𝐽))
2120elin2d 4205 . . . 4 ((𝜑𝐹(⇝𝑡𝐾)𝑃) → 𝑃 𝐽)
22 lmfss 23304 . . . . . . . 8 ((𝐾 ∈ (TopOn‘(𝑌 𝐽)) ∧ 𝐹(⇝𝑡𝐾)𝑃) → 𝐹 ⊆ (ℂ × (𝑌 𝐽)))
2318, 22sylan 580 . . . . . . 7 ((𝜑𝐹(⇝𝑡𝐾)𝑃) → 𝐹 ⊆ (ℂ × (𝑌 𝐽)))
24 rnss 5950 . . . . . . 7 (𝐹 ⊆ (ℂ × (𝑌 𝐽)) → ran 𝐹 ⊆ ran (ℂ × (𝑌 𝐽)))
2523, 24syl 17 . . . . . 6 ((𝜑𝐹(⇝𝑡𝐾)𝑃) → ran 𝐹 ⊆ ran (ℂ × (𝑌 𝐽)))
26 rnxpss 6192 . . . . . 6 ran (ℂ × (𝑌 𝐽)) ⊆ (𝑌 𝐽)
2725, 26sstrdi 3996 . . . . 5 ((𝜑𝐹(⇝𝑡𝐾)𝑃) → ran 𝐹 ⊆ (𝑌 𝐽))
28 inss2 4238 . . . . 5 (𝑌 𝐽) ⊆ 𝐽
2927, 28sstrdi 3996 . . . 4 ((𝜑𝐹(⇝𝑡𝐾)𝑃) → ran 𝐹 𝐽)
3021, 29jca 511 . . 3 ((𝜑𝐹(⇝𝑡𝐾)𝑃) → (𝑃 𝐽 ∧ ran 𝐹 𝐽))
3130ex 412 . 2 (𝜑 → (𝐹(⇝𝑡𝐾)𝑃 → (𝑃 𝐽 ∧ ran 𝐹 𝐽)))
32 simprl 771 . . . . . 6 ((𝜑 ∧ (𝑃 𝐽 ∧ ran 𝐹 𝐽)) → 𝑃 𝐽)
33 lmss.5 . . . . . . . 8 (𝜑𝑃𝑌)
3433adantr 480 . . . . . . 7 ((𝜑 ∧ (𝑃 𝐽 ∧ ran 𝐹 𝐽)) → 𝑃𝑌)
3534, 32elind 4200 . . . . . 6 ((𝜑 ∧ (𝑃 𝐽 ∧ ran 𝐹 𝐽)) → 𝑃 ∈ (𝑌 𝐽))
3632, 352thd 265 . . . . 5 ((𝜑 ∧ (𝑃 𝐽 ∧ ran 𝐹 𝐽)) → (𝑃 𝐽𝑃 ∈ (𝑌 𝐽)))
3714eleq2i 2833 . . . . . . . . 9 (𝑣𝐾𝑣 ∈ (𝐽t 𝑌))
381adantr 480 . . . . . . . . . . 11 ((𝜑 ∧ (𝑃 𝐽 ∧ ran 𝐹 𝐽)) → 𝐽 ∈ Top)
3915adantr 480 . . . . . . . . . . 11 ((𝜑 ∧ (𝑃 𝐽 ∧ ran 𝐹 𝐽)) → 𝑌𝑉)
40 elrest 17472 . . . . . . . . . . 11 ((𝐽 ∈ Top ∧ 𝑌𝑉) → (𝑣 ∈ (𝐽t 𝑌) ↔ ∃𝑢𝐽 𝑣 = (𝑢𝑌)))
4138, 39, 40syl2anc 584 . . . . . . . . . 10 ((𝜑 ∧ (𝑃 𝐽 ∧ ran 𝐹 𝐽)) → (𝑣 ∈ (𝐽t 𝑌) ↔ ∃𝑢𝐽 𝑣 = (𝑢𝑌)))
4241biimpa 476 . . . . . . . . 9 (((𝜑 ∧ (𝑃 𝐽 ∧ ran 𝐹 𝐽)) ∧ 𝑣 ∈ (𝐽t 𝑌)) → ∃𝑢𝐽 𝑣 = (𝑢𝑌))
4337, 42sylan2b 594 . . . . . . . 8 (((𝜑 ∧ (𝑃 𝐽 ∧ ran 𝐹 𝐽)) ∧ 𝑣𝐾) → ∃𝑢𝐽 𝑣 = (𝑢𝑌))
44 r19.29r 3116 . . . . . . . . . 10 ((∃𝑢𝐽 𝑣 = (𝑢𝑌) ∧ ∀𝑢𝐽 (𝑃𝑢 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ 𝑢)) → ∃𝑢𝐽 (𝑣 = (𝑢𝑌) ∧ (𝑃𝑢 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ 𝑢)))
4534biantrud 531 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑃 𝐽 ∧ ran 𝐹 𝐽)) → (𝑃𝑢 ↔ (𝑃𝑢𝑃𝑌)))
46 elin 3967 . . . . . . . . . . . . . . . . 17 (𝑃 ∈ (𝑢𝑌) ↔ (𝑃𝑢𝑃𝑌))
4745, 46bitr4di 289 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑃 𝐽 ∧ ran 𝐹 𝐽)) → (𝑃𝑢𝑃 ∈ (𝑢𝑌)))
48 lmss.2 . . . . . . . . . . . . . . . . . . . . 21 𝑍 = (ℤ𝑀)
4948uztrn2 12897 . . . . . . . . . . . . . . . . . . . 20 ((𝑗𝑍𝑘 ∈ (ℤ𝑗)) → 𝑘𝑍)
50 lmss.7 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝐹:𝑍𝑌)
5150adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑃 𝐽 ∧ ran 𝐹 𝐽)) → 𝐹:𝑍𝑌)
5251ffvelcdmda 7104 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ (𝑃 𝐽 ∧ ran 𝐹 𝐽)) ∧ 𝑘𝑍) → (𝐹𝑘) ∈ 𝑌)
5352biantrud 531 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑃 𝐽 ∧ ran 𝐹 𝐽)) ∧ 𝑘𝑍) → ((𝐹𝑘) ∈ 𝑢 ↔ ((𝐹𝑘) ∈ 𝑢 ∧ (𝐹𝑘) ∈ 𝑌)))
54 elin 3967 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹𝑘) ∈ (𝑢𝑌) ↔ ((𝐹𝑘) ∈ 𝑢 ∧ (𝐹𝑘) ∈ 𝑌))
5553, 54bitr4di 289 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑃 𝐽 ∧ ran 𝐹 𝐽)) ∧ 𝑘𝑍) → ((𝐹𝑘) ∈ 𝑢 ↔ (𝐹𝑘) ∈ (𝑢𝑌)))
5649, 55sylan2 593 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑃 𝐽 ∧ ran 𝐹 𝐽)) ∧ (𝑗𝑍𝑘 ∈ (ℤ𝑗))) → ((𝐹𝑘) ∈ 𝑢 ↔ (𝐹𝑘) ∈ (𝑢𝑌)))
5756anassrs 467 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝑃 𝐽 ∧ ran 𝐹 𝐽)) ∧ 𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) → ((𝐹𝑘) ∈ 𝑢 ↔ (𝐹𝑘) ∈ (𝑢𝑌)))
5857ralbidva 3176 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑃 𝐽 ∧ ran 𝐹 𝐽)) ∧ 𝑗𝑍) → (∀𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ 𝑢 ↔ ∀𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ (𝑢𝑌)))
5958rexbidva 3177 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑃 𝐽 ∧ ran 𝐹 𝐽)) → (∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ 𝑢 ↔ ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ (𝑢𝑌)))
6047, 59imbi12d 344 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑃 𝐽 ∧ ran 𝐹 𝐽)) → ((𝑃𝑢 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ 𝑢) ↔ (𝑃 ∈ (𝑢𝑌) → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ (𝑢𝑌))))
6160adantr 480 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑃 𝐽 ∧ ran 𝐹 𝐽)) ∧ 𝑢𝐽) → ((𝑃𝑢 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ 𝑢) ↔ (𝑃 ∈ (𝑢𝑌) → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ (𝑢𝑌))))
6261biimpd 229 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑃 𝐽 ∧ ran 𝐹 𝐽)) ∧ 𝑢𝐽) → ((𝑃𝑢 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ 𝑢) → (𝑃 ∈ (𝑢𝑌) → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ (𝑢𝑌))))
63 eleq2 2830 . . . . . . . . . . . . . . 15 (𝑣 = (𝑢𝑌) → (𝑃𝑣𝑃 ∈ (𝑢𝑌)))
64 eleq2 2830 . . . . . . . . . . . . . . . 16 (𝑣 = (𝑢𝑌) → ((𝐹𝑘) ∈ 𝑣 ↔ (𝐹𝑘) ∈ (𝑢𝑌)))
6564rexralbidv 3223 . . . . . . . . . . . . . . 15 (𝑣 = (𝑢𝑌) → (∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ 𝑣 ↔ ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ (𝑢𝑌)))
6663, 65imbi12d 344 . . . . . . . . . . . . . 14 (𝑣 = (𝑢𝑌) → ((𝑃𝑣 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ 𝑣) ↔ (𝑃 ∈ (𝑢𝑌) → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ (𝑢𝑌))))
6766imbi2d 340 . . . . . . . . . . . . 13 (𝑣 = (𝑢𝑌) → (((𝑃𝑢 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ 𝑢) → (𝑃𝑣 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ 𝑣)) ↔ ((𝑃𝑢 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ 𝑢) → (𝑃 ∈ (𝑢𝑌) → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ (𝑢𝑌)))))
6862, 67syl5ibrcom 247 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑃 𝐽 ∧ ran 𝐹 𝐽)) ∧ 𝑢𝐽) → (𝑣 = (𝑢𝑌) → ((𝑃𝑢 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ 𝑢) → (𝑃𝑣 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ 𝑣))))
6968impd 410 . . . . . . . . . . 11 (((𝜑 ∧ (𝑃 𝐽 ∧ ran 𝐹 𝐽)) ∧ 𝑢𝐽) → ((𝑣 = (𝑢𝑌) ∧ (𝑃𝑢 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ 𝑢)) → (𝑃𝑣 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ 𝑣)))
7069rexlimdva 3155 . . . . . . . . . 10 ((𝜑 ∧ (𝑃 𝐽 ∧ ran 𝐹 𝐽)) → (∃𝑢𝐽 (𝑣 = (𝑢𝑌) ∧ (𝑃𝑢 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ 𝑢)) → (𝑃𝑣 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ 𝑣)))
7144, 70syl5 34 . . . . . . . . 9 ((𝜑 ∧ (𝑃 𝐽 ∧ ran 𝐹 𝐽)) → ((∃𝑢𝐽 𝑣 = (𝑢𝑌) ∧ ∀𝑢𝐽 (𝑃𝑢 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ 𝑢)) → (𝑃𝑣 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ 𝑣)))
7271expdimp 452 . . . . . . . 8 (((𝜑 ∧ (𝑃 𝐽 ∧ ran 𝐹 𝐽)) ∧ ∃𝑢𝐽 𝑣 = (𝑢𝑌)) → (∀𝑢𝐽 (𝑃𝑢 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ 𝑢) → (𝑃𝑣 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ 𝑣)))
7343, 72syldan 591 . . . . . . 7 (((𝜑 ∧ (𝑃 𝐽 ∧ ran 𝐹 𝐽)) ∧ 𝑣𝐾) → (∀𝑢𝐽 (𝑃𝑢 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ 𝑢) → (𝑃𝑣 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ 𝑣)))
7473ralrimdva 3154 . . . . . 6 ((𝜑 ∧ (𝑃 𝐽 ∧ ran 𝐹 𝐽)) → (∀𝑢𝐽 (𝑃𝑢 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ 𝑢) → ∀𝑣𝐾 (𝑃𝑣 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ 𝑣)))
7538adantr 480 . . . . . . . . . . 11 (((𝜑 ∧ (𝑃 𝐽 ∧ ran 𝐹 𝐽)) ∧ 𝑢𝐽) → 𝐽 ∈ Top)
7639adantr 480 . . . . . . . . . . 11 (((𝜑 ∧ (𝑃 𝐽 ∧ ran 𝐹 𝐽)) ∧ 𝑢𝐽) → 𝑌𝑉)
77 simpr 484 . . . . . . . . . . 11 (((𝜑 ∧ (𝑃 𝐽 ∧ ran 𝐹 𝐽)) ∧ 𝑢𝐽) → 𝑢𝐽)
78 elrestr 17473 . . . . . . . . . . 11 ((𝐽 ∈ Top ∧ 𝑌𝑉𝑢𝐽) → (𝑢𝑌) ∈ (𝐽t 𝑌))
7975, 76, 77, 78syl3anc 1373 . . . . . . . . . 10 (((𝜑 ∧ (𝑃 𝐽 ∧ ran 𝐹 𝐽)) ∧ 𝑢𝐽) → (𝑢𝑌) ∈ (𝐽t 𝑌))
8079, 14eleqtrrdi 2852 . . . . . . . . 9 (((𝜑 ∧ (𝑃 𝐽 ∧ ran 𝐹 𝐽)) ∧ 𝑢𝐽) → (𝑢𝑌) ∈ 𝐾)
8166rspcv 3618 . . . . . . . . 9 ((𝑢𝑌) ∈ 𝐾 → (∀𝑣𝐾 (𝑃𝑣 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ 𝑣) → (𝑃 ∈ (𝑢𝑌) → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ (𝑢𝑌))))
8280, 81syl 17 . . . . . . . 8 (((𝜑 ∧ (𝑃 𝐽 ∧ ran 𝐹 𝐽)) ∧ 𝑢𝐽) → (∀𝑣𝐾 (𝑃𝑣 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ 𝑣) → (𝑃 ∈ (𝑢𝑌) → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ (𝑢𝑌))))
8382, 61sylibrd 259 . . . . . . 7 (((𝜑 ∧ (𝑃 𝐽 ∧ ran 𝐹 𝐽)) ∧ 𝑢𝐽) → (∀𝑣𝐾 (𝑃𝑣 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ 𝑣) → (𝑃𝑢 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ 𝑢)))
8483ralrimdva 3154 . . . . . 6 ((𝜑 ∧ (𝑃 𝐽 ∧ ran 𝐹 𝐽)) → (∀𝑣𝐾 (𝑃𝑣 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ 𝑣) → ∀𝑢𝐽 (𝑃𝑢 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ 𝑢)))
8574, 84impbid 212 . . . . 5 ((𝜑 ∧ (𝑃 𝐽 ∧ ran 𝐹 𝐽)) → (∀𝑢𝐽 (𝑃𝑢 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ 𝑢) ↔ ∀𝑣𝐾 (𝑃𝑣 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ 𝑣)))
8636, 85anbi12d 632 . . . 4 ((𝜑 ∧ (𝑃 𝐽 ∧ ran 𝐹 𝐽)) → ((𝑃 𝐽 ∧ ∀𝑢𝐽 (𝑃𝑢 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ 𝑢)) ↔ (𝑃 ∈ (𝑌 𝐽) ∧ ∀𝑣𝐾 (𝑃𝑣 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ 𝑣))))
8738, 2sylib 218 . . . . 5 ((𝜑 ∧ (𝑃 𝐽 ∧ ran 𝐹 𝐽)) → 𝐽 ∈ (TopOn‘ 𝐽))
88 lmss.6 . . . . . 6 (𝜑𝑀 ∈ ℤ)
8988adantr 480 . . . . 5 ((𝜑 ∧ (𝑃 𝐽 ∧ ran 𝐹 𝐽)) → 𝑀 ∈ ℤ)
9051ffnd 6737 . . . . . 6 ((𝜑 ∧ (𝑃 𝐽 ∧ ran 𝐹 𝐽)) → 𝐹 Fn 𝑍)
91 simprr 773 . . . . . 6 ((𝜑 ∧ (𝑃 𝐽 ∧ ran 𝐹 𝐽)) → ran 𝐹 𝐽)
92 df-f 6565 . . . . . 6 (𝐹:𝑍 𝐽 ↔ (𝐹 Fn 𝑍 ∧ ran 𝐹 𝐽))
9390, 91, 92sylanbrc 583 . . . . 5 ((𝜑 ∧ (𝑃 𝐽 ∧ ran 𝐹 𝐽)) → 𝐹:𝑍 𝐽)
94 eqidd 2738 . . . . 5 (((𝜑 ∧ (𝑃 𝐽 ∧ ran 𝐹 𝐽)) ∧ 𝑘𝑍) → (𝐹𝑘) = (𝐹𝑘))
9587, 48, 89, 93, 94lmbrf 23268 . . . 4 ((𝜑 ∧ (𝑃 𝐽 ∧ ran 𝐹 𝐽)) → (𝐹(⇝𝑡𝐽)𝑃 ↔ (𝑃 𝐽 ∧ ∀𝑢𝐽 (𝑃𝑢 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ 𝑢))))
9618adantr 480 . . . . 5 ((𝜑 ∧ (𝑃 𝐽 ∧ ran 𝐹 𝐽)) → 𝐾 ∈ (TopOn‘(𝑌 𝐽)))
9751frnd 6744 . . . . . . 7 ((𝜑 ∧ (𝑃 𝐽 ∧ ran 𝐹 𝐽)) → ran 𝐹𝑌)
9897, 91ssind 4241 . . . . . 6 ((𝜑 ∧ (𝑃 𝐽 ∧ ran 𝐹 𝐽)) → ran 𝐹 ⊆ (𝑌 𝐽))
99 df-f 6565 . . . . . 6 (𝐹:𝑍⟶(𝑌 𝐽) ↔ (𝐹 Fn 𝑍 ∧ ran 𝐹 ⊆ (𝑌 𝐽)))
10090, 98, 99sylanbrc 583 . . . . 5 ((𝜑 ∧ (𝑃 𝐽 ∧ ran 𝐹 𝐽)) → 𝐹:𝑍⟶(𝑌 𝐽))
10196, 48, 89, 100, 94lmbrf 23268 . . . 4 ((𝜑 ∧ (𝑃 𝐽 ∧ ran 𝐹 𝐽)) → (𝐹(⇝𝑡𝐾)𝑃 ↔ (𝑃 ∈ (𝑌 𝐽) ∧ ∀𝑣𝐾 (𝑃𝑣 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ 𝑣))))
10286, 95, 1013bitr4d 311 . . 3 ((𝜑 ∧ (𝑃 𝐽 ∧ ran 𝐹 𝐽)) → (𝐹(⇝𝑡𝐽)𝑃𝐹(⇝𝑡𝐾)𝑃))
103102ex 412 . 2 (𝜑 → ((𝑃 𝐽 ∧ ran 𝐹 𝐽) → (𝐹(⇝𝑡𝐽)𝑃𝐹(⇝𝑡𝐾)𝑃)))
10413, 31, 103pm5.21ndd 379 1 (𝜑 → (𝐹(⇝𝑡𝐽)𝑃𝐹(⇝𝑡𝐾)𝑃))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395   = wceq 1540  wcel 2108  wral 3061  wrex 3070  cin 3950  wss 3951   cuni 4907   class class class wbr 5143   × cxp 5683  ran crn 5686   Fn wfn 6556  wf 6557  cfv 6561  (class class class)co 7431  cc 11153  cz 12613  cuz 12878  t crest 17465  Topctop 22899  TopOnctopon 22916  𝑡clm 23234
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-cnex 11211  ax-resscn 11212  ax-pre-lttri 11229  ax-pre-lttrn 11230
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-int 4947  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-ov 7434  df-oprab 7435  df-mpo 7436  df-om 7888  df-1st 8014  df-2nd 8015  df-er 8745  df-pm 8869  df-en 8986  df-dom 8987  df-sdom 8988  df-fin 8989  df-fi 9451  df-pnf 11297  df-mnf 11298  df-xr 11299  df-ltxr 11300  df-le 11301  df-neg 11495  df-z 12614  df-uz 12879  df-rest 17467  df-topgen 17488  df-top 22900  df-topon 22917  df-bases 22953  df-lm 23237
This theorem is referenced by:  1stckgen  23562  minvecolem4b  30897  minvecolem4  30899  hhsscms  31297  lmlim  33946  climreeq  45628  xlimclim  45839
  Copyright terms: Public domain W3C validator