Theorem lmss 21102

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		eqid 2622	. . . . . . 7 ⊢ ∪ 𝐽 = ∪ 𝐽
3	2	toptopon 20722	. . . . . 6 ⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘∪ 𝐽))
4	1, 3	sylib 208	. . . . 5 ⊢ (𝜑 → 𝐽 ∈ (TopOn‘∪ 𝐽))
5		lmcl 21101	. . . . 5 ⊢ ((𝐽 ∈ (TopOn‘∪ 𝐽) ∧ 𝐹(⇝𝑡‘𝐽)𝑃) → 𝑃 ∈ ∪ 𝐽)
6	4, 5	sylan 488	. . . 4 ⊢ ((𝜑 ∧ 𝐹(⇝𝑡‘𝐽)𝑃) → 𝑃 ∈ ∪ 𝐽)
7		lmfss 21100	. . . . . . 7 ⊢ ((𝐽 ∈ (TopOn‘∪ 𝐽) ∧ 𝐹(⇝𝑡‘𝐽)𝑃) → 𝐹 ⊆ (ℂ × ∪ 𝐽))
8	4, 7	sylan 488	. . . . . 6 ⊢ ((𝜑 ∧ 𝐹(⇝𝑡‘𝐽)𝑃) → 𝐹 ⊆ (ℂ × ∪ 𝐽))
9		rnss 5354	. . . . . 6 ⊢ (𝐹 ⊆ (ℂ × ∪ 𝐽) → ran 𝐹 ⊆ ran (ℂ × ∪ 𝐽))
10	8, 9	syl 17	. . . . 5 ⊢ ((𝜑 ∧ 𝐹(⇝𝑡‘𝐽)𝑃) → ran 𝐹 ⊆ ran (ℂ × ∪ 𝐽))
11		rnxpss 5566	. . . . 5 ⊢ ran (ℂ × ∪ 𝐽) ⊆ ∪ 𝐽
12	10, 11	syl6ss 3615	. . . 4 ⊢ ((𝜑 ∧ 𝐹(⇝𝑡‘𝐽)𝑃) → ran 𝐹 ⊆ ∪ 𝐽)
13	6, 12	jca 554	. . 3 ⊢ ((𝜑 ∧ 𝐹(⇝𝑡‘𝐽)𝑃) → (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽))
14	13	ex 450	. 2 ⊢ (𝜑 → (𝐹(⇝𝑡‘𝐽)𝑃 → (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)))
15		inss2 3834	. . . . 5 ⊢ (𝑌 ∩ ∪ 𝐽) ⊆ ∪ 𝐽
16		lmss.1	. . . . . . 7 ⊢ 𝐾 = (𝐽 ↾t 𝑌)
17		lmss.3	. . . . . . . 8 ⊢ (𝜑 → 𝑌 ∈ 𝑉)
18		resttopon2 20972	. . . . . . . 8 ⊢ ((𝐽 ∈ (TopOn‘∪ 𝐽) ∧ 𝑌 ∈ 𝑉) → (𝐽 ↾t 𝑌) ∈ (TopOn‘(𝑌 ∩ ∪ 𝐽)))
19	4, 17, 18	syl2anc 693	. . . . . . 7 ⊢ (𝜑 → (𝐽 ↾t 𝑌) ∈ (TopOn‘(𝑌 ∩ ∪ 𝐽)))
20	16, 19	syl5eqel 2705	. . . . . 6 ⊢ (𝜑 → 𝐾 ∈ (TopOn‘(𝑌 ∩ ∪ 𝐽)))
21		lmcl 21101	. . . . . 6 ⊢ ((𝐾 ∈ (TopOn‘(𝑌 ∩ ∪ 𝐽)) ∧ 𝐹(⇝𝑡‘𝐾)𝑃) → 𝑃 ∈ (𝑌 ∩ ∪ 𝐽))
22	20, 21	sylan 488	. . . . 5 ⊢ ((𝜑 ∧ 𝐹(⇝𝑡‘𝐾)𝑃) → 𝑃 ∈ (𝑌 ∩ ∪ 𝐽))
23	15, 22	sseldi 3601	. . . 4 ⊢ ((𝜑 ∧ 𝐹(⇝𝑡‘𝐾)𝑃) → 𝑃 ∈ ∪ 𝐽)
24		lmfss 21100	. . . . . . . 8 ⊢ ((𝐾 ∈ (TopOn‘(𝑌 ∩ ∪ 𝐽)) ∧ 𝐹(⇝𝑡‘𝐾)𝑃) → 𝐹 ⊆ (ℂ × (𝑌 ∩ ∪ 𝐽)))
25	20, 24	sylan 488	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐹(⇝𝑡‘𝐾)𝑃) → 𝐹 ⊆ (ℂ × (𝑌 ∩ ∪ 𝐽)))
26		rnss 5354	. . . . . . 7 ⊢ (𝐹 ⊆ (ℂ × (𝑌 ∩ ∪ 𝐽)) → ran 𝐹 ⊆ ran (ℂ × (𝑌 ∩ ∪ 𝐽)))
27	25, 26	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ 𝐹(⇝𝑡‘𝐾)𝑃) → ran 𝐹 ⊆ ran (ℂ × (𝑌 ∩ ∪ 𝐽)))
28		rnxpss 5566	. . . . . 6 ⊢ ran (ℂ × (𝑌 ∩ ∪ 𝐽)) ⊆ (𝑌 ∩ ∪ 𝐽)
29	27, 28	syl6ss 3615	. . . . 5 ⊢ ((𝜑 ∧ 𝐹(⇝𝑡‘𝐾)𝑃) → ran 𝐹 ⊆ (𝑌 ∩ ∪ 𝐽))
30	29, 15	syl6ss 3615	. . . 4 ⊢ ((𝜑 ∧ 𝐹(⇝𝑡‘𝐾)𝑃) → ran 𝐹 ⊆ ∪ 𝐽)
31	23, 30	jca 554	. . 3 ⊢ ((𝜑 ∧ 𝐹(⇝𝑡‘𝐾)𝑃) → (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽))
32	31	ex 450	. 2 ⊢ (𝜑 → (𝐹(⇝𝑡‘𝐾)𝑃 → (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)))
33		simprl 794	. . . . . 6 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → 𝑃 ∈ ∪ 𝐽)
34		lmss.5	. . . . . . . 8 ⊢ (𝜑 → 𝑃 ∈ 𝑌)
35	34	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → 𝑃 ∈ 𝑌)
36	35, 33	elind 3798	. . . . . 6 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → 𝑃 ∈ (𝑌 ∩ ∪ 𝐽))
37	33, 36	2thd 255	. . . . 5 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → (𝑃 ∈ ∪ 𝐽 ↔ 𝑃 ∈ (𝑌 ∩ ∪ 𝐽)))
38	16	eleq2i 2693	. . . . . . . . 9 ⊢ (𝑣 ∈ 𝐾 ↔ 𝑣 ∈ (𝐽 ↾t 𝑌))
39	1	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → 𝐽 ∈ Top)
40	17	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → 𝑌 ∈ 𝑉)
41		elrest 16088	. . . . . . . . . . 11 ⊢ ((𝐽 ∈ Top ∧ 𝑌 ∈ 𝑉) → (𝑣 ∈ (𝐽 ↾t 𝑌) ↔ ∃𝑢 ∈ 𝐽 𝑣 = (𝑢 ∩ 𝑌)))
42	39, 40, 41	syl2anc 693	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → (𝑣 ∈ (𝐽 ↾t 𝑌) ↔ ∃𝑢 ∈ 𝐽 𝑣 = (𝑢 ∩ 𝑌)))
43	42	biimpa 501	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) ∧ 𝑣 ∈ (𝐽 ↾t 𝑌)) → ∃𝑢 ∈ 𝐽 𝑣 = (𝑢 ∩ 𝑌))
44	38, 43	sylan2b 492	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) ∧ 𝑣 ∈ 𝐾) → ∃𝑢 ∈ 𝐽 𝑣 = (𝑢 ∩ 𝑌))
45		r19.29r 3073	. . . . . . . . . 10 ⊢ ((∃𝑢 ∈ 𝐽 𝑣 = (𝑢 ∩ 𝑌) ∧ ∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢)) → ∃𝑢 ∈ 𝐽 (𝑣 = (𝑢 ∩ 𝑌) ∧ (𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢)))
46	35	biantrud 528	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → (𝑃 ∈ 𝑢 ↔ (𝑃 ∈ 𝑢 ∧ 𝑃 ∈ 𝑌)))
47		elin 3796	. . . . . . . . . . . . . . . . 17 ⊢ (𝑃 ∈ (𝑢 ∩ 𝑌) ↔ (𝑃 ∈ 𝑢 ∧ 𝑃 ∈ 𝑌))
48	46, 47	syl6bbr 278	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → (𝑃 ∈ 𝑢 ↔ 𝑃 ∈ (𝑢 ∩ 𝑌)))
49		lmss.2	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑍 = (ℤ≥‘𝑀)
50	49	uztrn2 11705	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → 𝑘 ∈ 𝑍)
51		lmss.7	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝐹:𝑍⟶𝑌)
52	51	adantr 481	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → 𝐹:𝑍⟶𝑌)
53	52	ffvelrnda 6359	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ 𝑌)
54	53	biantrud 528	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) ∧ 𝑘 ∈ 𝑍) → ((𝐹‘𝑘) ∈ 𝑢 ↔ ((𝐹‘𝑘) ∈ 𝑢 ∧ (𝐹‘𝑘) ∈ 𝑌)))
55		elin 3796	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐹‘𝑘) ∈ (𝑢 ∩ 𝑌) ↔ ((𝐹‘𝑘) ∈ 𝑢 ∧ (𝐹‘𝑘) ∈ 𝑌))
56	54, 55	syl6bbr 278	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) ∧ 𝑘 ∈ 𝑍) → ((𝐹‘𝑘) ∈ 𝑢 ↔ (𝐹‘𝑘) ∈ (𝑢 ∩ 𝑌)))
57	50, 56	sylan2 491	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) ∧ (𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗))) → ((𝐹‘𝑘) ∈ 𝑢 ↔ (𝐹‘𝑘) ∈ (𝑢 ∩ 𝑌)))
58	57	anassrs 680	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → ((𝐹‘𝑘) ∈ 𝑢 ↔ (𝐹‘𝑘) ∈ (𝑢 ∩ 𝑌)))
59	58	ralbidva 2985	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) ∧ 𝑗 ∈ 𝑍) → (∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢 ↔ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ (𝑢 ∩ 𝑌)))
60	59	rexbidva 3049	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → (∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢 ↔ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ (𝑢 ∩ 𝑌)))
61	48, 60	imbi12d 334	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → ((𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢) ↔ (𝑃 ∈ (𝑢 ∩ 𝑌) → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ (𝑢 ∩ 𝑌))))
62	61	adantr 481	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) ∧ 𝑢 ∈ 𝐽) → ((𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢) ↔ (𝑃 ∈ (𝑢 ∩ 𝑌) → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ (𝑢 ∩ 𝑌))))
63	62	biimpd 219	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) ∧ 𝑢 ∈ 𝐽) → ((𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢) → (𝑃 ∈ (𝑢 ∩ 𝑌) → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ (𝑢 ∩ 𝑌))))
64		eleq2 2690	. . . . . . . . . . . . . . 15 ⊢ (𝑣 = (𝑢 ∩ 𝑌) → (𝑃 ∈ 𝑣 ↔ 𝑃 ∈ (𝑢 ∩ 𝑌)))
65		eleq2 2690	. . . . . . . . . . . . . . . 16 ⊢ (𝑣 = (𝑢 ∩ 𝑌) → ((𝐹‘𝑘) ∈ 𝑣 ↔ (𝐹‘𝑘) ∈ (𝑢 ∩ 𝑌)))
66	65	rexralbidv 3058	. . . . . . . . . . . . . . 15 ⊢ (𝑣 = (𝑢 ∩ 𝑌) → (∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑣 ↔ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ (𝑢 ∩ 𝑌)))
67	64, 66	imbi12d 334	. . . . . . . . . . . . . 14 ⊢ (𝑣 = (𝑢 ∩ 𝑌) → ((𝑃 ∈ 𝑣 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑣) ↔ (𝑃 ∈ (𝑢 ∩ 𝑌) → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ (𝑢 ∩ 𝑌))))
68	67	imbi2d 330	. . . . . . . . . . . . 13 ⊢ (𝑣 = (𝑢 ∩ 𝑌) → (((𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢) → (𝑃 ∈ 𝑣 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑣)) ↔ ((𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢) → (𝑃 ∈ (𝑢 ∩ 𝑌) → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ (𝑢 ∩ 𝑌)))))
69	63, 68	syl5ibrcom 237	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) ∧ 𝑢 ∈ 𝐽) → (𝑣 = (𝑢 ∩ 𝑌) → ((𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢) → (𝑃 ∈ 𝑣 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑣))))
70	69	impd 447	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) ∧ 𝑢 ∈ 𝐽) → ((𝑣 = (𝑢 ∩ 𝑌) ∧ (𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢)) → (𝑃 ∈ 𝑣 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑣)))
71	70	rexlimdva 3031	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → (∃𝑢 ∈ 𝐽 (𝑣 = (𝑢 ∩ 𝑌) ∧ (𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢)) → (𝑃 ∈ 𝑣 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑣)))
72	45, 71	syl5 34	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → ((∃𝑢 ∈ 𝐽 𝑣 = (𝑢 ∩ 𝑌) ∧ ∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢)) → (𝑃 ∈ 𝑣 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑣)))
73	72	expdimp 453	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) ∧ ∃𝑢 ∈ 𝐽 𝑣 = (𝑢 ∩ 𝑌)) → (∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢) → (𝑃 ∈ 𝑣 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑣)))
74	44, 73	syldan 487	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) ∧ 𝑣 ∈ 𝐾) → (∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢) → (𝑃 ∈ 𝑣 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑣)))
75	74	ralrimdva 2969	. . . . . 6 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → (∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢) → ∀𝑣 ∈ 𝐾 (𝑃 ∈ 𝑣 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑣)))
76	39	adantr 481	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) ∧ 𝑢 ∈ 𝐽) → 𝐽 ∈ Top)
77	40	adantr 481	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) ∧ 𝑢 ∈ 𝐽) → 𝑌 ∈ 𝑉)
78		simpr 477	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) ∧ 𝑢 ∈ 𝐽) → 𝑢 ∈ 𝐽)
79		elrestr 16089	. . . . . . . . . . 11 ⊢ ((𝐽 ∈ Top ∧ 𝑌 ∈ 𝑉 ∧ 𝑢 ∈ 𝐽) → (𝑢 ∩ 𝑌) ∈ (𝐽 ↾t 𝑌))
80	76, 77, 78, 79	syl3anc 1326	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) ∧ 𝑢 ∈ 𝐽) → (𝑢 ∩ 𝑌) ∈ (𝐽 ↾t 𝑌))
81	80, 16	syl6eleqr 2712	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) ∧ 𝑢 ∈ 𝐽) → (𝑢 ∩ 𝑌) ∈ 𝐾)
82	67	rspcv 3305	. . . . . . . . 9 ⊢ ((𝑢 ∩ 𝑌) ∈ 𝐾 → (∀𝑣 ∈ 𝐾 (𝑃 ∈ 𝑣 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑣) → (𝑃 ∈ (𝑢 ∩ 𝑌) → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ (𝑢 ∩ 𝑌))))
83	81, 82	syl 17	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) ∧ 𝑢 ∈ 𝐽) → (∀𝑣 ∈ 𝐾 (𝑃 ∈ 𝑣 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑣) → (𝑃 ∈ (𝑢 ∩ 𝑌) → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ (𝑢 ∩ 𝑌))))
84	83, 62	sylibrd 249	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) ∧ 𝑢 ∈ 𝐽) → (∀𝑣 ∈ 𝐾 (𝑃 ∈ 𝑣 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑣) → (𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢)))
85	84	ralrimdva 2969	. . . . . 6 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → (∀𝑣 ∈ 𝐾 (𝑃 ∈ 𝑣 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑣) → ∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢)))
86	75, 85	impbid 202	. . . . 5 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → (∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢) ↔ ∀𝑣 ∈ 𝐾 (𝑃 ∈ 𝑣 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑣)))
87	37, 86	anbi12d 747	. . . 4 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → ((𝑃 ∈ ∪ 𝐽 ∧ ∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢)) ↔ (𝑃 ∈ (𝑌 ∩ ∪ 𝐽) ∧ ∀𝑣 ∈ 𝐾 (𝑃 ∈ 𝑣 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑣))))
88	39, 3	sylib 208	. . . . 5 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → 𝐽 ∈ (TopOn‘∪ 𝐽))
89		lmss.6	. . . . . 6 ⊢ (𝜑 → 𝑀 ∈ ℤ)
90	89	adantr 481	. . . . 5 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → 𝑀 ∈ ℤ)
91		ffn 6045	. . . . . . 7 ⊢ (𝐹:𝑍⟶𝑌 → 𝐹 Fn 𝑍)
92	52, 91	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → 𝐹 Fn 𝑍)
93		simprr 796	. . . . . 6 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → ran 𝐹 ⊆ ∪ 𝐽)
94		df-f 5892	. . . . . 6 ⊢ (𝐹:𝑍⟶∪ 𝐽 ↔ (𝐹 Fn 𝑍 ∧ ran 𝐹 ⊆ ∪ 𝐽))
95	92, 93, 94	sylanbrc 698	. . . . 5 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → 𝐹:𝑍⟶∪ 𝐽)
96		eqidd 2623	. . . . 5 ⊢ (((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = (𝐹‘𝑘))
97	88, 49, 90, 95, 96	lmbrf 21064	. . . 4 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → (𝐹(⇝𝑡‘𝐽)𝑃 ↔ (𝑃 ∈ ∪ 𝐽 ∧ ∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢))))
98	20	adantr 481	. . . . 5 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → 𝐾 ∈ (TopOn‘(𝑌 ∩ ∪ 𝐽)))
99		frn 6053	. . . . . . . 8 ⊢ (𝐹:𝑍⟶𝑌 → ran 𝐹 ⊆ 𝑌)
100	52, 99	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → ran 𝐹 ⊆ 𝑌)
101	100, 93	ssind 3837	. . . . . 6 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → ran 𝐹 ⊆ (𝑌 ∩ ∪ 𝐽))
102		df-f 5892	. . . . . 6 ⊢ (𝐹:𝑍⟶(𝑌 ∩ ∪ 𝐽) ↔ (𝐹 Fn 𝑍 ∧ ran 𝐹 ⊆ (𝑌 ∩ ∪ 𝐽)))
103	92, 101, 102	sylanbrc 698	. . . . 5 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → 𝐹:𝑍⟶(𝑌 ∩ ∪ 𝐽))
104	98, 49, 90, 103, 96	lmbrf 21064	. . . 4 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → (𝐹(⇝𝑡‘𝐾)𝑃 ↔ (𝑃 ∈ (𝑌 ∩ ∪ 𝐽) ∧ ∀𝑣 ∈ 𝐾 (𝑃 ∈ 𝑣 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑣))))
105	87, 97, 104	3bitr4d 300	. . 3 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → (𝐹(⇝𝑡‘𝐽)𝑃 ↔ 𝐹(⇝𝑡‘𝐾)𝑃))
106	105	ex 450	. 2 ⊢ (𝜑 → ((𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽) → (𝐹(⇝𝑡‘𝐽)𝑃 ↔ 𝐹(⇝𝑡‘𝐾)𝑃)))
107	14, 32, 106	pm5.21ndd 369	1 ⊢ (𝜑 → (𝐹(⇝𝑡‘𝐽)𝑃 ↔ 𝐹(⇝𝑡‘𝐾)𝑃))

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 384   = wceq 1483   ∈ wcel 1990  ∀wral 2912  ∃wrex 2913   ∩ cin 3573   ⊆ wss 3574  ∪ cuni 4436   class class class wbr 4653   × cxp 5112  ran crn 5115   Fn wfn 5883  ⟶wf 5884  ‘cfv 5888  (class class class)co 6650  ℂcc 9934  ℤcz 11377  ℤ_≥cuz 11687   ↾_t crest 16081  Topctop 20698  TopOnctopon 20715  ⇝_𝑡clm 21030

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-cnex 9992  ax-resscn 9993  ax-pre-lttri 10010  ax-pre-lttrn 10011

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-reu 2919  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-int 4476  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-om 7066  df-1st 7168  df-2nd 7169  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-oadd 7564  df-er 7742  df-pm 7860  df-en 7956  df-dom 7957  df-sdom 7958  df-fin 7959  df-fi 8317  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080  df-neg 10269  df-z 11378  df-uz 11688  df-rest 16083  df-topgen 16104  df-top 20699  df-topon 20716  df-bases 20750  df-lm 21033

This theorem is referenced by:  1stckgen  21357  minvecolem4b  27734  minvecolem4  27736  hhsscms  28136  lmlim  29993  climreeq  39845  xlimclim  40050