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 35865

Description: Lemma for cvmopn 35867. (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 779	. . . . . 6 ⊢ (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) → 𝐹 ∈ (𝐶 CovMap 𝐽))
2		cvmcn 35849	. . . . . . . . . 10 ⊢ (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐹 ∈ (𝐶 Cn 𝐽))
3	2	adantr 486	. . . . . . . . 9 ⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) → 𝐹 ∈ (𝐶 Cn 𝐽))
4		cvmseu.1	. . . . . . . . . 10 ⊢ 𝐵 = ∪ 𝐶
5		eqid 2762	. . . . . . . . . 10 ⊢ ∪ 𝐽 = ∪ 𝐽
6	4, 5	cnf 23477	. . . . . . . . 9 ⊢ (𝐹 ∈ (𝐶 Cn 𝐽) → 𝐹:𝐵⟶∪ 𝐽)
7	3, 6	syl 18	. . . . . . . 8 ⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) → 𝐹:𝐵⟶∪ 𝐽)
8	7	adantr 486	. . . . . . 7 ⊢ (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) → 𝐹:𝐵⟶∪ 𝐽)
9		elssuni 4902	. . . . . . . . . 10 ⊢ (𝐴 ∈ 𝐶 → 𝐴 ⊆ ∪ 𝐶)
10	9, 4	sseqtrrdi 3975	. . . . . . . . 9 ⊢ (𝐴 ∈ 𝐶 → 𝐴 ⊆ 𝐵)
11	10	adantl 487	. . . . . . . 8 ⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) → 𝐴 ⊆ 𝐵)
12	11	sselda 3934	. . . . . . 7 ⊢ (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) → 𝑧 ∈ 𝐵)
13	8, 12	ffvelcdmd 7082	. . . . . 6 ⊢ (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) → (𝐹‘𝑧) ∈ ∪ 𝐽)
14		cvmcov.1	. . . . . . 7 ⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (^◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾_t 𝑢)Homeo(𝐽 ↾_t 𝑘))))})
15	14, 5	cvmcov 35850	. . . . . 6 ⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ (𝐹‘𝑧) ∈ ∪ 𝐽) → ∃𝑡 ∈ 𝐽 ((𝐹‘𝑧) ∈ 𝑡 ∧ (𝑆‘𝑡) ≠ ∅))
16	1, 13, 15	syl2anc 596	. . . . 5 ⊢ (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) → ∃𝑡 ∈ 𝐽 ((𝐹‘𝑧) ∈ 𝑡 ∧ (𝑆‘𝑡) ≠ ∅))
17		n0 4303	. . . . . . . 8 ⊢ ((𝑆‘𝑡) ≠ ∅ ↔ ∃𝑤 𝑤 ∈ (𝑆‘𝑡))
18		inss2 4186	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥)) ⊆ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥)
19		resima2 6013	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥)) ⊆ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥) → ((𝐹 ↾ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥)) “ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))) = (𝐹 “ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))))
20	18, 19	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ ((𝐹 ↾ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥)) “ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))) = (𝐹 “ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥)))
21		simprr 785	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) ∧ ((𝐹‘𝑧) ∈ 𝑡 ∧ 𝑤 ∈ (𝑆‘𝑡))) → 𝑤 ∈ (𝑆‘𝑡))
22	1	adantr 486	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) ∧ ((𝐹‘𝑧) ∈ 𝑡 ∧ 𝑤 ∈ (𝑆‘𝑡))) → 𝐹 ∈ (𝐶 CovMap 𝐽))
23	12	adantr 486	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) ∧ ((𝐹‘𝑧) ∈ 𝑡 ∧ 𝑤 ∈ (𝑆‘𝑡))) → 𝑧 ∈ 𝐵)
24		simprl 783	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) ∧ ((𝐹‘𝑧) ∈ 𝑡 ∧ 𝑤 ∈ (𝑆‘𝑡))) → (𝐹‘𝑧) ∈ 𝑡)
25		eqid 2762	. . . . . . . . . . . . . . . . . . 19 ⊢ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥) = (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥)
26	14, 4, 25	cvmsiota 35864	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ (𝑤 ∈ (𝑆‘𝑡) ∧ 𝑧 ∈ 𝐵 ∧ (𝐹‘𝑧) ∈ 𝑡)) → ((℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥) ∈ 𝑤 ∧ 𝑧 ∈ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥)))
27	22, 21, 23, 24, 26	syl13anc 1399	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) ∧ ((𝐹‘𝑧) ∈ 𝑡 ∧ 𝑤 ∈ (𝑆‘𝑡))) → ((℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥) ∈ 𝑤 ∧ 𝑧 ∈ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥)))
28	27	simpld 500	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) ∧ ((𝐹‘𝑧) ∈ 𝑡 ∧ 𝑤 ∈ (𝑆‘𝑡))) → (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥) ∈ 𝑤)
29	14	cvmshmeo 35858	. . . . . . . . . . . . . . . 16 ⊢ ((𝑤 ∈ (𝑆‘𝑡) ∧ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥) ∈ 𝑤) → (𝐹 ↾ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥)) ∈ ((𝐶 ↾_t (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))Homeo(𝐽 ↾_t 𝑡)))
30	21, 28, 29	syl2anc 596	. . . . . . . . . . . . . . 15 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) ∧ ((𝐹‘𝑧) ∈ 𝑡 ∧ 𝑤 ∈ (𝑆‘𝑡))) → (𝐹 ↾ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥)) ∈ ((𝐶 ↾_t (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))Homeo(𝐽 ↾_t 𝑡)))
31		cvmtop1 35847	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐶 ∈ Top)
32	22, 31	syl 18	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) ∧ ((𝐹‘𝑧) ∈ 𝑡 ∧ 𝑤 ∈ (𝑆‘𝑡))) → 𝐶 ∈ Top)
33		simpllr 788	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) ∧ ((𝐹‘𝑧) ∈ 𝑡 ∧ 𝑤 ∈ (𝑆‘𝑡))) → 𝐴 ∈ 𝐶)
34		elrestr 17519	. . . . . . . . . . . . . . . 16 ⊢ ((𝐶 ∈ Top ∧ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥) ∈ 𝑤 ∧ 𝐴 ∈ 𝐶) → (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥)) ∈ (𝐶 ↾_t (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥)))
35	32, 28, 33, 34	syl3anc 1398	. . . . . . . . . . . . . . 15 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) ∧ ((𝐹‘𝑧) ∈ 𝑡 ∧ 𝑤 ∈ (𝑆‘𝑡))) → (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥)) ∈ (𝐶 ↾_t (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥)))
36		hmeoima 23997	. . . . . . . . . . . . . . 15 ⊢ (((𝐹 ↾ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥)) ∈ ((𝐶 ↾_t (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))Homeo(𝐽 ↾_t 𝑡)) ∧ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥)) ∈ (𝐶 ↾_t (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))) → ((𝐹 ↾ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥)) “ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))) ∈ (𝐽 ↾_t 𝑡))
37	30, 35, 36	syl2anc 596	. . . . . . . . . . . . . 14 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) ∧ ((𝐹‘𝑧) ∈ 𝑡 ∧ 𝑤 ∈ (𝑆‘𝑡))) → ((𝐹 ↾ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥)) “ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))) ∈ (𝐽 ↾_t 𝑡))
38	20, 37	eqeltrrid 2867	. . . . . . . . . . . . 13 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) ∧ ((𝐹‘𝑧) ∈ 𝑡 ∧ 𝑤 ∈ (𝑆‘𝑡))) → (𝐹 “ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))) ∈ (𝐽 ↾_t 𝑡))
39		cvmtop2 35848	. . . . . . . . . . . . . . . 16 ⊢ (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐽 ∈ Top)
40	39	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) → 𝐽 ∈ Top)
41	40	ad2antrr 739	. . . . . . . . . . . . . 14 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) ∧ ((𝐹‘𝑧) ∈ 𝑡 ∧ 𝑤 ∈ (𝑆‘𝑡))) → 𝐽 ∈ Top)
42	14	cvmsrcl 35851	. . . . . . . . . . . . . . 15 ⊢ (𝑤 ∈ (𝑆‘𝑡) → 𝑡 ∈ 𝐽)
43	42	ad2antll 742	. . . . . . . . . . . . . 14 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) ∧ ((𝐹‘𝑧) ∈ 𝑡 ∧ 𝑤 ∈ (𝑆‘𝑡))) → 𝑡 ∈ 𝐽)
44		restopn2 23408	. . . . . . . . . . . . . 14 ⊢ ((𝐽 ∈ Top ∧ 𝑡 ∈ 𝐽) → ((𝐹 “ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))) ∈ (𝐽 ↾_t 𝑡) ↔ ((𝐹 “ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))) ∈ 𝐽 ∧ (𝐹 “ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))) ⊆ 𝑡)))
45	41, 43, 44	syl2anc 596	. . . . . . . . . . . . 13 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) ∧ ((𝐹‘𝑧) ∈ 𝑡 ∧ 𝑤 ∈ (𝑆‘𝑡))) → ((𝐹 “ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))) ∈ (𝐽 ↾_t 𝑡) ↔ ((𝐹 “ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))) ∈ 𝐽 ∧ (𝐹 “ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))) ⊆ 𝑡)))
46	38, 45	mpbid 235	. . . . . . . . . . . 12 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) ∧ ((𝐹‘𝑧) ∈ 𝑡 ∧ 𝑤 ∈ (𝑆‘𝑡))) → ((𝐹 “ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))) ∈ 𝐽 ∧ (𝐹 “ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))) ⊆ 𝑡))
47	46	simpld 500	. . . . . . . . . . 11 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) ∧ ((𝐹‘𝑧) ∈ 𝑡 ∧ 𝑤 ∈ (𝑆‘𝑡))) → (𝐹 “ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))) ∈ 𝐽)
48	7	ffnd 6707	. . . . . . . . . . . . 13 ⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) → 𝐹 Fn 𝐵)
49	48	ad2antrr 739	. . . . . . . . . . . 12 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) ∧ ((𝐹‘𝑧) ∈ 𝑡 ∧ 𝑤 ∈ (𝑆‘𝑡))) → 𝐹 Fn 𝐵)
50		inss1 4185	. . . . . . . . . . . . 13 ⊢ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥)) ⊆ 𝐴
51	33, 10	syl 18	. . . . . . . . . . . . 13 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) ∧ ((𝐹‘𝑧) ∈ 𝑡 ∧ 𝑤 ∈ (𝑆‘𝑡))) → 𝐴 ⊆ 𝐵)
52	50, 51	sstrid 3945	. . . . . . . . . . . 12 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) ∧ ((𝐹‘𝑧) ∈ 𝑡 ∧ 𝑤 ∈ (𝑆‘𝑡))) → (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥)) ⊆ 𝐵)
53		simplr 781	. . . . . . . . . . . . 13 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) ∧ ((𝐹‘𝑧) ∈ 𝑡 ∧ 𝑤 ∈ (𝑆‘𝑡))) → 𝑧 ∈ 𝐴)
54	27	simprd 501	. . . . . . . . . . . . 13 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) ∧ ((𝐹‘𝑧) ∈ 𝑡 ∧ 𝑤 ∈ (𝑆‘𝑡))) → 𝑧 ∈ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))
55	53, 54	elind 4149	. . . . . . . . . . . 12 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) ∧ ((𝐹‘𝑧) ∈ 𝑡 ∧ 𝑤 ∈ (𝑆‘𝑡))) → 𝑧 ∈ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥)))
56		fnfvima 7236	. . . . . . . . . . . 12 ⊢ ((𝐹 Fn 𝐵 ∧ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥)) ⊆ 𝐵 ∧ 𝑧 ∈ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))) → (𝐹‘𝑧) ∈ (𝐹 “ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))))
57	49, 52, 55, 56	syl3anc 1398	. . . . . . . . . . 11 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) ∧ ((𝐹‘𝑧) ∈ 𝑡 ∧ 𝑤 ∈ (𝑆‘𝑡))) → (𝐹‘𝑧) ∈ (𝐹 “ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))))
58		imass2 6102	. . . . . . . . . . . 12 ⊢ ((𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥)) ⊆ 𝐴 → (𝐹 “ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))) ⊆ (𝐹 “ 𝐴))
59	50, 58	mp1i 14	. . . . . . . . . . 11 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) ∧ ((𝐹‘𝑧) ∈ 𝑡 ∧ 𝑤 ∈ (𝑆‘𝑡))) → (𝐹 “ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))) ⊆ (𝐹 “ 𝐴))
60		eleq2 2851	. . . . . . . . . . . . 13 ⊢ (𝑦 = (𝐹 “ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))) → ((𝐹‘𝑧) ∈ 𝑦 ↔ (𝐹‘𝑧) ∈ (𝐹 “ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥)))))
61		sseq1 3959	. . . . . . . . . . . . 13 ⊢ (𝑦 = (𝐹 “ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))) → (𝑦 ⊆ (𝐹 “ 𝐴) ↔ (𝐹 “ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))) ⊆ (𝐹 “ 𝐴)))
62	60, 61	anbi12d 644	. . . . . . . . . . . 12 ⊢ (𝑦 = (𝐹 “ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))) → (((𝐹‘𝑧) ∈ 𝑦 ∧ 𝑦 ⊆ (𝐹 “ 𝐴)) ↔ ((𝐹‘𝑧) ∈ (𝐹 “ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))) ∧ (𝐹 “ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))) ⊆ (𝐹 “ 𝐴))))
63	62	rspcev 3579	. . . . . . . . . . 11 ⊢ (((𝐹 “ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))) ∈ 𝐽 ∧ ((𝐹‘𝑧) ∈ (𝐹 “ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))) ∧ (𝐹 “ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))) ⊆ (𝐹 “ 𝐴))) → ∃𝑦 ∈ 𝐽 ((𝐹‘𝑧) ∈ 𝑦 ∧ 𝑦 ⊆ (𝐹 “ 𝐴)))
64	47, 57, 59, 63	syl12anc 850	. . . . . . . . . 10 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) ∧ ((𝐹‘𝑧) ∈ 𝑡 ∧ 𝑤 ∈ (𝑆‘𝑡))) → ∃𝑦 ∈ 𝐽 ((𝐹‘𝑧) ∈ 𝑦 ∧ 𝑦 ⊆ (𝐹 “ 𝐴)))
65	64	expr 462	. . . . . . . . 9 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) ∧ (𝐹‘𝑧) ∈ 𝑡) → (𝑤 ∈ (𝑆‘𝑡) → ∃𝑦 ∈ 𝐽 ((𝐹‘𝑧) ∈ 𝑦 ∧ 𝑦 ⊆ (𝐹 “ 𝐴))))
66	65	exlimdv 1966	. . . . . . . 8 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) ∧ (𝐹‘𝑧) ∈ 𝑡) → (∃𝑤 𝑤 ∈ (𝑆‘𝑡) → ∃𝑦 ∈ 𝐽 ((𝐹‘𝑧) ∈ 𝑦 ∧ 𝑦 ⊆ (𝐹 “ 𝐴))))
67	17, 66	biimtrid 245	. . . . . . 7 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) ∧ (𝐹‘𝑧) ∈ 𝑡) → ((𝑆‘𝑡) ≠ ∅ → ∃𝑦 ∈ 𝐽 ((𝐹‘𝑧) ∈ 𝑦 ∧ 𝑦 ⊆ (𝐹 “ 𝐴))))
68	67	expimpd 459	. . . . . 6 ⊢ (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) → (((𝐹‘𝑧) ∈ 𝑡 ∧ (𝑆‘𝑡) ≠ ∅) → ∃𝑦 ∈ 𝐽 ((𝐹‘𝑧) ∈ 𝑦 ∧ 𝑦 ⊆ (𝐹 “ 𝐴))))
69	68	rexlimdvw 3170	. . . . 5 ⊢ (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) → (∃𝑡 ∈ 𝐽 ((𝐹‘𝑧) ∈ 𝑡 ∧ (𝑆‘𝑡) ≠ ∅) → ∃𝑦 ∈ 𝐽 ((𝐹‘𝑧) ∈ 𝑦 ∧ 𝑦 ⊆ (𝐹 “ 𝐴))))
70	16, 69	mpd 16	. . . 4 ⊢ (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) → ∃𝑦 ∈ 𝐽 ((𝐹‘𝑧) ∈ 𝑦 ∧ 𝑦 ⊆ (𝐹 “ 𝐴)))
71	70	ralrimiva 3156	. . 3 ⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) → ∀𝑧 ∈ 𝐴 ∃𝑦 ∈ 𝐽 ((𝐹‘𝑧) ∈ 𝑦 ∧ 𝑦 ⊆ (𝐹 “ 𝐴)))
72		eleq1 2850	. . . . . . 7 ⊢ (𝑥 = (𝐹‘𝑧) → (𝑥 ∈ 𝑦 ↔ (𝐹‘𝑧) ∈ 𝑦))
73	72	anbi1d 643	. . . . . 6 ⊢ (𝑥 = (𝐹‘𝑧) → ((𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ (𝐹 “ 𝐴)) ↔ ((𝐹‘𝑧) ∈ 𝑦 ∧ 𝑦 ⊆ (𝐹 “ 𝐴))))
74	73	rexbidv 3188	. . . . 5 ⊢ (𝑥 = (𝐹‘𝑧) → (∃𝑦 ∈ 𝐽 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ (𝐹 “ 𝐴)) ↔ ∃𝑦 ∈ 𝐽 ((𝐹‘𝑧) ∈ 𝑦 ∧ 𝑦 ⊆ (𝐹 “ 𝐴))))
75	74	ralima 7240	. . . 4 ⊢ ((𝐹 Fn 𝐵 ∧ 𝐴 ⊆ 𝐵) → (∀𝑥 ∈ (𝐹 “ 𝐴)∃𝑦 ∈ 𝐽 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ (𝐹 “ 𝐴)) ↔ ∀𝑧 ∈ 𝐴 ∃𝑦 ∈ 𝐽 ((𝐹‘𝑧) ∈ 𝑦 ∧ 𝑦 ⊆ (𝐹 “ 𝐴))))
76	48, 11, 75	syl2anc 596	. . 3 ⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) → (∀𝑥 ∈ (𝐹 “ 𝐴)∃𝑦 ∈ 𝐽 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ (𝐹 “ 𝐴)) ↔ ∀𝑧 ∈ 𝐴 ∃𝑦 ∈ 𝐽 ((𝐹‘𝑧) ∈ 𝑦 ∧ 𝑦 ⊆ (𝐹 “ 𝐴))))
77	71, 76	mpbird 260	. 2 ⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) → ∀𝑥 ∈ (𝐹 “ 𝐴)∃𝑦 ∈ 𝐽 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ (𝐹 “ 𝐴)))
78		eltop2 23206	. . 3 ⊢ (𝐽 ∈ Top → ((𝐹 “ 𝐴) ∈ 𝐽 ↔ ∀𝑥 ∈ (𝐹 “ 𝐴)∃𝑦 ∈ 𝐽 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ (𝐹 “ 𝐴))))
79	40, 78	syl 18	. 2 ⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) → ((𝐹 “ 𝐴) ∈ 𝐽 ↔ ∀𝑥 ∈ (𝐹 “ 𝐴)∃𝑦 ∈ 𝐽 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ (𝐹 “ 𝐴))))
80	77, 79	mpbird 260	1 ⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) → (𝐹 “ 𝐴) ∈ 𝐽)

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 = wceq 1570 ∃wex 1812 ∈ wcel 2145 ≠ wne 2957 ∀wral 3078 ∃wrex 3088 {crab 3414 ∖ cdif 3899 ∩ cin 3901 ⊆ wss 3902 ∅c0 4282 𝒫 cpw 4560 {csn 4587 ∪ cuni 4870 ↦ cmpt 5190 ^◡ccnv 5658 ↾ cres 5661 “ cima 5662 Fn wfn 6532 ⟶wf 6533 ‘cfv 6537 ℩crio 7373 (class class class)co 7417 ↾_t crest 17511 Topctop 23124 Cn ccn 23455 Homeochmeo 23985 CovMap ccvm 35842

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2215 ax-ext 2734 ax-rep 5236 ax-sep 5255 ax-nul 5267 ax-pow 5334 ax-pr 5402 ax-un 7740

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2566 df-eu 2596 df-clab 2741 df-cleq 2754 df-clel 2837 df-nfc 2911 df-ne 2958 df-ral 3079 df-rex 3089 df-rmo 3367 df-reu 3368 df-rab 3415 df-v 3455 df-sbc 3743 df-csb 3851 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-pss 3922 df-nul 4283 df-if 4486 df-pw 4562 df-sn 4588 df-pr 4590 df-op 4594 df-uni 4871 df-int 4911 df-iun 4956 df-br 5108 df-opab 5172 df-mpt 5191 df-tr 5217 df-id 5554 df-eprel 5559 df-po 5567 df-so 5568 df-fr 5612 df-we 5614 df-xp 5665 df-rel 5666 df-cnv 5667 df-co 5668 df-dm 5669 df-rn 5670 df-res 5671 df-ima 5672 df-ord 6364 df-on 6365 df-lim 6366 df-suc 6367 df-iota 6493 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544 df-fv 6545 df-riota 7374 df-ov 7420 df-oprab 7421 df-mpo 7422 df-om 7867 df-1st 7990 df-2nd 7991 df-map 8832 df-en 8957 df-fin 8960 df-fi 9385 df-rest 17513 df-topgen 17534 df-top 23125 df-topon 23142 df-bases 23177 df-cn 23458 df-hmeo 23987 df-cvm 35843

This theorem is used by: cvmopn 35867

W3C validator