Metamath Proof Explorer

Theorem lmss

Description: Limit on a subspace. (Contributed by NM, 30-Jan-2008) (Revised by Mario Carneiro, 30-Dec-2013)

Ref Expression
Hypotheses lmss.1 ⊢ 𝐾 = ( 𝐽 ↾t 𝑌 )
lmss.2 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
lmss.3 ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
lmss.4 ⊢ ( 𝜑 → 𝐽 ∈ Top )
lmss.5 ⊢ ( 𝜑 → 𝑃 ∈ 𝑌 )
lmss.6 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
lmss.7 ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ 𝑌 )
Assertion lmss ( 𝜑 → ( 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ↔ 𝐹 ( ⇝𝑡 ‘ 𝐾 ) 𝑃 ) )

Proof

Step Hyp Ref Expression
1 lmss.1 ⊢ 𝐾 = ( 𝐽 ↾t 𝑌 )
2 lmss.2 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
3 lmss.3 ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
4 lmss.4 ⊢ ( 𝜑 → 𝐽 ∈ Top )
5 lmss.5 ⊢ ( 𝜑 → 𝑃 ∈ 𝑌 )
6 lmss.6 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
7 lmss.7 ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ 𝑌 )
8 toptopon2 ⊢ ( 𝐽 ∈ Top ↔ 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) )
9 4 8 sylib ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) )
10 lmcl ⊢ ( ( 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) ∧ 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ) → 𝑃 ∈ ∪ 𝐽 )
11 9 10 sylan ⊢ ( ( 𝜑 ∧ 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ) → 𝑃 ∈ ∪ 𝐽 )
12 lmfss ⊢ ( ( 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) ∧ 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ) → 𝐹 ⊆ ( ℂ × ∪ 𝐽 ) )
13 9 12 sylan ⊢ ( ( 𝜑 ∧ 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ) → 𝐹 ⊆ ( ℂ × ∪ 𝐽 ) )
14 rnss ⊢ ( 𝐹 ⊆ ( ℂ × ∪ 𝐽 ) → ran 𝐹 ⊆ ran ( ℂ × ∪ 𝐽 ) )
15 13 14 syl ⊢ ( ( 𝜑 ∧ 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ) → ran 𝐹 ⊆ ran ( ℂ × ∪ 𝐽 ) )
16 rnxpss ⊢ ran ( ℂ × ∪ 𝐽 ) ⊆ ∪ 𝐽
17 15 16 sstrdi ⊢ ( ( 𝜑 ∧ 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ) → ran 𝐹 ⊆ ∪ 𝐽 )
18 11 17 jca ⊢ ( ( 𝜑 ∧ 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ) → ( 𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽 ) )
19 18 ex ⊢ ( 𝜑 → ( 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 → ( 𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽 ) ) )
20 resttopon2 ⊢ ( ( 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) ∧ 𝑌 ∈ 𝑉 ) → ( 𝐽 ↾t 𝑌 ) ∈ ( TopOn ‘ ( 𝑌 ∩ ∪ 𝐽 ) ) )
21 9 3 20 syl2anc ⊢ ( 𝜑 → ( 𝐽 ↾t 𝑌 ) ∈ ( TopOn ‘ ( 𝑌 ∩ ∪ 𝐽 ) ) )
22 1 21 eqeltrid ⊢ ( 𝜑 → 𝐾 ∈ ( TopOn ‘ ( 𝑌 ∩ ∪ 𝐽 ) ) )
23 lmcl ⊢ ( ( 𝐾 ∈ ( TopOn ‘ ( 𝑌 ∩ ∪ 𝐽 ) ) ∧ 𝐹 ( ⇝𝑡 ‘ 𝐾 ) 𝑃 ) → 𝑃 ∈ ( 𝑌 ∩ ∪ 𝐽 ) )
24 22 23 sylan ⊢ ( ( 𝜑 ∧ 𝐹 ( ⇝𝑡 ‘ 𝐾 ) 𝑃 ) → 𝑃 ∈ ( 𝑌 ∩ ∪ 𝐽 ) )
25 24 elin2d ⊢ ( ( 𝜑 ∧ 𝐹 ( ⇝𝑡 ‘ 𝐾 ) 𝑃 ) → 𝑃 ∈ ∪ 𝐽 )
26 lmfss ⊢ ( ( 𝐾 ∈ ( TopOn ‘ ( 𝑌 ∩ ∪ 𝐽 ) ) ∧ 𝐹 ( ⇝𝑡 ‘ 𝐾 ) 𝑃 ) → 𝐹 ⊆ ( ℂ × ( 𝑌 ∩ ∪ 𝐽 ) ) )
27 22 26 sylan ⊢ ( ( 𝜑 ∧ 𝐹 ( ⇝𝑡 ‘ 𝐾 ) 𝑃 ) → 𝐹 ⊆ ( ℂ × ( 𝑌 ∩ ∪ 𝐽 ) ) )
28 rnss ⊢ ( 𝐹 ⊆ ( ℂ × ( 𝑌 ∩ ∪ 𝐽 ) ) → ran 𝐹 ⊆ ran ( ℂ × ( 𝑌 ∩ ∪ 𝐽 ) ) )
29 27 28 syl ⊢ ( ( 𝜑 ∧ 𝐹 ( ⇝𝑡 ‘ 𝐾 ) 𝑃 ) → ran 𝐹 ⊆ ran ( ℂ × ( 𝑌 ∩ ∪ 𝐽 ) ) )
30 rnxpss ⊢ ran ( ℂ × ( 𝑌 ∩ ∪ 𝐽 ) ) ⊆ ( 𝑌 ∩ ∪ 𝐽 )
31 29 30 sstrdi ⊢ ( ( 𝜑 ∧ 𝐹 ( ⇝𝑡 ‘ 𝐾 ) 𝑃 ) → ran 𝐹 ⊆ ( 𝑌 ∩ ∪ 𝐽 ) )
32 inss2 ⊢ ( 𝑌 ∩ ∪ 𝐽 ) ⊆ ∪ 𝐽
33 31 32 sstrdi ⊢ ( ( 𝜑 ∧ 𝐹 ( ⇝𝑡 ‘ 𝐾 ) 𝑃 ) → ran 𝐹 ⊆ ∪ 𝐽 )
34 25 33 jca ⊢ ( ( 𝜑 ∧ 𝐹 ( ⇝𝑡 ‘ 𝐾 ) 𝑃 ) → ( 𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽 ) )
35 34 ex ⊢ ( 𝜑 → ( 𝐹 ( ⇝𝑡 ‘ 𝐾 ) 𝑃 → ( 𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽 ) ) )
36 simprl ⊢ ( ( 𝜑 ∧ ( 𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽 ) ) → 𝑃 ∈ ∪ 𝐽 )
37 5 adantr ⊢ ( ( 𝜑 ∧ ( 𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽 ) ) → 𝑃 ∈ 𝑌 )
38 37 36 elind ⊢ ( ( 𝜑 ∧ ( 𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽 ) ) → 𝑃 ∈ ( 𝑌 ∩ ∪ 𝐽 ) )
39 36 38 2thd ⊢ ( ( 𝜑 ∧ ( 𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽 ) ) → ( 𝑃 ∈ ∪ 𝐽 ↔ 𝑃 ∈ ( 𝑌 ∩ ∪ 𝐽 ) ) )
40 1 eleq2i ⊢ ( 𝑣 ∈ 𝐾 ↔ 𝑣 ∈ ( 𝐽 ↾t 𝑌 ) )
41 4 adantr ⊢ ( ( 𝜑 ∧ ( 𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽 ) ) → 𝐽 ∈ Top )
42 3 adantr ⊢ ( ( 𝜑 ∧ ( 𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽 ) ) → 𝑌 ∈ 𝑉 )
43 elrest ⊢ ( ( 𝐽 ∈ Top ∧ 𝑌 ∈ 𝑉 ) → ( 𝑣 ∈ ( 𝐽 ↾t 𝑌 ) ↔ ∃ 𝑢 ∈ 𝐽 𝑣 = ( 𝑢 ∩ 𝑌 ) ) )
44 41 42 43 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽 ) ) → ( 𝑣 ∈ ( 𝐽 ↾t 𝑌 ) ↔ ∃ 𝑢 ∈ 𝐽 𝑣 = ( 𝑢 ∩ 𝑌 ) ) )
45 44 biimpa ⊢ ( ( ( 𝜑 ∧ ( 𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽 ) ) ∧ 𝑣 ∈ ( 𝐽 ↾t 𝑌 ) ) → ∃ 𝑢 ∈ 𝐽 𝑣 = ( 𝑢 ∩ 𝑌 ) )
46 40 45 sylan2b ⊢ ( ( ( 𝜑 ∧ ( 𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽 ) ) ∧ 𝑣 ∈ 𝐾 ) → ∃ 𝑢 ∈ 𝐽 𝑣 = ( 𝑢 ∩ 𝑌 ) )
47 r19.29r ⊢ ( ( ∃ 𝑢 ∈ 𝐽 𝑣 = ( 𝑢 ∩ 𝑌 ) ∧ ∀ 𝑢 ∈ 𝐽 ( 𝑃 ∈ 𝑢 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ) → ∃ 𝑢 ∈ 𝐽 ( 𝑣 = ( 𝑢 ∩ 𝑌 ) ∧ ( 𝑃 ∈ 𝑢 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ) )
48 37 biantrud ⊢ ( ( 𝜑 ∧ ( 𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽 ) ) → ( 𝑃 ∈ 𝑢 ↔ ( 𝑃 ∈ 𝑢 ∧ 𝑃 ∈ 𝑌 ) ) )
49 elin ⊢ ( 𝑃 ∈ ( 𝑢 ∩ 𝑌 ) ↔ ( 𝑃 ∈ 𝑢 ∧ 𝑃 ∈ 𝑌 ) )
50 48 49 bitr4di ⊢ ( ( 𝜑 ∧ ( 𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽 ) ) → ( 𝑃 ∈ 𝑢 ↔ 𝑃 ∈ ( 𝑢 ∩ 𝑌 ) ) )
51 2 uztrn2 ⊢ ( ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 𝑘 ∈ 𝑍 )
52 7 adantr ⊢ ( ( 𝜑 ∧ ( 𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽 ) ) → 𝐹 : 𝑍 ⟶ 𝑌 )
53 52 ffvelrnda ⊢ ( ( ( 𝜑 ∧ ( 𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽 ) ) ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ 𝑌 )
54 53 biantrud ⊢ ( ( ( 𝜑 ∧ ( 𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽 ) ) ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ↔ ( ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑌 ) ) )
55 elin ⊢ ( ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑢 ∩ 𝑌 ) ↔ ( ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑌 ) )
56 54 55 bitr4di ⊢ ( ( ( 𝜑 ∧ ( 𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽 ) ) ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ↔ ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑢 ∩ 𝑌 ) ) )
57 51 56 sylan2 ⊢ ( ( ( 𝜑 ∧ ( 𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽 ) ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ↔ ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑢 ∩ 𝑌 ) ) )
58 57 anassrs ⊢ ( ( ( ( 𝜑 ∧ ( 𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽 ) ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ↔ ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑢 ∩ 𝑌 ) ) )
59 58 ralbidva ⊢ ( ( ( 𝜑 ∧ ( 𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽 ) ) ∧ 𝑗 ∈ 𝑍 ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ↔ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑢 ∩ 𝑌 ) ) )
60 59 rexbidva ⊢ ( ( 𝜑 ∧ ( 𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽 ) ) → ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ↔ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑢 ∩ 𝑌 ) ) )
61 50 60 imbi12d ⊢ ( ( 𝜑 ∧ ( 𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽 ) ) → ( ( 𝑃 ∈ 𝑢 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ↔ ( 𝑃 ∈ ( 𝑢 ∩ 𝑌 ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑢 ∩ 𝑌 ) ) ) )
62 61 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽 ) ) ∧ 𝑢 ∈ 𝐽 ) → ( ( 𝑃 ∈ 𝑢 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ↔ ( 𝑃 ∈ ( 𝑢 ∩ 𝑌 ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑢 ∩ 𝑌 ) ) ) )
63 62 biimpd ⊢ ( ( ( 𝜑 ∧ ( 𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽 ) ) ∧ 𝑢 ∈ 𝐽 ) → ( ( 𝑃 ∈ 𝑢 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) → ( 𝑃 ∈ ( 𝑢 ∩ 𝑌 ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑢 ∩ 𝑌 ) ) ) )
64 eleq2 ⊢ ( 𝑣 = ( 𝑢 ∩ 𝑌 ) → ( 𝑃 ∈ 𝑣 ↔ 𝑃 ∈ ( 𝑢 ∩ 𝑌 ) ) )
65 eleq2 ⊢ ( 𝑣 = ( 𝑢 ∩ 𝑌 ) → ( ( 𝐹 ‘ 𝑘 ) ∈ 𝑣 ↔ ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑢 ∩ 𝑌 ) ) )
66 65 rexralbidv ⊢ ( 𝑣 = ( 𝑢 ∩ 𝑌 ) → ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ 𝑣 ↔ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑢 ∩ 𝑌 ) ) )
67 64 66 imbi12d ⊢ ( 𝑣 = ( 𝑢 ∩ 𝑌 ) → ( ( 𝑃 ∈ 𝑣 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ 𝑣 ) ↔ ( 𝑃 ∈ ( 𝑢 ∩ 𝑌 ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑢 ∩ 𝑌 ) ) ) )
68 67 imbi2d ⊢ ( 𝑣 = ( 𝑢 ∩ 𝑌 ) → ( ( ( 𝑃 ∈ 𝑢 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) → ( 𝑃 ∈ 𝑣 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ 𝑣 ) ) ↔ ( ( 𝑃 ∈ 𝑢 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) → ( 𝑃 ∈ ( 𝑢 ∩ 𝑌 ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑢 ∩ 𝑌 ) ) ) ) )
69 63 68 syl5ibrcom ⊢ ( ( ( 𝜑 ∧ ( 𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽 ) ) ∧ 𝑢 ∈ 𝐽 ) → ( 𝑣 = ( 𝑢 ∩ 𝑌 ) → ( ( 𝑃 ∈ 𝑢 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) → ( 𝑃 ∈ 𝑣 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ 𝑣 ) ) ) )
70 69 impd ⊢ ( ( ( 𝜑 ∧ ( 𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽 ) ) ∧ 𝑢 ∈ 𝐽 ) → ( ( 𝑣 = ( 𝑢 ∩ 𝑌 ) ∧ ( 𝑃 ∈ 𝑢 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ) → ( 𝑃 ∈ 𝑣 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ 𝑣 ) ) )
71 70 rexlimdva ⊢ ( ( 𝜑 ∧ ( 𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽 ) ) → ( ∃ 𝑢 ∈ 𝐽 ( 𝑣 = ( 𝑢 ∩ 𝑌 ) ∧ ( 𝑃 ∈ 𝑢 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ) → ( 𝑃 ∈ 𝑣 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ 𝑣 ) ) )
72 47 71 syl5 ⊢ ( ( 𝜑 ∧ ( 𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽 ) ) → ( ( ∃ 𝑢 ∈ 𝐽 𝑣 = ( 𝑢 ∩ 𝑌 ) ∧ ∀ 𝑢 ∈ 𝐽 ( 𝑃 ∈ 𝑢 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ) → ( 𝑃 ∈ 𝑣 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ 𝑣 ) ) )
73 72 expdimp ⊢ ( ( ( 𝜑 ∧ ( 𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽 ) ) ∧ ∃ 𝑢 ∈ 𝐽 𝑣 = ( 𝑢 ∩ 𝑌 ) ) → ( ∀ 𝑢 ∈ 𝐽 ( 𝑃 ∈ 𝑢 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) → ( 𝑃 ∈ 𝑣 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ 𝑣 ) ) )
74 46 73 syldan ⊢ ( ( ( 𝜑 ∧ ( 𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽 ) ) ∧ 𝑣 ∈ 𝐾 ) → ( ∀ 𝑢 ∈ 𝐽 ( 𝑃 ∈ 𝑢 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) → ( 𝑃 ∈ 𝑣 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ 𝑣 ) ) )
75 74 ralrimdva ⊢ ( ( 𝜑 ∧ ( 𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽 ) ) → ( ∀ 𝑢 ∈ 𝐽 ( 𝑃 ∈ 𝑢 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) → ∀ 𝑣 ∈ 𝐾 ( 𝑃 ∈ 𝑣 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ 𝑣 ) ) )
76 41 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽 ) ) ∧ 𝑢 ∈ 𝐽 ) → 𝐽 ∈ Top )
77 42 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽 ) ) ∧ 𝑢 ∈ 𝐽 ) → 𝑌 ∈ 𝑉 )
78 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽 ) ) ∧ 𝑢 ∈ 𝐽 ) → 𝑢 ∈ 𝐽 )
79 elrestr ⊢ ( ( 𝐽 ∈ Top ∧ 𝑌 ∈ 𝑉 ∧ 𝑢 ∈ 𝐽 ) → ( 𝑢 ∩ 𝑌 ) ∈ ( 𝐽 ↾t 𝑌 ) )
80 76 77 78 79 syl3anc ⊢ ( ( ( 𝜑 ∧ ( 𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽 ) ) ∧ 𝑢 ∈ 𝐽 ) → ( 𝑢 ∩ 𝑌 ) ∈ ( 𝐽 ↾t 𝑌 ) )
81 80 1 eleqtrrdi ⊢ ( ( ( 𝜑 ∧ ( 𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽 ) ) ∧ 𝑢 ∈ 𝐽 ) → ( 𝑢 ∩ 𝑌 ) ∈ 𝐾 )
82 67 rspcv ⊢ ( ( 𝑢 ∩ 𝑌 ) ∈ 𝐾 → ( ∀ 𝑣 ∈ 𝐾 ( 𝑃 ∈ 𝑣 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ 𝑣 ) → ( 𝑃 ∈ ( 𝑢 ∩ 𝑌 ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑢 ∩ 𝑌 ) ) ) )
83 81 82 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽 ) ) ∧ 𝑢 ∈ 𝐽 ) → ( ∀ 𝑣 ∈ 𝐾 ( 𝑃 ∈ 𝑣 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ 𝑣 ) → ( 𝑃 ∈ ( 𝑢 ∩ 𝑌 ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑢 ∩ 𝑌 ) ) ) )
84 83 62 sylibrd ⊢ ( ( ( 𝜑 ∧ ( 𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽 ) ) ∧ 𝑢 ∈ 𝐽 ) → ( ∀ 𝑣 ∈ 𝐾 ( 𝑃 ∈ 𝑣 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ 𝑣 ) → ( 𝑃 ∈ 𝑢 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ) )
85 84 ralrimdva ⊢ ( ( 𝜑 ∧ ( 𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽 ) ) → ( ∀ 𝑣 ∈ 𝐾 ( 𝑃 ∈ 𝑣 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ 𝑣 ) → ∀ 𝑢 ∈ 𝐽 ( 𝑃 ∈ 𝑢 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ) )
86 75 85 impbid ⊢ ( ( 𝜑 ∧ ( 𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽 ) ) → ( ∀ 𝑢 ∈ 𝐽 ( 𝑃 ∈ 𝑢 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ↔ ∀ 𝑣 ∈ 𝐾 ( 𝑃 ∈ 𝑣 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ 𝑣 ) ) )
87 39 86 anbi12d ⊢ ( ( 𝜑 ∧ ( 𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽 ) ) → ( ( 𝑃 ∈ ∪ 𝐽 ∧ ∀ 𝑢 ∈ 𝐽 ( 𝑃 ∈ 𝑢 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ) ↔ ( 𝑃 ∈ ( 𝑌 ∩ ∪ 𝐽 ) ∧ ∀ 𝑣 ∈ 𝐾 ( 𝑃 ∈ 𝑣 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ 𝑣 ) ) ) )
88 41 8 sylib ⊢ ( ( 𝜑 ∧ ( 𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽 ) ) → 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) )
89 6 adantr ⊢ ( ( 𝜑 ∧ ( 𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽 ) ) → 𝑀 ∈ ℤ )
90 52 ffnd ⊢ ( ( 𝜑 ∧ ( 𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽 ) ) → 𝐹 Fn 𝑍 )
91 simprr ⊢ ( ( 𝜑 ∧ ( 𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽 ) ) → ran 𝐹 ⊆ ∪ 𝐽 )
92 df-f ⊢ ( 𝐹 : 𝑍 ⟶ ∪ 𝐽 ↔ ( 𝐹 Fn 𝑍 ∧ ran 𝐹 ⊆ ∪ 𝐽 ) )
93 90 91 92 sylanbrc ⊢ ( ( 𝜑 ∧ ( 𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽 ) ) → 𝐹 : 𝑍 ⟶ ∪ 𝐽 )
94 eqidd ⊢ ( ( ( 𝜑 ∧ ( 𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽 ) ) ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑘 ) )
95 88 2 89 93 94 lmbrf ⊢ ( ( 𝜑 ∧ ( 𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽 ) ) → ( 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ↔ ( 𝑃 ∈ ∪ 𝐽 ∧ ∀ 𝑢 ∈ 𝐽 ( 𝑃 ∈ 𝑢 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ) ) )
96 22 adantr ⊢ ( ( 𝜑 ∧ ( 𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽 ) ) → 𝐾 ∈ ( TopOn ‘ ( 𝑌 ∩ ∪ 𝐽 ) ) )
97 52 frnd ⊢ ( ( 𝜑 ∧ ( 𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽 ) ) → ran 𝐹 ⊆ 𝑌 )
98 97 91 ssind ⊢ ( ( 𝜑 ∧ ( 𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽 ) ) → ran 𝐹 ⊆ ( 𝑌 ∩ ∪ 𝐽 ) )
99 df-f ⊢ ( 𝐹 : 𝑍 ⟶ ( 𝑌 ∩ ∪ 𝐽 ) ↔ ( 𝐹 Fn 𝑍 ∧ ran 𝐹 ⊆ ( 𝑌 ∩ ∪ 𝐽 ) ) )
100 90 98 99 sylanbrc ⊢ ( ( 𝜑 ∧ ( 𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽 ) ) → 𝐹 : 𝑍 ⟶ ( 𝑌 ∩ ∪ 𝐽 ) )
101 96 2 89 100 94 lmbrf ⊢ ( ( 𝜑 ∧ ( 𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽 ) ) → ( 𝐹 ( ⇝𝑡 ‘ 𝐾 ) 𝑃 ↔ ( 𝑃 ∈ ( 𝑌 ∩ ∪ 𝐽 ) ∧ ∀ 𝑣 ∈ 𝐾 ( 𝑃 ∈ 𝑣 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ 𝑣 ) ) ) )
102 87 95 101 3bitr4d ⊢ ( ( 𝜑 ∧ ( 𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽 ) ) → ( 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ↔ 𝐹 ( ⇝𝑡 ‘ 𝐾 ) 𝑃 ) )
103 102 ex ⊢ ( 𝜑 → ( ( 𝑃 ∈ ∪ 𝐽 ∧ ran 𝐹 ⊆ ∪ 𝐽 ) → ( 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ↔ 𝐹 ( ⇝𝑡 ‘ 𝐾 ) 𝑃 ) ) )
104 19 35 103 pm5.21ndd ⊢ ( 𝜑 → ( 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ↔ 𝐹 ( ⇝𝑡 ‘ 𝐾 ) 𝑃 ) )