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 36012

Description: Lemma for cvmopn 36014. (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 35996	. . . . . . . . . 10 ⊢ (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐹 ∈ (𝐶 Cn 𝐽))
3	2	adantr 486	. . . . . . . . 9 ⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) → 𝐹 ∈ (𝐶 Cn 𝐽))
4		cvmseu.1	. . . . . . . . . 10 ⊢ 𝐵 = ∪ 𝐶
5		eqid 2761	. . . . . . . . . 10 ⊢ ∪ 𝐽 = ∪ 𝐽
6	4, 5	cnf 23544	. . . . . . . . 9 ⊢ (𝐹 ∈ (𝐶 Cn 𝐽) → 𝐹:𝐵⟶∪ 𝐽)
7	3, 6	syl 18	. . . . . . . 8 ⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) → 𝐹:𝐵⟶∪ 𝐽)
8	7	adantr 486	. . . . . . 7 ⊢ (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) → 𝐹:𝐵⟶∪ 𝐽)
9		elssuni 4899	. . . . . . . . . 10 ⊢ (𝐴 ∈ 𝐶 → 𝐴 ⊆ ∪ 𝐶)
10	9, 4	sseqtrrdi 3972	. . . . . . . . 9 ⊢ (𝐴 ∈ 𝐶 → 𝐴 ⊆ 𝐵)
11	10	adantl 487	. . . . . . . 8 ⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) → 𝐴 ⊆ 𝐵)
12	11	sselda 3931	. . . . . . 7 ⊢ (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) → 𝑧 ∈ 𝐵)
13	8, 12	ffvelcdmd 7077	. . . . . 6 ⊢ (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) → (𝐹‘𝑧) ∈ ∪ 𝐽)
14		cvmcov.1	. . . . . . 7 ⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (^◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾_t 𝑢)Homeo(𝐽 ↾_t 𝑘))))})
15	14, 5	cvmcov 35997	. . . . . 6 ⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ (𝐹‘𝑧) ∈ ∪ 𝐽) → ∃𝑡 ∈ 𝐽 ((𝐹‘𝑧) ∈ 𝑡 ∧ (𝑆‘𝑡) ≠ ∅))
16	1, 13, 15	syl2anc 596	. . . . 5 ⊢ (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) → ∃𝑡 ∈ 𝐽 ((𝐹‘𝑧) ∈ 𝑡 ∧ (𝑆‘𝑡) ≠ ∅))
17		n0 4300	. . . . . . . 8 ⊢ ((𝑆‘𝑡) ≠ ∅ ↔ ∃𝑤 𝑤 ∈ (𝑆‘𝑡))
18		inss2 4183	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥)) ⊆ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥)
19		resima2 6007	. . . . . . . . . . . . . . 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 2761	. . . . . . . . . . . . . . . . . . 19 ⊢ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥) = (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥)
26	14, 4, 25	cvmsiota 36011	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ (𝑤 ∈ (𝑆‘𝑡) ∧ 𝑧 ∈ 𝐵 ∧ (𝐹‘𝑧) ∈ 𝑡)) → ((℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥) ∈ 𝑤 ∧ 𝑧 ∈ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥)))
27	22, 21, 23, 24, 26	syl13anc 1399	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) ∧ ((𝐹‘𝑧) ∈ 𝑡 ∧ 𝑤 ∈ (𝑆‘𝑡))) → ((℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥) ∈ 𝑤 ∧ 𝑧 ∈ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥)))
28	27	simpld 500	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) ∧ ((𝐹‘𝑧) ∈ 𝑡 ∧ 𝑤 ∈ (𝑆‘𝑡))) → (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥) ∈ 𝑤)
29	14	cvmshmeo 36005	. . . . . . . . . . . . . . . 16 ⊢ ((𝑤 ∈ (𝑆‘𝑡) ∧ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥) ∈ 𝑤) → (𝐹 ↾ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥)) ∈ ((𝐶 ↾_t (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))Homeo(𝐽 ↾_t 𝑡)))
30	21, 28, 29	syl2anc 596	. . . . . . . . . . . . . . 15 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) ∧ ((𝐹‘𝑧) ∈ 𝑡 ∧ 𝑤 ∈ (𝑆‘𝑡))) → (𝐹 ↾ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥)) ∈ ((𝐶 ↾_t (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))Homeo(𝐽 ↾_t 𝑡)))
31		cvmtop1 35994	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐶 ∈ Top)
32	22, 31	syl 18	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) ∧ ((𝐹‘𝑧) ∈ 𝑡 ∧ 𝑤 ∈ (𝑆‘𝑡))) → 𝐶 ∈ Top)
33		simpllr 788	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) ∧ ((𝐹‘𝑧) ∈ 𝑡 ∧ 𝑤 ∈ (𝑆‘𝑡))) → 𝐴 ∈ 𝐶)
34		elrestr 17579	. . . . . . . . . . . . . . . 16 ⊢ ((𝐶 ∈ Top ∧ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥) ∈ 𝑤 ∧ 𝐴 ∈ 𝐶) → (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥)) ∈ (𝐶 ↾_t (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥)))
35	32, 28, 33, 34	syl3anc 1398	. . . . . . . . . . . . . . 15 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) ∧ ((𝐹‘𝑧) ∈ 𝑡 ∧ 𝑤 ∈ (𝑆‘𝑡))) → (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥)) ∈ (𝐶 ↾_t (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥)))
36		hmeoima 24064	. . . . . . . . . . . . . . 15 ⊢ (((𝐹 ↾ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥)) ∈ ((𝐶 ↾_t (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))Homeo(𝐽 ↾_t 𝑡)) ∧ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥)) ∈ (𝐶 ↾_t (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))) → ((𝐹 ↾ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥)) “ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))) ∈ (𝐽 ↾_t 𝑡))
37	30, 35, 36	syl2anc 596	. . . . . . . . . . . . . 14 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) ∧ ((𝐹‘𝑧) ∈ 𝑡 ∧ 𝑤 ∈ (𝑆‘𝑡))) → ((𝐹 ↾ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥)) “ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))) ∈ (𝐽 ↾_t 𝑡))
38	20, 37	eqeltrrid 2866	. . . . . . . . . . . . 13 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) ∧ ((𝐹‘𝑧) ∈ 𝑡 ∧ 𝑤 ∈ (𝑆‘𝑡))) → (𝐹 “ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))) ∈ (𝐽 ↾_t 𝑡))
39		cvmtop2 35995	. . . . . . . . . . . . . . . 16 ⊢ (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐽 ∈ Top)
40	39	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) → 𝐽 ∈ Top)
41	40	ad2antrr 739	. . . . . . . . . . . . . 14 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) ∧ ((𝐹‘𝑧) ∈ 𝑡 ∧ 𝑤 ∈ (𝑆‘𝑡))) → 𝐽 ∈ Top)
42	14	cvmsrcl 35998	. . . . . . . . . . . . . . 15 ⊢ (𝑤 ∈ (𝑆‘𝑡) → 𝑡 ∈ 𝐽)
43	42	ad2antll 742	. . . . . . . . . . . . . 14 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) ∧ ((𝐹‘𝑧) ∈ 𝑡 ∧ 𝑤 ∈ (𝑆‘𝑡))) → 𝑡 ∈ 𝐽)
44		restopn2 23475	. . . . . . . . . . . . . 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 6702	. . . . . . . . . . . . 13 ⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) → 𝐹 Fn 𝐵)
49	48	ad2antrr 739	. . . . . . . . . . . 12 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) ∧ ((𝐹‘𝑧) ∈ 𝑡 ∧ 𝑤 ∈ (𝑆‘𝑡))) → 𝐹 Fn 𝐵)
50		inss1 4182	. . . . . . . . . . . . 13 ⊢ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥)) ⊆ 𝐴
51	33, 10	syl 18	. . . . . . . . . . . . 13 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) ∧ ((𝐹‘𝑧) ∈ 𝑡 ∧ 𝑤 ∈ (𝑆‘𝑡))) → 𝐴 ⊆ 𝐵)
52	50, 51	sstrid 3942	. . . . . . . . . . . 12 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) ∧ ((𝐹‘𝑧) ∈ 𝑡 ∧ 𝑤 ∈ (𝑆‘𝑡))) → (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥)) ⊆ 𝐵)
53		simplr 781	. . . . . . . . . . . . 13 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) ∧ ((𝐹‘𝑧) ∈ 𝑡 ∧ 𝑤 ∈ (𝑆‘𝑡))) → 𝑧 ∈ 𝐴)
54	27	simprd 501	. . . . . . . . . . . . 13 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) ∧ ((𝐹‘𝑧) ∈ 𝑡 ∧ 𝑤 ∈ (𝑆‘𝑡))) → 𝑧 ∈ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))
55	53, 54	elind 4146	. . . . . . . . . . . 12 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) ∧ ((𝐹‘𝑧) ∈ 𝑡 ∧ 𝑤 ∈ (𝑆‘𝑡))) → 𝑧 ∈ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥)))
56		fnfvima 7231	. . . . . . . . . . . 12 ⊢ ((𝐹 Fn 𝐵 ∧ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥)) ⊆ 𝐵 ∧ 𝑧 ∈ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))) → (𝐹‘𝑧) ∈ (𝐹 “ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))))
57	49, 52, 55, 56	syl3anc 1398	. . . . . . . . . . 11 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) ∧ ((𝐹‘𝑧) ∈ 𝑡 ∧ 𝑤 ∈ (𝑆‘𝑡))) → (𝐹‘𝑧) ∈ (𝐹 “ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))))
58		imass2 6096	. . . . . . . . . . . 12 ⊢ ((𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥)) ⊆ 𝐴 → (𝐹 “ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))) ⊆ (𝐹 “ 𝐴))
59	50, 58	mp1i 14	. . . . . . . . . . 11 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) ∧ ((𝐹‘𝑧) ∈ 𝑡 ∧ 𝑤 ∈ (𝑆‘𝑡))) → (𝐹 “ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))) ⊆ (𝐹 “ 𝐴))
60		eleq2 2850	. . . . . . . . . . . . 13 ⊢ (𝑦 = (𝐹 “ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))) → ((𝐹‘𝑧) ∈ 𝑦 ↔ (𝐹‘𝑧) ∈ (𝐹 “ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥)))))
61		sseq1 3956	. . . . . . . . . . . . 13 ⊢ (𝑦 = (𝐹 “ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))) → (𝑦 ⊆ (𝐹 “ 𝐴) ↔ (𝐹 “ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))) ⊆ (𝐹 “ 𝐴)))
62	60, 61	anbi12d 644	. . . . . . . . . . . 12 ⊢ (𝑦 = (𝐹 “ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))) → (((𝐹‘𝑧) ∈ 𝑦 ∧ 𝑦 ⊆ (𝐹 “ 𝐴)) ↔ ((𝐹‘𝑧) ∈ (𝐹 “ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))) ∧ (𝐹 “ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))) ⊆ (𝐹 “ 𝐴))))
63	62	rspcev 3577	. . . . . . . . . . 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 3169	. . . . 5 ⊢ (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) → (∃𝑡 ∈ 𝐽 ((𝐹‘𝑧) ∈ 𝑡 ∧ (𝑆‘𝑡) ≠ ∅) → ∃𝑦 ∈ 𝐽 ((𝐹‘𝑧) ∈ 𝑦 ∧ 𝑦 ⊆ (𝐹 “ 𝐴))))
70	16, 69	mpd 16	. . . 4 ⊢ (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) → ∃𝑦 ∈ 𝐽 ((𝐹‘𝑧) ∈ 𝑦 ∧ 𝑦 ⊆ (𝐹 “ 𝐴)))
71	70	ralrimiva 3155	. . 3 ⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) → ∀𝑧 ∈ 𝐴 ∃𝑦 ∈ 𝐽 ((𝐹‘𝑧) ∈ 𝑦 ∧ 𝑦 ⊆ (𝐹 “ 𝐴)))
72		eleq1 2849	. . . . . . 7 ⊢ (𝑥 = (𝐹‘𝑧) → (𝑥 ∈ 𝑦 ↔ (𝐹‘𝑧) ∈ 𝑦))
73	72	anbi1d 643	. . . . . 6 ⊢ (𝑥 = (𝐹‘𝑧) → ((𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ (𝐹 “ 𝐴)) ↔ ((𝐹‘𝑧) ∈ 𝑦 ∧ 𝑦 ⊆ (𝐹 “ 𝐴))))
74	73	rexbidv 3187	. . . . 5 ⊢ (𝑥 = (𝐹‘𝑧) → (∃𝑦 ∈ 𝐽 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ (𝐹 “ 𝐴)) ↔ ∃𝑦 ∈ 𝐽 ((𝐹‘𝑧) ∈ 𝑦 ∧ 𝑦 ⊆ (𝐹 “ 𝐴))))
75	74	ralima 7235	. . . 4 ⊢ ((𝐹 Fn 𝐵 ∧ 𝐴 ⊆ 𝐵) → (∀𝑥 ∈ (𝐹 “ 𝐴)∃𝑦 ∈ 𝐽 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ (𝐹 “ 𝐴)) ↔ ∀𝑧 ∈ 𝐴 ∃𝑦 ∈ 𝐽 ((𝐹‘𝑧) ∈ 𝑦 ∧ 𝑦 ⊆ (𝐹 “ 𝐴))))
76	48, 11, 75	syl2anc 596	. . 3 ⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) → (∀𝑥 ∈ (𝐹 “ 𝐴)∃𝑦 ∈ 𝐽 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ (𝐹 “ 𝐴)) ↔ ∀𝑧 ∈ 𝐴 ∃𝑦 ∈ 𝐽 ((𝐹‘𝑧) ∈ 𝑦 ∧ 𝑦 ⊆ (𝐹 “ 𝐴))))
77	71, 76	mpbird 260	. 2 ⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) → ∀𝑥 ∈ (𝐹 “ 𝐴)∃𝑦 ∈ 𝐽 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ (𝐹 “ 𝐴)))
78		eltop2 23273	. . 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 2956 ∀wral 3077 ∃wrex 3087 {crab 3413 ∖ cdif 3896 ∩ cin 3898 ⊆ wss 3899 ∅c0 4279 𝒫 cpw 4557 {csn 4584 ∪ cuni 4867 ↦ cmpt 5186 ^◡ccnv 5650 ↾ cres 5653 “ cima 5654 Fn wfn 6526 ⟶wf 6527 ‘cfv 6531 ℩crio 7368 (class class class)co 7412 ↾_t crest 17571 Topctop 23191 Cn ccn 23522 Homeochmeo 24052 CovMap ccvm 35989

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 2213 ax-ext 2733 ax-rep 5232 ax-sep 5249 ax-nul 5260 ax-pow 5327 ax-pr 5391 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 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-ral 3078 df-rex 3088 df-rmo 3366 df-reu 3367 df-rab 3414 df-v 3453 df-sbc 3740 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-nul 4280 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-op 4591 df-uni 4868 df-int 4908 df-iun 4953 df-br 5104 df-opab 5168 df-mpt 5187 df-tr 5213 df-id 5546 df-eprel 5551 df-po 5559 df-so 5560 df-fr 5604 df-we 5606 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-rn 5662 df-res 5663 df-ima 5664 df-ord 6358 df-on 6359 df-lim 6360 df-suc 6361 df-iota 6487 df-fun 6533 df-fn 6534 df-f 6535 df-f1 6536 df-fo 6537 df-f1o 6538 df-fv 6539 df-riota 7369 df-ov 7415 df-oprab 7416 df-mpo 7417 df-om 7867 df-1st 7990 df-2nd 7991 df-map 8833 df-en 8958 df-fin 8961 df-fi 9387 df-rest 17573 df-topgen 17594 df-top 23192 df-topon 23209 df-bases 23244 df-cn 23525 df-hmeo 24054 df-cvm 35990

This theorem is used by: cvmopn 36014

W3C validator