Theorem lmss 13040

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 2170	. . . . . . 7 ⊢ ∪ 𝐽 = ∪ 𝐽
3	2	toptopon 12810	. . . . . 6 ⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘∪ 𝐽))
4	1, 3	sylib 121	. . . . 5 ⊢ (𝜑 → 𝐽 ∈ (TopOn‘∪ 𝐽))
5		lmcl 13039	. . . . 5 ⊢ ((𝐽 ∈ (TopOn‘∪ 𝐽) ∧ 𝐹(⇝𝑡‘𝐽)𝑃) → 𝑃 ∈ ∪ 𝐽)
6	4, 5	sylan 281	. . . 4 ⊢ ((𝜑 ∧ 𝐹(⇝𝑡‘𝐽)𝑃) → 𝑃 ∈ ∪ 𝐽)
7		lmfss 13038	. . . . . . 7 ⊢ ((𝐽 ∈ (TopOn‘∪ 𝐽) ∧ 𝐹(⇝𝑡‘𝐽)𝑃) → 𝐹 ⊆ (ℂ × ∪ 𝐽))
8	4, 7	sylan 281	. . . . . 6 ⊢ ((𝜑 ∧ 𝐹(⇝𝑡‘𝐽)𝑃) → 𝐹 ⊆ (ℂ × ∪ 𝐽))
9		rnss 4841	. . . . . 6 ⊢ (𝐹 ⊆ (ℂ × ∪ 𝐽) → ran 𝐹 ⊆ ran (ℂ × ∪ 𝐽))
10	8, 9	syl 14	. . . . 5 ⊢ ((𝜑 ∧ 𝐹(⇝𝑡‘𝐽)𝑃) → ran 𝐹 ⊆ ran (ℂ × ∪ 𝐽))
11		rnxpss 5042	. . . . 5 ⊢ ran (ℂ × ∪ 𝐽) ⊆ ∪ 𝐽
12	10, 11	sstrdi 3159	. . . 4 ⊢ ((𝜑 ∧ 𝐹(⇝𝑡‘𝐽)𝑃) → ran 𝐹 ⊆ ∪ 𝐽)
13	6, 12	jca 304	. . 3 ⊢ ((𝜑 ∧ 𝐹(⇝𝑡‘𝐽)𝑃) → (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽))
14	13	ex 114	. 2 ⊢ (𝜑 → (𝐹(⇝𝑡‘𝐽)𝑃 → (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)))
15		inss2 3348	. . . . 5 ⊢ (𝑌 ∩ ∪ 𝐽) ⊆ ∪ 𝐽
16		lmss.1	. . . . . . 7 ⊢ 𝐾 = (𝐽 ↾t 𝑌)
17		lmss.3	. . . . . . . 8 ⊢ (𝜑 → 𝑌 ∈ 𝑉)
18		resttopon2 12972	. . . . . . . 8 ⊢ ((𝐽 ∈ (TopOn‘∪ 𝐽) ∧ 𝑌 ∈ 𝑉) → (𝐽 ↾t 𝑌) ∈ (TopOn‘(𝑌 ∩ ∪ 𝐽)))
19	4, 17, 18	syl2anc 409	. . . . . . 7 ⊢ (𝜑 → (𝐽 ↾t 𝑌) ∈ (TopOn‘(𝑌 ∩ ∪ 𝐽)))
20	16, 19	eqeltrid 2257	. . . . . 6 ⊢ (𝜑 → 𝐾 ∈ (TopOn‘(𝑌 ∩ ∪ 𝐽)))
21		lmcl 13039	. . . . . 6 ⊢ ((𝐾 ∈ (TopOn‘(𝑌 ∩ ∪ 𝐽)) ∧ 𝐹(⇝𝑡‘𝐾)𝑃) → 𝑃 ∈ (𝑌 ∩ ∪ 𝐽))
22	20, 21	sylan 281	. . . . 5 ⊢ ((𝜑 ∧ 𝐹(⇝𝑡‘𝐾)𝑃) → 𝑃 ∈ (𝑌 ∩ ∪ 𝐽))
23	15, 22	sselid 3145	. . . 4 ⊢ ((𝜑 ∧ 𝐹(⇝𝑡‘𝐾)𝑃) → 𝑃 ∈ ∪ 𝐽)
24		lmfss 13038	. . . . . . . 8 ⊢ ((𝐾 ∈ (TopOn‘(𝑌 ∩ ∪ 𝐽)) ∧ 𝐹(⇝𝑡‘𝐾)𝑃) → 𝐹 ⊆ (ℂ × (𝑌 ∩ ∪ 𝐽)))
25	20, 24	sylan 281	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐹(⇝𝑡‘𝐾)𝑃) → 𝐹 ⊆ (ℂ × (𝑌 ∩ ∪ 𝐽)))
26		rnss 4841	. . . . . . 7 ⊢ (𝐹 ⊆ (ℂ × (𝑌 ∩ ∪ 𝐽)) → ran 𝐹 ⊆ ran (ℂ × (𝑌 ∩ ∪ 𝐽)))
27	25, 26	syl 14	. . . . . 6 ⊢ ((𝜑 ∧ 𝐹(⇝𝑡‘𝐾)𝑃) → ran 𝐹 ⊆ ran (ℂ × (𝑌 ∩ ∪ 𝐽)))
28		rnxpss 5042	. . . . . 6 ⊢ ran (ℂ × (𝑌 ∩ ∪ 𝐽)) ⊆ (𝑌 ∩ ∪ 𝐽)
29	27, 28	sstrdi 3159	. . . . 5 ⊢ ((𝜑 ∧ 𝐹(⇝𝑡‘𝐾)𝑃) → ran 𝐹 ⊆ (𝑌 ∩ ∪ 𝐽))
30	29, 15	sstrdi 3159	. . . 4 ⊢ ((𝜑 ∧ 𝐹(⇝𝑡‘𝐾)𝑃) → ran 𝐹 ⊆ ∪ 𝐽)
31	23, 30	jca 304	. . 3 ⊢ ((𝜑 ∧ 𝐹(⇝𝑡‘𝐾)𝑃) → (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽))
32	31	ex 114	. 2 ⊢ (𝜑 → (𝐹(⇝𝑡‘𝐾)𝑃 → (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)))
33		simprl 526	. . . . . 6 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → 𝑃 ∈ ∪ 𝐽)
34		lmss.5	. . . . . . . 8 ⊢ (𝜑 → 𝑃 ∈ 𝑌)
35	34	adantr 274	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → 𝑃 ∈ 𝑌)
36	35, 33	elind 3312	. . . . . 6 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → 𝑃 ∈ (𝑌 ∩ ∪ 𝐽))
37	33, 36	2thd 174	. . . . 5 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → (𝑃 ∈ ∪ 𝐽 ↔ 𝑃 ∈ (𝑌 ∩ ∪ 𝐽)))
38	16	eleq2i 2237	. . . . . . . . 9 ⊢ (𝑣 ∈ 𝐾 ↔ 𝑣 ∈ (𝐽 ↾t 𝑌))
39	1	adantr 274	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → 𝐽 ∈ Top)
40	17	adantr 274	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → 𝑌 ∈ 𝑉)
41		elrest 12586	. . . . . . . . . . 11 ⊢ ((𝐽 ∈ Top ∧ 𝑌 ∈ 𝑉) → (𝑣 ∈ (𝐽 ↾t 𝑌) ↔ ∃𝑢 ∈ 𝐽 𝑣 = (𝑢 ∩ 𝑌)))
42	39, 40, 41	syl2anc 409	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → (𝑣 ∈ (𝐽 ↾t 𝑌) ↔ ∃𝑢 ∈ 𝐽 𝑣 = (𝑢 ∩ 𝑌)))
43	42	biimpa 294	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) ∧ 𝑣 ∈ (𝐽 ↾t 𝑌)) → ∃𝑢 ∈ 𝐽 𝑣 = (𝑢 ∩ 𝑌))
44	38, 43	sylan2b 285	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) ∧ 𝑣 ∈ 𝐾) → ∃𝑢 ∈ 𝐽 𝑣 = (𝑢 ∩ 𝑌))
45		r19.29r 2608	. . . . . . . . . 10 ⊢ ((∃𝑢 ∈ 𝐽 𝑣 = (𝑢 ∩ 𝑌) ∧ ∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢)) → ∃𝑢 ∈ 𝐽 (𝑣 = (𝑢 ∩ 𝑌) ∧ (𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢)))
46	35	biantrud 302	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → (𝑃 ∈ 𝑢 ↔ (𝑃 ∈ 𝑢 ∧ 𝑃 ∈ 𝑌)))
47		elin 3310	. . . . . . . . . . . . . . . . 17 ⊢ (𝑃 ∈ (𝑢 ∩ 𝑌) ↔ (𝑃 ∈ 𝑢 ∧ 𝑃 ∈ 𝑌))
48	46, 47	bitr4di 197	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → (𝑃 ∈ 𝑢 ↔ 𝑃 ∈ (𝑢 ∩ 𝑌)))
49		lmss.2	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑍 = (ℤ≥‘𝑀)
50	49	uztrn2 9504	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → 𝑘 ∈ 𝑍)
51		lmss.7	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝐹:𝑍⟶𝑌)
52	51	adantr 274	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → 𝐹:𝑍⟶𝑌)
53	52	ffvelrnda 5631	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ 𝑌)
54	53	biantrud 302	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) ∧ 𝑘 ∈ 𝑍) → ((𝐹‘𝑘) ∈ 𝑢 ↔ ((𝐹‘𝑘) ∈ 𝑢 ∧ (𝐹‘𝑘) ∈ 𝑌)))
55		elin 3310	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐹‘𝑘) ∈ (𝑢 ∩ 𝑌) ↔ ((𝐹‘𝑘) ∈ 𝑢 ∧ (𝐹‘𝑘) ∈ 𝑌))
56	54, 55	bitr4di 197	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) ∧ 𝑘 ∈ 𝑍) → ((𝐹‘𝑘) ∈ 𝑢 ↔ (𝐹‘𝑘) ∈ (𝑢 ∩ 𝑌)))
57	50, 56	sylan2 284	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) ∧ (𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗))) → ((𝐹‘𝑘) ∈ 𝑢 ↔ (𝐹‘𝑘) ∈ (𝑢 ∩ 𝑌)))
58	57	anassrs 398	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → ((𝐹‘𝑘) ∈ 𝑢 ↔ (𝐹‘𝑘) ∈ (𝑢 ∩ 𝑌)))
59	58	ralbidva 2466	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) ∧ 𝑗 ∈ 𝑍) → (∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢 ↔ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ (𝑢 ∩ 𝑌)))
60	59	rexbidva 2467	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → (∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢 ↔ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ (𝑢 ∩ 𝑌)))
61	48, 60	imbi12d 233	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → ((𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢) ↔ (𝑃 ∈ (𝑢 ∩ 𝑌) → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ (𝑢 ∩ 𝑌))))
62	61	adantr 274	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) ∧ 𝑢 ∈ 𝐽) → ((𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢) ↔ (𝑃 ∈ (𝑢 ∩ 𝑌) → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ (𝑢 ∩ 𝑌))))
63	62	biimpd 143	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) ∧ 𝑢 ∈ 𝐽) → ((𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢) → (𝑃 ∈ (𝑢 ∩ 𝑌) → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ (𝑢 ∩ 𝑌))))
64		eleq2 2234	. . . . . . . . . . . . . . 15 ⊢ (𝑣 = (𝑢 ∩ 𝑌) → (𝑃 ∈ 𝑣 ↔ 𝑃 ∈ (𝑢 ∩ 𝑌)))
65		eleq2 2234	. . . . . . . . . . . . . . . 16 ⊢ (𝑣 = (𝑢 ∩ 𝑌) → ((𝐹‘𝑘) ∈ 𝑣 ↔ (𝐹‘𝑘) ∈ (𝑢 ∩ 𝑌)))
66	65	rexralbidv 2496	. . . . . . . . . . . . . . 15 ⊢ (𝑣 = (𝑢 ∩ 𝑌) → (∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑣 ↔ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ (𝑢 ∩ 𝑌)))
67	64, 66	imbi12d 233	. . . . . . . . . . . . . 14 ⊢ (𝑣 = (𝑢 ∩ 𝑌) → ((𝑃 ∈ 𝑣 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑣) ↔ (𝑃 ∈ (𝑢 ∩ 𝑌) → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ (𝑢 ∩ 𝑌))))
68	67	imbi2d 229	. . . . . . . . . . . . 13 ⊢ (𝑣 = (𝑢 ∩ 𝑌) → (((𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢) → (𝑃 ∈ 𝑣 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑣)) ↔ ((𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢) → (𝑃 ∈ (𝑢 ∩ 𝑌) → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ (𝑢 ∩ 𝑌)))))
69	63, 68	syl5ibrcom 156	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) ∧ 𝑢 ∈ 𝐽) → (𝑣 = (𝑢 ∩ 𝑌) → ((𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢) → (𝑃 ∈ 𝑣 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑣))))
70	69	impd 252	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) ∧ 𝑢 ∈ 𝐽) → ((𝑣 = (𝑢 ∩ 𝑌) ∧ (𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢)) → (𝑃 ∈ 𝑣 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑣)))
71	70	rexlimdva 2587	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → (∃𝑢 ∈ 𝐽 (𝑣 = (𝑢 ∩ 𝑌) ∧ (𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢)) → (𝑃 ∈ 𝑣 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑣)))
72	45, 71	syl5 32	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → ((∃𝑢 ∈ 𝐽 𝑣 = (𝑢 ∩ 𝑌) ∧ ∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢)) → (𝑃 ∈ 𝑣 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑣)))
73	72	expdimp 257	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) ∧ ∃𝑢 ∈ 𝐽 𝑣 = (𝑢 ∩ 𝑌)) → (∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢) → (𝑃 ∈ 𝑣 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑣)))
74	44, 73	syldan 280	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) ∧ 𝑣 ∈ 𝐾) → (∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢) → (𝑃 ∈ 𝑣 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑣)))
75	74	ralrimdva 2550	. . . . . 6 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → (∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢) → ∀𝑣 ∈ 𝐾 (𝑃 ∈ 𝑣 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑣)))
76	39	adantr 274	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) ∧ 𝑢 ∈ 𝐽) → 𝐽 ∈ Top)
77	40	adantr 274	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) ∧ 𝑢 ∈ 𝐽) → 𝑌 ∈ 𝑉)
78		simpr 109	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) ∧ 𝑢 ∈ 𝐽) → 𝑢 ∈ 𝐽)
79		elrestr 12587	. . . . . . . . . . 11 ⊢ ((𝐽 ∈ Top ∧ 𝑌 ∈ 𝑉 ∧ 𝑢 ∈ 𝐽) → (𝑢 ∩ 𝑌) ∈ (𝐽 ↾t 𝑌))
80	76, 77, 78, 79	syl3anc 1233	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) ∧ 𝑢 ∈ 𝐽) → (𝑢 ∩ 𝑌) ∈ (𝐽 ↾t 𝑌))
81	80, 16	eleqtrrdi 2264	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) ∧ 𝑢 ∈ 𝐽) → (𝑢 ∩ 𝑌) ∈ 𝐾)
82	67	rspcv 2830	. . . . . . . . 9 ⊢ ((𝑢 ∩ 𝑌) ∈ 𝐾 → (∀𝑣 ∈ 𝐾 (𝑃 ∈ 𝑣 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑣) → (𝑃 ∈ (𝑢 ∩ 𝑌) → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ (𝑢 ∩ 𝑌))))
83	81, 82	syl 14	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) ∧ 𝑢 ∈ 𝐽) → (∀𝑣 ∈ 𝐾 (𝑃 ∈ 𝑣 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑣) → (𝑃 ∈ (𝑢 ∩ 𝑌) → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ (𝑢 ∩ 𝑌))))
84	83, 62	sylibrd 168	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) ∧ 𝑢 ∈ 𝐽) → (∀𝑣 ∈ 𝐾 (𝑃 ∈ 𝑣 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑣) → (𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢)))
85	84	ralrimdva 2550	. . . . . 6 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → (∀𝑣 ∈ 𝐾 (𝑃 ∈ 𝑣 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑣) → ∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢)))
86	75, 85	impbid 128	. . . . 5 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → (∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢) ↔ ∀𝑣 ∈ 𝐾 (𝑃 ∈ 𝑣 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑣)))
87	37, 86	anbi12d 470	. . . 4 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → ((𝑃 ∈ ∪ 𝐽 ∧ ∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢)) ↔ (𝑃 ∈ (𝑌 ∩ ∪ 𝐽) ∧ ∀𝑣 ∈ 𝐾 (𝑃 ∈ 𝑣 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑣))))
88	39, 3	sylib 121	. . . . 5 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → 𝐽 ∈ (TopOn‘∪ 𝐽))
89		lmss.6	. . . . . 6 ⊢ (𝜑 → 𝑀 ∈ ℤ)
90	89	adantr 274	. . . . 5 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → 𝑀 ∈ ℤ)
91	52	ffnd 5348	. . . . . 6 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → 𝐹 Fn 𝑍)
92		simprr 527	. . . . . 6 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → ran 𝐹 ⊆ ∪ 𝐽)
93		df-f 5202	. . . . . 6 ⊢ (𝐹:𝑍⟶∪ 𝐽 ↔ (𝐹 Fn 𝑍 ∧ ran 𝐹 ⊆ ∪ 𝐽))
94	91, 92, 93	sylanbrc 415	. . . . 5 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → 𝐹:𝑍⟶∪ 𝐽)
95		eqidd 2171	. . . . 5 ⊢ (((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = (𝐹‘𝑘))
96	88, 49, 90, 94, 95	lmbrf 13009	. . . 4 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → (𝐹(⇝𝑡‘𝐽)𝑃 ↔ (𝑃 ∈ ∪ 𝐽 ∧ ∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢))))
97	20	adantr 274	. . . . 5 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → 𝐾 ∈ (TopOn‘(𝑌 ∩ ∪ 𝐽)))
98	52	frnd 5357	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → ran 𝐹 ⊆ 𝑌)
99	98, 92	ssind 3351	. . . . . 6 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → ran 𝐹 ⊆ (𝑌 ∩ ∪ 𝐽))
100		df-f 5202	. . . . . 6 ⊢ (𝐹:𝑍⟶(𝑌 ∩ ∪ 𝐽) ↔ (𝐹 Fn 𝑍 ∧ ran 𝐹 ⊆ (𝑌 ∩ ∪ 𝐽)))
101	91, 99, 100	sylanbrc 415	. . . . 5 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → 𝐹:𝑍⟶(𝑌 ∩ ∪ 𝐽))
102	97, 49, 90, 101, 95	lmbrf 13009	. . . 4 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → (𝐹(⇝𝑡‘𝐾)𝑃 ↔ (𝑃 ∈ (𝑌 ∩ ∪ 𝐽) ∧ ∀𝑣 ∈ 𝐾 (𝑃 ∈ 𝑣 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑣))))
103	87, 96, 102	3bitr4d 219	. . 3 ⊢ ((𝜑 ∧ (𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽)) → (𝐹(⇝𝑡‘𝐽)𝑃 ↔ 𝐹(⇝𝑡‘𝐾)𝑃))
104	103	ex 114	. 2 ⊢ (𝜑 → ((𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽) → (𝐹(⇝𝑡‘𝐽)𝑃 ↔ 𝐹(⇝𝑡‘𝐾)𝑃)))
105	14, 32, 104	pm5.21ndd 700	1 ⊢ (𝜑 → (𝐹(⇝𝑡‘𝐽)𝑃 ↔ 𝐹(⇝𝑡‘𝐾)𝑃))

Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104   = wceq 1348   ∈ wcel 2141  ∀wral 2448  ∃wrex 2449   ∩ cin 3120   ⊆ wss 3121  ∪ cuni 3796   class class class wbr 3989   × cxp 4609  ran crn 4612   Fn wfn 5193  ⟶wf 5194  ‘cfv 5198  (class class class)co 5853  ℂcc 7772  ℤcz 9212  ℤ_≥cuz 9487   ↾_t crest 12579  Topctop 12789  TopOnctopon 12802  ⇝_𝑡clm 12981

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 609  ax-in2 610  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-13 2143  ax-14 2144  ax-ext 2152  ax-coll 4104  ax-sep 4107  ax-pow 4160  ax-pr 4194  ax-un 4418  ax-setind 4521  ax-cnex 7865  ax-resscn 7866  ax-1cn 7867  ax-1re 7868  ax-icn 7869  ax-addcl 7870  ax-addrcl 7871  ax-mulcl 7872  ax-addcom 7874  ax-addass 7876  ax-distr 7878  ax-i2m1 7879  ax-0lt1 7880  ax-0id 7882  ax-rnegex 7883  ax-cnre 7885  ax-pre-ltirr 7886  ax-pre-ltwlin 7887  ax-pre-lttrn 7888  ax-pre-apti 7889  ax-pre-ltadd 7890

This theorem depends on definitions:  df-bi 116  df-dc 830  df-3or 974  df-3an 975  df-tru 1351  df-fal 1354  df-nf 1454  df-sb 1756  df-eu 2022  df-mo 2023  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-ne 2341  df-nel 2436  df-ral 2453  df-rex 2454  df-reu 2455  df-rab 2457  df-v 2732  df-sbc 2956  df-csb 3050  df-dif 3123  df-un 3125  df-in 3127  df-ss 3134  df-if 3527  df-pw 3568  df-sn 3589  df-pr 3590  df-op 3592  df-uni 3797  df-int 3832  df-iun 3875  df-br 3990  df-opab 4051  df-mpt 4052  df-id 4278  df-xp 4617  df-rel 4618  df-cnv 4619  df-co 4620  df-dm 4621  df-rn 4622  df-res 4623  df-ima 4624  df-iota 5160  df-fun 5200  df-fn 5201  df-f 5202  df-f1 5203  df-fo 5204  df-f1o 5205  df-fv 5206  df-riota 5809  df-ov 5856  df-oprab 5857  df-mpo 5858  df-1st 6119  df-2nd 6120  df-pm 6629  df-pnf 7956  df-mnf 7957  df-xr 7958  df-ltxr 7959  df-le 7960  df-sub 8092  df-neg 8093  df-inn 8879  df-n0 9136  df-z 9213  df-uz 9488  df-rest 12581  df-topgen 12600  df-top 12790  df-topon 12803  df-bases 12835  df-lm 12984

This theorem is referenced by: (None)