Theorem lmss 14885

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 2209	. . . . . . 7 ⊢ ∪ 𝐽 = ∪ 𝐽
3	2	toptopon 14657	. . . . . 6 ⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘∪ 𝐽))
4	1, 3	sylib 122	. . . . 5 ⊢ (𝜑 → 𝐽 ∈ (TopOn‘∪ 𝐽))
5		lmcl 14884	. . . . 5 ⊢ ((𝐽 ∈ (TopOn‘∪ 𝐽) ∧ 𝐹(⇝𝑡‘𝐽)𝑃) → 𝑃 ∈ ∪ 𝐽)
6	4, 5	sylan 283	. . . 4 ⊢ ((𝜑 ∧ 𝐹(⇝𝑡‘𝐽)𝑃) → 𝑃 ∈ ∪ 𝐽)
7		lmfss 14883	. . . . . . 7 ⊢ ((𝐽 ∈ (TopOn‘∪ 𝐽) ∧ 𝐹(⇝𝑡‘𝐽)𝑃) → 𝐹 ⊆ (ℂ × ∪ 𝐽))
8	4, 7	sylan 283	. . . . . 6 ⊢ ((𝜑 ∧ 𝐹(⇝𝑡‘𝐽)𝑃) → 𝐹 ⊆ (ℂ × ∪ 𝐽))
9		rnss 4930	. . . . . 6 ⊢ (𝐹 ⊆ (ℂ × ∪ 𝐽) → ran 𝐹 ⊆ ran (ℂ × ∪ 𝐽))
10	8, 9	syl 14	. . . . 5 ⊢ ((𝜑 ∧ 𝐹(⇝𝑡‘𝐽)𝑃) → ran 𝐹 ⊆ ran (ℂ × ∪ 𝐽))
11		rnxpss 5136	. . . . 5 ⊢ ran (ℂ × ∪ 𝐽) ⊆ ∪ 𝐽
12	10, 11	sstrdi 3216	. . . 4 ⊢ ((𝜑 ∧ 𝐹(⇝𝑡‘𝐽)𝑃) → ran 𝐹 ⊆ ∪ 𝐽)
13	6, 12	jca 306	. . 3 ⊢ ((𝜑 ∧ 𝐹(⇝𝑡‘𝐽)𝑃) → (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽))
14	13	ex 115	. 2 ⊢ (𝜑 → (𝐹(⇝𝑡‘𝐽)𝑃 → (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)))
15		inss2 3405	. . . . 5 ⊢ (𝑌 ∩ ∪ 𝐽) ⊆ ∪ 𝐽
16		lmss.1	. . . . . . 7 ⊢ 𝐾 = (𝐽 ↾t 𝑌)
17		lmss.3	. . . . . . . 8 ⊢ (𝜑 → 𝑌 ∈ 𝑉)
18		resttopon2 14817	. . . . . . . 8 ⊢ ((𝐽 ∈ (TopOn‘∪ 𝐽) ∧ 𝑌 ∈ 𝑉) → (𝐽 ↾t 𝑌) ∈ (TopOn‘(𝑌 ∩ ∪ 𝐽)))
19	4, 17, 18	syl2anc 411	. . . . . . 7 ⊢ (𝜑 → (𝐽 ↾t 𝑌) ∈ (TopOn‘(𝑌 ∩ ∪ 𝐽)))
20	16, 19	eqeltrid 2296	. . . . . 6 ⊢ (𝜑 → 𝐾 ∈ (TopOn‘(𝑌 ∩ ∪ 𝐽)))
21		lmcl 14884	. . . . . 6 ⊢ ((𝐾 ∈ (TopOn‘(𝑌 ∩ ∪ 𝐽)) ∧ 𝐹(⇝𝑡‘𝐾)𝑃) → 𝑃 ∈ (𝑌 ∩ ∪ 𝐽))
22	20, 21	sylan 283	. . . . 5 ⊢ ((𝜑 ∧ 𝐹(⇝𝑡‘𝐾)𝑃) → 𝑃 ∈ (𝑌 ∩ ∪ 𝐽))
23	15, 22	sselid 3202	. . . 4 ⊢ ((𝜑 ∧ 𝐹(⇝𝑡‘𝐾)𝑃) → 𝑃 ∈ ∪ 𝐽)
24		lmfss 14883	. . . . . . . 8 ⊢ ((𝐾 ∈ (TopOn‘(𝑌 ∩ ∪ 𝐽)) ∧ 𝐹(⇝𝑡‘𝐾)𝑃) → 𝐹 ⊆ (ℂ × (𝑌 ∩ ∪ 𝐽)))
25	20, 24	sylan 283	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐹(⇝𝑡‘𝐾)𝑃) → 𝐹 ⊆ (ℂ × (𝑌 ∩ ∪ 𝐽)))
26		rnss 4930	. . . . . . 7 ⊢ (𝐹 ⊆ (ℂ × (𝑌 ∩ ∪ 𝐽)) → ran 𝐹 ⊆ ran (ℂ × (𝑌 ∩ ∪ 𝐽)))
27	25, 26	syl 14	. . . . . 6 ⊢ ((𝜑 ∧ 𝐹(⇝𝑡‘𝐾)𝑃) → ran 𝐹 ⊆ ran (ℂ × (𝑌 ∩ ∪ 𝐽)))
28		rnxpss 5136	. . . . . 6 ⊢ ran (ℂ × (𝑌 ∩ ∪ 𝐽)) ⊆ (𝑌 ∩ ∪ 𝐽)
29	27, 28	sstrdi 3216	. . . . 5 ⊢ ((𝜑 ∧ 𝐹(⇝𝑡‘𝐾)𝑃) → ran 𝐹 ⊆ (𝑌 ∩ ∪ 𝐽))
30	29, 15	sstrdi 3216	. . . 4 ⊢ ((𝜑 ∧ 𝐹(⇝𝑡‘𝐾)𝑃) → ran 𝐹 ⊆ ∪ 𝐽)
31	23, 30	jca 306	. . 3 ⊢ ((𝜑 ∧ 𝐹(⇝𝑡‘𝐾)𝑃) → (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽))
32	31	ex 115	. 2 ⊢ (𝜑 → (𝐹(⇝𝑡‘𝐾)𝑃 → (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)))
33		simprl 529	. . . . . 6 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → 𝑃 ∈ ∪ 𝐽)
34		lmss.5	. . . . . . . 8 ⊢ (𝜑 → 𝑃 ∈ 𝑌)
35	34	adantr 276	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → 𝑃 ∈ 𝑌)
36	35, 33	elind 3369	. . . . . 6 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → 𝑃 ∈ (𝑌 ∩ ∪ 𝐽))
37	33, 36	2thd 175	. . . . 5 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → (𝑃 ∈ ∪ 𝐽 ↔ 𝑃 ∈ (𝑌 ∩ ∪ 𝐽)))
38	16	eleq2i 2276	. . . . . . . . 9 ⊢ (𝑣 ∈ 𝐾 ↔ 𝑣 ∈ (𝐽 ↾t 𝑌))
39	1	adantr 276	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → 𝐽 ∈ Top)
40	17	adantr 276	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → 𝑌 ∈ 𝑉)
41		elrest 13245	. . . . . . . . . . 11 ⊢ ((𝐽 ∈ Top ∧ 𝑌 ∈ 𝑉) → (𝑣 ∈ (𝐽 ↾t 𝑌) ↔ ∃𝑢 ∈ 𝐽 𝑣 = (𝑢 ∩ 𝑌)))
42	39, 40, 41	syl2anc 411	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → (𝑣 ∈ (𝐽 ↾t 𝑌) ↔ ∃𝑢 ∈ 𝐽 𝑣 = (𝑢 ∩ 𝑌)))
43	42	biimpa 296	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) ∧ 𝑣 ∈ (𝐽 ↾t 𝑌)) → ∃𝑢 ∈ 𝐽 𝑣 = (𝑢 ∩ 𝑌))
44	38, 43	sylan2b 287	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) ∧ 𝑣 ∈ 𝐾) → ∃𝑢 ∈ 𝐽 𝑣 = (𝑢 ∩ 𝑌))
45		r19.29r 2649	. . . . . . . . . 10 ⊢ ((∃𝑢 ∈ 𝐽 𝑣 = (𝑢 ∩ 𝑌) ∧ ∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢)) → ∃𝑢 ∈ 𝐽 (𝑣 = (𝑢 ∩ 𝑌) ∧ (𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢)))
46	35	biantrud 304	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → (𝑃 ∈ 𝑢 ↔ (𝑃 ∈ 𝑢 ∧ 𝑃 ∈ 𝑌)))
47		elin 3367	. . . . . . . . . . . . . . . . 17 ⊢ (𝑃 ∈ (𝑢 ∩ 𝑌) ↔ (𝑃 ∈ 𝑢 ∧ 𝑃 ∈ 𝑌))
48	46, 47	bitr4di 198	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → (𝑃 ∈ 𝑢 ↔ 𝑃 ∈ (𝑢 ∩ 𝑌)))
49		lmss.2	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑍 = (ℤ≥‘𝑀)
50	49	uztrn2 9708	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → 𝑘 ∈ 𝑍)
51		lmss.7	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝐹:𝑍⟶𝑌)
52	51	adantr 276	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → 𝐹:𝑍⟶𝑌)
53	52	ffvelcdmda 5743	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ 𝑌)
54	53	biantrud 304	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) ∧ 𝑘 ∈ 𝑍) → ((𝐹‘𝑘) ∈ 𝑢 ↔ ((𝐹‘𝑘) ∈ 𝑢 ∧ (𝐹‘𝑘) ∈ 𝑌)))
55		elin 3367	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐹‘𝑘) ∈ (𝑢 ∩ 𝑌) ↔ ((𝐹‘𝑘) ∈ 𝑢 ∧ (𝐹‘𝑘) ∈ 𝑌))
56	54, 55	bitr4di 198	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) ∧ 𝑘 ∈ 𝑍) → ((𝐹‘𝑘) ∈ 𝑢 ↔ (𝐹‘𝑘) ∈ (𝑢 ∩ 𝑌)))
57	50, 56	sylan2 286	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) ∧ (𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗))) → ((𝐹‘𝑘) ∈ 𝑢 ↔ (𝐹‘𝑘) ∈ (𝑢 ∩ 𝑌)))
58	57	anassrs 400	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → ((𝐹‘𝑘) ∈ 𝑢 ↔ (𝐹‘𝑘) ∈ (𝑢 ∩ 𝑌)))
59	58	ralbidva 2506	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) ∧ 𝑗 ∈ 𝑍) → (∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢 ↔ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ (𝑢 ∩ 𝑌)))
60	59	rexbidva 2507	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → (∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢 ↔ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ (𝑢 ∩ 𝑌)))
61	48, 60	imbi12d 234	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → ((𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢) ↔ (𝑃 ∈ (𝑢 ∩ 𝑌) → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ (𝑢 ∩ 𝑌))))
62	61	adantr 276	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) ∧ 𝑢 ∈ 𝐽) → ((𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢) ↔ (𝑃 ∈ (𝑢 ∩ 𝑌) → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ (𝑢 ∩ 𝑌))))
63	62	biimpd 144	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) ∧ 𝑢 ∈ 𝐽) → ((𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢) → (𝑃 ∈ (𝑢 ∩ 𝑌) → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ (𝑢 ∩ 𝑌))))
64		eleq2 2273	. . . . . . . . . . . . . . 15 ⊢ (𝑣 = (𝑢 ∩ 𝑌) → (𝑃 ∈ 𝑣 ↔ 𝑃 ∈ (𝑢 ∩ 𝑌)))
65		eleq2 2273	. . . . . . . . . . . . . . . 16 ⊢ (𝑣 = (𝑢 ∩ 𝑌) → ((𝐹‘𝑘) ∈ 𝑣 ↔ (𝐹‘𝑘) ∈ (𝑢 ∩ 𝑌)))
66	65	rexralbidv 2536	. . . . . . . . . . . . . . 15 ⊢ (𝑣 = (𝑢 ∩ 𝑌) → (∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑣 ↔ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ (𝑢 ∩ 𝑌)))
67	64, 66	imbi12d 234	. . . . . . . . . . . . . 14 ⊢ (𝑣 = (𝑢 ∩ 𝑌) → ((𝑃 ∈ 𝑣 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑣) ↔ (𝑃 ∈ (𝑢 ∩ 𝑌) → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ (𝑢 ∩ 𝑌))))
68	67	imbi2d 230	. . . . . . . . . . . . 13 ⊢ (𝑣 = (𝑢 ∩ 𝑌) → (((𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢) → (𝑃 ∈ 𝑣 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑣)) ↔ ((𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢) → (𝑃 ∈ (𝑢 ∩ 𝑌) → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ (𝑢 ∩ 𝑌)))))
69	63, 68	syl5ibrcom 157	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) ∧ 𝑢 ∈ 𝐽) → (𝑣 = (𝑢 ∩ 𝑌) → ((𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢) → (𝑃 ∈ 𝑣 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑣))))
70	69	impd 254	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) ∧ 𝑢 ∈ 𝐽) → ((𝑣 = (𝑢 ∩ 𝑌) ∧ (𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢)) → (𝑃 ∈ 𝑣 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑣)))
71	70	rexlimdva 2628	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → (∃𝑢 ∈ 𝐽 (𝑣 = (𝑢 ∩ 𝑌) ∧ (𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢)) → (𝑃 ∈ 𝑣 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑣)))
72	45, 71	syl5 32	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → ((∃𝑢 ∈ 𝐽 𝑣 = (𝑢 ∩ 𝑌) ∧ ∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢)) → (𝑃 ∈ 𝑣 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑣)))
73	72	expdimp 259	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) ∧ ∃𝑢 ∈ 𝐽 𝑣 = (𝑢 ∩ 𝑌)) → (∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢) → (𝑃 ∈ 𝑣 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑣)))
74	44, 73	syldan 282	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) ∧ 𝑣 ∈ 𝐾) → (∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢) → (𝑃 ∈ 𝑣 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑣)))
75	74	ralrimdva 2590	. . . . . 6 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → (∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢) → ∀𝑣 ∈ 𝐾 (𝑃 ∈ 𝑣 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑣)))
76	39	adantr 276	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) ∧ 𝑢 ∈ 𝐽) → 𝐽 ∈ Top)
77	40	adantr 276	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) ∧ 𝑢 ∈ 𝐽) → 𝑌 ∈ 𝑉)
78		simpr 110	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) ∧ 𝑢 ∈ 𝐽) → 𝑢 ∈ 𝐽)
79		elrestr 13246	. . . . . . . . . . 11 ⊢ ((𝐽 ∈ Top ∧ 𝑌 ∈ 𝑉 ∧ 𝑢 ∈ 𝐽) → (𝑢 ∩ 𝑌) ∈ (𝐽 ↾t 𝑌))
80	76, 77, 78, 79	syl3anc 1252	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) ∧ 𝑢 ∈ 𝐽) → (𝑢 ∩ 𝑌) ∈ (𝐽 ↾t 𝑌))
81	80, 16	eleqtrrdi 2303	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) ∧ 𝑢 ∈ 𝐽) → (𝑢 ∩ 𝑌) ∈ 𝐾)
82	67	rspcv 2883	. . . . . . . . 9 ⊢ ((𝑢 ∩ 𝑌) ∈ 𝐾 → (∀𝑣 ∈ 𝐾 (𝑃 ∈ 𝑣 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑣) → (𝑃 ∈ (𝑢 ∩ 𝑌) → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ (𝑢 ∩ 𝑌))))
83	81, 82	syl 14	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) ∧ 𝑢 ∈ 𝐽) → (∀𝑣 ∈ 𝐾 (𝑃 ∈ 𝑣 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑣) → (𝑃 ∈ (𝑢 ∩ 𝑌) → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ (𝑢 ∩ 𝑌))))
84	83, 62	sylibrd 169	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) ∧ 𝑢 ∈ 𝐽) → (∀𝑣 ∈ 𝐾 (𝑃 ∈ 𝑣 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑣) → (𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢)))
85	84	ralrimdva 2590	. . . . . 6 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → (∀𝑣 ∈ 𝐾 (𝑃 ∈ 𝑣 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑣) → ∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢)))
86	75, 85	impbid 129	. . . . 5 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → (∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢) ↔ ∀𝑣 ∈ 𝐾 (𝑃 ∈ 𝑣 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑣)))
87	37, 86	anbi12d 473	. . . 4 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → ((𝑃 ∈ ∪ 𝐽 ∧ ∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢)) ↔ (𝑃 ∈ (𝑌 ∩ ∪ 𝐽) ∧ ∀𝑣 ∈ 𝐾 (𝑃 ∈ 𝑣 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑣))))
88	39, 3	sylib 122	. . . . 5 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → 𝐽 ∈ (TopOn‘∪ 𝐽))
89		lmss.6	. . . . . 6 ⊢ (𝜑 → 𝑀 ∈ ℤ)
90	89	adantr 276	. . . . 5 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → 𝑀 ∈ ℤ)
91	52	ffnd 5450	. . . . . 6 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → 𝐹 Fn 𝑍)
92		simprr 531	. . . . . 6 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → ran 𝐹 ⊆ ∪ 𝐽)
93		df-f 5298	. . . . . 6 ⊢ (𝐹:𝑍⟶∪ 𝐽 ↔ (𝐹 Fn 𝑍 ∧ ran 𝐹 ⊆ ∪ 𝐽))
94	91, 92, 93	sylanbrc 417	. . . . 5 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → 𝐹:𝑍⟶∪ 𝐽)
95		eqidd 2210	. . . . 5 ⊢ (((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = (𝐹‘𝑘))
96	88, 49, 90, 94, 95	lmbrf 14854	. . . 4 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → (𝐹(⇝𝑡‘𝐽)𝑃 ↔ (𝑃 ∈ ∪ 𝐽 ∧ ∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢))))
97	20	adantr 276	. . . . 5 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → 𝐾 ∈ (TopOn‘(𝑌 ∩ ∪ 𝐽)))
98	52	frnd 5459	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → ran 𝐹 ⊆ 𝑌)
99	98, 92	ssind 3408	. . . . . 6 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → ran 𝐹 ⊆ (𝑌 ∩ ∪ 𝐽))
100		df-f 5298	. . . . . 6 ⊢ (𝐹:𝑍⟶(𝑌 ∩ ∪ 𝐽) ↔ (𝐹 Fn 𝑍 ∧ ran 𝐹 ⊆ (𝑌 ∩ ∪ 𝐽)))
101	91, 99, 100	sylanbrc 417	. . . . 5 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → 𝐹:𝑍⟶(𝑌 ∩ ∪ 𝐽))
102	97, 49, 90, 101, 95	lmbrf 14854	. . . 4 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → (𝐹(⇝𝑡‘𝐾)𝑃 ↔ (𝑃 ∈ (𝑌 ∩ ∪ 𝐽) ∧ ∀𝑣 ∈ 𝐾 (𝑃 ∈ 𝑣 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑣))))
103	87, 96, 102	3bitr4d 220	. . 3 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → (𝐹(⇝𝑡‘𝐽)𝑃 ↔ 𝐹(⇝𝑡‘𝐾)𝑃))
104	103	ex 115	. 2 ⊢ (𝜑 → ((𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽) → (𝐹(⇝𝑡‘𝐽)𝑃 ↔ 𝐹(⇝𝑡‘𝐾)𝑃)))
105	14, 32, 104	pm5.21ndd 709	1 ⊢ (𝜑 → (𝐹(⇝𝑡‘𝐽)𝑃 ↔ 𝐹(⇝𝑡‘𝐾)𝑃))

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105   = wceq 1375   ∈ wcel 2180  ∀wral 2488  ∃wrex 2489   ∩ cin 3176   ⊆ wss 3177  ∪ cuni 3867   class class class wbr 4062   × cxp 4694  ran crn 4697   Fn wfn 5289  ⟶wf 5290  ‘cfv 5294  (class class class)co 5974  ℂcc 7965  ℤcz 9414  ℤ_≥cuz 9690   ↾_t crest 13238  Topctop 14636  TopOnctopon 14649  ⇝_𝑡clm 14826

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 617  ax-in2 618  ax-io 713  ax-5 1473  ax-7 1474  ax-gen 1475  ax-ie1 1519  ax-ie2 1520  ax-8 1530  ax-10 1531  ax-11 1532  ax-i12 1533  ax-bndl 1535  ax-4 1536  ax-17 1552  ax-i9 1556  ax-ial 1560  ax-i5r 1561  ax-13 2182  ax-14 2183  ax-ext 2191  ax-coll 4178  ax-sep 4181  ax-pow 4237  ax-pr 4272  ax-un 4501  ax-setind 4606  ax-cnex 8058  ax-resscn 8059  ax-1cn 8060  ax-1re 8061  ax-icn 8062  ax-addcl 8063  ax-addrcl 8064  ax-mulcl 8065  ax-addcom 8067  ax-addass 8069  ax-distr 8071  ax-i2m1 8072  ax-0lt1 8073  ax-0id 8075  ax-rnegex 8076  ax-cnre 8078  ax-pre-ltirr 8079  ax-pre-ltwlin 8080  ax-pre-lttrn 8081  ax-pre-apti 8082  ax-pre-ltadd 8083

This theorem depends on definitions:  df-bi 117  df-dc 839  df-3or 984  df-3an 985  df-tru 1378  df-fal 1381  df-nf 1487  df-sb 1789  df-eu 2060  df-mo 2061  df-clab 2196  df-cleq 2202  df-clel 2205  df-nfc 2341  df-ne 2381  df-nel 2476  df-ral 2493  df-rex 2494  df-reu 2495  df-rab 2497  df-v 2781  df-sbc 3009  df-csb 3105  df-dif 3179  df-un 3181  df-in 3183  df-ss 3190  df-if 3583  df-pw 3631  df-sn 3652  df-pr 3653  df-op 3655  df-uni 3868  df-int 3903  df-iun 3946  df-br 4063  df-opab 4125  df-mpt 4126  df-id 4361  df-xp 4702  df-rel 4703  df-cnv 4704  df-co 4705  df-dm 4706  df-rn 4707  df-res 4708  df-ima 4709  df-iota 5254  df-fun 5296  df-fn 5297  df-f 5298  df-f1 5299  df-fo 5300  df-f1o 5301  df-fv 5302  df-riota 5927  df-ov 5977  df-oprab 5978  df-mpo 5979  df-1st 6256  df-2nd 6257  df-pm 6768  df-pnf 8151  df-mnf 8152  df-xr 8153  df-ltxr 8154  df-le 8155  df-sub 8287  df-neg 8288  df-inn 9079  df-n0 9338  df-z 9415  df-uz 9691  df-rest 13240  df-topgen 13259  df-top 14637  df-topon 14650  df-bases 14682  df-lm 14829

This theorem is referenced by: (None)