Metamath Proof Explorer

Theorem cnpflfi

Description: Forward direction of cnpflf . (Contributed by Mario Carneiro, 9-Apr-2015) (Revised by Stefan O'Rear, 9-Aug-2015)

Ref Expression
Assertion cnpflfi ( ( 𝐴 ∈ ( 𝐽 fLim 𝐿 ) ∧ 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) ) → ( 𝐹 ‘ 𝐴 ) ∈ ( ( 𝐾 fLimf 𝐿 ) ‘ 𝐹 ) )

Proof

Step Hyp Ref Expression
1 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
2 eqid ⊢ ∪ 𝐾 = ∪ 𝐾
3 1 2 cnpf ⊢ ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) → 𝐹 : ∪ 𝐽 ⟶ ∪ 𝐾 )
4 3 adantl ⊢ ( ( 𝐴 ∈ ( 𝐽 fLim 𝐿 ) ∧ 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) ) → 𝐹 : ∪ 𝐽 ⟶ ∪ 𝐾 )
5 1 flimelbas ⊢ ( 𝐴 ∈ ( 𝐽 fLim 𝐿 ) → 𝐴 ∈ ∪ 𝐽 )
6 5 adantr ⊢ ( ( 𝐴 ∈ ( 𝐽 fLim 𝐿 ) ∧ 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) ) → 𝐴 ∈ ∪ 𝐽 )
7 4 6 ffvelrnd ⊢ ( ( 𝐴 ∈ ( 𝐽 fLim 𝐿 ) ∧ 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) ) → ( 𝐹 ‘ 𝐴 ) ∈ ∪ 𝐾 )
8 simplr ⊢ ( ( ( 𝐴 ∈ ( 𝐽 fLim 𝐿 ) ∧ 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) ) ∧ ( 𝑥 ∈ 𝐾 ∧ ( 𝐹 ‘ 𝐴 ) ∈ 𝑥 ) ) → 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) )
9 simprl ⊢ ( ( ( 𝐴 ∈ ( 𝐽 fLim 𝐿 ) ∧ 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) ) ∧ ( 𝑥 ∈ 𝐾 ∧ ( 𝐹 ‘ 𝐴 ) ∈ 𝑥 ) ) → 𝑥 ∈ 𝐾 )
10 simprr ⊢ ( ( ( 𝐴 ∈ ( 𝐽 fLim 𝐿 ) ∧ 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) ) ∧ ( 𝑥 ∈ 𝐾 ∧ ( 𝐹 ‘ 𝐴 ) ∈ 𝑥 ) ) → ( 𝐹 ‘ 𝐴 ) ∈ 𝑥 )
11 cnpimaex ⊢ ( ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) ∧ 𝑥 ∈ 𝐾 ∧ ( 𝐹 ‘ 𝐴 ) ∈ 𝑥 ) → ∃ 𝑦 ∈ 𝐽 ( 𝐴 ∈ 𝑦 ∧ ( 𝐹 “ 𝑦 ) ⊆ 𝑥 ) )
12 8 9 10 11 syl3anc ⊢ ( ( ( 𝐴 ∈ ( 𝐽 fLim 𝐿 ) ∧ 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) ) ∧ ( 𝑥 ∈ 𝐾 ∧ ( 𝐹 ‘ 𝐴 ) ∈ 𝑥 ) ) → ∃ 𝑦 ∈ 𝐽 ( 𝐴 ∈ 𝑦 ∧ ( 𝐹 “ 𝑦 ) ⊆ 𝑥 ) )
13 anass ⊢ ( ( ( 𝑦 ∈ 𝐽 ∧ 𝐴 ∈ 𝑦 ) ∧ ( 𝐹 “ 𝑦 ) ⊆ 𝑥 ) ↔ ( 𝑦 ∈ 𝐽 ∧ ( 𝐴 ∈ 𝑦 ∧ ( 𝐹 “ 𝑦 ) ⊆ 𝑥 ) ) )
14 simpl ⊢ ( ( 𝐴 ∈ ( 𝐽 fLim 𝐿 ) ∧ 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) ) → 𝐴 ∈ ( 𝐽 fLim 𝐿 ) )
15 flimtop ⊢ ( 𝐴 ∈ ( 𝐽 fLim 𝐿 ) → 𝐽 ∈ Top )
16 15 adantr ⊢ ( ( 𝐴 ∈ ( 𝐽 fLim 𝐿 ) ∧ 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) ) → 𝐽 ∈ Top )
17 toptopon2 ⊢ ( 𝐽 ∈ Top ↔ 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) )
18 16 17 sylib ⊢ ( ( 𝐴 ∈ ( 𝐽 fLim 𝐿 ) ∧ 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) ) → 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) )
19 1 flimfil ⊢ ( 𝐴 ∈ ( 𝐽 fLim 𝐿 ) → 𝐿 ∈ ( Fil ‘ ∪ 𝐽 ) )
20 19 adantr ⊢ ( ( 𝐴 ∈ ( 𝐽 fLim 𝐿 ) ∧ 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) ) → 𝐿 ∈ ( Fil ‘ ∪ 𝐽 ) )
21 flimopn ⊢ ( ( 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) ∧ 𝐿 ∈ ( Fil ‘ ∪ 𝐽 ) ) → ( 𝐴 ∈ ( 𝐽 fLim 𝐿 ) ↔ ( 𝐴 ∈ ∪ 𝐽 ∧ ∀ 𝑦 ∈ 𝐽 ( 𝐴 ∈ 𝑦 → 𝑦 ∈ 𝐿 ) ) ) )
22 18 20 21 syl2anc ⊢ ( ( 𝐴 ∈ ( 𝐽 fLim 𝐿 ) ∧ 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) ) → ( 𝐴 ∈ ( 𝐽 fLim 𝐿 ) ↔ ( 𝐴 ∈ ∪ 𝐽 ∧ ∀ 𝑦 ∈ 𝐽 ( 𝐴 ∈ 𝑦 → 𝑦 ∈ 𝐿 ) ) ) )
23 14 22 mpbid ⊢ ( ( 𝐴 ∈ ( 𝐽 fLim 𝐿 ) ∧ 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) ) → ( 𝐴 ∈ ∪ 𝐽 ∧ ∀ 𝑦 ∈ 𝐽 ( 𝐴 ∈ 𝑦 → 𝑦 ∈ 𝐿 ) ) )
24 23 simprd ⊢ ( ( 𝐴 ∈ ( 𝐽 fLim 𝐿 ) ∧ 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) ) → ∀ 𝑦 ∈ 𝐽 ( 𝐴 ∈ 𝑦 → 𝑦 ∈ 𝐿 ) )
25 24 adantr ⊢ ( ( ( 𝐴 ∈ ( 𝐽 fLim 𝐿 ) ∧ 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) ) ∧ ( 𝑥 ∈ 𝐾 ∧ ( 𝐹 ‘ 𝐴 ) ∈ 𝑥 ) ) → ∀ 𝑦 ∈ 𝐽 ( 𝐴 ∈ 𝑦 → 𝑦 ∈ 𝐿 ) )
26 25 r19.21bi ⊢ ( ( ( ( 𝐴 ∈ ( 𝐽 fLim 𝐿 ) ∧ 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) ) ∧ ( 𝑥 ∈ 𝐾 ∧ ( 𝐹 ‘ 𝐴 ) ∈ 𝑥 ) ) ∧ 𝑦 ∈ 𝐽 ) → ( 𝐴 ∈ 𝑦 → 𝑦 ∈ 𝐿 ) )
27 26 expimpd ⊢ ( ( ( 𝐴 ∈ ( 𝐽 fLim 𝐿 ) ∧ 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) ) ∧ ( 𝑥 ∈ 𝐾 ∧ ( 𝐹 ‘ 𝐴 ) ∈ 𝑥 ) ) → ( ( 𝑦 ∈ 𝐽 ∧ 𝐴 ∈ 𝑦 ) → 𝑦 ∈ 𝐿 ) )
28 27 anim1d ⊢ ( ( ( 𝐴 ∈ ( 𝐽 fLim 𝐿 ) ∧ 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) ) ∧ ( 𝑥 ∈ 𝐾 ∧ ( 𝐹 ‘ 𝐴 ) ∈ 𝑥 ) ) → ( ( ( 𝑦 ∈ 𝐽 ∧ 𝐴 ∈ 𝑦 ) ∧ ( 𝐹 “ 𝑦 ) ⊆ 𝑥 ) → ( 𝑦 ∈ 𝐿 ∧ ( 𝐹 “ 𝑦 ) ⊆ 𝑥 ) ) )
29 13 28 syl5bir ⊢ ( ( ( 𝐴 ∈ ( 𝐽 fLim 𝐿 ) ∧ 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) ) ∧ ( 𝑥 ∈ 𝐾 ∧ ( 𝐹 ‘ 𝐴 ) ∈ 𝑥 ) ) → ( ( 𝑦 ∈ 𝐽 ∧ ( 𝐴 ∈ 𝑦 ∧ ( 𝐹 “ 𝑦 ) ⊆ 𝑥 ) ) → ( 𝑦 ∈ 𝐿 ∧ ( 𝐹 “ 𝑦 ) ⊆ 𝑥 ) ) )
30 29 reximdv2 ⊢ ( ( ( 𝐴 ∈ ( 𝐽 fLim 𝐿 ) ∧ 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) ) ∧ ( 𝑥 ∈ 𝐾 ∧ ( 𝐹 ‘ 𝐴 ) ∈ 𝑥 ) ) → ( ∃ 𝑦 ∈ 𝐽 ( 𝐴 ∈ 𝑦 ∧ ( 𝐹 “ 𝑦 ) ⊆ 𝑥 ) → ∃ 𝑦 ∈ 𝐿 ( 𝐹 “ 𝑦 ) ⊆ 𝑥 ) )
31 12 30 mpd ⊢ ( ( ( 𝐴 ∈ ( 𝐽 fLim 𝐿 ) ∧ 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) ) ∧ ( 𝑥 ∈ 𝐾 ∧ ( 𝐹 ‘ 𝐴 ) ∈ 𝑥 ) ) → ∃ 𝑦 ∈ 𝐿 ( 𝐹 “ 𝑦 ) ⊆ 𝑥 )
32 31 expr ⊢ ( ( ( 𝐴 ∈ ( 𝐽 fLim 𝐿 ) ∧ 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) ) ∧ 𝑥 ∈ 𝐾 ) → ( ( 𝐹 ‘ 𝐴 ) ∈ 𝑥 → ∃ 𝑦 ∈ 𝐿 ( 𝐹 “ 𝑦 ) ⊆ 𝑥 ) )
33 32 ralrimiva ⊢ ( ( 𝐴 ∈ ( 𝐽 fLim 𝐿 ) ∧ 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) ) → ∀ 𝑥 ∈ 𝐾 ( ( 𝐹 ‘ 𝐴 ) ∈ 𝑥 → ∃ 𝑦 ∈ 𝐿 ( 𝐹 “ 𝑦 ) ⊆ 𝑥 ) )
34 cnptop2 ⊢ ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) → 𝐾 ∈ Top )
35 34 adantl ⊢ ( ( 𝐴 ∈ ( 𝐽 fLim 𝐿 ) ∧ 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) ) → 𝐾 ∈ Top )
36 toptopon2 ⊢ ( 𝐾 ∈ Top ↔ 𝐾 ∈ ( TopOn ‘ ∪ 𝐾 ) )
37 35 36 sylib ⊢ ( ( 𝐴 ∈ ( 𝐽 fLim 𝐿 ) ∧ 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) ) → 𝐾 ∈ ( TopOn ‘ ∪ 𝐾 ) )
38 isflf ⊢ ( ( 𝐾 ∈ ( TopOn ‘ ∪ 𝐾 ) ∧ 𝐿 ∈ ( Fil ‘ ∪ 𝐽 ) ∧ 𝐹 : ∪ 𝐽 ⟶ ∪ 𝐾 ) → ( ( 𝐹 ‘ 𝐴 ) ∈ ( ( 𝐾 fLimf 𝐿 ) ‘ 𝐹 ) ↔ ( ( 𝐹 ‘ 𝐴 ) ∈ ∪ 𝐾 ∧ ∀ 𝑥 ∈ 𝐾 ( ( 𝐹 ‘ 𝐴 ) ∈ 𝑥 → ∃ 𝑦 ∈ 𝐿 ( 𝐹 “ 𝑦 ) ⊆ 𝑥 ) ) ) )
39 37 20 4 38 syl3anc ⊢ ( ( 𝐴 ∈ ( 𝐽 fLim 𝐿 ) ∧ 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) ) → ( ( 𝐹 ‘ 𝐴 ) ∈ ( ( 𝐾 fLimf 𝐿 ) ‘ 𝐹 ) ↔ ( ( 𝐹 ‘ 𝐴 ) ∈ ∪ 𝐾 ∧ ∀ 𝑥 ∈ 𝐾 ( ( 𝐹 ‘ 𝐴 ) ∈ 𝑥 → ∃ 𝑦 ∈ 𝐿 ( 𝐹 “ 𝑦 ) ⊆ 𝑥 ) ) ) )
40 7 33 39 mpbir2and ⊢ ( ( 𝐴 ∈ ( 𝐽 fLim 𝐿 ) ∧ 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) ) → ( 𝐹 ‘ 𝐴 ) ∈ ( ( 𝐾 fLimf 𝐿 ) ‘ 𝐹 ) )