Theorem lmss 22149

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.

Step	Hyp	Ref	Expression
1		lmss.4	. . . . . 6 ⊢ (𝜑 → 𝐽 ∈ Top)
2		toptopon2 21769	. . . . . 6 ⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘∪ 𝐽))
3	1, 2	sylib 221	. . . . 5 ⊢ (𝜑 → 𝐽 ∈ (TopOn‘∪ 𝐽))
4		lmcl 22148	. . . . 5 ⊢ ((𝐽 ∈ (TopOn‘∪ 𝐽) ∧ 𝐹(⇝𝑡‘𝐽)𝑃) → 𝑃 ∈ ∪ 𝐽)
5	3, 4	sylan 583	. . . 4 ⊢ ((𝜑 ∧ 𝐹(⇝𝑡‘𝐽)𝑃) → 𝑃 ∈ ∪ 𝐽)
6		lmfss 22147	. . . . . . 7 ⊢ ((𝐽 ∈ (TopOn‘∪ 𝐽) ∧ 𝐹(⇝𝑡‘𝐽)𝑃) → 𝐹 ⊆ (ℂ × ∪ 𝐽))
7	3, 6	sylan 583	. . . . . 6 ⊢ ((𝜑 ∧ 𝐹(⇝𝑡‘𝐽)𝑃) → 𝐹 ⊆ (ℂ × ∪ 𝐽))
8		rnss 5793	. . . . . 6 ⊢ (𝐹 ⊆ (ℂ × ∪ 𝐽) → ran 𝐹 ⊆ ran (ℂ × ∪ 𝐽))
9	7, 8	syl 17	. . . . 5 ⊢ ((𝜑 ∧ 𝐹(⇝𝑡‘𝐽)𝑃) → ran 𝐹 ⊆ ran (ℂ × ∪ 𝐽))
10		rnxpss 6015	. . . . 5 ⊢ ran (ℂ × ∪ 𝐽) ⊆ ∪ 𝐽
11	9, 10	sstrdi 3899	. . . 4 ⊢ ((𝜑 ∧ 𝐹(⇝𝑡‘𝐽)𝑃) → ran 𝐹 ⊆ ∪ 𝐽)
12	5, 11	jca 515	. . 3 ⊢ ((𝜑 ∧ 𝐹(⇝𝑡‘𝐽)𝑃) → (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽))
13	12	ex 416	. 2 ⊢ (𝜑 → (𝐹(⇝𝑡‘𝐽)𝑃 → (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)))
14		lmss.1	. . . . . . 7 ⊢ 𝐾 = (𝐽 ↾t 𝑌)
15		lmss.3	. . . . . . . 8 ⊢ (𝜑 → 𝑌 ∈ 𝑉)
16		resttopon2 22019	. . . . . . . 8 ⊢ ((𝐽 ∈ (TopOn‘∪ 𝐽) ∧ 𝑌 ∈ 𝑉) → (𝐽 ↾t 𝑌) ∈ (TopOn‘(𝑌 ∩ ∪ 𝐽)))
17	3, 15, 16	syl2anc 587	. . . . . . 7 ⊢ (𝜑 → (𝐽 ↾t 𝑌) ∈ (TopOn‘(𝑌 ∩ ∪ 𝐽)))
18	14, 17	eqeltrid 2835	. . . . . 6 ⊢ (𝜑 → 𝐾 ∈ (TopOn‘(𝑌 ∩ ∪ 𝐽)))
19		lmcl 22148	. . . . . 6 ⊢ ((𝐾 ∈ (TopOn‘(𝑌 ∩ ∪ 𝐽)) ∧ 𝐹(⇝𝑡‘𝐾)𝑃) → 𝑃 ∈ (𝑌 ∩ ∪ 𝐽))
20	18, 19	sylan 583	. . . . 5 ⊢ ((𝜑 ∧ 𝐹(⇝𝑡‘𝐾)𝑃) → 𝑃 ∈ (𝑌 ∩ ∪ 𝐽))
21	20	elin2d 4099	. . . 4 ⊢ ((𝜑 ∧ 𝐹(⇝𝑡‘𝐾)𝑃) → 𝑃 ∈ ∪ 𝐽)
22		lmfss 22147	. . . . . . . 8 ⊢ ((𝐾 ∈ (TopOn‘(𝑌 ∩ ∪ 𝐽)) ∧ 𝐹(⇝𝑡‘𝐾)𝑃) → 𝐹 ⊆ (ℂ × (𝑌 ∩ ∪ 𝐽)))
23	18, 22	sylan 583	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐹(⇝𝑡‘𝐾)𝑃) → 𝐹 ⊆ (ℂ × (𝑌 ∩ ∪ 𝐽)))
24		rnss 5793	. . . . . . 7 ⊢ (𝐹 ⊆ (ℂ × (𝑌 ∩ ∪ 𝐽)) → ran 𝐹 ⊆ ran (ℂ × (𝑌 ∩ ∪ 𝐽)))
25	23, 24	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ 𝐹(⇝𝑡‘𝐾)𝑃) → ran 𝐹 ⊆ ran (ℂ × (𝑌 ∩ ∪ 𝐽)))
26		rnxpss 6015	. . . . . 6 ⊢ ran (ℂ × (𝑌 ∩ ∪ 𝐽)) ⊆ (𝑌 ∩ ∪ 𝐽)
27	25, 26	sstrdi 3899	. . . . 5 ⊢ ((𝜑 ∧ 𝐹(⇝𝑡‘𝐾)𝑃) → ran 𝐹 ⊆ (𝑌 ∩ ∪ 𝐽))
28		inss2 4130	. . . . 5 ⊢ (𝑌 ∩ ∪ 𝐽) ⊆ ∪ 𝐽
29	27, 28	sstrdi 3899	. . . 4 ⊢ ((𝜑 ∧ 𝐹(⇝𝑡‘𝐾)𝑃) → ran 𝐹 ⊆ ∪ 𝐽)
30	21, 29	jca 515	. . 3 ⊢ ((𝜑 ∧ 𝐹(⇝𝑡‘𝐾)𝑃) → (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽))
31	30	ex 416	. 2 ⊢ (𝜑 → (𝐹(⇝𝑡‘𝐾)𝑃 → (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)))
32		simprl 771	. . . . . 6 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → 𝑃 ∈ ∪ 𝐽)
33		lmss.5	. . . . . . . 8 ⊢ (𝜑 → 𝑃 ∈ 𝑌)
34	33	adantr 484	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → 𝑃 ∈ 𝑌)
35	34, 32	elind 4094	. . . . . 6 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → 𝑃 ∈ (𝑌 ∩ ∪ 𝐽))
36	32, 35	2thd 268	. . . . 5 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → (𝑃 ∈ ∪ 𝐽 ↔ 𝑃 ∈ (𝑌 ∩ ∪ 𝐽)))
37	14	eleq2i 2822	. . . . . . . . 9 ⊢ (𝑣 ∈ 𝐾 ↔ 𝑣 ∈ (𝐽 ↾t 𝑌))
38	1	adantr 484	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → 𝐽 ∈ Top)
39	15	adantr 484	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → 𝑌 ∈ 𝑉)
40		elrest 16886	. . . . . . . . . . 11 ⊢ ((𝐽 ∈ Top ∧ 𝑌 ∈ 𝑉) → (𝑣 ∈ (𝐽 ↾t 𝑌) ↔ ∃𝑢 ∈ 𝐽 𝑣 = (𝑢 ∩ 𝑌)))
41	38, 39, 40	syl2anc 587	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → (𝑣 ∈ (𝐽 ↾t 𝑌) ↔ ∃𝑢 ∈ 𝐽 𝑣 = (𝑢 ∩ 𝑌)))
42	41	biimpa 480	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) ∧ 𝑣 ∈ (𝐽 ↾t 𝑌)) → ∃𝑢 ∈ 𝐽 𝑣 = (𝑢 ∩ 𝑌))
43	37, 42	sylan2b 597	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) ∧ 𝑣 ∈ 𝐾) → ∃𝑢 ∈ 𝐽 𝑣 = (𝑢 ∩ 𝑌))
44		r19.29r 3167	. . . . . . . . . 10 ⊢ ((∃𝑢 ∈ 𝐽 𝑣 = (𝑢 ∩ 𝑌) ∧ ∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢)) → ∃𝑢 ∈ 𝐽 (𝑣 = (𝑢 ∩ 𝑌) ∧ (𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢)))
45	34	biantrud 535	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → (𝑃 ∈ 𝑢 ↔ (𝑃 ∈ 𝑢 ∧ 𝑃 ∈ 𝑌)))
46		elin 3869	. . . . . . . . . . . . . . . . 17 ⊢ (𝑃 ∈ (𝑢 ∩ 𝑌) ↔ (𝑃 ∈ 𝑢 ∧ 𝑃 ∈ 𝑌))
47	45, 46	bitr4di 292	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → (𝑃 ∈ 𝑢 ↔ 𝑃 ∈ (𝑢 ∩ 𝑌)))
48		lmss.2	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑍 = (ℤ≥‘𝑀)
49	48	uztrn2 12422	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → 𝑘 ∈ 𝑍)
50		lmss.7	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝐹:𝑍⟶𝑌)
51	50	adantr 484	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → 𝐹:𝑍⟶𝑌)
52	51	ffvelrnda 6882	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ 𝑌)
53	52	biantrud 535	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) ∧ 𝑘 ∈ 𝑍) → ((𝐹‘𝑘) ∈ 𝑢 ↔ ((𝐹‘𝑘) ∈ 𝑢 ∧ (𝐹‘𝑘) ∈ 𝑌)))
54		elin 3869	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐹‘𝑘) ∈ (𝑢 ∩ 𝑌) ↔ ((𝐹‘𝑘) ∈ 𝑢 ∧ (𝐹‘𝑘) ∈ 𝑌))
55	53, 54	bitr4di 292	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) ∧ 𝑘 ∈ 𝑍) → ((𝐹‘𝑘) ∈ 𝑢 ↔ (𝐹‘𝑘) ∈ (𝑢 ∩ 𝑌)))
56	49, 55	sylan2 596	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) ∧ (𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗))) → ((𝐹‘𝑘) ∈ 𝑢 ↔ (𝐹‘𝑘) ∈ (𝑢 ∩ 𝑌)))
57	56	anassrs 471	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → ((𝐹‘𝑘) ∈ 𝑢 ↔ (𝐹‘𝑘) ∈ (𝑢 ∩ 𝑌)))
58	57	ralbidva 3107	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) ∧ 𝑗 ∈ 𝑍) → (∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢 ↔ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ (𝑢 ∩ 𝑌)))
59	58	rexbidva 3205	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → (∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢 ↔ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ (𝑢 ∩ 𝑌)))
60	47, 59	imbi12d 348	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → ((𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢) ↔ (𝑃 ∈ (𝑢 ∩ 𝑌) → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ (𝑢 ∩ 𝑌))))
61	60	adantr 484	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) ∧ 𝑢 ∈ 𝐽) → ((𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢) ↔ (𝑃 ∈ (𝑢 ∩ 𝑌) → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ (𝑢 ∩ 𝑌))))
62	61	biimpd 232	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) ∧ 𝑢 ∈ 𝐽) → ((𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢) → (𝑃 ∈ (𝑢 ∩ 𝑌) → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ (𝑢 ∩ 𝑌))))
63		eleq2 2819	. . . . . . . . . . . . . . 15 ⊢ (𝑣 = (𝑢 ∩ 𝑌) → (𝑃 ∈ 𝑣 ↔ 𝑃 ∈ (𝑢 ∩ 𝑌)))
64		eleq2 2819	. . . . . . . . . . . . . . . 16 ⊢ (𝑣 = (𝑢 ∩ 𝑌) → ((𝐹‘𝑘) ∈ 𝑣 ↔ (𝐹‘𝑘) ∈ (𝑢 ∩ 𝑌)))
65	64	rexralbidv 3210	. . . . . . . . . . . . . . 15 ⊢ (𝑣 = (𝑢 ∩ 𝑌) → (∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑣 ↔ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ (𝑢 ∩ 𝑌)))
66	63, 65	imbi12d 348	. . . . . . . . . . . . . 14 ⊢ (𝑣 = (𝑢 ∩ 𝑌) → ((𝑃 ∈ 𝑣 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑣) ↔ (𝑃 ∈ (𝑢 ∩ 𝑌) → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ (𝑢 ∩ 𝑌))))
67	66	imbi2d 344	. . . . . . . . . . . . 13 ⊢ (𝑣 = (𝑢 ∩ 𝑌) → (((𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢) → (𝑃 ∈ 𝑣 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑣)) ↔ ((𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢) → (𝑃 ∈ (𝑢 ∩ 𝑌) → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ (𝑢 ∩ 𝑌)))))
68	62, 67	syl5ibrcom 250	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) ∧ 𝑢 ∈ 𝐽) → (𝑣 = (𝑢 ∩ 𝑌) → ((𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢) → (𝑃 ∈ 𝑣 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑣))))
69	68	impd 414	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) ∧ 𝑢 ∈ 𝐽) → ((𝑣 = (𝑢 ∩ 𝑌) ∧ (𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢)) → (𝑃 ∈ 𝑣 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑣)))
70	69	rexlimdva 3193	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → (∃𝑢 ∈ 𝐽 (𝑣 = (𝑢 ∩ 𝑌) ∧ (𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢)) → (𝑃 ∈ 𝑣 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑣)))
71	44, 70	syl5 34	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → ((∃𝑢 ∈ 𝐽 𝑣 = (𝑢 ∩ 𝑌) ∧ ∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢)) → (𝑃 ∈ 𝑣 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑣)))
72	71	expdimp 456	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) ∧ ∃𝑢 ∈ 𝐽 𝑣 = (𝑢 ∩ 𝑌)) → (∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢) → (𝑃 ∈ 𝑣 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑣)))
73	43, 72	syldan 594	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) ∧ 𝑣 ∈ 𝐾) → (∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢) → (𝑃 ∈ 𝑣 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑣)))
74	73	ralrimdva 3100	. . . . . 6 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → (∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢) → ∀𝑣 ∈ 𝐾 (𝑃 ∈ 𝑣 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑣)))
75	38	adantr 484	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) ∧ 𝑢 ∈ 𝐽) → 𝐽 ∈ Top)
76	39	adantr 484	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) ∧ 𝑢 ∈ 𝐽) → 𝑌 ∈ 𝑉)
77		simpr 488	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) ∧ 𝑢 ∈ 𝐽) → 𝑢 ∈ 𝐽)
78		elrestr 16887	. . . . . . . . . . 11 ⊢ ((𝐽 ∈ Top ∧ 𝑌 ∈ 𝑉 ∧ 𝑢 ∈ 𝐽) → (𝑢 ∩ 𝑌) ∈ (𝐽 ↾t 𝑌))
79	75, 76, 77, 78	syl3anc 1373	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) ∧ 𝑢 ∈ 𝐽) → (𝑢 ∩ 𝑌) ∈ (𝐽 ↾t 𝑌))
80	79, 14	eleqtrrdi 2842	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) ∧ 𝑢 ∈ 𝐽) → (𝑢 ∩ 𝑌) ∈ 𝐾)
81	66	rspcv 3522	. . . . . . . . 9 ⊢ ((𝑢 ∩ 𝑌) ∈ 𝐾 → (∀𝑣 ∈ 𝐾 (𝑃 ∈ 𝑣 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑣) → (𝑃 ∈ (𝑢 ∩ 𝑌) → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ (𝑢 ∩ 𝑌))))
82	80, 81	syl 17	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) ∧ 𝑢 ∈ 𝐽) → (∀𝑣 ∈ 𝐾 (𝑃 ∈ 𝑣 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑣) → (𝑃 ∈ (𝑢 ∩ 𝑌) → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ (𝑢 ∩ 𝑌))))
83	82, 61	sylibrd 262	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) ∧ 𝑢 ∈ 𝐽) → (∀𝑣 ∈ 𝐾 (𝑃 ∈ 𝑣 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑣) → (𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢)))
84	83	ralrimdva 3100	. . . . . 6 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → (∀𝑣 ∈ 𝐾 (𝑃 ∈ 𝑣 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑣) → ∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢)))
85	74, 84	impbid 215	. . . . 5 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → (∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢) ↔ ∀𝑣 ∈ 𝐾 (𝑃 ∈ 𝑣 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑣)))
86	36, 85	anbi12d 634	. . . 4 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → ((𝑃 ∈ ∪ 𝐽 ∧ ∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢)) ↔ (𝑃 ∈ (𝑌 ∩ ∪ 𝐽) ∧ ∀𝑣 ∈ 𝐾 (𝑃 ∈ 𝑣 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑣))))
87	38, 2	sylib 221	. . . . 5 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → 𝐽 ∈ (TopOn‘∪ 𝐽))
88		lmss.6	. . . . . 6 ⊢ (𝜑 → 𝑀 ∈ ℤ)
89	88	adantr 484	. . . . 5 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → 𝑀 ∈ ℤ)
90	51	ffnd 6524	. . . . . 6 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → 𝐹 Fn 𝑍)
91		simprr 773	. . . . . 6 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → ran 𝐹 ⊆ ∪ 𝐽)
92		df-f 6362	. . . . . 6 ⊢ (𝐹:𝑍⟶∪ 𝐽 ↔ (𝐹 Fn 𝑍 ∧ ran 𝐹 ⊆ ∪ 𝐽))
93	90, 91, 92	sylanbrc 586	. . . . 5 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → 𝐹:𝑍⟶∪ 𝐽)
94		eqidd 2737	. . . . 5 ⊢ (((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = (𝐹‘𝑘))
95	87, 48, 89, 93, 94	lmbrf 22111	. . . 4 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → (𝐹(⇝𝑡‘𝐽)𝑃 ↔ (𝑃 ∈ ∪ 𝐽 ∧ ∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢))))
96	18	adantr 484	. . . . 5 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → 𝐾 ∈ (TopOn‘(𝑌 ∩ ∪ 𝐽)))
97	51	frnd 6531	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → ran 𝐹 ⊆ 𝑌)
98	97, 91	ssind 4133	. . . . . 6 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → ran 𝐹 ⊆ (𝑌 ∩ ∪ 𝐽))
99		df-f 6362	. . . . . 6 ⊢ (𝐹:𝑍⟶(𝑌 ∩ ∪ 𝐽) ↔ (𝐹 Fn 𝑍 ∧ ran 𝐹 ⊆ (𝑌 ∩ ∪ 𝐽)))
100	90, 98, 99	sylanbrc 586	. . . . 5 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → 𝐹:𝑍⟶(𝑌 ∩ ∪ 𝐽))
101	96, 48, 89, 100, 94	lmbrf 22111	. . . 4 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → (𝐹(⇝𝑡‘𝐾)𝑃 ↔ (𝑃 ∈ (𝑌 ∩ ∪ 𝐽) ∧ ∀𝑣 ∈ 𝐾 (𝑃 ∈ 𝑣 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑣))))
102	86, 95, 101	3bitr4d 314	. . 3 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → (𝐹(⇝𝑡‘𝐽)𝑃 ↔ 𝐹(⇝𝑡‘𝐾)𝑃))
103	102	ex 416	. 2 ⊢ (𝜑 → ((𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽) → (𝐹(⇝𝑡‘𝐽)𝑃 ↔ 𝐹(⇝𝑡‘𝐾)𝑃)))
104	13, 31, 103	pm5.21ndd 384	1 ⊢ (𝜑 → (𝐹(⇝𝑡‘𝐽)𝑃 ↔ 𝐹(⇝𝑡‘𝐾)𝑃))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1543   ∈ wcel 2112  ∀wral 3051  ∃wrex 3052   ∩ cin 3852   ⊆ wss 3853  ∪ cuni 4805   class class class wbr 5039   × cxp 5534  ran crn 5537   Fn wfn 6353  ⟶wf 6354  ‘cfv 6358  (class class class)co 7191  ℂcc 10692  ℤcz 12141  ℤ_≥cuz 12403   ↾_t crest 16879  Topctop 21744  TopOnctopon 21761  ⇝_𝑡clm 22077

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2160  ax-12 2177  ax-ext 2708  ax-rep 5164  ax-sep 5177  ax-nul 5184  ax-pow 5243  ax-pr 5307  ax-un 7501  ax-cnex 10750  ax-resscn 10751  ax-pre-lttri 10768  ax-pre-lttrn 10769

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2073  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2728  df-clel 2809  df-nfc 2879  df-ne 2933  df-nel 3037  df-ral 3056  df-rex 3057  df-reu 3058  df-rab 3060  df-v 3400  df-sbc 3684  df-csb 3799  df-dif 3856  df-un 3858  df-in 3860  df-ss 3870  df-pss 3872  df-nul 4224  df-if 4426  df-pw 4501  df-sn 4528  df-pr 4530  df-tp 4532  df-op 4534  df-uni 4806  df-int 4846  df-iun 4892  df-br 5040  df-opab 5102  df-mpt 5121  df-tr 5147  df-id 5440  df-eprel 5445  df-po 5453  df-so 5454  df-fr 5494  df-we 5496  df-xp 5542  df-rel 5543  df-cnv 5544  df-co 5545  df-dm 5546  df-rn 5547  df-res 5548  df-ima 5549  df-ord 6194  df-on 6195  df-lim 6196  df-suc 6197  df-iota 6316  df-fun 6360  df-fn 6361  df-f 6362  df-f1 6363  df-fo 6364  df-f1o 6365  df-fv 6366  df-ov 7194  df-oprab 7195  df-mpo 7196  df-om 7623  df-1st 7739  df-2nd 7740  df-er 8369  df-pm 8489  df-en 8605  df-dom 8606  df-sdom 8607  df-fin 8608  df-fi 9005  df-pnf 10834  df-mnf 10835  df-xr 10836  df-ltxr 10837  df-le 10838  df-neg 11030  df-z 12142  df-uz 12404  df-rest 16881  df-topgen 16902  df-top 21745  df-topon 21762  df-bases 21797  df-lm 22080

This theorem is referenced by:  1stckgen  22405  minvecolem4b  28913  minvecolem4  28915  hhsscms  29313  lmlim  31565  climreeq  42772  xlimclim  42983