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 35250

Description: Lemma for cvmopn 35252. (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 766	. . . . . 6 ⊢ (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) → 𝐹 ∈ (𝐶 CovMap 𝐽))
2		cvmcn 35234	. . . . . . . . . 10 ⊢ (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐹 ∈ (𝐶 Cn 𝐽))
3	2	adantr 480	. . . . . . . . 9 ⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) → 𝐹 ∈ (𝐶 Cn 𝐽))
4		cvmseu.1	. . . . . . . . . 10 ⊢ 𝐵 = ∪ 𝐶
5		eqid 2729	. . . . . . . . . 10 ⊢ ∪ 𝐽 = ∪ 𝐽
6	4, 5	cnf 23149	. . . . . . . . 9 ⊢ (𝐹 ∈ (𝐶 Cn 𝐽) → 𝐹:𝐵⟶∪ 𝐽)
7	3, 6	syl 17	. . . . . . . 8 ⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) → 𝐹:𝐵⟶∪ 𝐽)
8	7	adantr 480	. . . . . . 7 ⊢ (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) → 𝐹:𝐵⟶∪ 𝐽)
9		elssuni 4891	. . . . . . . . . 10 ⊢ (𝐴 ∈ 𝐶 → 𝐴 ⊆ ∪ 𝐶)
10	9, 4	sseqtrrdi 3979	. . . . . . . . 9 ⊢ (𝐴 ∈ 𝐶 → 𝐴 ⊆ 𝐵)
11	10	adantl 481	. . . . . . . 8 ⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) → 𝐴 ⊆ 𝐵)
12	11	sselda 3937	. . . . . . 7 ⊢ (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) → 𝑧 ∈ 𝐵)
13	8, 12	ffvelcdmd 7023	. . . . . 6 ⊢ (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) → (𝐹‘𝑧) ∈ ∪ 𝐽)
14		cvmcov.1	. . . . . . 7 ⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (^◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾_t 𝑢)Homeo(𝐽 ↾_t 𝑘))))})
15	14, 5	cvmcov 35235	. . . . . 6 ⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ (𝐹‘𝑧) ∈ ∪ 𝐽) → ∃𝑡 ∈ 𝐽 ((𝐹‘𝑧) ∈ 𝑡 ∧ (𝑆‘𝑡) ≠ ∅))
16	1, 13, 15	syl2anc 584	. . . . 5 ⊢ (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) → ∃𝑡 ∈ 𝐽 ((𝐹‘𝑧) ∈ 𝑡 ∧ (𝑆‘𝑡) ≠ ∅))
17		n0 4306	. . . . . . . 8 ⊢ ((𝑆‘𝑡) ≠ ∅ ↔ ∃𝑤 𝑤 ∈ (𝑆‘𝑡))
18		inss2 4191	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥)) ⊆ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥)
19		resima2 5971	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥)) ⊆ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥) → ((𝐹 ↾ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥)) “ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))) = (𝐹 “ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))))
20	18, 19	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ ((𝐹 ↾ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥)) “ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))) = (𝐹 “ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥)))
21		simprr 772	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) ∧ ((𝐹‘𝑧) ∈ 𝑡 ∧ 𝑤 ∈ (𝑆‘𝑡))) → 𝑤 ∈ (𝑆‘𝑡))
22	1	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) ∧ ((𝐹‘𝑧) ∈ 𝑡 ∧ 𝑤 ∈ (𝑆‘𝑡))) → 𝐹 ∈ (𝐶 CovMap 𝐽))
23	12	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) ∧ ((𝐹‘𝑧) ∈ 𝑡 ∧ 𝑤 ∈ (𝑆‘𝑡))) → 𝑧 ∈ 𝐵)
24		simprl 770	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) ∧ ((𝐹‘𝑧) ∈ 𝑡 ∧ 𝑤 ∈ (𝑆‘𝑡))) → (𝐹‘𝑧) ∈ 𝑡)
25		eqid 2729	. . . . . . . . . . . . . . . . . . 19 ⊢ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥) = (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥)
26	14, 4, 25	cvmsiota 35249	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ (𝑤 ∈ (𝑆‘𝑡) ∧ 𝑧 ∈ 𝐵 ∧ (𝐹‘𝑧) ∈ 𝑡)) → ((℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥) ∈ 𝑤 ∧ 𝑧 ∈ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥)))
27	22, 21, 23, 24, 26	syl13anc 1374	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) ∧ ((𝐹‘𝑧) ∈ 𝑡 ∧ 𝑤 ∈ (𝑆‘𝑡))) → ((℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥) ∈ 𝑤 ∧ 𝑧 ∈ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥)))
28	27	simpld 494	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) ∧ ((𝐹‘𝑧) ∈ 𝑡 ∧ 𝑤 ∈ (𝑆‘𝑡))) → (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥) ∈ 𝑤)
29	14	cvmshmeo 35243	. . . . . . . . . . . . . . . 16 ⊢ ((𝑤 ∈ (𝑆‘𝑡) ∧ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥) ∈ 𝑤) → (𝐹 ↾ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥)) ∈ ((𝐶 ↾_t (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))Homeo(𝐽 ↾_t 𝑡)))
30	21, 28, 29	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) ∧ ((𝐹‘𝑧) ∈ 𝑡 ∧ 𝑤 ∈ (𝑆‘𝑡))) → (𝐹 ↾ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥)) ∈ ((𝐶 ↾_t (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))Homeo(𝐽 ↾_t 𝑡)))
31		cvmtop1 35232	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐶 ∈ Top)
32	22, 31	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) ∧ ((𝐹‘𝑧) ∈ 𝑡 ∧ 𝑤 ∈ (𝑆‘𝑡))) → 𝐶 ∈ Top)
33		simpllr 775	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) ∧ ((𝐹‘𝑧) ∈ 𝑡 ∧ 𝑤 ∈ (𝑆‘𝑡))) → 𝐴 ∈ 𝐶)
34		elrestr 17350	. . . . . . . . . . . . . . . 16 ⊢ ((𝐶 ∈ Top ∧ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥) ∈ 𝑤 ∧ 𝐴 ∈ 𝐶) → (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥)) ∈ (𝐶 ↾_t (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥)))
35	32, 28, 33, 34	syl3anc 1373	. . . . . . . . . . . . . . 15 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) ∧ ((𝐹‘𝑧) ∈ 𝑡 ∧ 𝑤 ∈ (𝑆‘𝑡))) → (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥)) ∈ (𝐶 ↾_t (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥)))
36		hmeoima 23668	. . . . . . . . . . . . . . 15 ⊢ (((𝐹 ↾ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥)) ∈ ((𝐶 ↾_t (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))Homeo(𝐽 ↾_t 𝑡)) ∧ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥)) ∈ (𝐶 ↾_t (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))) → ((𝐹 ↾ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥)) “ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))) ∈ (𝐽 ↾_t 𝑡))
37	30, 35, 36	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) ∧ ((𝐹‘𝑧) ∈ 𝑡 ∧ 𝑤 ∈ (𝑆‘𝑡))) → ((𝐹 ↾ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥)) “ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))) ∈ (𝐽 ↾_t 𝑡))
38	20, 37	eqeltrrid 2833	. . . . . . . . . . . . 13 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) ∧ ((𝐹‘𝑧) ∈ 𝑡 ∧ 𝑤 ∈ (𝑆‘𝑡))) → (𝐹 “ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))) ∈ (𝐽 ↾_t 𝑡))
39		cvmtop2 35233	. . . . . . . . . . . . . . . 16 ⊢ (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐽 ∈ Top)
40	39	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) → 𝐽 ∈ Top)
41	40	ad2antrr 726	. . . . . . . . . . . . . 14 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) ∧ ((𝐹‘𝑧) ∈ 𝑡 ∧ 𝑤 ∈ (𝑆‘𝑡))) → 𝐽 ∈ Top)
42	14	cvmsrcl 35236	. . . . . . . . . . . . . . 15 ⊢ (𝑤 ∈ (𝑆‘𝑡) → 𝑡 ∈ 𝐽)
43	42	ad2antll 729	. . . . . . . . . . . . . 14 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) ∧ ((𝐹‘𝑧) ∈ 𝑡 ∧ 𝑤 ∈ (𝑆‘𝑡))) → 𝑡 ∈ 𝐽)
44		restopn2 23080	. . . . . . . . . . . . . 14 ⊢ ((𝐽 ∈ Top ∧ 𝑡 ∈ 𝐽) → ((𝐹 “ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))) ∈ (𝐽 ↾_t 𝑡) ↔ ((𝐹 “ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))) ∈ 𝐽 ∧ (𝐹 “ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))) ⊆ 𝑡)))
45	41, 43, 44	syl2anc 584	. . . . . . . . . . . . 13 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) ∧ ((𝐹‘𝑧) ∈ 𝑡 ∧ 𝑤 ∈ (𝑆‘𝑡))) → ((𝐹 “ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))) ∈ (𝐽 ↾_t 𝑡) ↔ ((𝐹 “ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))) ∈ 𝐽 ∧ (𝐹 “ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))) ⊆ 𝑡)))
46	38, 45	mpbid 232	. . . . . . . . . . . 12 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) ∧ ((𝐹‘𝑧) ∈ 𝑡 ∧ 𝑤 ∈ (𝑆‘𝑡))) → ((𝐹 “ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))) ∈ 𝐽 ∧ (𝐹 “ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))) ⊆ 𝑡))
47	46	simpld 494	. . . . . . . . . . 11 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) ∧ ((𝐹‘𝑧) ∈ 𝑡 ∧ 𝑤 ∈ (𝑆‘𝑡))) → (𝐹 “ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))) ∈ 𝐽)
48	7	ffnd 6657	. . . . . . . . . . . . 13 ⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) → 𝐹 Fn 𝐵)
49	48	ad2antrr 726	. . . . . . . . . . . 12 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) ∧ ((𝐹‘𝑧) ∈ 𝑡 ∧ 𝑤 ∈ (𝑆‘𝑡))) → 𝐹 Fn 𝐵)
50		inss1 4190	. . . . . . . . . . . . 13 ⊢ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥)) ⊆ 𝐴
51	33, 10	syl 17	. . . . . . . . . . . . 13 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) ∧ ((𝐹‘𝑧) ∈ 𝑡 ∧ 𝑤 ∈ (𝑆‘𝑡))) → 𝐴 ⊆ 𝐵)
52	50, 51	sstrid 3949	. . . . . . . . . . . 12 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) ∧ ((𝐹‘𝑧) ∈ 𝑡 ∧ 𝑤 ∈ (𝑆‘𝑡))) → (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥)) ⊆ 𝐵)
53		simplr 768	. . . . . . . . . . . . 13 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) ∧ ((𝐹‘𝑧) ∈ 𝑡 ∧ 𝑤 ∈ (𝑆‘𝑡))) → 𝑧 ∈ 𝐴)
54	27	simprd 495	. . . . . . . . . . . . 13 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) ∧ ((𝐹‘𝑧) ∈ 𝑡 ∧ 𝑤 ∈ (𝑆‘𝑡))) → 𝑧 ∈ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))
55	53, 54	elind 4153	. . . . . . . . . . . 12 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) ∧ ((𝐹‘𝑧) ∈ 𝑡 ∧ 𝑤 ∈ (𝑆‘𝑡))) → 𝑧 ∈ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥)))
56		fnfvima 7173	. . . . . . . . . . . 12 ⊢ ((𝐹 Fn 𝐵 ∧ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥)) ⊆ 𝐵 ∧ 𝑧 ∈ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))) → (𝐹‘𝑧) ∈ (𝐹 “ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))))
57	49, 52, 55, 56	syl3anc 1373	. . . . . . . . . . 11 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) ∧ ((𝐹‘𝑧) ∈ 𝑡 ∧ 𝑤 ∈ (𝑆‘𝑡))) → (𝐹‘𝑧) ∈ (𝐹 “ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))))
58		imass2 6057	. . . . . . . . . . . 12 ⊢ ((𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥)) ⊆ 𝐴 → (𝐹 “ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))) ⊆ (𝐹 “ 𝐴))
59	50, 58	mp1i 13	. . . . . . . . . . 11 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) ∧ ((𝐹‘𝑧) ∈ 𝑡 ∧ 𝑤 ∈ (𝑆‘𝑡))) → (𝐹 “ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))) ⊆ (𝐹 “ 𝐴))
60		eleq2 2817	. . . . . . . . . . . . 13 ⊢ (𝑦 = (𝐹 “ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))) → ((𝐹‘𝑧) ∈ 𝑦 ↔ (𝐹‘𝑧) ∈ (𝐹 “ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥)))))
61		sseq1 3963	. . . . . . . . . . . . 13 ⊢ (𝑦 = (𝐹 “ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))) → (𝑦 ⊆ (𝐹 “ 𝐴) ↔ (𝐹 “ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))) ⊆ (𝐹 “ 𝐴)))
62	60, 61	anbi12d 632	. . . . . . . . . . . 12 ⊢ (𝑦 = (𝐹 “ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))) → (((𝐹‘𝑧) ∈ 𝑦 ∧ 𝑦 ⊆ (𝐹 “ 𝐴)) ↔ ((𝐹‘𝑧) ∈ (𝐹 “ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))) ∧ (𝐹 “ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))) ⊆ (𝐹 “ 𝐴))))
63	62	rspcev 3579	. . . . . . . . . . 11 ⊢ (((𝐹 “ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))) ∈ 𝐽 ∧ ((𝐹‘𝑧) ∈ (𝐹 “ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))) ∧ (𝐹 “ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))) ⊆ (𝐹 “ 𝐴))) → ∃𝑦 ∈ 𝐽 ((𝐹‘𝑧) ∈ 𝑦 ∧ 𝑦 ⊆ (𝐹 “ 𝐴)))
64	47, 57, 59, 63	syl12anc 836	. . . . . . . . . 10 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) ∧ ((𝐹‘𝑧) ∈ 𝑡 ∧ 𝑤 ∈ (𝑆‘𝑡))) → ∃𝑦 ∈ 𝐽 ((𝐹‘𝑧) ∈ 𝑦 ∧ 𝑦 ⊆ (𝐹 “ 𝐴)))
65	64	expr 456	. . . . . . . . 9 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) ∧ (𝐹‘𝑧) ∈ 𝑡) → (𝑤 ∈ (𝑆‘𝑡) → ∃𝑦 ∈ 𝐽 ((𝐹‘𝑧) ∈ 𝑦 ∧ 𝑦 ⊆ (𝐹 “ 𝐴))))
66	65	exlimdv 1933	. . . . . . . 8 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) ∧ (𝐹‘𝑧) ∈ 𝑡) → (∃𝑤 𝑤 ∈ (𝑆‘𝑡) → ∃𝑦 ∈ 𝐽 ((𝐹‘𝑧) ∈ 𝑦 ∧ 𝑦 ⊆ (𝐹 “ 𝐴))))
67	17, 66	biimtrid 242	. . . . . . 7 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) ∧ (𝐹‘𝑧) ∈ 𝑡) → ((𝑆‘𝑡) ≠ ∅ → ∃𝑦 ∈ 𝐽 ((𝐹‘𝑧) ∈ 𝑦 ∧ 𝑦 ⊆ (𝐹 “ 𝐴))))
68	67	expimpd 453	. . . . . 6 ⊢ (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) → (((𝐹‘𝑧) ∈ 𝑡 ∧ (𝑆‘𝑡) ≠ ∅) → ∃𝑦 ∈ 𝐽 ((𝐹‘𝑧) ∈ 𝑦 ∧ 𝑦 ⊆ (𝐹 “ 𝐴))))
69	68	rexlimdvw 3135	. . . . 5 ⊢ (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) → (∃𝑡 ∈ 𝐽 ((𝐹‘𝑧) ∈ 𝑡 ∧ (𝑆‘𝑡) ≠ ∅) → ∃𝑦 ∈ 𝐽 ((𝐹‘𝑧) ∈ 𝑦 ∧ 𝑦 ⊆ (𝐹 “ 𝐴))))
70	16, 69	mpd 15	. . . 4 ⊢ (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) → ∃𝑦 ∈ 𝐽 ((𝐹‘𝑧) ∈ 𝑦 ∧ 𝑦 ⊆ (𝐹 “ 𝐴)))
71	70	ralrimiva 3121	. . 3 ⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) → ∀𝑧 ∈ 𝐴 ∃𝑦 ∈ 𝐽 ((𝐹‘𝑧) ∈ 𝑦 ∧ 𝑦 ⊆ (𝐹 “ 𝐴)))
72		eleq1 2816	. . . . . . 7 ⊢ (𝑥 = (𝐹‘𝑧) → (𝑥 ∈ 𝑦 ↔ (𝐹‘𝑧) ∈ 𝑦))
73	72	anbi1d 631	. . . . . 6 ⊢ (𝑥 = (𝐹‘𝑧) → ((𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ (𝐹 “ 𝐴)) ↔ ((𝐹‘𝑧) ∈ 𝑦 ∧ 𝑦 ⊆ (𝐹 “ 𝐴))))
74	73	rexbidv 3153	. . . . 5 ⊢ (𝑥 = (𝐹‘𝑧) → (∃𝑦 ∈ 𝐽 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ (𝐹 “ 𝐴)) ↔ ∃𝑦 ∈ 𝐽 ((𝐹‘𝑧) ∈ 𝑦 ∧ 𝑦 ⊆ (𝐹 “ 𝐴))))
75	74	ralima 7177	. . . 4 ⊢ ((𝐹 Fn 𝐵 ∧ 𝐴 ⊆ 𝐵) → (∀𝑥 ∈ (𝐹 “ 𝐴)∃𝑦 ∈ 𝐽 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ (𝐹 “ 𝐴)) ↔ ∀𝑧 ∈ 𝐴 ∃𝑦 ∈ 𝐽 ((𝐹‘𝑧) ∈ 𝑦 ∧ 𝑦 ⊆ (𝐹 “ 𝐴))))
76	48, 11, 75	syl2anc 584	. . 3 ⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) → (∀𝑥 ∈ (𝐹 “ 𝐴)∃𝑦 ∈ 𝐽 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ (𝐹 “ 𝐴)) ↔ ∀𝑧 ∈ 𝐴 ∃𝑦 ∈ 𝐽 ((𝐹‘𝑧) ∈ 𝑦 ∧ 𝑦 ⊆ (𝐹 “ 𝐴))))
77	71, 76	mpbird 257	. 2 ⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) → ∀𝑥 ∈ (𝐹 “ 𝐴)∃𝑦 ∈ 𝐽 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ (𝐹 “ 𝐴)))
78		eltop2 22878	. . 3 ⊢ (𝐽 ∈ Top → ((𝐹 “ 𝐴) ∈ 𝐽 ↔ ∀𝑥 ∈ (𝐹 “ 𝐴)∃𝑦 ∈ 𝐽 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ (𝐹 “ 𝐴))))
79	40, 78	syl 17	. 2 ⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) → ((𝐹 “ 𝐴) ∈ 𝐽 ↔ ∀𝑥 ∈ (𝐹 “ 𝐴)∃𝑦 ∈ 𝐽 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ (𝐹 “ 𝐴))))
80	77, 79	mpbird 257	1 ⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) → (𝐹 “ 𝐴) ∈ 𝐽)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1540 ∃wex 1779 ∈ wcel 2109 ≠ wne 2925 ∀wral 3044 ∃wrex 3053 {crab 3396 ∖ cdif 3902 ∩ cin 3904 ⊆ wss 3905 ∅c0 4286 𝒫 cpw 4553 {csn 4579 ∪ cuni 4861 ↦ cmpt 5176 ^◡ccnv 5622 ↾ cres 5625 “ cima 5626 Fn wfn 6481 ⟶wf 6482 ‘cfv 6486 ℩crio 7309 (class class class)co 7353 ↾_t crest 17342 Topctop 22796 Cn ccn 23127 Homeochmeo 23656 CovMap ccvm 35227

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-rep 5221 ax-sep 5238 ax-nul 5248 ax-pow 5307 ax-pr 5374 ax-un 7675

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-ral 3045 df-rex 3054 df-rmo 3345 df-reu 3346 df-rab 3397 df-v 3440 df-sbc 3745 df-csb 3854 df-dif 3908 df-un 3910 df-in 3912 df-ss 3922 df-pss 3925 df-nul 4287 df-if 4479 df-pw 4555 df-sn 4580 df-pr 4582 df-op 4586 df-uni 4862 df-int 4900 df-iun 4946 df-br 5096 df-opab 5158 df-mpt 5177 df-tr 5203 df-id 5518 df-eprel 5523 df-po 5531 df-so 5532 df-fr 5576 df-we 5578 df-xp 5629 df-rel 5630 df-cnv 5631 df-co 5632 df-dm 5633 df-rn 5634 df-res 5635 df-ima 5636 df-ord 6314 df-on 6315 df-lim 6316 df-suc 6317 df-iota 6442 df-fun 6488 df-fn 6489 df-f 6490 df-f1 6491 df-fo 6492 df-f1o 6493 df-fv 6494 df-riota 7310 df-ov 7356 df-oprab 7357 df-mpo 7358 df-om 7807 df-1st 7931 df-2nd 7932 df-map 8762 df-en 8880 df-fin 8883 df-fi 9320 df-rest 17344 df-topgen 17365 df-top 22797 df-topon 22814 df-bases 22849 df-cn 23130 df-hmeo 23658 df-cvm 35228

This theorem is referenced by: cvmopn 35252

W3C validator