cvmsss2

Description: An open subset of an evenly covered set is evenly covered. (Contributed by Mario Carneiro, 7-Jul-2015)

		Ref	Expression
	Hypothesis	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))))\})$
	Assertion	cvmsss2	$⊢ (F \in (C CovMap J) \land V \in J \land V \subseteq U) \to (S (U) \neq \emptyset \to S (V) \neq \emptyset)$

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		n0	$⊢ S (U) \neq \emptyset \leftrightarrow \exists x x \in S (U)$
3		simpl2	$⊢ ((F \in (C CovMap J) \land V \in J \land V \subseteq U) \land x \in S (U)) \to V \in J$
4		simpl1	$⊢ ((F \in (C CovMap J) \land V \in J \land V \subseteq U) \land x \in S (U)) \to F \in (C CovMap J)$
5		cvmtop1	$⊢ F \in (C CovMap J) \to C \in Top$
6	4 5	syl	$⊢ ((F \in (C CovMap J) \land V \in J \land V \subseteq U) \land x \in S (U)) \to C \in Top$
7	6	adantr	$⊢ (((F \in (C CovMap J) \land V \in J \land V \subseteq U) \land x \in S (U)) \land y \in x) \to C \in Top$
8	1	cvmsss	$⊢ x \in S (U) \to x \subseteq C$
9	8	adantl	$⊢ ((F \in (C CovMap J) \land V \in J \land V \subseteq U) \land x \in S (U)) \to x \subseteq C$
10	9	sselda	$⊢ (((F \in (C CovMap J) \land V \in J \land V \subseteq U) \land x \in S (U)) \land y \in x) \to y \in C$
11		cvmcn	$⊢ F \in (C CovMap J) \to F \in (C Cn J)$
12	4 11	syl	$⊢ ((F \in (C CovMap J) \land V \in J \land V \subseteq U) \land x \in S (U)) \to F \in (C Cn J)$
13		cnima	$⊢ (F \in (C Cn J) \land V \in J) \to F^{-1} [V] \in C$
14	12 3 13	syl2anc	$⊢ ((F \in (C CovMap J) \land V \in J \land V \subseteq U) \land x \in S (U)) \to F^{-1} [V] \in C$
15	14	adantr	$⊢ (((F \in (C CovMap J) \land V \in J \land V \subseteq U) \land x \in S (U)) \land y \in x) \to F^{-1} [V] \in C$
16		inopn	$⊢ (C \in Top \land y \in C \land F^{-1} [V] \in C) \to y \cap F^{-1} [V] \in C$
17	7 10 15 16	syl3anc	$⊢ (((F \in (C CovMap J) \land V \in J \land V \subseteq U) \land x \in S (U)) \land y \in x) \to y \cap F^{-1} [V] \in C$
18	17	fmpttd	$⊢ ((F \in (C CovMap J) \land V \in J \land V \subseteq U) \land x \in S (U)) \to (y \in x ⟼ y \cap F^{-1} [V]) : x ⟶ C$
19	18	frnd	$⊢ ((F \in (C CovMap J) \land V \in J \land V \subseteq U) \land x \in S (U)) \to ran (y \in x ⟼ y \cap F^{-1} [V]) \subseteq C$
20	1	cvmsn0	$⊢ x \in S (U) \to x \neq \emptyset$
21	20	adantl	$⊢ ((F \in (C CovMap J) \land V \in J \land V \subseteq U) \land x \in S (U)) \to x \neq \emptyset$
22		dmmptg	$⊢ \forall y \in x y \cap F^{-1} [V] \in V \to dom (y \in x ⟼ y \cap F^{-1} [V]) = x$
23		inex1g	$⊢ y \in x \to y \cap F^{-1} [V] \in V$
24	22 23	mprg	$⊢ dom (y \in x ⟼ y \cap F^{-1} [V]) = x$
25	24	eqeq1i	$⊢ dom (y \in x ⟼ y \cap F^{-1} [V]) = \emptyset \leftrightarrow x = \emptyset$
26		dm0rn0	$⊢ dom (y \in x ⟼ y \cap F^{-1} [V]) = \emptyset \leftrightarrow ran (y \in x ⟼ y \cap F^{-1} [V]) = \emptyset$
27	25 26	bitr3i	$⊢ x = \emptyset \leftrightarrow ran (y \in x ⟼ y \cap F^{-1} [V]) = \emptyset$
28	27	necon3bii	$⊢ x \neq \emptyset \leftrightarrow ran (y \in x ⟼ y \cap F^{-1} [V]) \neq \emptyset$
29	21 28	sylib	$⊢ ((F \in (C CovMap J) \land V \in J \land V \subseteq U) \land x \in S (U)) \to ran (y \in x ⟼ y \cap F^{-1} [V]) \neq \emptyset$
30	19 29	jca	$⊢ ((F \in (C CovMap J) \land V \in J \land V \subseteq U) \land x \in S (U)) \to (ran (y \in x ⟼ y \cap F^{-1} [V]) \subseteq C \land ran (y \in x ⟼ y \cap F^{-1} [V]) \neq \emptyset)$
31		inss2	$⊢ y \cap F^{-1} [V] \subseteq F^{-1} [V]$
32		elpw2g	$⊢ F^{-1} [V] \in C \to (y \cap F^{-1} [V] \in 𝒫 F^{-1} [V] \leftrightarrow y \cap F^{-1} [V] \subseteq F^{-1} [V])$
33	15 32	syl	$⊢ (((F \in (C CovMap J) \land V \in J \land V \subseteq U) \land x \in S (U)) \land y \in x) \to (y \cap F^{-1} [V] \in 𝒫 F^{-1} [V] \leftrightarrow y \cap F^{-1} [V] \subseteq F^{-1} [V])$
34	31 33	mpbiri	$⊢ (((F \in (C CovMap J) \land V \in J \land V \subseteq U) \land x \in S (U)) \land y \in x) \to y \cap F^{-1} [V] \in 𝒫 F^{-1} [V]$
35	34	fmpttd	$⊢ ((F \in (C CovMap J) \land V \in J \land V \subseteq U) \land x \in S (U)) \to (y \in x ⟼ y \cap F^{-1} [V]) : x ⟶ 𝒫 F^{-1} [V]$
36	35	frnd	$⊢ ((F \in (C CovMap J) \land V \in J \land V \subseteq U) \land x \in S (U)) \to ran (y \in x ⟼ y \cap F^{-1} [V]) \subseteq 𝒫 F^{-1} [V]$
37		sspwuni	$⊢ ran (y \in x ⟼ y \cap F^{-1} [V]) \subseteq 𝒫 F^{-1} [V] \leftrightarrow ⋃ ran (y \in x ⟼ y \cap F^{-1} [V]) \subseteq F^{-1} [V]$
38	36 37	sylib	$⊢ ((F \in (C CovMap J) \land V \in J \land V \subseteq U) \land x \in S (U)) \to ⋃ ran (y \in x ⟼ y \cap F^{-1} [V]) \subseteq F^{-1} [V]$
39		simpl3	$⊢ ((F \in (C CovMap J) \land V \in J \land V \subseteq U) \land x \in S (U)) \to V \subseteq U$
40		imass2	$⊢ V \subseteq U \to F^{-1} [V] \subseteq F^{-1} [U]$
41	39 40	syl	$⊢ ((F \in (C CovMap J) \land V \in J \land V \subseteq U) \land x \in S (U)) \to F^{-1} [V] \subseteq F^{-1} [U]$
42	1	cvmsuni	$⊢ x \in S (U) \to ⋃ x = F^{-1} [U]$
43	42	adantl	$⊢ ((F \in (C CovMap J) \land V \in J \land V \subseteq U) \land x \in S (U)) \to ⋃ x = F^{-1} [U]$
44	41 43	sseqtrrd	$⊢ ((F \in (C CovMap J) \land V \in J \land V \subseteq U) \land x \in S (U)) \to F^{-1} [V] \subseteq ⋃ x$
45	44	sselda	$⊢ (((F \in (C CovMap J) \land V \in J \land V \subseteq U) \land x \in S (U)) \land z \in F^{-1} [V]) \to z \in ⋃ x$
46		eqid	$⊢ t \cap F^{-1} [V] = t \cap F^{-1} [V]$
47		ineq1	$⊢ y = t \to y \cap F^{-1} [V] = t \cap F^{-1} [V]$
48	47	rspceeqv	$⊢ (t \in x \land t \cap F^{-1} [V] = t \cap F^{-1} [V]) \to \exists y \in x t \cap F^{-1} [V] = y \cap F^{-1} [V]$
49	46 48	mpan2	$⊢ t \in x \to \exists y \in x t \cap F^{-1} [V] = y \cap F^{-1} [V]$
50	49	ad2antrl	$⊢ ((((F \in (C CovMap J) \land V \in J \land V \subseteq U) \land x \in S (U)) \land z \in F^{-1} [V]) \land (t \in x \land z \in t)) \to \exists y \in x t \cap F^{-1} [V] = y \cap F^{-1} [V]$
51		vex	$⊢ t \in V$
52	51	inex1	$⊢ t \cap F^{-1} [V] \in V$
53		eqid	$⊢ (y \in x ⟼ y \cap F^{-1} [V]) = (y \in x ⟼ y \cap F^{-1} [V])$
54	53	elrnmpt	$⊢ t \cap F^{-1} [V] \in V \to (t \cap F^{-1} [V] \in ran (y \in x ⟼ y \cap F^{-1} [V]) \leftrightarrow \exists y \in x t \cap F^{-1} [V] = y \cap F^{-1} [V])$
55	52 54	ax-mp	$⊢ t \cap F^{-1} [V] \in ran (y \in x ⟼ y \cap F^{-1} [V]) \leftrightarrow \exists y \in x t \cap F^{-1} [V] = y \cap F^{-1} [V]$
56	50 55	sylibr	$⊢ ((((F \in (C CovMap J) \land V \in J \land V \subseteq U) \land x \in S (U)) \land z \in F^{-1} [V]) \land (t \in x \land z \in t)) \to t \cap F^{-1} [V] \in ran (y \in x ⟼ y \cap F^{-1} [V])$
57		simprr	$⊢ ((((F \in (C CovMap J) \land V \in J \land V \subseteq U) \land x \in S (U)) \land z \in F^{-1} [V]) \land (t \in x \land z \in t)) \to z \in t$
58		simplr	$⊢ ((((F \in (C CovMap J) \land V \in J \land V \subseteq U) \land x \in S (U)) \land z \in F^{-1} [V]) \land (t \in x \land z \in t)) \to z \in F^{-1} [V]$
59	57 58	elind	$⊢ ((((F \in (C CovMap J) \land V \in J \land V \subseteq U) \land x \in S (U)) \land z \in F^{-1} [V]) \land (t \in x \land z \in t)) \to z \in (t \cap F^{-1} [V])$
60		eleq2	$⊢ w = t \cap F^{-1} [V] \to (z \in w \leftrightarrow z \in (t \cap F^{-1} [V]))$
61	60	rspcev	$⊢ (t \cap F^{-1} [V] \in ran (y \in x ⟼ y \cap F^{-1} [V]) \land z \in (t \cap F^{-1} [V])) \to \exists w \in ran (y \in x ⟼ y \cap F^{-1} [V]) z \in w$
62	56 59 61	syl2anc	$⊢ ((((F \in (C CovMap J) \land V \in J \land V \subseteq U) \land x \in S (U)) \land z \in F^{-1} [V]) \land (t \in x \land z \in t)) \to \exists w \in ran (y \in x ⟼ y \cap F^{-1} [V]) z \in w$
63	62	rexlimdvaa	$⊢ (((F \in (C CovMap J) \land V \in J \land V \subseteq U) \land x \in S (U)) \land z \in F^{-1} [V]) \to (\exists t \in x z \in t \to \exists w \in ran (y \in x ⟼ y \cap F^{-1} [V]) z \in w)$
64		eluni2	$⊢ z \in ⋃ x \leftrightarrow \exists t \in x z \in t$
65		eluni2	$⊢ z \in ⋃ ran (y \in x ⟼ y \cap F^{-1} [V]) \leftrightarrow \exists w \in ran (y \in x ⟼ y \cap F^{-1} [V]) z \in w$
66	63 64 65	3imtr4g	$⊢ (((F \in (C CovMap J) \land V \in J \land V \subseteq U) \land x \in S (U)) \land z \in F^{-1} [V]) \to (z \in ⋃ x \to z \in ⋃ ran (y \in x ⟼ y \cap F^{-1} [V]))$
67	45 66	mpd	$⊢ (((F \in (C CovMap J) \land V \in J \land V \subseteq U) \land x \in S (U)) \land z \in F^{-1} [V]) \to z \in ⋃ ran (y \in x ⟼ y \cap F^{-1} [V])$
68	38 67	eqelssd	$⊢ ((F \in (C CovMap J) \land V \in J \land V \subseteq U) \land x \in S (U)) \to ⋃ ran (y \in x ⟼ y \cap F^{-1} [V]) = F^{-1} [V]$
69		eldifsn	$⊢ z \in (ran (y \in x ⟼ y \cap F^{-1} [V]) ∖ \{t \cap F^{-1} [V]\}) \leftrightarrow (z \in ran (y \in x ⟼ y \cap F^{-1} [V]) \land z \neq t \cap F^{-1} [V])$
70		vex	$⊢ z \in V$
71	53	elrnmpt	$⊢ z \in V \to (z \in ran (y \in x ⟼ y \cap F^{-1} [V]) \leftrightarrow \exists y \in x z = y \cap F^{-1} [V])$
72	70 71	ax-mp	$⊢ z \in ran (y \in x ⟼ y \cap F^{-1} [V]) \leftrightarrow \exists y \in x z = y \cap F^{-1} [V]$
73	47	equcoms	$⊢ t = y \to y \cap F^{-1} [V] = t \cap F^{-1} [V]$
74	73	necon3ai	$⊢ y \cap F^{-1} [V] \neq t \cap F^{-1} [V] \to \neg t = y$
75		simpllr	$⊢ ((((F \in (C CovMap J) \land V \in J \land V \subseteq U) \land x \in S (U)) \land t \in x) \land y \in x) \to x \in S (U)$
76		simplr	$⊢ ((((F \in (C CovMap J) \land V \in J \land V \subseteq U) \land x \in S (U)) \land t \in x) \land y \in x) \to t \in x$
77		simpr	$⊢ ((((F \in (C CovMap J) \land V \in J \land V \subseteq U) \land x \in S (U)) \land t \in x) \land y \in x) \to y \in x$
78	1	cvmsdisj	$⊢ (x \in S (U) \land t \in x \land y \in x) \to (t = y \lor t \cap y = \emptyset)$
79	75 76 77 78	syl3anc	$⊢ ((((F \in (C CovMap J) \land V \in J \land V \subseteq U) \land x \in S (U)) \land t \in x) \land y \in x) \to (t = y \lor t \cap y = \emptyset)$
80	79	ord	$⊢ ((((F \in (C CovMap J) \land V \in J \land V \subseteq U) \land x \in S (U)) \land t \in x) \land y \in x) \to (\neg t = y \to t \cap y = \emptyset)$
81		inss1	$⊢ (t \cap y) \cap F^{-1} [V] \subseteq t \cap y$
82		sseq0	$⊢ ((t \cap y) \cap F^{-1} [V] \subseteq t \cap y \land t \cap y = \emptyset) \to (t \cap y) \cap F^{-1} [V] = \emptyset$
83	81 82	mpan	$⊢ t \cap y = \emptyset \to (t \cap y) \cap F^{-1} [V] = \emptyset$
84	74 80 83	syl56	$⊢ ((((F \in (C CovMap J) \land V \in J \land V \subseteq U) \land x \in S (U)) \land t \in x) \land y \in x) \to (y \cap F^{-1} [V] \neq t \cap F^{-1} [V] \to (t \cap y) \cap F^{-1} [V] = \emptyset)$
85		neeq1	$⊢ z = y \cap F^{-1} [V] \to (z \neq t \cap F^{-1} [V] \leftrightarrow y \cap F^{-1} [V] \neq t \cap F^{-1} [V])$
86		ineq2	$⊢ z = y \cap F^{-1} [V] \to (t \cap F^{-1} [V]) \cap z = (t \cap F^{-1} [V]) \cap (y \cap F^{-1} [V])$
87		inindir	$⊢ (t \cap y) \cap F^{-1} [V] = (t \cap F^{-1} [V]) \cap (y \cap F^{-1} [V])$
88	86 87	eqtr4di	$⊢ z = y \cap F^{-1} [V] \to (t \cap F^{-1} [V]) \cap z = (t \cap y) \cap F^{-1} [V]$
89	88	eqeq1d	$⊢ z = y \cap F^{-1} [V] \to ((t \cap F^{-1} [V]) \cap z = \emptyset \leftrightarrow (t \cap y) \cap F^{-1} [V] = \emptyset)$
90	85 89	imbi12d	$⊢ z = y \cap F^{-1} [V] \to ((z \neq t \cap F^{-1} [V] \to (t \cap F^{-1} [V]) \cap z = \emptyset) \leftrightarrow (y \cap F^{-1} [V] \neq t \cap F^{-1} [V] \to (t \cap y) \cap F^{-1} [V] = \emptyset))$
91	84 90	syl5ibrcom	$⊢ ((((F \in (C CovMap J) \land V \in J \land V \subseteq U) \land x \in S (U)) \land t \in x) \land y \in x) \to (z = y \cap F^{-1} [V] \to (z \neq t \cap F^{-1} [V] \to (t \cap F^{-1} [V]) \cap z = \emptyset))$
92	91	rexlimdva	$⊢ (((F \in (C CovMap J) \land V \in J \land V \subseteq U) \land x \in S (U)) \land t \in x) \to (\exists y \in x z = y \cap F^{-1} [V] \to (z \neq t \cap F^{-1} [V] \to (t \cap F^{-1} [V]) \cap z = \emptyset))$
93	72 92	biimtrid	$⊢ (((F \in (C CovMap J) \land V \in J \land V \subseteq U) \land x \in S (U)) \land t \in x) \to (z \in ran (y \in x ⟼ y \cap F^{-1} [V]) \to (z \neq t \cap F^{-1} [V] \to (t \cap F^{-1} [V]) \cap z = \emptyset))$
94	93	impd	$⊢ (((F \in (C CovMap J) \land V \in J \land V \subseteq U) \land x \in S (U)) \land t \in x) \to ((z \in ran (y \in x ⟼ y \cap F^{-1} [V]) \land z \neq t \cap F^{-1} [V]) \to (t \cap F^{-1} [V]) \cap z = \emptyset)$
95	69 94	biimtrid	$⊢ (((F \in (C CovMap J) \land V \in J \land V \subseteq U) \land x \in S (U)) \land t \in x) \to (z \in (ran (y \in x ⟼ y \cap F^{-1} [V]) ∖ \{t \cap F^{-1} [V]\}) \to (t \cap F^{-1} [V]) \cap z = \emptyset)$
96	95	ralrimiv	$⊢ (((F \in (C CovMap J) \land V \in J \land V \subseteq U) \land x \in S (U)) \land t \in x) \to \forall z \in (ran (y \in x ⟼ y \cap F^{-1} [V]) ∖ \{t \cap F^{-1} [V]\}) (t \cap F^{-1} [V]) \cap z = \emptyset$
97		inss1	$⊢ t \cap F^{-1} [V] \subseteq t$
98		resabs1	$⊢ t \cap F^{-1} [V] \subseteq t \to {({F ↾}_{t}) ↾}_{(t \cap F^{-1} [V])} = {F ↾}_{(t \cap F^{-1} [V])}$
99	97 98	ax-mp	$⊢ {({F ↾}_{t}) ↾}_{(t \cap F^{-1} [V])} = {F ↾}_{(t \cap F^{-1} [V])}$
100	1	cvmshmeo	$⊢ (x \in S (U) \land t \in x) \to {F ↾}_{t} \in ((C ↾_{𝑡} t) Homeo (J ↾_{𝑡} U))$
101	100	adantll	$⊢ (((F \in (C CovMap J) \land V \in J \land V \subseteq U) \land x \in S (U)) \land t \in x) \to {F ↾}_{t} \in ((C ↾_{𝑡} t) Homeo (J ↾_{𝑡} U))$
102	6	adantr	$⊢ (((F \in (C CovMap J) \land V \in J \land V \subseteq U) \land x \in S (U)) \land t \in x) \to C \in Top$
103	9	sselda	$⊢ (((F \in (C CovMap J) \land V \in J \land V \subseteq U) \land x \in S (U)) \land t \in x) \to t \in C$
104		elssuni	$⊢ t \in C \to t \subseteq ⋃ C$
105	103 104	syl	$⊢ (((F \in (C CovMap J) \land V \in J \land V \subseteq U) \land x \in S (U)) \land t \in x) \to t \subseteq ⋃ C$
106		eqid	$⊢ ⋃ C = ⋃ C$
107	106	restuni	$⊢ (C \in Top \land t \subseteq ⋃ C) \to t = ⋃ (C ↾_{𝑡} t)$
108	102 105 107	syl2anc	$⊢ (((F \in (C CovMap J) \land V \in J \land V \subseteq U) \land x \in S (U)) \land t \in x) \to t = ⋃ (C ↾_{𝑡} t)$
109	97 108	sseqtrid	$⊢ (((F \in (C CovMap J) \land V \in J \land V \subseteq U) \land x \in S (U)) \land t \in x) \to t \cap F^{-1} [V] \subseteq ⋃ (C ↾_{𝑡} t)$
110		eqid	$⊢ ⋃ (C ↾_{𝑡} t) = ⋃ (C ↾_{𝑡} t)$
111	110	hmeores	$⊢ ({F ↾}_{t} \in ((C ↾_{𝑡} t) Homeo (J ↾_{𝑡} U)) \land t \cap F^{-1} [V] \subseteq ⋃ (C ↾_{𝑡} t)) \to {({F ↾}_{t}) ↾}_{(t \cap F^{-1} [V])} \in (((C ↾_{𝑡} t) ↾_{𝑡} (t \cap F^{-1} [V])) Homeo ((J ↾_{𝑡} U) ↾_{𝑡} ({F ↾}_{t}) [t \cap F^{-1} [V]]))$
112	101 109 111	syl2anc	$⊢ (((F \in (C CovMap J) \land V \in J \land V \subseteq U) \land x \in S (U)) \land t \in x) \to {({F ↾}_{t}) ↾}_{(t \cap F^{-1} [V])} \in (((C ↾_{𝑡} t) ↾_{𝑡} (t \cap F^{-1} [V])) Homeo ((J ↾_{𝑡} U) ↾_{𝑡} ({F ↾}_{t}) [t \cap F^{-1} [V]]))$
113	99 112	eqeltrrid	$⊢ (((F \in (C CovMap J) \land V \in J \land V \subseteq U) \land x \in S (U)) \land t \in x) \to {F ↾}_{(t \cap F^{-1} [V])} \in (((C ↾_{𝑡} t) ↾_{𝑡} (t \cap F^{-1} [V])) Homeo ((J ↾_{𝑡} U) ↾_{𝑡} ({F ↾}_{t}) [t \cap F^{-1} [V]]))$
114	97	a1i	$⊢ (((F \in (C CovMap J) \land V \in J \land V \subseteq U) \land x \in S (U)) \land t \in x) \to t \cap F^{-1} [V] \subseteq t$
115		simpr	$⊢ (((F \in (C CovMap J) \land V \in J \land V \subseteq U) \land x \in S (U)) \land t \in x) \to t \in x$
116		restabs	$⊢ (C \in Top \land t \cap F^{-1} [V] \subseteq t \land t \in x) \to (C ↾_{𝑡} t) ↾_{𝑡} (t \cap F^{-1} [V]) = C ↾_{𝑡} (t \cap F^{-1} [V])$
117	102 114 115 116	syl3anc	$⊢ (((F \in (C CovMap J) \land V \in J \land V \subseteq U) \land x \in S (U)) \land t \in x) \to (C ↾_{𝑡} t) ↾_{𝑡} (t \cap F^{-1} [V]) = C ↾_{𝑡} (t \cap F^{-1} [V])$
118		incom	$⊢ t \cap F^{-1} [V] = F^{-1} [V] \cap t$
119		cnvresima	$⊢ {({F ↾}_{t})}^{-1} [V] = F^{-1} [V] \cap t$
120	118 119	eqtr4i	$⊢ t \cap F^{-1} [V] = {({F ↾}_{t})}^{-1} [V]$
121	120	imaeq2i	$⊢ ({F ↾}_{t}) [t \cap F^{-1} [V]] = ({F ↾}_{t}) [{({F ↾}_{t})}^{-1} [V]]$
122	4	adantr	$⊢ (((F \in (C CovMap J) \land V \in J \land V \subseteq U) \land x \in S (U)) \land t \in x) \to F \in (C CovMap J)$
123		simplr	$⊢ (((F \in (C CovMap J) \land V \in J \land V \subseteq U) \land x \in S (U)) \land t \in x) \to x \in S (U)$
124	1	cvmsf1o	$⊢ (F \in (C CovMap J) \land x \in S (U) \land t \in x) \to ({F ↾}_{t}) : t \underset{1-1 onto}{⟶} U$
125	122 123 115 124	syl3anc	$⊢ (((F \in (C CovMap J) \land V \in J \land V \subseteq U) \land x \in S (U)) \land t \in x) \to ({F ↾}_{t}) : t \underset{1-1 onto}{⟶} U$
126		f1ofo	$⊢ ({F ↾}_{t}) : t \underset{1-1 onto}{⟶} U \to ({F ↾}_{t}) : t \underset{onto}{⟶} U$
127	125 126	syl	$⊢ (((F \in (C CovMap J) \land V \in J \land V \subseteq U) \land x \in S (U)) \land t \in x) \to ({F ↾}_{t}) : t \underset{onto}{⟶} U$
128	39	adantr	$⊢ (((F \in (C CovMap J) \land V \in J \land V \subseteq U) \land x \in S (U)) \land t \in x) \to V \subseteq U$
129		foimacnv	$⊢ (({F ↾}_{t}) : t \underset{onto}{⟶} U \land V \subseteq U) \to ({F ↾}_{t}) [{({F ↾}_{t})}^{-1} [V]] = V$
130	127 128 129	syl2anc	$⊢ (((F \in (C CovMap J) \land V \in J \land V \subseteq U) \land x \in S (U)) \land t \in x) \to ({F ↾}_{t}) [{({F ↾}_{t})}^{-1} [V]] = V$
131	121 130	eqtrid	$⊢ (((F \in (C CovMap J) \land V \in J \land V \subseteq U) \land x \in S (U)) \land t \in x) \to ({F ↾}_{t}) [t \cap F^{-1} [V]] = V$
132	131	oveq2d	$⊢ (((F \in (C CovMap J) \land V \in J \land V \subseteq U) \land x \in S (U)) \land t \in x) \to (J ↾_{𝑡} U) ↾_{𝑡} ({F ↾}_{t}) [t \cap F^{-1} [V]] = (J ↾_{𝑡} U) ↾_{𝑡} V$
133		cvmtop2	$⊢ F \in (C CovMap J) \to J \in Top$
134	4 133	syl	$⊢ ((F \in (C CovMap J) \land V \in J \land V \subseteq U) \land x \in S (U)) \to J \in Top$
135	1	cvmsrcl	$⊢ x \in S (U) \to U \in J$
136	135	adantl	$⊢ ((F \in (C CovMap J) \land V \in J \land V \subseteq U) \land x \in S (U)) \to U \in J$
137		restabs	$⊢ (J \in Top \land V \subseteq U \land U \in J) \to (J ↾_{𝑡} U) ↾_{𝑡} V = J ↾_{𝑡} V$
138	134 39 136 137	syl3anc	$⊢ ((F \in (C CovMap J) \land V \in J \land V \subseteq U) \land x \in S (U)) \to (J ↾_{𝑡} U) ↾_{𝑡} V = J ↾_{𝑡} V$
139	138	adantr	$⊢ (((F \in (C CovMap J) \land V \in J \land V \subseteq U) \land x \in S (U)) \land t \in x) \to (J ↾_{𝑡} U) ↾_{𝑡} V = J ↾_{𝑡} V$
140	132 139	eqtrd	$⊢ (((F \in (C CovMap J) \land V \in J \land V \subseteq U) \land x \in S (U)) \land t \in x) \to (J ↾_{𝑡} U) ↾_{𝑡} ({F ↾}_{t}) [t \cap F^{-1} [V]] = J ↾_{𝑡} V$
141	117 140	oveq12d	$⊢ (((F \in (C CovMap J) \land V \in J \land V \subseteq U) \land x \in S (U)) \land t \in x) \to ((C ↾_{𝑡} t) ↾_{𝑡} (t \cap F^{-1} [V])) Homeo ((J ↾_{𝑡} U) ↾_{𝑡} ({F ↾}_{t}) [t \cap F^{-1} [V]]) = (C ↾_{𝑡} (t \cap F^{-1} [V])) Homeo (J ↾_{𝑡} V)$
142	113 141	eleqtrd	$⊢ (((F \in (C CovMap J) \land V \in J \land V \subseteq U) \land x \in S (U)) \land t \in x) \to {F ↾}_{(t \cap F^{-1} [V])} \in ((C ↾_{𝑡} (t \cap F^{-1} [V])) Homeo (J ↾_{𝑡} V))$
143	96 142	jca	$⊢ (((F \in (C CovMap J) \land V \in J \land V \subseteq U) \land x \in S (U)) \land t \in x) \to (\forall z \in (ran (y \in x ⟼ y \cap F^{-1} [V]) ∖ \{t \cap F^{-1} [V]\}) (t \cap F^{-1} [V]) \cap z = \emptyset \land {F ↾}_{(t \cap F^{-1} [V])} \in ((C ↾_{𝑡} (t \cap F^{-1} [V])) Homeo (J ↾_{𝑡} V)))$
144	143	ralrimiva	$⊢ ((F \in (C CovMap J) \land V \in J \land V \subseteq U) \land x \in S (U)) \to \forall t \in x (\forall z \in (ran (y \in x ⟼ y \cap F^{-1} [V]) ∖ \{t \cap F^{-1} [V]\}) (t \cap F^{-1} [V]) \cap z = \emptyset \land {F ↾}_{(t \cap F^{-1} [V])} \in ((C ↾_{𝑡} (t \cap F^{-1} [V])) Homeo (J ↾_{𝑡} V)))$
145	52	rgenw	$⊢ \forall t \in x t \cap F^{-1} [V] \in V$
146	47	cbvmptv	$⊢ (y \in x ⟼ y \cap F^{-1} [V]) = (t \in x ⟼ t \cap F^{-1} [V])$
147		sneq	$⊢ w = t \cap F^{-1} [V] \to \{w\} = \{t \cap F^{-1} [V]\}$
148	147	difeq2d	$⊢ w = t \cap F^{-1} [V] \to ran (y \in x ⟼ y \cap F^{-1} [V]) ∖ \{w\} = ran (y \in x ⟼ y \cap F^{-1} [V]) ∖ \{t \cap F^{-1} [V]\}$
149		ineq1	$⊢ w = t \cap F^{-1} [V] \to w \cap z = (t \cap F^{-1} [V]) \cap z$
150	149	eqeq1d	$⊢ w = t \cap F^{-1} [V] \to (w \cap z = \emptyset \leftrightarrow (t \cap F^{-1} [V]) \cap z = \emptyset)$
151	148 150	raleqbidv	$⊢ w = t \cap F^{-1} [V] \to (\forall z \in (ran (y \in x ⟼ y \cap F^{-1} [V]) ∖ \{w\}) w \cap z = \emptyset \leftrightarrow \forall z \in (ran (y \in x ⟼ y \cap F^{-1} [V]) ∖ \{t \cap F^{-1} [V]\}) (t \cap F^{-1} [V]) \cap z = \emptyset)$
152		reseq2	$⊢ w = t \cap F^{-1} [V] \to {F ↾}_{w} = {F ↾}_{(t \cap F^{-1} [V])}$
153		oveq2	$⊢ w = t \cap F^{-1} [V] \to C ↾_{𝑡} w = C ↾_{𝑡} (t \cap F^{-1} [V])$
154	153	oveq1d	$⊢ w = t \cap F^{-1} [V] \to (C ↾_{𝑡} w) Homeo (J ↾_{𝑡} V) = (C ↾_{𝑡} (t \cap F^{-1} [V])) Homeo (J ↾_{𝑡} V)$
155	152 154	eleq12d	$⊢ w = t \cap F^{-1} [V] \to ({F ↾}_{w} \in ((C ↾_{𝑡} w) Homeo (J ↾_{𝑡} V)) \leftrightarrow {F ↾}_{(t \cap F^{-1} [V])} \in ((C ↾_{𝑡} (t \cap F^{-1} [V])) Homeo (J ↾_{𝑡} V)))$
156	151 155	anbi12d	$⊢ w = t \cap F^{-1} [V] \to ((\forall z \in (ran (y \in x ⟼ y \cap F^{-1} [V]) ∖ \{w\}) w \cap z = \emptyset \land {F ↾}_{w} \in ((C ↾_{𝑡} w) Homeo (J ↾_{𝑡} V))) \leftrightarrow (\forall z \in (ran (y \in x ⟼ y \cap F^{-1} [V]) ∖ \{t \cap F^{-1} [V]\}) (t \cap F^{-1} [V]) \cap z = \emptyset \land {F ↾}_{(t \cap F^{-1} [V])} \in ((C ↾_{𝑡} (t \cap F^{-1} [V])) Homeo (J ↾_{𝑡} V))))$
157	146 156	ralrnmptw	$⊢ \forall t \in x t \cap F^{-1} [V] \in V \to (\forall w \in ran (y \in x ⟼ y \cap F^{-1} [V]) (\forall z \in (ran (y \in x ⟼ y \cap F^{-1} [V]) ∖ \{w\}) w \cap z = \emptyset \land {F ↾}_{w} \in ((C ↾_{𝑡} w) Homeo (J ↾_{𝑡} V))) \leftrightarrow \forall t \in x (\forall z \in (ran (y \in x ⟼ y \cap F^{-1} [V]) ∖ \{t \cap F^{-1} [V]\}) (t \cap F^{-1} [V]) \cap z = \emptyset \land {F ↾}_{(t \cap F^{-1} [V])} \in ((C ↾_{𝑡} (t \cap F^{-1} [V])) Homeo (J ↾_{𝑡} V))))$
158	145 157	ax-mp	$⊢ \forall w \in ran (y \in x ⟼ y \cap F^{-1} [V]) (\forall z \in (ran (y \in x ⟼ y \cap F^{-1} [V]) ∖ \{w\}) w \cap z = \emptyset \land {F ↾}_{w} \in ((C ↾_{𝑡} w) Homeo (J ↾_{𝑡} V))) \leftrightarrow \forall t \in x (\forall z \in (ran (y \in x ⟼ y \cap F^{-1} [V]) ∖ \{t \cap F^{-1} [V]\}) (t \cap F^{-1} [V]) \cap z = \emptyset \land {F ↾}_{(t \cap F^{-1} [V])} \in ((C ↾_{𝑡} (t \cap F^{-1} [V])) Homeo (J ↾_{𝑡} V)))$
159	144 158	sylibr	$⊢ ((F \in (C CovMap J) \land V \in J \land V \subseteq U) \land x \in S (U)) \to \forall w \in ran (y \in x ⟼ y \cap F^{-1} [V]) (\forall z \in (ran (y \in x ⟼ y \cap F^{-1} [V]) ∖ \{w\}) w \cap z = \emptyset \land {F ↾}_{w} \in ((C ↾_{𝑡} w) Homeo (J ↾_{𝑡} V)))$
160	68 159	jca	$⊢ ((F \in (C CovMap J) \land V \in J \land V \subseteq U) \land x \in S (U)) \to (⋃ ran (y \in x ⟼ y \cap F^{-1} [V]) = F^{-1} [V] \land \forall w \in ran (y \in x ⟼ y \cap F^{-1} [V]) (\forall z \in (ran (y \in x ⟼ y \cap F^{-1} [V]) ∖ \{w\}) w \cap z = \emptyset \land {F ↾}_{w} \in ((C ↾_{𝑡} w) Homeo (J ↾_{𝑡} V))))$
161	1	cvmscbv	$⊢ S = (a \in J ⟼ \{b \in (𝒫 C ∖ \{\emptyset\}) \| (⋃ b = F^{-1} [a] \land \forall w \in b (\forall z \in (b ∖ \{w\}) w \cap z = \emptyset \land {F ↾}_{w} \in ((C ↾_{𝑡} w) Homeo (J ↾_{𝑡} a))))\})$
162	161	cvmsval	$⊢ C \in Top \to (ran (y \in x ⟼ y \cap F^{-1} [V]) \in S (V) \leftrightarrow (V \in J \land (ran (y \in x ⟼ y \cap F^{-1} [V]) \subseteq C \land ran (y \in x ⟼ y \cap F^{-1} [V]) \neq \emptyset) \land (⋃ ran (y \in x ⟼ y \cap F^{-1} [V]) = F^{-1} [V] \land \forall w \in ran (y \in x ⟼ y \cap F^{-1} [V]) (\forall z \in (ran (y \in x ⟼ y \cap F^{-1} [V]) ∖ \{w\}) w \cap z = \emptyset \land {F ↾}_{w} \in ((C ↾_{𝑡} w) Homeo (J ↾_{𝑡} V))))))$
163	6 162	syl	$⊢ ((F \in (C CovMap J) \land V \in J \land V \subseteq U) \land x \in S (U)) \to (ran (y \in x ⟼ y \cap F^{-1} [V]) \in S (V) \leftrightarrow (V \in J \land (ran (y \in x ⟼ y \cap F^{-1} [V]) \subseteq C \land ran (y \in x ⟼ y \cap F^{-1} [V]) \neq \emptyset) \land (⋃ ran (y \in x ⟼ y \cap F^{-1} [V]) = F^{-1} [V] \land \forall w \in ran (y \in x ⟼ y \cap F^{-1} [V]) (\forall z \in (ran (y \in x ⟼ y \cap F^{-1} [V]) ∖ \{w\}) w \cap z = \emptyset \land {F ↾}_{w} \in ((C ↾_{𝑡} w) Homeo (J ↾_{𝑡} V))))))$
164	3 30 160 163	mpbir3and	$⊢ ((F \in (C CovMap J) \land V \in J \land V \subseteq U) \land x \in S (U)) \to ran (y \in x ⟼ y \cap F^{-1} [V]) \in S (V)$
165	164	ne0d	$⊢ ((F \in (C CovMap J) \land V \in J \land V \subseteq U) \land x \in S (U)) \to S (V) \neq \emptyset$
166	165	ex	$⊢ (F \in (C CovMap J) \land V \in J \land V \subseteq U) \to (x \in S (U) \to S (V) \neq \emptyset)$
167	166	exlimdv	$⊢ (F \in (C CovMap J) \land V \in J \land V \subseteq U) \to (\exists x x \in S (U) \to S (V) \neq \emptyset)$
168	2 167	biimtrid	$⊢ (F \in (C CovMap J) \land V \in J \land V \subseteq U) \to (S (U) \neq \emptyset \to S (V) \neq \emptyset)$

Metamath Proof Explorer

Theorem cvmsss2

Proof