cvmopnlem

	Ref	Expression
Hypotheses	cvmcov.1	$⊢ S = (k \in J ⟼ \{s \in (𝒫 C ∖ \{\emptyset\}) \| (⋃ s = F^{-1} [k] \land \forall u \in s (\forall v \in (s ∖ \{u\}) u \cap v = \emptyset \land {F ↾}_{u} \in ((C ↾_{𝑡} u) Homeo (J ↾_{𝑡} k))))\})$
	cvmseu.1	$⊢ B = ⋃ C$
Assertion	cvmopnlem	$⊢ (F \in (C CovMap J) \land A \in C) \to F [A] \in J$

Proof

Step	Hyp	Ref	Expression
1		cvmcov.1	$⊢ S = (k \in J ⟼ \{s \in (𝒫 C ∖ \{\emptyset\}) \| (⋃ s = F^{-1} [k] \land \forall u \in s (\forall v \in (s ∖ \{u\}) u \cap v = \emptyset \land {F ↾}_{u} \in ((C ↾_{𝑡} u) Homeo (J ↾_{𝑡} k))))\})$
2		cvmseu.1	$⊢ B = ⋃ C$
3		simpll	$⊢ ((F \in (C CovMap J) \land A \in C) \land z \in A) \to F \in (C CovMap J)$
4		cvmcn	$⊢ F \in (C CovMap J) \to F \in (C Cn J)$
5	4	adantr	$⊢ (F \in (C CovMap J) \land A \in C) \to F \in (C Cn J)$
6		eqid	$⊢ ⋃ J = ⋃ J$
7	2 6	cnf	$⊢ F \in (C Cn J) \to F : B ⟶ ⋃ J$
8	5 7	syl	$⊢ (F \in (C CovMap J) \land A \in C) \to F : B ⟶ ⋃ J$
9	8	adantr	$⊢ ((F \in (C CovMap J) \land A \in C) \land z \in A) \to F : B ⟶ ⋃ J$
10		elssuni	$⊢ A \in C \to A \subseteq ⋃ C$
11	10 2	sseqtrrdi	$⊢ A \in C \to A \subseteq B$
12	11	adantl	$⊢ (F \in (C CovMap J) \land A \in C) \to A \subseteq B$
13	12	sselda	$⊢ ((F \in (C CovMap J) \land A \in C) \land z \in A) \to z \in B$
14	9 13	ffvelrnd	$⊢ ((F \in (C CovMap J) \land A \in C) \land z \in A) \to F (z) \in ⋃ J$
15	1 6	cvmcov	$⊢ (F \in (C CovMap J) \land F (z) \in ⋃ J) \to \exists t \in J (F (z) \in t \land S (t) \neq \emptyset)$
16	3 14 15	syl2anc	$⊢ ((F \in (C CovMap J) \land A \in C) \land z \in A) \to \exists t \in J (F (z) \in t \land S (t) \neq \emptyset)$
17		n0	$⊢ S (t) \neq \emptyset \leftrightarrow \exists w w \in S (t)$
18		inss2	$⊢ A \cap (ι x \in w \| z \in x) \subseteq (ι x \in w \| z \in x)$
19		resima2	$⊢ A \cap (ι x \in w \| z \in x) \subseteq (ι x \in w \| z \in x) \to ({F ↾}_{(ι x \in w \| z \in x)}) [A \cap (ι x \in w \| z \in x)] = F [A \cap (ι x \in w \| z \in x)]$
20	18 19	ax-mp	$⊢ ({F ↾}_{(ι x \in w \| z \in x)}) [A \cap (ι x \in w \| z \in x)] = F [A \cap (ι x \in w \| z \in x)]$
21		simprr	$⊢ (((F \in (C CovMap J) \land A \in C) \land z \in A) \land (F (z) \in t \land w \in S (t))) \to w \in S (t)$
22	3	adantr	$⊢ (((F \in (C CovMap J) \land A \in C) \land z \in A) \land (F (z) \in t \land w \in S (t))) \to F \in (C CovMap J)$
23	13	adantr	$⊢ (((F \in (C CovMap J) \land A \in C) \land z \in A) \land (F (z) \in t \land w \in S (t))) \to z \in B$
24		simprl	$⊢ (((F \in (C CovMap J) \land A \in C) \land z \in A) \land (F (z) \in t \land w \in S (t))) \to F (z) \in t$
25		eqid	$⊢ (ι x \in w \| z \in x) = (ι x \in w \| z \in x)$
26	1 2 25	cvmsiota	$⊢ (F \in (C CovMap J) \land (w \in S (t) \land z \in B \land F (z) \in t)) \to ((ι x \in w \| z \in x) \in w \land z \in (ι x \in w \| z \in x))$
27	22 21 23 24 26	syl13anc	$⊢ (((F \in (C CovMap J) \land A \in C) \land z \in A) \land (F (z) \in t \land w \in S (t))) \to ((ι x \in w \| z \in x) \in w \land z \in (ι x \in w \| z \in x))$
28	27	simpld	$⊢ (((F \in (C CovMap J) \land A \in C) \land z \in A) \land (F (z) \in t \land w \in S (t))) \to (ι x \in w \| z \in x) \in w$
29	1	cvmshmeo	$⊢ (w \in S (t) \land (ι x \in w \| z \in x) \in w) \to {F ↾}_{(ι x \in w \| z \in x)} \in ((C ↾_{𝑡} (ι x \in w \| z \in x)) Homeo (J ↾_{𝑡} t))$
30	21 28 29	syl2anc	$⊢ (((F \in (C CovMap J) \land A \in C) \land z \in A) \land (F (z) \in t \land w \in S (t))) \to {F ↾}_{(ι x \in w \| z \in x)} \in ((C ↾_{𝑡} (ι x \in w \| z \in x)) Homeo (J ↾_{𝑡} t))$
31		cvmtop1	$⊢ F \in (C CovMap J) \to C \in Top$
32	22 31	syl	$⊢ (((F \in (C CovMap J) \land A \in C) \land z \in A) \land (F (z) \in t \land w \in S (t))) \to C \in Top$
33		simpllr	$⊢ (((F \in (C CovMap J) \land A \in C) \land z \in A) \land (F (z) \in t \land w \in S (t))) \to A \in C$
34		elrestr	$⊢ (C \in Top \land (ι x \in w \| z \in x) \in w \land A \in C) \to A \cap (ι x \in w \| z \in x) \in (C ↾_{𝑡} (ι x \in w \| z \in x))$
35	32 28 33 34	syl3anc	$⊢ (((F \in (C CovMap J) \land A \in C) \land z \in A) \land (F (z) \in t \land w \in S (t))) \to A \cap (ι x \in w \| z \in x) \in (C ↾_{𝑡} (ι x \in w \| z \in x))$
36		hmeoima	$⊢ ({F ↾}_{(ι x \in w \| z \in x)} \in ((C ↾_{𝑡} (ι x \in w \| z \in x)) Homeo (J ↾_{𝑡} t)) \land A \cap (ι x \in w \| z \in x) \in (C ↾_{𝑡} (ι x \in w \| z \in x))) \to ({F ↾}_{(ι x \in w \| z \in x)}) [A \cap (ι x \in w \| z \in x)] \in (J ↾_{𝑡} t)$
37	30 35 36	syl2anc	$⊢ (((F \in (C CovMap J) \land A \in C) \land z \in A) \land (F (z) \in t \land w \in S (t))) \to ({F ↾}_{(ι x \in w \| z \in x)}) [A \cap (ι x \in w \| z \in x)] \in (J ↾_{𝑡} t)$
38	20 37	eqeltrrid	$⊢ (((F \in (C CovMap J) \land A \in C) \land z \in A) \land (F (z) \in t \land w \in S (t))) \to F [A \cap (ι x \in w \| z \in x)] \in (J ↾_{𝑡} t)$
39		cvmtop2	$⊢ F \in (C CovMap J) \to J \in Top$
40	39	adantr	$⊢ (F \in (C CovMap J) \land A \in C) \to J \in Top$
41	40	ad2antrr	$⊢ (((F \in (C CovMap J) \land A \in C) \land z \in A) \land (F (z) \in t \land w \in S (t))) \to J \in Top$
42	1	cvmsrcl	$⊢ w \in S (t) \to t \in J$
43	42	ad2antll	$⊢ (((F \in (C CovMap J) \land A \in C) \land z \in A) \land (F (z) \in t \land w \in S (t))) \to t \in J$
44		restopn2	$⊢ (J \in Top \land t \in J) \to (F [A \cap (ι x \in w \| z \in x)] \in (J ↾_{𝑡} t) \leftrightarrow (F [A \cap (ι x \in w \| z \in x)] \in J \land F [A \cap (ι x \in w \| z \in x)] \subseteq t))$
45	41 43 44	syl2anc	$⊢ (((F \in (C CovMap J) \land A \in C) \land z \in A) \land (F (z) \in t \land w \in S (t))) \to (F [A \cap (ι x \in w \| z \in x)] \in (J ↾_{𝑡} t) \leftrightarrow (F [A \cap (ι x \in w \| z \in x)] \in J \land F [A \cap (ι x \in w \| z \in x)] \subseteq t))$
46	38 45	mpbid	$⊢ (((F \in (C CovMap J) \land A \in C) \land z \in A) \land (F (z) \in t \land w \in S (t))) \to (F [A \cap (ι x \in w \| z \in x)] \in J \land F [A \cap (ι x \in w \| z \in x)] \subseteq t)$
47	46	simpld	$⊢ (((F \in (C CovMap J) \land A \in C) \land z \in A) \land (F (z) \in t \land w \in S (t))) \to F [A \cap (ι x \in w \| z \in x)] \in J$
48	8	ffnd	$⊢ (F \in (C CovMap J) \land A \in C) \to F Fn B$
49	48	ad2antrr	$⊢ (((F \in (C CovMap J) \land A \in C) \land z \in A) \land (F (z) \in t \land w \in S (t))) \to F Fn B$
50		inss1	$⊢ A \cap (ι x \in w \| z \in x) \subseteq A$
51	33 11	syl	$⊢ (((F \in (C CovMap J) \land A \in C) \land z \in A) \land (F (z) \in t \land w \in S (t))) \to A \subseteq B$
52	50 51	sstrid	$⊢ (((F \in (C CovMap J) \land A \in C) \land z \in A) \land (F (z) \in t \land w \in S (t))) \to A \cap (ι x \in w \| z \in x) \subseteq B$
53		simplr	$⊢ (((F \in (C CovMap J) \land A \in C) \land z \in A) \land (F (z) \in t \land w \in S (t))) \to z \in A$
54	27	simprd	$⊢ (((F \in (C CovMap J) \land A \in C) \land z \in A) \land (F (z) \in t \land w \in S (t))) \to z \in (ι x \in w \| z \in x)$
55	53 54	elind	$⊢ (((F \in (C CovMap J) \land A \in C) \land z \in A) \land (F (z) \in t \land w \in S (t))) \to z \in (A \cap (ι x \in w \| z \in x))$
56		fnfvima	$⊢ (F Fn B \land A \cap (ι x \in w \| z \in x) \subseteq B \land z \in (A \cap (ι x \in w \| z \in x))) \to F (z) \in F [A \cap (ι x \in w \| z \in x)]$
57	49 52 55 56	syl3anc	$⊢ (((F \in (C CovMap J) \land A \in C) \land z \in A) \land (F (z) \in t \land w \in S (t))) \to F (z) \in F [A \cap (ι x \in w \| z \in x)]$
58		imass2	$⊢ A \cap (ι x \in w \| z \in x) \subseteq A \to F [A \cap (ι x \in w \| z \in x)] \subseteq F [A]$
59	50 58	mp1i	$⊢ (((F \in (C CovMap J) \land A \in C) \land z \in A) \land (F (z) \in t \land w \in S (t))) \to F [A \cap (ι x \in w \| z \in x)] \subseteq F [A]$
60		eleq2	$⊢ y = F [A \cap (ι x \in w \| z \in x)] \to (F (z) \in y \leftrightarrow F (z) \in F [A \cap (ι x \in w \| z \in x)])$
61		sseq1	$⊢ y = F [A \cap (ι x \in w \| z \in x)] \to (y \subseteq F [A] \leftrightarrow F [A \cap (ι x \in w \| z \in x)] \subseteq F [A])$
62	60 61	anbi12d	$⊢ y = F [A \cap (ι x \in w \| z \in x)] \to ((F (z) \in y \land y \subseteq F [A]) \leftrightarrow (F (z) \in F [A \cap (ι x \in w \| z \in x)] \land F [A \cap (ι x \in w \| z \in x)] \subseteq F [A]))$
63	62	rspcev	$⊢ (F [A \cap (ι x \in w \| z \in x)] \in J \land (F (z) \in F [A \cap (ι x \in w \| z \in x)] \land F [A \cap (ι x \in w \| z \in x)] \subseteq F [A])) \to \exists y \in J (F (z) \in y \land y \subseteq F [A])$
64	47 57 59 63	syl12anc	$⊢ (((F \in (C CovMap J) \land A \in C) \land z \in A) \land (F (z) \in t \land w \in S (t))) \to \exists y \in J (F (z) \in y \land y \subseteq F [A])$
65	64	expr	$⊢ (((F \in (C CovMap J) \land A \in C) \land z \in A) \land F (z) \in t) \to (w \in S (t) \to \exists y \in J (F (z) \in y \land y \subseteq F [A]))$
66	65	exlimdv	$⊢ (((F \in (C CovMap J) \land A \in C) \land z \in A) \land F (z) \in t) \to (\exists w w \in S (t) \to \exists y \in J (F (z) \in y \land y \subseteq F [A]))$
67	17 66	syl5bi	$⊢ (((F \in (C CovMap J) \land A \in C) \land z \in A) \land F (z) \in t) \to (S (t) \neq \emptyset \to \exists y \in J (F (z) \in y \land y \subseteq F [A]))$
68	67	expimpd	$⊢ ((F \in (C CovMap J) \land A \in C) \land z \in A) \to ((F (z) \in t \land S (t) \neq \emptyset) \to \exists y \in J (F (z) \in y \land y \subseteq F [A]))$
69	68	rexlimdvw	$⊢ ((F \in (C CovMap J) \land A \in C) \land z \in A) \to (\exists t \in J (F (z) \in t \land S (t) \neq \emptyset) \to \exists y \in J (F (z) \in y \land y \subseteq F [A]))$
70	16 69	mpd	$⊢ ((F \in (C CovMap J) \land A \in C) \land z \in A) \to \exists y \in J (F (z) \in y \land y \subseteq F [A])$
71	70	ralrimiva	$⊢ (F \in (C CovMap J) \land A \in C) \to \forall z \in A \exists y \in J (F (z) \in y \land y \subseteq F [A])$
72		eleq1	$⊢ x = F (z) \to (x \in y \leftrightarrow F (z) \in y)$
73	72	anbi1d	$⊢ x = F (z) \to ((x \in y \land y \subseteq F [A]) \leftrightarrow (F (z) \in y \land y \subseteq F [A]))$
74	73	rexbidv	$⊢ x = F (z) \to (\exists y \in J (x \in y \land y \subseteq F [A]) \leftrightarrow \exists y \in J (F (z) \in y \land y \subseteq F [A]))$
75	74	ralima	$⊢ (F Fn B \land A \subseteq B) \to (\forall x \in F [A] \exists y \in J (x \in y \land y \subseteq F [A]) \leftrightarrow \forall z \in A \exists y \in J (F (z) \in y \land y \subseteq F [A]))$
76	48 12 75	syl2anc	$⊢ (F \in (C CovMap J) \land A \in C) \to (\forall x \in F [A] \exists y \in J (x \in y \land y \subseteq F [A]) \leftrightarrow \forall z \in A \exists y \in J (F (z) \in y \land y \subseteq F [A]))$
77	71 76	mpbird	$⊢ (F \in (C CovMap J) \land A \in C) \to \forall x \in F [A] \exists y \in J (x \in y \land y \subseteq F [A])$
78		eltop2	$⊢ J \in Top \to (F [A] \in J \leftrightarrow \forall x \in F [A] \exists y \in J (x \in y \land y \subseteq F [A]))$
79	40 78	syl	$⊢ (F \in (C CovMap J) \land A \in C) \to (F [A] \in J \leftrightarrow \forall x \in F [A] \exists y \in J (x \in y \land y \subseteq F [A]))$
80	77 79	mpbird	$⊢ (F \in (C CovMap J) \land A \in C) \to F [A] \in J$

Metamath Proof Explorer

Theorem cvmopnlem

Proof