Theorem cnpimaex

Description: Property of a function continuous at a point. (Contributed by FL, 31-Dec-2006)

	Ref	Expression
Assertion	cnpimaex	⊢ ( ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ∧ 𝐴 ∈ 𝐾 ∧ ( 𝐹 ‘ 𝑃 ) ∈ 𝐴 ) → ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ( 𝐹 “ 𝑥 ) ⊆ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ∪ 𝐽 = ∪ 𝐽
2		eqid	⊢ ∪ 𝐾 = ∪ 𝐾
3	1 2	iscnp2	⊢ ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ↔ ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝑃 ∈ ∪ 𝐽 ) ∧ ( 𝐹 : ∪ 𝐽 ⟶ ∪ 𝐾 ∧ ∀ 𝑦 ∈ 𝐾 ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑦 → ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ( 𝐹 “ 𝑥 ) ⊆ 𝑦 ) ) ) ) )
4	3	simprbi	⊢ ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) → ( 𝐹 : ∪ 𝐽 ⟶ ∪ 𝐾 ∧ ∀ 𝑦 ∈ 𝐾 ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑦 → ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ( 𝐹 “ 𝑥 ) ⊆ 𝑦 ) ) ) )
5		eleq2	⊢ ( 𝑦 = 𝐴 → ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑦 ↔ ( 𝐹 ‘ 𝑃 ) ∈ 𝐴 ) )
6		sseq2	⊢ ( 𝑦 = 𝐴 → ( ( 𝐹 “ 𝑥 ) ⊆ 𝑦 ↔ ( 𝐹 “ 𝑥 ) ⊆ 𝐴 ) )
7	6	anbi2d	⊢ ( 𝑦 = 𝐴 → ( ( 𝑃 ∈ 𝑥 ∧ ( 𝐹 “ 𝑥 ) ⊆ 𝑦 ) ↔ ( 𝑃 ∈ 𝑥 ∧ ( 𝐹 “ 𝑥 ) ⊆ 𝐴 ) ) )
8	7	rexbidv	⊢ ( 𝑦 = 𝐴 → ( ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ( 𝐹 “ 𝑥 ) ⊆ 𝑦 ) ↔ ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ( 𝐹 “ 𝑥 ) ⊆ 𝐴 ) ) )
9	5 8	imbi12d	⊢ ( 𝑦 = 𝐴 → ( ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑦 → ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ( 𝐹 “ 𝑥 ) ⊆ 𝑦 ) ) ↔ ( ( 𝐹 ‘ 𝑃 ) ∈ 𝐴 → ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ( 𝐹 “ 𝑥 ) ⊆ 𝐴 ) ) ) )
10	9	rspccv	⊢ ( ∀ 𝑦 ∈ 𝐾 ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑦 → ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ( 𝐹 “ 𝑥 ) ⊆ 𝑦 ) ) → ( 𝐴 ∈ 𝐾 → ( ( 𝐹 ‘ 𝑃 ) ∈ 𝐴 → ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ( 𝐹 “ 𝑥 ) ⊆ 𝐴 ) ) ) )
11	4 10	simpl2im	⊢ ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) → ( 𝐴 ∈ 𝐾 → ( ( 𝐹 ‘ 𝑃 ) ∈ 𝐴 → ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ( 𝐹 “ 𝑥 ) ⊆ 𝐴 ) ) ) )
12	11	3imp	⊢ ( ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ∧ 𝐴 ∈ 𝐾 ∧ ( 𝐹 ‘ 𝑃 ) ∈ 𝐴 ) → ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ( 𝐹 “ 𝑥 ) ⊆ 𝐴 ) )