cncmp

Description: Compactness is respected by a continuous onto map. (Contributed by Jeff Hankins, 12-Jul-2009) (Proof shortened by Mario Carneiro, 22-Aug-2015)

		Ref	Expression
	Hypothesis	cncmp.2	$⊢ Y = ⋃ K$
	Assertion	cncmp	$⊢ (J \in Comp \land F : X \underset{onto}{⟶} Y \land F \in (J Cn K)) \to K \in Comp$

Proof

Step	Hyp	Ref	Expression
1		cncmp.2	$⊢ Y = ⋃ K$
2		cntop2	$⊢ F \in (J Cn K) \to K \in Top$
3	2	3ad2ant3	$⊢ (J \in Comp \land F : X \underset{onto}{⟶} Y \land F \in (J Cn K)) \to K \in Top$
4		elpwi	$⊢ u \in 𝒫 K \to u \subseteq K$
5		simpl1	$⊢ ((J \in Comp \land F : X \underset{onto}{⟶} Y \land F \in (J Cn K)) \land (u \subseteq K \land Y = ⋃ u)) \to J \in Comp$
6		simpl3	$⊢ ((J \in Comp \land F : X \underset{onto}{⟶} Y \land F \in (J Cn K)) \land (u \subseteq K \land Y = ⋃ u)) \to F \in (J Cn K)$
7		simprl	$⊢ ((J \in Comp \land F : X \underset{onto}{⟶} Y \land F \in (J Cn K)) \land (u \subseteq K \land Y = ⋃ u)) \to u \subseteq K$
8	7	sselda	$⊢ (((J \in Comp \land F : X \underset{onto}{⟶} Y \land F \in (J Cn K)) \land (u \subseteq K \land Y = ⋃ u)) \land y \in u) \to y \in K$
9		cnima	$⊢ (F \in (J Cn K) \land y \in K) \to F^{-1} [y] \in J$
10	6 8 9	syl2an2r	$⊢ (((J \in Comp \land F : X \underset{onto}{⟶} Y \land F \in (J Cn K)) \land (u \subseteq K \land Y = ⋃ u)) \land y \in u) \to F^{-1} [y] \in J$
11	10	fmpttd	$⊢ ((J \in Comp \land F : X \underset{onto}{⟶} Y \land F \in (J Cn K)) \land (u \subseteq K \land Y = ⋃ u)) \to (y \in u ⟼ F^{-1} [y]) : u ⟶ J$
12	11	frnd	$⊢ ((J \in Comp \land F : X \underset{onto}{⟶} Y \land F \in (J Cn K)) \land (u \subseteq K \land Y = ⋃ u)) \to ran (y \in u ⟼ F^{-1} [y]) \subseteq J$
13		simprr	$⊢ ((J \in Comp \land F : X \underset{onto}{⟶} Y \land F \in (J Cn K)) \land (u \subseteq K \land Y = ⋃ u)) \to Y = ⋃ u$
14	13	imaeq2d	$⊢ ((J \in Comp \land F : X \underset{onto}{⟶} Y \land F \in (J Cn K)) \land (u \subseteq K \land Y = ⋃ u)) \to F^{-1} [Y] = F^{-1} [⋃ u]$
15		eqid	$⊢ ⋃ J = ⋃ J$
16	15 1	cnf	$⊢ F \in (J Cn K) \to F : ⋃ J ⟶ Y$
17	6 16	syl	$⊢ ((J \in Comp \land F : X \underset{onto}{⟶} Y \land F \in (J Cn K)) \land (u \subseteq K \land Y = ⋃ u)) \to F : ⋃ J ⟶ Y$
18		fimacnv	$⊢ F : ⋃ J ⟶ Y \to F^{-1} [Y] = ⋃ J$
19	17 18	syl	$⊢ ((J \in Comp \land F : X \underset{onto}{⟶} Y \land F \in (J Cn K)) \land (u \subseteq K \land Y = ⋃ u)) \to F^{-1} [Y] = ⋃ J$
20	10	ralrimiva	$⊢ ((J \in Comp \land F : X \underset{onto}{⟶} Y \land F \in (J Cn K)) \land (u \subseteq K \land Y = ⋃ u)) \to \forall y \in u F^{-1} [y] \in J$
21		dfiun2g	$⊢ \forall y \in u F^{-1} [y] \in J \to ⋃_{y \in u} F^{-1} [y] = ⋃ \{x \| \exists y \in u x = F^{-1} [y]\}$
22	20 21	syl	$⊢ ((J \in Comp \land F : X \underset{onto}{⟶} Y \land F \in (J Cn K)) \land (u \subseteq K \land Y = ⋃ u)) \to ⋃_{y \in u} F^{-1} [y] = ⋃ \{x \| \exists y \in u x = F^{-1} [y]\}$
23		imauni	$⊢ F^{-1} [⋃ u] = ⋃_{y \in u} F^{-1} [y]$
24		eqid	$⊢ (y \in u ⟼ F^{-1} [y]) = (y \in u ⟼ F^{-1} [y])$
25	24	rnmpt	$⊢ ran (y \in u ⟼ F^{-1} [y]) = \{x \| \exists y \in u x = F^{-1} [y]\}$
26	25	unieqi	$⊢ ⋃ ran (y \in u ⟼ F^{-1} [y]) = ⋃ \{x \| \exists y \in u x = F^{-1} [y]\}$
27	22 23 26	3eqtr4g	$⊢ ((J \in Comp \land F : X \underset{onto}{⟶} Y \land F \in (J Cn K)) \land (u \subseteq K \land Y = ⋃ u)) \to F^{-1} [⋃ u] = ⋃ ran (y \in u ⟼ F^{-1} [y])$
28	14 19 27	3eqtr3d	$⊢ ((J \in Comp \land F : X \underset{onto}{⟶} Y \land F \in (J Cn K)) \land (u \subseteq K \land Y = ⋃ u)) \to ⋃ J = ⋃ ran (y \in u ⟼ F^{-1} [y])$
29	15	cmpcov	$⊢ (J \in Comp \land ran (y \in u ⟼ F^{-1} [y]) \subseteq J \land ⋃ J = ⋃ ran (y \in u ⟼ F^{-1} [y])) \to \exists s \in (𝒫 ran (y \in u ⟼ F^{-1} [y]) \cap Fin) ⋃ J = ⋃ s$
30	5 12 28 29	syl3anc	$⊢ ((J \in Comp \land F : X \underset{onto}{⟶} Y \land F \in (J Cn K)) \land (u \subseteq K \land Y = ⋃ u)) \to \exists s \in (𝒫 ran (y \in u ⟼ F^{-1} [y]) \cap Fin) ⋃ J = ⋃ s$
31		elfpw	$⊢ s \in (𝒫 ran (y \in u ⟼ F^{-1} [y]) \cap Fin) \leftrightarrow (s \subseteq ran (y \in u ⟼ F^{-1} [y]) \land s \in Fin)$
32		simprll	$⊢ (((J \in Comp \land F : X \underset{onto}{⟶} Y \land F \in (J Cn K)) \land (u \subseteq K \land Y = ⋃ u)) \land ((s \subseteq ran (y \in u ⟼ F^{-1} [y]) \land s \in Fin) \land ⋃ J = ⋃ s)) \to s \subseteq ran (y \in u ⟼ F^{-1} [y])$
33	32	sselda	$⊢ ((((J \in Comp \land F : X \underset{onto}{⟶} Y \land F \in (J Cn K)) \land (u \subseteq K \land Y = ⋃ u)) \land ((s \subseteq ran (y \in u ⟼ F^{-1} [y]) \land s \in Fin) \land ⋃ J = ⋃ s)) \land c \in s) \to c \in ran (y \in u ⟼ F^{-1} [y])$
34		simpll2	$⊢ (((J \in Comp \land F : X \underset{onto}{⟶} Y \land F \in (J Cn K)) \land (u \subseteq K \land Y = ⋃ u)) \land y \in u) \to F : X \underset{onto}{⟶} Y$
35		elssuni	$⊢ y \in K \to y \subseteq ⋃ K$
36	35 1	sseqtrrdi	$⊢ y \in K \to y \subseteq Y$
37	8 36	syl	$⊢ (((J \in Comp \land F : X \underset{onto}{⟶} Y \land F \in (J Cn K)) \land (u \subseteq K \land Y = ⋃ u)) \land y \in u) \to y \subseteq Y$
38		foimacnv	$⊢ (F : X \underset{onto}{⟶} Y \land y \subseteq Y) \to F [F^{-1} [y]] = y$
39	34 37 38	syl2anc	$⊢ (((J \in Comp \land F : X \underset{onto}{⟶} Y \land F \in (J Cn K)) \land (u \subseteq K \land Y = ⋃ u)) \land y \in u) \to F [F^{-1} [y]] = y$
40		simpr	$⊢ (((J \in Comp \land F : X \underset{onto}{⟶} Y \land F \in (J Cn K)) \land (u \subseteq K \land Y = ⋃ u)) \land y \in u) \to y \in u$
41	39 40	eqeltrd	$⊢ (((J \in Comp \land F : X \underset{onto}{⟶} Y \land F \in (J Cn K)) \land (u \subseteq K \land Y = ⋃ u)) \land y \in u) \to F [F^{-1} [y]] \in u$
42	41	ralrimiva	$⊢ ((J \in Comp \land F : X \underset{onto}{⟶} Y \land F \in (J Cn K)) \land (u \subseteq K \land Y = ⋃ u)) \to \forall y \in u F [F^{-1} [y]] \in u$
43		imaeq2	$⊢ c = F^{-1} [y] \to F [c] = F [F^{-1} [y]]$
44	43	eleq1d	$⊢ c = F^{-1} [y] \to (F [c] \in u \leftrightarrow F [F^{-1} [y]] \in u)$
45	24 44	ralrnmptw	$⊢ \forall y \in u F^{-1} [y] \in J \to (\forall c \in ran (y \in u ⟼ F^{-1} [y]) F [c] \in u \leftrightarrow \forall y \in u F [F^{-1} [y]] \in u)$
46	20 45	syl	$⊢ ((J \in Comp \land F : X \underset{onto}{⟶} Y \land F \in (J Cn K)) \land (u \subseteq K \land Y = ⋃ u)) \to (\forall c \in ran (y \in u ⟼ F^{-1} [y]) F [c] \in u \leftrightarrow \forall y \in u F [F^{-1} [y]] \in u)$
47	42 46	mpbird	$⊢ ((J \in Comp \land F : X \underset{onto}{⟶} Y \land F \in (J Cn K)) \land (u \subseteq K \land Y = ⋃ u)) \to \forall c \in ran (y \in u ⟼ F^{-1} [y]) F [c] \in u$
48	47	adantr	$⊢ (((J \in Comp \land F : X \underset{onto}{⟶} Y \land F \in (J Cn K)) \land (u \subseteq K \land Y = ⋃ u)) \land ((s \subseteq ran (y \in u ⟼ F^{-1} [y]) \land s \in Fin) \land ⋃ J = ⋃ s)) \to \forall c \in ran (y \in u ⟼ F^{-1} [y]) F [c] \in u$
49	48	r19.21bi	$⊢ ((((J \in Comp \land F : X \underset{onto}{⟶} Y \land F \in (J Cn K)) \land (u \subseteq K \land Y = ⋃ u)) \land ((s \subseteq ran (y \in u ⟼ F^{-1} [y]) \land s \in Fin) \land ⋃ J = ⋃ s)) \land c \in ran (y \in u ⟼ F^{-1} [y])) \to F [c] \in u$
50	33 49	syldan	$⊢ ((((J \in Comp \land F : X \underset{onto}{⟶} Y \land F \in (J Cn K)) \land (u \subseteq K \land Y = ⋃ u)) \land ((s \subseteq ran (y \in u ⟼ F^{-1} [y]) \land s \in Fin) \land ⋃ J = ⋃ s)) \land c \in s) \to F [c] \in u$
51	50	fmpttd	$⊢ (((J \in Comp \land F : X \underset{onto}{⟶} Y \land F \in (J Cn K)) \land (u \subseteq K \land Y = ⋃ u)) \land ((s \subseteq ran (y \in u ⟼ F^{-1} [y]) \land s \in Fin) \land ⋃ J = ⋃ s)) \to (c \in s ⟼ F [c]) : s ⟶ u$
52	51	frnd	$⊢ (((J \in Comp \land F : X \underset{onto}{⟶} Y \land F \in (J Cn K)) \land (u \subseteq K \land Y = ⋃ u)) \land ((s \subseteq ran (y \in u ⟼ F^{-1} [y]) \land s \in Fin) \land ⋃ J = ⋃ s)) \to ran (c \in s ⟼ F [c]) \subseteq u$
53		simprlr	$⊢ (((J \in Comp \land F : X \underset{onto}{⟶} Y \land F \in (J Cn K)) \land (u \subseteq K \land Y = ⋃ u)) \land ((s \subseteq ran (y \in u ⟼ F^{-1} [y]) \land s \in Fin) \land ⋃ J = ⋃ s)) \to s \in Fin$
54		eqid	$⊢ (c \in s ⟼ F [c]) = (c \in s ⟼ F [c])$
55	54	rnmpt	$⊢ ran (c \in s ⟼ F [c]) = \{d \| \exists c \in s d = F [c]\}$
56		abrexfi	$⊢ s \in Fin \to \{d \| \exists c \in s d = F [c]\} \in Fin$
57	55 56	eqeltrid	$⊢ s \in Fin \to ran (c \in s ⟼ F [c]) \in Fin$
58	53 57	syl	$⊢ (((J \in Comp \land F : X \underset{onto}{⟶} Y \land F \in (J Cn K)) \land (u \subseteq K \land Y = ⋃ u)) \land ((s \subseteq ran (y \in u ⟼ F^{-1} [y]) \land s \in Fin) \land ⋃ J = ⋃ s)) \to ran (c \in s ⟼ F [c]) \in Fin$
59		elfpw	$⊢ ran (c \in s ⟼ F [c]) \in (𝒫 u \cap Fin) \leftrightarrow (ran (c \in s ⟼ F [c]) \subseteq u \land ran (c \in s ⟼ F [c]) \in Fin)$
60	52 58 59	sylanbrc	$⊢ (((J \in Comp \land F : X \underset{onto}{⟶} Y \land F \in (J Cn K)) \land (u \subseteq K \land Y = ⋃ u)) \land ((s \subseteq ran (y \in u ⟼ F^{-1} [y]) \land s \in Fin) \land ⋃ J = ⋃ s)) \to ran (c \in s ⟼ F [c]) \in (𝒫 u \cap Fin)$
61	17	adantr	$⊢ (((J \in Comp \land F : X \underset{onto}{⟶} Y \land F \in (J Cn K)) \land (u \subseteq K \land Y = ⋃ u)) \land ((s \subseteq ran (y \in u ⟼ F^{-1} [y]) \land s \in Fin) \land ⋃ J = ⋃ s)) \to F : ⋃ J ⟶ Y$
62	61	fdmd	$⊢ (((J \in Comp \land F : X \underset{onto}{⟶} Y \land F \in (J Cn K)) \land (u \subseteq K \land Y = ⋃ u)) \land ((s \subseteq ran (y \in u ⟼ F^{-1} [y]) \land s \in Fin) \land ⋃ J = ⋃ s)) \to dom F = ⋃ J$
63		simpll2	$⊢ (((J \in Comp \land F : X \underset{onto}{⟶} Y \land F \in (J Cn K)) \land (u \subseteq K \land Y = ⋃ u)) \land ((s \subseteq ran (y \in u ⟼ F^{-1} [y]) \land s \in Fin) \land ⋃ J = ⋃ s)) \to F : X \underset{onto}{⟶} Y$
64		fof	$⊢ F : X \underset{onto}{⟶} Y \to F : X ⟶ Y$
65		fdm	$⊢ F : X ⟶ Y \to dom F = X$
66	63 64 65	3syl	$⊢ (((J \in Comp \land F : X \underset{onto}{⟶} Y \land F \in (J Cn K)) \land (u \subseteq K \land Y = ⋃ u)) \land ((s \subseteq ran (y \in u ⟼ F^{-1} [y]) \land s \in Fin) \land ⋃ J = ⋃ s)) \to dom F = X$
67		simprr	$⊢ (((J \in Comp \land F : X \underset{onto}{⟶} Y \land F \in (J Cn K)) \land (u \subseteq K \land Y = ⋃ u)) \land ((s \subseteq ran (y \in u ⟼ F^{-1} [y]) \land s \in Fin) \land ⋃ J = ⋃ s)) \to ⋃ J = ⋃ s$
68	62 66 67	3eqtr3d	$⊢ (((J \in Comp \land F : X \underset{onto}{⟶} Y \land F \in (J Cn K)) \land (u \subseteq K \land Y = ⋃ u)) \land ((s \subseteq ran (y \in u ⟼ F^{-1} [y]) \land s \in Fin) \land ⋃ J = ⋃ s)) \to X = ⋃ s$
69	68	imaeq2d	$⊢ (((J \in Comp \land F : X \underset{onto}{⟶} Y \land F \in (J Cn K)) \land (u \subseteq K \land Y = ⋃ u)) \land ((s \subseteq ran (y \in u ⟼ F^{-1} [y]) \land s \in Fin) \land ⋃ J = ⋃ s)) \to F [X] = F [⋃ s]$
70		foima	$⊢ F : X \underset{onto}{⟶} Y \to F [X] = Y$
71	63 70	syl	$⊢ (((J \in Comp \land F : X \underset{onto}{⟶} Y \land F \in (J Cn K)) \land (u \subseteq K \land Y = ⋃ u)) \land ((s \subseteq ran (y \in u ⟼ F^{-1} [y]) \land s \in Fin) \land ⋃ J = ⋃ s)) \to F [X] = Y$
72	50	ralrimiva	$⊢ (((J \in Comp \land F : X \underset{onto}{⟶} Y \land F \in (J Cn K)) \land (u \subseteq K \land Y = ⋃ u)) \land ((s \subseteq ran (y \in u ⟼ F^{-1} [y]) \land s \in Fin) \land ⋃ J = ⋃ s)) \to \forall c \in s F [c] \in u$
73		dfiun2g	$⊢ \forall c \in s F [c] \in u \to ⋃_{c \in s} F [c] = ⋃ \{d \| \exists c \in s d = F [c]\}$
74	72 73	syl	$⊢ (((J \in Comp \land F : X \underset{onto}{⟶} Y \land F \in (J Cn K)) \land (u \subseteq K \land Y = ⋃ u)) \land ((s \subseteq ran (y \in u ⟼ F^{-1} [y]) \land s \in Fin) \land ⋃ J = ⋃ s)) \to ⋃_{c \in s} F [c] = ⋃ \{d \| \exists c \in s d = F [c]\}$
75		imauni	$⊢ F [⋃ s] = ⋃_{c \in s} F [c]$
76	55	unieqi	$⊢ ⋃ ran (c \in s ⟼ F [c]) = ⋃ \{d \| \exists c \in s d = F [c]\}$
77	74 75 76	3eqtr4g	$⊢ (((J \in Comp \land F : X \underset{onto}{⟶} Y \land F \in (J Cn K)) \land (u \subseteq K \land Y = ⋃ u)) \land ((s \subseteq ran (y \in u ⟼ F^{-1} [y]) \land s \in Fin) \land ⋃ J = ⋃ s)) \to F [⋃ s] = ⋃ ran (c \in s ⟼ F [c])$
78	69 71 77	3eqtr3d	$⊢ (((J \in Comp \land F : X \underset{onto}{⟶} Y \land F \in (J Cn K)) \land (u \subseteq K \land Y = ⋃ u)) \land ((s \subseteq ran (y \in u ⟼ F^{-1} [y]) \land s \in Fin) \land ⋃ J = ⋃ s)) \to Y = ⋃ ran (c \in s ⟼ F [c])$
79		unieq	$⊢ v = ran (c \in s ⟼ F [c]) \to ⋃ v = ⋃ ran (c \in s ⟼ F [c])$
80	79	rspceeqv	$⊢ (ran (c \in s ⟼ F [c]) \in (𝒫 u \cap Fin) \land Y = ⋃ ran (c \in s ⟼ F [c])) \to \exists v \in (𝒫 u \cap Fin) Y = ⋃ v$
81	60 78 80	syl2anc	$⊢ (((J \in Comp \land F : X \underset{onto}{⟶} Y \land F \in (J Cn K)) \land (u \subseteq K \land Y = ⋃ u)) \land ((s \subseteq ran (y \in u ⟼ F^{-1} [y]) \land s \in Fin) \land ⋃ J = ⋃ s)) \to \exists v \in (𝒫 u \cap Fin) Y = ⋃ v$
82	81	expr	$⊢ (((J \in Comp \land F : X \underset{onto}{⟶} Y \land F \in (J Cn K)) \land (u \subseteq K \land Y = ⋃ u)) \land (s \subseteq ran (y \in u ⟼ F^{-1} [y]) \land s \in Fin)) \to (⋃ J = ⋃ s \to \exists v \in (𝒫 u \cap Fin) Y = ⋃ v)$
83	31 82	sylan2b	$⊢ (((J \in Comp \land F : X \underset{onto}{⟶} Y \land F \in (J Cn K)) \land (u \subseteq K \land Y = ⋃ u)) \land s \in (𝒫 ran (y \in u ⟼ F^{-1} [y]) \cap Fin)) \to (⋃ J = ⋃ s \to \exists v \in (𝒫 u \cap Fin) Y = ⋃ v)$
84	83	rexlimdva	$⊢ ((J \in Comp \land F : X \underset{onto}{⟶} Y \land F \in (J Cn K)) \land (u \subseteq K \land Y = ⋃ u)) \to (\exists s \in (𝒫 ran (y \in u ⟼ F^{-1} [y]) \cap Fin) ⋃ J = ⋃ s \to \exists v \in (𝒫 u \cap Fin) Y = ⋃ v)$
85	30 84	mpd	$⊢ ((J \in Comp \land F : X \underset{onto}{⟶} Y \land F \in (J Cn K)) \land (u \subseteq K \land Y = ⋃ u)) \to \exists v \in (𝒫 u \cap Fin) Y = ⋃ v$
86	85	expr	$⊢ ((J \in Comp \land F : X \underset{onto}{⟶} Y \land F \in (J Cn K)) \land u \subseteq K) \to (Y = ⋃ u \to \exists v \in (𝒫 u \cap Fin) Y = ⋃ v)$
87	4 86	sylan2	$⊢ ((J \in Comp \land F : X \underset{onto}{⟶} Y \land F \in (J Cn K)) \land u \in 𝒫 K) \to (Y = ⋃ u \to \exists v \in (𝒫 u \cap Fin) Y = ⋃ v)$
88	87	ralrimiva	$⊢ (J \in Comp \land F : X \underset{onto}{⟶} Y \land F \in (J Cn K)) \to \forall u \in 𝒫 K (Y = ⋃ u \to \exists v \in (𝒫 u \cap Fin) Y = ⋃ v)$
89	1	iscmp	$⊢ K \in Comp \leftrightarrow (K \in Top \land \forall u \in 𝒫 K (Y = ⋃ u \to \exists v \in (𝒫 u \cap Fin) Y = ⋃ v))$
90	3 88 89	sylanbrc	$⊢ (J \in Comp \land F : X \underset{onto}{⟶} Y \land F \in (J Cn K)) \to K \in Comp$

Metamath Proof Explorer

Theorem cncmp

Proof