Theorem lmss 23206

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 22826	. . . . . 6 ⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘∪ 𝐽))
3	1, 2	sylib 218	. . . . 5 ⊢ (𝜑 → 𝐽 ∈ (TopOn‘∪ 𝐽))
4		lmcl 23205	. . . . 5 ⊢ ((𝐽 ∈ (TopOn‘∪ 𝐽) ∧ 𝐹(⇝𝑡‘𝐽)𝑃) → 𝑃 ∈ ∪ 𝐽)
5	3, 4	sylan 580	. . . 4 ⊢ ((𝜑 ∧ 𝐹(⇝𝑡‘𝐽)𝑃) → 𝑃 ∈ ∪ 𝐽)
6		lmfss 23204	. . . . . . 7 ⊢ ((𝐽 ∈ (TopOn‘∪ 𝐽) ∧ 𝐹(⇝𝑡‘𝐽)𝑃) → 𝐹 ⊆ (ℂ × ∪ 𝐽))
7	3, 6	sylan 580	. . . . . 6 ⊢ ((𝜑 ∧ 𝐹(⇝𝑡‘𝐽)𝑃) → 𝐹 ⊆ (ℂ × ∪ 𝐽))
8		rnss 5876	. . . . . 6 ⊢ (𝐹 ⊆ (ℂ × ∪ 𝐽) → ran 𝐹 ⊆ ran (ℂ × ∪ 𝐽))
9	7, 8	syl 17	. . . . 5 ⊢ ((𝜑 ∧ 𝐹(⇝𝑡‘𝐽)𝑃) → ran 𝐹 ⊆ ran (ℂ × ∪ 𝐽))
10		rnxpss 6116	. . . . 5 ⊢ ran (ℂ × ∪ 𝐽) ⊆ ∪ 𝐽
11	9, 10	sstrdi 3945	. . . 4 ⊢ ((𝜑 ∧ 𝐹(⇝𝑡‘𝐽)𝑃) → ran 𝐹 ⊆ ∪ 𝐽)
12	5, 11	jca 511	. . 3 ⊢ ((𝜑 ∧ 𝐹(⇝𝑡‘𝐽)𝑃) → (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽))
13	12	ex 412	. 2 ⊢ (𝜑 → (𝐹(⇝𝑡‘𝐽)𝑃 → (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)))
14		lmss.1	. . . . . . 7 ⊢ 𝐾 = (𝐽 ↾t 𝑌)
15		lmss.3	. . . . . . . 8 ⊢ (𝜑 → 𝑌 ∈ 𝑉)
16		resttopon2 23076	. . . . . . . 8 ⊢ ((𝐽 ∈ (TopOn‘∪ 𝐽) ∧ 𝑌 ∈ 𝑉) → (𝐽 ↾t 𝑌) ∈ (TopOn‘(𝑌 ∩ ∪ 𝐽)))
17	3, 15, 16	syl2anc 584	. . . . . . 7 ⊢ (𝜑 → (𝐽 ↾t 𝑌) ∈ (TopOn‘(𝑌 ∩ ∪ 𝐽)))
18	14, 17	eqeltrid 2833	. . . . . 6 ⊢ (𝜑 → 𝐾 ∈ (TopOn‘(𝑌 ∩ ∪ 𝐽)))
19		lmcl 23205	. . . . . 6 ⊢ ((𝐾 ∈ (TopOn‘(𝑌 ∩ ∪ 𝐽)) ∧ 𝐹(⇝𝑡‘𝐾)𝑃) → 𝑃 ∈ (𝑌 ∩ ∪ 𝐽))
20	18, 19	sylan 580	. . . . 5 ⊢ ((𝜑 ∧ 𝐹(⇝𝑡‘𝐾)𝑃) → 𝑃 ∈ (𝑌 ∩ ∪ 𝐽))
21	20	elin2d 4153	. . . 4 ⊢ ((𝜑 ∧ 𝐹(⇝𝑡‘𝐾)𝑃) → 𝑃 ∈ ∪ 𝐽)
22		lmfss 23204	. . . . . . . 8 ⊢ ((𝐾 ∈ (TopOn‘(𝑌 ∩ ∪ 𝐽)) ∧ 𝐹(⇝𝑡‘𝐾)𝑃) → 𝐹 ⊆ (ℂ × (𝑌 ∩ ∪ 𝐽)))
23	18, 22	sylan 580	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐹(⇝𝑡‘𝐾)𝑃) → 𝐹 ⊆ (ℂ × (𝑌 ∩ ∪ 𝐽)))
24		rnss 5876	. . . . . . 7 ⊢ (𝐹 ⊆ (ℂ × (𝑌 ∩ ∪ 𝐽)) → ran 𝐹 ⊆ ran (ℂ × (𝑌 ∩ ∪ 𝐽)))
25	23, 24	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ 𝐹(⇝𝑡‘𝐾)𝑃) → ran 𝐹 ⊆ ran (ℂ × (𝑌 ∩ ∪ 𝐽)))
26		rnxpss 6116	. . . . . 6 ⊢ ran (ℂ × (𝑌 ∩ ∪ 𝐽)) ⊆ (𝑌 ∩ ∪ 𝐽)
27	25, 26	sstrdi 3945	. . . . 5 ⊢ ((𝜑 ∧ 𝐹(⇝𝑡‘𝐾)𝑃) → ran 𝐹 ⊆ (𝑌 ∩ ∪ 𝐽))
28		inss2 4186	. . . . 5 ⊢ (𝑌 ∩ ∪ 𝐽) ⊆ ∪ 𝐽
29	27, 28	sstrdi 3945	. . . 4 ⊢ ((𝜑 ∧ 𝐹(⇝𝑡‘𝐾)𝑃) → ran 𝐹 ⊆ ∪ 𝐽)
30	21, 29	jca 511	. . 3 ⊢ ((𝜑 ∧ 𝐹(⇝𝑡‘𝐾)𝑃) → (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽))
31	30	ex 412	. 2 ⊢ (𝜑 → (𝐹(⇝𝑡‘𝐾)𝑃 → (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)))
32		simprl 770	. . . . . 6 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → 𝑃 ∈ ∪ 𝐽)
33		lmss.5	. . . . . . . 8 ⊢ (𝜑 → 𝑃 ∈ 𝑌)
34	33	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → 𝑃 ∈ 𝑌)
35	34, 32	elind 4148	. . . . . 6 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → 𝑃 ∈ (𝑌 ∩ ∪ 𝐽))
36	32, 35	2thd 265	. . . . 5 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → (𝑃 ∈ ∪ 𝐽 ↔ 𝑃 ∈ (𝑌 ∩ ∪ 𝐽)))
37	14	eleq2i 2821	. . . . . . . . 9 ⊢ (𝑣 ∈ 𝐾 ↔ 𝑣 ∈ (𝐽 ↾t 𝑌))
38	1	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → 𝐽 ∈ Top)
39	15	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → 𝑌 ∈ 𝑉)
40		elrest 17323	. . . . . . . . . . 11 ⊢ ((𝐽 ∈ Top ∧ 𝑌 ∈ 𝑉) → (𝑣 ∈ (𝐽 ↾t 𝑌) ↔ ∃𝑢 ∈ 𝐽 𝑣 = (𝑢 ∩ 𝑌)))
41	38, 39, 40	syl2anc 584	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → (𝑣 ∈ (𝐽 ↾t 𝑌) ↔ ∃𝑢 ∈ 𝐽 𝑣 = (𝑢 ∩ 𝑌)))
42	41	biimpa 476	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) ∧ 𝑣 ∈ (𝐽 ↾t 𝑌)) → ∃𝑢 ∈ 𝐽 𝑣 = (𝑢 ∩ 𝑌))
43	37, 42	sylan2b 594	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) ∧ 𝑣 ∈ 𝐾) → ∃𝑢 ∈ 𝐽 𝑣 = (𝑢 ∩ 𝑌))
44		r19.29r 3094	. . . . . . . . . 10 ⊢ ((∃𝑢 ∈ 𝐽 𝑣 = (𝑢 ∩ 𝑌) ∧ ∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢)) → ∃𝑢 ∈ 𝐽 (𝑣 = (𝑢 ∩ 𝑌) ∧ (𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢)))
45	34	biantrud 531	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → (𝑃 ∈ 𝑢 ↔ (𝑃 ∈ 𝑢 ∧ 𝑃 ∈ 𝑌)))
46		elin 3916	. . . . . . . . . . . . . . . . 17 ⊢ (𝑃 ∈ (𝑢 ∩ 𝑌) ↔ (𝑃 ∈ 𝑢 ∧ 𝑃 ∈ 𝑌))
47	45, 46	bitr4di 289	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → (𝑃 ∈ 𝑢 ↔ 𝑃 ∈ (𝑢 ∩ 𝑌)))
48		lmss.2	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑍 = (ℤ≥‘𝑀)
49	48	uztrn2 12743	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → 𝑘 ∈ 𝑍)
50		lmss.7	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝐹:𝑍⟶𝑌)
51	50	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → 𝐹:𝑍⟶𝑌)
52	51	ffvelcdmda 7012	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ 𝑌)
53	52	biantrud 531	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) ∧ 𝑘 ∈ 𝑍) → ((𝐹‘𝑘) ∈ 𝑢 ↔ ((𝐹‘𝑘) ∈ 𝑢 ∧ (𝐹‘𝑘) ∈ 𝑌)))
54		elin 3916	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐹‘𝑘) ∈ (𝑢 ∩ 𝑌) ↔ ((𝐹‘𝑘) ∈ 𝑢 ∧ (𝐹‘𝑘) ∈ 𝑌))
55	53, 54	bitr4di 289	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) ∧ 𝑘 ∈ 𝑍) → ((𝐹‘𝑘) ∈ 𝑢 ↔ (𝐹‘𝑘) ∈ (𝑢 ∩ 𝑌)))
56	49, 55	sylan2 593	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) ∧ (𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗))) → ((𝐹‘𝑘) ∈ 𝑢 ↔ (𝐹‘𝑘) ∈ (𝑢 ∩ 𝑌)))
57	56	anassrs 467	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → ((𝐹‘𝑘) ∈ 𝑢 ↔ (𝐹‘𝑘) ∈ (𝑢 ∩ 𝑌)))
58	57	ralbidva 3151	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) ∧ 𝑗 ∈ 𝑍) → (∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢 ↔ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ (𝑢 ∩ 𝑌)))
59	58	rexbidva 3152	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → (∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢 ↔ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ (𝑢 ∩ 𝑌)))
60	47, 59	imbi12d 344	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → ((𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢) ↔ (𝑃 ∈ (𝑢 ∩ 𝑌) → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ (𝑢 ∩ 𝑌))))
61	60	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) ∧ 𝑢 ∈ 𝐽) → ((𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢) ↔ (𝑃 ∈ (𝑢 ∩ 𝑌) → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ (𝑢 ∩ 𝑌))))
62	61	biimpd 229	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) ∧ 𝑢 ∈ 𝐽) → ((𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢) → (𝑃 ∈ (𝑢 ∩ 𝑌) → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ (𝑢 ∩ 𝑌))))
63		eleq2 2818	. . . . . . . . . . . . . . 15 ⊢ (𝑣 = (𝑢 ∩ 𝑌) → (𝑃 ∈ 𝑣 ↔ 𝑃 ∈ (𝑢 ∩ 𝑌)))
64		eleq2 2818	. . . . . . . . . . . . . . . 16 ⊢ (𝑣 = (𝑢 ∩ 𝑌) → ((𝐹‘𝑘) ∈ 𝑣 ↔ (𝐹‘𝑘) ∈ (𝑢 ∩ 𝑌)))
65	64	rexralbidv 3196	. . . . . . . . . . . . . . 15 ⊢ (𝑣 = (𝑢 ∩ 𝑌) → (∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑣 ↔ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ (𝑢 ∩ 𝑌)))
66	63, 65	imbi12d 344	. . . . . . . . . . . . . 14 ⊢ (𝑣 = (𝑢 ∩ 𝑌) → ((𝑃 ∈ 𝑣 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑣) ↔ (𝑃 ∈ (𝑢 ∩ 𝑌) → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ (𝑢 ∩ 𝑌))))
67	66	imbi2d 340	. . . . . . . . . . . . 13 ⊢ (𝑣 = (𝑢 ∩ 𝑌) → (((𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢) → (𝑃 ∈ 𝑣 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑣)) ↔ ((𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢) → (𝑃 ∈ (𝑢 ∩ 𝑌) → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ (𝑢 ∩ 𝑌)))))
68	62, 67	syl5ibrcom 247	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) ∧ 𝑢 ∈ 𝐽) → (𝑣 = (𝑢 ∩ 𝑌) → ((𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢) → (𝑃 ∈ 𝑣 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑣))))
69	68	impd 410	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) ∧ 𝑢 ∈ 𝐽) → ((𝑣 = (𝑢 ∩ 𝑌) ∧ (𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢)) → (𝑃 ∈ 𝑣 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑣)))
70	69	rexlimdva 3131	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → (∃𝑢 ∈ 𝐽 (𝑣 = (𝑢 ∩ 𝑌) ∧ (𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢)) → (𝑃 ∈ 𝑣 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑣)))
71	44, 70	syl5 34	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → ((∃𝑢 ∈ 𝐽 𝑣 = (𝑢 ∩ 𝑌) ∧ ∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢)) → (𝑃 ∈ 𝑣 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑣)))
72	71	expdimp 452	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) ∧ ∃𝑢 ∈ 𝐽 𝑣 = (𝑢 ∩ 𝑌)) → (∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢) → (𝑃 ∈ 𝑣 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑣)))
73	43, 72	syldan 591	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) ∧ 𝑣 ∈ 𝐾) → (∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢) → (𝑃 ∈ 𝑣 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑣)))
74	73	ralrimdva 3130	. . . . . 6 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → (∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢) → ∀𝑣 ∈ 𝐾 (𝑃 ∈ 𝑣 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑣)))
75	38	adantr 480	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) ∧ 𝑢 ∈ 𝐽) → 𝐽 ∈ Top)
76	39	adantr 480	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) ∧ 𝑢 ∈ 𝐽) → 𝑌 ∈ 𝑉)
77		simpr 484	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) ∧ 𝑢 ∈ 𝐽) → 𝑢 ∈ 𝐽)
78		elrestr 17324	. . . . . . . . . . 11 ⊢ ((𝐽 ∈ Top ∧ 𝑌 ∈ 𝑉 ∧ 𝑢 ∈ 𝐽) → (𝑢 ∩ 𝑌) ∈ (𝐽 ↾t 𝑌))
79	75, 76, 77, 78	syl3anc 1373	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) ∧ 𝑢 ∈ 𝐽) → (𝑢 ∩ 𝑌) ∈ (𝐽 ↾t 𝑌))
80	79, 14	eleqtrrdi 2840	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) ∧ 𝑢 ∈ 𝐽) → (𝑢 ∩ 𝑌) ∈ 𝐾)
81	66	rspcv 3571	. . . . . . . . 9 ⊢ ((𝑢 ∩ 𝑌) ∈ 𝐾 → (∀𝑣 ∈ 𝐾 (𝑃 ∈ 𝑣 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑣) → (𝑃 ∈ (𝑢 ∩ 𝑌) → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ (𝑢 ∩ 𝑌))))
82	80, 81	syl 17	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) ∧ 𝑢 ∈ 𝐽) → (∀𝑣 ∈ 𝐾 (𝑃 ∈ 𝑣 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑣) → (𝑃 ∈ (𝑢 ∩ 𝑌) → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ (𝑢 ∩ 𝑌))))
83	82, 61	sylibrd 259	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) ∧ 𝑢 ∈ 𝐽) → (∀𝑣 ∈ 𝐾 (𝑃 ∈ 𝑣 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑣) → (𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢)))
84	83	ralrimdva 3130	. . . . . 6 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → (∀𝑣 ∈ 𝐾 (𝑃 ∈ 𝑣 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑣) → ∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢)))
85	74, 84	impbid 212	. . . . 5 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → (∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢) ↔ ∀𝑣 ∈ 𝐾 (𝑃 ∈ 𝑣 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑣)))
86	36, 85	anbi12d 632	. . . 4 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → ((𝑃 ∈ ∪ 𝐽 ∧ ∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢)) ↔ (𝑃 ∈ (𝑌 ∩ ∪ 𝐽) ∧ ∀𝑣 ∈ 𝐾 (𝑃 ∈ 𝑣 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑣))))
87	38, 2	sylib 218	. . . . 5 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → 𝐽 ∈ (TopOn‘∪ 𝐽))
88		lmss.6	. . . . . 6 ⊢ (𝜑 → 𝑀 ∈ ℤ)
89	88	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → 𝑀 ∈ ℤ)
90	51	ffnd 6648	. . . . . 6 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → 𝐹 Fn 𝑍)
91		simprr 772	. . . . . 6 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → ran 𝐹 ⊆ ∪ 𝐽)
92		df-f 6481	. . . . . 6 ⊢ (𝐹:𝑍⟶∪ 𝐽 ↔ (𝐹 Fn 𝑍 ∧ ran 𝐹 ⊆ ∪ 𝐽))
93	90, 91, 92	sylanbrc 583	. . . . 5 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → 𝐹:𝑍⟶∪ 𝐽)
94		eqidd 2731	. . . . 5 ⊢ (((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = (𝐹‘𝑘))
95	87, 48, 89, 93, 94	lmbrf 23168	. . . 4 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → (𝐹(⇝𝑡‘𝐽)𝑃 ↔ (𝑃 ∈ ∪ 𝐽 ∧ ∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢))))
96	18	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → 𝐾 ∈ (TopOn‘(𝑌 ∩ ∪ 𝐽)))
97	51	frnd 6655	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → ran 𝐹 ⊆ 𝑌)
98	97, 91	ssind 4189	. . . . . 6 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → ran 𝐹 ⊆ (𝑌 ∩ ∪ 𝐽))
99		df-f 6481	. . . . . 6 ⊢ (𝐹:𝑍⟶(𝑌 ∩ ∪ 𝐽) ↔ (𝐹 Fn 𝑍 ∧ ran 𝐹 ⊆ (𝑌 ∩ ∪ 𝐽)))
100	90, 98, 99	sylanbrc 583	. . . . 5 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → 𝐹:𝑍⟶(𝑌 ∩ ∪ 𝐽))
101	96, 48, 89, 100, 94	lmbrf 23168	. . . 4 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → (𝐹(⇝𝑡‘𝐾)𝑃 ↔ (𝑃 ∈ (𝑌 ∩ ∪ 𝐽) ∧ ∀𝑣 ∈ 𝐾 (𝑃 ∈ 𝑣 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑣))))
102	86, 95, 101	3bitr4d 311	. . 3 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → (𝐹(⇝𝑡‘𝐽)𝑃 ↔ 𝐹(⇝𝑡‘𝐾)𝑃))
103	102	ex 412	. 2 ⊢ (𝜑 → ((𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽) → (𝐹(⇝𝑡‘𝐽)𝑃 ↔ 𝐹(⇝𝑡‘𝐾)𝑃)))
104	13, 31, 103	pm5.21ndd 379	1 ⊢ (𝜑 → (𝐹(⇝𝑡‘𝐽)𝑃 ↔ 𝐹(⇝𝑡‘𝐾)𝑃))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1541   ∈ wcel 2110  ∀wral 3045  ∃wrex 3054   ∩ cin 3899   ⊆ wss 3900  ∪ cuni 4857   class class class wbr 5089   × cxp 5612  ran crn 5615   Fn wfn 6472  ⟶wf 6473  ‘cfv 6477  (class class class)co 7341  ℂcc 10996  ℤcz 12460  ℤ_≥cuz 12724   ↾_t crest 17316  Topctop 22801  TopOnctopon 22818  ⇝_𝑡clm 23134

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2112  ax-9 2120  ax-10 2143  ax-11 2159  ax-12 2179  ax-ext 2702  ax-rep 5215  ax-sep 5232  ax-nul 5242  ax-pow 5301  ax-pr 5368  ax-un 7663  ax-cnex 11054  ax-resscn 11055  ax-pre-lttri 11072  ax-pre-lttrn 11073

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-nel 3031  df-ral 3046  df-rex 3055  df-reu 3345  df-rab 3394  df-v 3436  df-sbc 3740  df-csb 3849  df-dif 3903  df-un 3905  df-in 3907  df-ss 3917  df-pss 3920  df-nul 4282  df-if 4474  df-pw 4550  df-sn 4575  df-pr 4577  df-op 4581  df-uni 4858  df-int 4896  df-iun 4941  df-br 5090  df-opab 5152  df-mpt 5171  df-tr 5197  df-id 5509  df-eprel 5514  df-po 5522  df-so 5523  df-fr 5567  df-we 5569  df-xp 5620  df-rel 5621  df-cnv 5622  df-co 5623  df-dm 5624  df-rn 5625  df-res 5626  df-ima 5627  df-ord 6305  df-on 6306  df-lim 6307  df-suc 6308  df-iota 6433  df-fun 6479  df-fn 6480  df-f 6481  df-f1 6482  df-fo 6483  df-f1o 6484  df-fv 6485  df-ov 7344  df-oprab 7345  df-mpo 7346  df-om 7792  df-1st 7916  df-2nd 7917  df-er 8617  df-pm 8748  df-en 8865  df-dom 8866  df-sdom 8867  df-fin 8868  df-fi 9290  df-pnf 11140  df-mnf 11141  df-xr 11142  df-ltxr 11143  df-le 11144  df-neg 11339  df-z 12461  df-uz 12725  df-rest 17318  df-topgen 17339  df-top 22802  df-topon 22819  df-bases 22854  df-lm 23137

This theorem is referenced by:  1stckgen  23462  minvecolem4b  30848  minvecolem4  30850  hhsscms  31248  lmlim  33950  climreeq  45632  xlimclim  45841