cvmopnlem - Mathbox for Mario Carneiro

	Mathbox for Mario Carneiro		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > cvmopnlem		Structured version Visualization version GIF version

Theorem cvmopnlem 34338

Description: Lemma for cvmopn 34340. (Contributed by Mario Carneiro, 7-May-2015.)

**Hypotheses**
Ref	Expression
cvmcov.1	⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (^◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾_t 𝑢)Homeo(𝐽 ↾_t 𝑘))))})
cvmseu.1	⊢ 𝐵 = ∪ 𝐶

**Assertion**
Ref	Expression
cvmopnlem	⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) → (𝐹 “ 𝐴) ∈ 𝐽)

Distinct variable groups: 𝑘,𝑠,𝑢,𝑣,𝐶 𝑘,𝐹,𝑠,𝑢,𝑣 𝑘,𝐽,𝑠,𝑢,𝑣 𝑢,𝐴,𝑣 𝑣,𝐵 Allowed substitution hints: 𝐴(𝑘,𝑠) 𝐵(𝑢,𝑘,𝑠) 𝑆(𝑣,𝑢,𝑘,𝑠)

Proof of Theorem cvmopnlem Dummy variables 𝑡 𝑤 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		simpll 765	. . . . . 6 ⊢ (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) → 𝐹 ∈ (𝐶 CovMap 𝐽))
2		cvmcn 34322	. . . . . . . . . 10 ⊢ (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐹 ∈ (𝐶 Cn 𝐽))
3	2	adantr 481	. . . . . . . . 9 ⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) → 𝐹 ∈ (𝐶 Cn 𝐽))
4		cvmseu.1	. . . . . . . . . 10 ⊢ 𝐵 = ∪ 𝐶
5		eqid 2732	. . . . . . . . . 10 ⊢ ∪ 𝐽 = ∪ 𝐽
6	4, 5	cnf 22757	. . . . . . . . 9 ⊢ (𝐹 ∈ (𝐶 Cn 𝐽) → 𝐹:𝐵⟶∪ 𝐽)
7	3, 6	syl 17	. . . . . . . 8 ⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) → 𝐹:𝐵⟶∪ 𝐽)
8	7	adantr 481	. . . . . . 7 ⊢ (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) → 𝐹:𝐵⟶∪ 𝐽)
9		elssuni 4941	. . . . . . . . . 10 ⊢ (𝐴 ∈ 𝐶 → 𝐴 ⊆ ∪ 𝐶)
10	9, 4	sseqtrrdi 4033	. . . . . . . . 9 ⊢ (𝐴 ∈ 𝐶 → 𝐴 ⊆ 𝐵)
11	10	adantl 482	. . . . . . . 8 ⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) → 𝐴 ⊆ 𝐵)
12	11	sselda 3982	. . . . . . 7 ⊢ (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) → 𝑧 ∈ 𝐵)
13	8, 12	ffvelcdmd 7087	. . . . . 6 ⊢ (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) → (𝐹‘𝑧) ∈ ∪ 𝐽)
14		cvmcov.1	. . . . . . 7 ⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (^◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾_t 𝑢)Homeo(𝐽 ↾_t 𝑘))))})
15	14, 5	cvmcov 34323	. . . . . 6 ⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ (𝐹‘𝑧) ∈ ∪ 𝐽) → ∃𝑡 ∈ 𝐽 ((𝐹‘𝑧) ∈ 𝑡 ∧ (𝑆‘𝑡) ≠ ∅))
16	1, 13, 15	syl2anc 584	. . . . 5 ⊢ (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) → ∃𝑡 ∈ 𝐽 ((𝐹‘𝑧) ∈ 𝑡 ∧ (𝑆‘𝑡) ≠ ∅))
17		n0 4346	. . . . . . . 8 ⊢ ((𝑆‘𝑡) ≠ ∅ ↔ ∃𝑤 𝑤 ∈ (𝑆‘𝑡))
18		inss2 4229	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥)) ⊆ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥)
19		resima2 6016	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥)) ⊆ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥) → ((𝐹 ↾ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥)) “ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))) = (𝐹 “ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))))
20	18, 19	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ ((𝐹 ↾ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥)) “ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))) = (𝐹 “ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥)))
21		simprr 771	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) ∧ ((𝐹‘𝑧) ∈ 𝑡 ∧ 𝑤 ∈ (𝑆‘𝑡))) → 𝑤 ∈ (𝑆‘𝑡))
22	1	adantr 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) ∧ ((𝐹‘𝑧) ∈ 𝑡 ∧ 𝑤 ∈ (𝑆‘𝑡))) → 𝐹 ∈ (𝐶 CovMap 𝐽))
23	12	adantr 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) ∧ ((𝐹‘𝑧) ∈ 𝑡 ∧ 𝑤 ∈ (𝑆‘𝑡))) → 𝑧 ∈ 𝐵)
24		simprl 769	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) ∧ ((𝐹‘𝑧) ∈ 𝑡 ∧ 𝑤 ∈ (𝑆‘𝑡))) → (𝐹‘𝑧) ∈ 𝑡)
25		eqid 2732	. . . . . . . . . . . . . . . . . . 19 ⊢ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥) = (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥)
26	14, 4, 25	cvmsiota 34337	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ (𝑤 ∈ (𝑆‘𝑡) ∧ 𝑧 ∈ 𝐵 ∧ (𝐹‘𝑧) ∈ 𝑡)) → ((℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥) ∈ 𝑤 ∧ 𝑧 ∈ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥)))
27	22, 21, 23, 24, 26	syl13anc 1372	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) ∧ ((𝐹‘𝑧) ∈ 𝑡 ∧ 𝑤 ∈ (𝑆‘𝑡))) → ((℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥) ∈ 𝑤 ∧ 𝑧 ∈ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥)))
28	27	simpld 495	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) ∧ ((𝐹‘𝑧) ∈ 𝑡 ∧ 𝑤 ∈ (𝑆‘𝑡))) → (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥) ∈ 𝑤)
29	14	cvmshmeo 34331	. . . . . . . . . . . . . . . 16 ⊢ ((𝑤 ∈ (𝑆‘𝑡) ∧ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥) ∈ 𝑤) → (𝐹 ↾ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥)) ∈ ((𝐶 ↾_t (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))Homeo(𝐽 ↾_t 𝑡)))
30	21, 28, 29	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) ∧ ((𝐹‘𝑧) ∈ 𝑡 ∧ 𝑤 ∈ (𝑆‘𝑡))) → (𝐹 ↾ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥)) ∈ ((𝐶 ↾_t (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))Homeo(𝐽 ↾_t 𝑡)))
31		cvmtop1 34320	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐶 ∈ Top)
32	22, 31	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) ∧ ((𝐹‘𝑧) ∈ 𝑡 ∧ 𝑤 ∈ (𝑆‘𝑡))) → 𝐶 ∈ Top)
33		simpllr 774	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) ∧ ((𝐹‘𝑧) ∈ 𝑡 ∧ 𝑤 ∈ (𝑆‘𝑡))) → 𝐴 ∈ 𝐶)
34		elrestr 17376	. . . . . . . . . . . . . . . 16 ⊢ ((𝐶 ∈ Top ∧ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥) ∈ 𝑤 ∧ 𝐴 ∈ 𝐶) → (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥)) ∈ (𝐶 ↾_t (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥)))
35	32, 28, 33, 34	syl3anc 1371	. . . . . . . . . . . . . . 15 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) ∧ ((𝐹‘𝑧) ∈ 𝑡 ∧ 𝑤 ∈ (𝑆‘𝑡))) → (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥)) ∈ (𝐶 ↾_t (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥)))
36		hmeoima 23276	. . . . . . . . . . . . . . 15 ⊢ (((𝐹 ↾ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥)) ∈ ((𝐶 ↾_t (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))Homeo(𝐽 ↾_t 𝑡)) ∧ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥)) ∈ (𝐶 ↾_t (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))) → ((𝐹 ↾ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥)) “ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))) ∈ (𝐽 ↾_t 𝑡))
37	30, 35, 36	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) ∧ ((𝐹‘𝑧) ∈ 𝑡 ∧ 𝑤 ∈ (𝑆‘𝑡))) → ((𝐹 ↾ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥)) “ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))) ∈ (𝐽 ↾_t 𝑡))
38	20, 37	eqeltrrid 2838	. . . . . . . . . . . . 13 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) ∧ ((𝐹‘𝑧) ∈ 𝑡 ∧ 𝑤 ∈ (𝑆‘𝑡))) → (𝐹 “ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))) ∈ (𝐽 ↾_t 𝑡))
39		cvmtop2 34321	. . . . . . . . . . . . . . . 16 ⊢ (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐽 ∈ Top)
40	39	adantr 481	. . . . . . . . . . . . . . 15 ⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) → 𝐽 ∈ Top)
41	40	ad2antrr 724	. . . . . . . . . . . . . 14 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) ∧ ((𝐹‘𝑧) ∈ 𝑡 ∧ 𝑤 ∈ (𝑆‘𝑡))) → 𝐽 ∈ Top)
42	14	cvmsrcl 34324	. . . . . . . . . . . . . . 15 ⊢ (𝑤 ∈ (𝑆‘𝑡) → 𝑡 ∈ 𝐽)
43	42	ad2antll 727	. . . . . . . . . . . . . 14 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) ∧ ((𝐹‘𝑧) ∈ 𝑡 ∧ 𝑤 ∈ (𝑆‘𝑡))) → 𝑡 ∈ 𝐽)
44		restopn2 22688	. . . . . . . . . . . . . 14 ⊢ ((𝐽 ∈ Top ∧ 𝑡 ∈ 𝐽) → ((𝐹 “ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))) ∈ (𝐽 ↾_t 𝑡) ↔ ((𝐹 “ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))) ∈ 𝐽 ∧ (𝐹 “ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))) ⊆ 𝑡)))
45	41, 43, 44	syl2anc 584	. . . . . . . . . . . . 13 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) ∧ ((𝐹‘𝑧) ∈ 𝑡 ∧ 𝑤 ∈ (𝑆‘𝑡))) → ((𝐹 “ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))) ∈ (𝐽 ↾_t 𝑡) ↔ ((𝐹 “ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))) ∈ 𝐽 ∧ (𝐹 “ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))) ⊆ 𝑡)))
46	38, 45	mpbid 231	. . . . . . . . . . . 12 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) ∧ ((𝐹‘𝑧) ∈ 𝑡 ∧ 𝑤 ∈ (𝑆‘𝑡))) → ((𝐹 “ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))) ∈ 𝐽 ∧ (𝐹 “ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))) ⊆ 𝑡))
47	46	simpld 495	. . . . . . . . . . 11 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) ∧ ((𝐹‘𝑧) ∈ 𝑡 ∧ 𝑤 ∈ (𝑆‘𝑡))) → (𝐹 “ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))) ∈ 𝐽)
48	7	ffnd 6718	. . . . . . . . . . . . 13 ⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) → 𝐹 Fn 𝐵)
49	48	ad2antrr 724	. . . . . . . . . . . 12 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) ∧ ((𝐹‘𝑧) ∈ 𝑡 ∧ 𝑤 ∈ (𝑆‘𝑡))) → 𝐹 Fn 𝐵)
50		inss1 4228	. . . . . . . . . . . . 13 ⊢ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥)) ⊆ 𝐴
51	33, 10	syl 17	. . . . . . . . . . . . 13 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) ∧ ((𝐹‘𝑧) ∈ 𝑡 ∧ 𝑤 ∈ (𝑆‘𝑡))) → 𝐴 ⊆ 𝐵)
52	50, 51	sstrid 3993	. . . . . . . . . . . 12 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) ∧ ((𝐹‘𝑧) ∈ 𝑡 ∧ 𝑤 ∈ (𝑆‘𝑡))) → (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥)) ⊆ 𝐵)
53		simplr 767	. . . . . . . . . . . . 13 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) ∧ ((𝐹‘𝑧) ∈ 𝑡 ∧ 𝑤 ∈ (𝑆‘𝑡))) → 𝑧 ∈ 𝐴)
54	27	simprd 496	. . . . . . . . . . . . 13 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) ∧ ((𝐹‘𝑧) ∈ 𝑡 ∧ 𝑤 ∈ (𝑆‘𝑡))) → 𝑧 ∈ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))
55	53, 54	elind 4194	. . . . . . . . . . . 12 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) ∧ ((𝐹‘𝑧) ∈ 𝑡 ∧ 𝑤 ∈ (𝑆‘𝑡))) → 𝑧 ∈ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥)))
56		fnfvima 7237	. . . . . . . . . . . 12 ⊢ ((𝐹 Fn 𝐵 ∧ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥)) ⊆ 𝐵 ∧ 𝑧 ∈ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))) → (𝐹‘𝑧) ∈ (𝐹 “ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))))
57	49, 52, 55, 56	syl3anc 1371	. . . . . . . . . . 11 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) ∧ ((𝐹‘𝑧) ∈ 𝑡 ∧ 𝑤 ∈ (𝑆‘𝑡))) → (𝐹‘𝑧) ∈ (𝐹 “ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))))
58		imass2 6101	. . . . . . . . . . . 12 ⊢ ((𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥)) ⊆ 𝐴 → (𝐹 “ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))) ⊆ (𝐹 “ 𝐴))
59	50, 58	mp1i 13	. . . . . . . . . . 11 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) ∧ ((𝐹‘𝑧) ∈ 𝑡 ∧ 𝑤 ∈ (𝑆‘𝑡))) → (𝐹 “ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))) ⊆ (𝐹 “ 𝐴))
60		eleq2 2822	. . . . . . . . . . . . 13 ⊢ (𝑦 = (𝐹 “ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))) → ((𝐹‘𝑧) ∈ 𝑦 ↔ (𝐹‘𝑧) ∈ (𝐹 “ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥)))))
61		sseq1 4007	. . . . . . . . . . . . 13 ⊢ (𝑦 = (𝐹 “ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))) → (𝑦 ⊆ (𝐹 “ 𝐴) ↔ (𝐹 “ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))) ⊆ (𝐹 “ 𝐴)))
62	60, 61	anbi12d 631	. . . . . . . . . . . 12 ⊢ (𝑦 = (𝐹 “ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))) → (((𝐹‘𝑧) ∈ 𝑦 ∧ 𝑦 ⊆ (𝐹 “ 𝐴)) ↔ ((𝐹‘𝑧) ∈ (𝐹 “ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))) ∧ (𝐹 “ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))) ⊆ (𝐹 “ 𝐴))))
63	62	rspcev 3612	. . . . . . . . . . 11 ⊢ (((𝐹 “ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))) ∈ 𝐽 ∧ ((𝐹‘𝑧) ∈ (𝐹 “ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))) ∧ (𝐹 “ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))) ⊆ (𝐹 “ 𝐴))) → ∃𝑦 ∈ 𝐽 ((𝐹‘𝑧) ∈ 𝑦 ∧ 𝑦 ⊆ (𝐹 “ 𝐴)))
64	47, 57, 59, 63	syl12anc 835	. . . . . . . . . 10 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) ∧ ((𝐹‘𝑧) ∈ 𝑡 ∧ 𝑤 ∈ (𝑆‘𝑡))) → ∃𝑦 ∈ 𝐽 ((𝐹‘𝑧) ∈ 𝑦 ∧ 𝑦 ⊆ (𝐹 “ 𝐴)))
65	64	expr 457	. . . . . . . . 9 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) ∧ (𝐹‘𝑧) ∈ 𝑡) → (𝑤 ∈ (𝑆‘𝑡) → ∃𝑦 ∈ 𝐽 ((𝐹‘𝑧) ∈ 𝑦 ∧ 𝑦 ⊆ (𝐹 “ 𝐴))))
66	65	exlimdv 1936	. . . . . . . 8 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) ∧ (𝐹‘𝑧) ∈ 𝑡) → (∃𝑤 𝑤 ∈ (𝑆‘𝑡) → ∃𝑦 ∈ 𝐽 ((𝐹‘𝑧) ∈ 𝑦 ∧ 𝑦 ⊆ (𝐹 “ 𝐴))))
67	17, 66	biimtrid 241	. . . . . . 7 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) ∧ (𝐹‘𝑧) ∈ 𝑡) → ((𝑆‘𝑡) ≠ ∅ → ∃𝑦 ∈ 𝐽 ((𝐹‘𝑧) ∈ 𝑦 ∧ 𝑦 ⊆ (𝐹 “ 𝐴))))
68	67	expimpd 454	. . . . . 6 ⊢ (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) → (((𝐹‘𝑧) ∈ 𝑡 ∧ (𝑆‘𝑡) ≠ ∅) → ∃𝑦 ∈ 𝐽 ((𝐹‘𝑧) ∈ 𝑦 ∧ 𝑦 ⊆ (𝐹 “ 𝐴))))
69	68	rexlimdvw 3160	. . . . 5 ⊢ (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) → (∃𝑡 ∈ 𝐽 ((𝐹‘𝑧) ∈ 𝑡 ∧ (𝑆‘𝑡) ≠ ∅) → ∃𝑦 ∈ 𝐽 ((𝐹‘𝑧) ∈ 𝑦 ∧ 𝑦 ⊆ (𝐹 “ 𝐴))))
70	16, 69	mpd 15	. . . 4 ⊢ (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) → ∃𝑦 ∈ 𝐽 ((𝐹‘𝑧) ∈ 𝑦 ∧ 𝑦 ⊆ (𝐹 “ 𝐴)))
71	70	ralrimiva 3146	. . 3 ⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) → ∀𝑧 ∈ 𝐴 ∃𝑦 ∈ 𝐽 ((𝐹‘𝑧) ∈ 𝑦 ∧ 𝑦 ⊆ (𝐹 “ 𝐴)))
72		eleq1 2821	. . . . . . 7 ⊢ (𝑥 = (𝐹‘𝑧) → (𝑥 ∈ 𝑦 ↔ (𝐹‘𝑧) ∈ 𝑦))
73	72	anbi1d 630	. . . . . 6 ⊢ (𝑥 = (𝐹‘𝑧) → ((𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ (𝐹 “ 𝐴)) ↔ ((𝐹‘𝑧) ∈ 𝑦 ∧ 𝑦 ⊆ (𝐹 “ 𝐴))))
74	73	rexbidv 3178	. . . . 5 ⊢ (𝑥 = (𝐹‘𝑧) → (∃𝑦 ∈ 𝐽 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ (𝐹 “ 𝐴)) ↔ ∃𝑦 ∈ 𝐽 ((𝐹‘𝑧) ∈ 𝑦 ∧ 𝑦 ⊆ (𝐹 “ 𝐴))))
75	74	ralima 7242	. . . 4 ⊢ ((𝐹 Fn 𝐵 ∧ 𝐴 ⊆ 𝐵) → (∀𝑥 ∈ (𝐹 “ 𝐴)∃𝑦 ∈ 𝐽 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ (𝐹 “ 𝐴)) ↔ ∀𝑧 ∈ 𝐴 ∃𝑦 ∈ 𝐽 ((𝐹‘𝑧) ∈ 𝑦 ∧ 𝑦 ⊆ (𝐹 “ 𝐴))))
76	48, 11, 75	syl2anc 584	. . 3 ⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) → (∀𝑥 ∈ (𝐹 “ 𝐴)∃𝑦 ∈ 𝐽 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ (𝐹 “ 𝐴)) ↔ ∀𝑧 ∈ 𝐴 ∃𝑦 ∈ 𝐽 ((𝐹‘𝑧) ∈ 𝑦 ∧ 𝑦 ⊆ (𝐹 “ 𝐴))))
77	71, 76	mpbird 256	. 2 ⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) → ∀𝑥 ∈ (𝐹 “ 𝐴)∃𝑦 ∈ 𝐽 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ (𝐹 “ 𝐴)))
78		eltop2 22485	. . 3 ⊢ (𝐽 ∈ Top → ((𝐹 “ 𝐴) ∈ 𝐽 ↔ ∀𝑥 ∈ (𝐹 “ 𝐴)∃𝑦 ∈ 𝐽 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ (𝐹 “ 𝐴))))
79	40, 78	syl 17	. 2 ⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) → ((𝐹 “ 𝐴) ∈ 𝐽 ↔ ∀𝑥 ∈ (𝐹 “ 𝐴)∃𝑦 ∈ 𝐽 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ (𝐹 “ 𝐴))))
80	77, 79	mpbird 256	1 ⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) → (𝐹 “ 𝐴) ∈ 𝐽)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 396 = wceq 1541 ∃wex 1781 ∈ wcel 2106 ≠ wne 2940 ∀wral 3061 ∃wrex 3070 {crab 3432 ∖ cdif 3945 ∩ cin 3947 ⊆ wss 3948 ∅c0 4322 𝒫 cpw 4602 {csn 4628 ∪ cuni 4908 ↦ cmpt 5231 ^◡ccnv 5675 ↾ cres 5678 “ cima 5679 Fn wfn 6538 ⟶wf 6539 ‘cfv 6543 ℩crio 7366 (class class class)co 7411 ↾_t crest 17368 Topctop 22402 Cn ccn 22735 Homeochmeo 23264 CovMap ccvm 34315

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2703 ax-rep 5285 ax-sep 5299 ax-nul 5306 ax-pow 5363 ax-pr 5427 ax-un 7727

This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3or 1088 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2534 df-eu 2563 df-clab 2710 df-cleq 2724 df-clel 2810 df-nfc 2885 df-ne 2941 df-ral 3062 df-rex 3071 df-rmo 3376 df-reu 3377 df-rab 3433 df-v 3476 df-sbc 3778 df-csb 3894 df-dif 3951 df-un 3953 df-in 3955 df-ss 3965 df-pss 3967 df-nul 4323 df-if 4529 df-pw 4604 df-sn 4629 df-pr 4631 df-op 4635 df-uni 4909 df-int 4951 df-iun 4999 df-br 5149 df-opab 5211 df-mpt 5232 df-tr 5266 df-id 5574 df-eprel 5580 df-po 5588 df-so 5589 df-fr 5631 df-we 5633 df-xp 5682 df-rel 5683 df-cnv 5684 df-co 5685 df-dm 5686 df-rn 5687 df-res 5688 df-ima 5689 df-ord 6367 df-on 6368 df-lim 6369 df-suc 6370 df-iota 6495 df-fun 6545 df-fn 6546 df-f 6547 df-f1 6548 df-fo 6549 df-f1o 6550 df-fv 6551 df-riota 7367 df-ov 7414 df-oprab 7415 df-mpo 7416 df-om 7858 df-1st 7977 df-2nd 7978 df-map 8824 df-en 8942 df-fin 8945 df-fi 9408 df-rest 17370 df-topgen 17391 df-top 22403 df-topon 22420 df-bases 22456 df-cn 22738 df-hmeo 23266 df-cvm 34316

This theorem is referenced by: cvmopn 34340

W3C validator