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 36223

Description: Lemma for cvmopn 36225. (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 36207	. . . . . . . . . 10 ⊢ (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐹 ∈ (𝐶 Cn 𝐽))
3	2	adantr 486	. . . . . . . . 9 ⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) → 𝐹 ∈ (𝐶 Cn 𝐽))
4		cvmseu.1	. . . . . . . . . 10 ⊢ 𝐵 = ∪ 𝐶
5		eqid 2763	. . . . . . . . . 10 ⊢ ∪ 𝐽 = ∪ 𝐽
6	4, 5	cnf 23597	. . . . . . . . 9 ⊢ (𝐹 ∈ (𝐶 Cn 𝐽) → 𝐹:𝐵⟶∪ 𝐽)
7	3, 6	syl 18	. . . . . . . 8 ⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) → 𝐹:𝐵⟶∪ 𝐽)
8	7	adantr 486	. . . . . . 7 ⊢ (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) → 𝐹:𝐵⟶∪ 𝐽)
9		elssuni 4902	. . . . . . . . . 10 ⊢ (𝐴 ∈ 𝐶 → 𝐴 ⊆ ∪ 𝐶)
10	9, 4	sseqtrrdi 3954	. . . . . . . . 9 ⊢ (𝐴 ∈ 𝐶 → 𝐴 ⊆ 𝐵)
11	10	adantl 487	. . . . . . . 8 ⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) → 𝐴 ⊆ 𝐵)
12	11	sselda 3913	. . . . . . 7 ⊢ (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) → 𝑧 ∈ 𝐵)
13	8, 12	ffvelcdmd 7112	. . . . . 6 ⊢ (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) → (𝐹‘𝑧) ∈ ∪ 𝐽)
14		cvmcov.1	. . . . . . 7 ⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (^◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾_t 𝑢)Homeo(𝐽 ↾_t 𝑘))))})
15	14, 5	cvmcov 36208	. . . . . 6 ⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ (𝐹‘𝑧) ∈ ∪ 𝐽) → ∃𝑡 ∈ 𝐽 ((𝐹‘𝑧) ∈ 𝑡 ∧ (𝑆‘𝑡) ≠ ∅))
16	1, 13, 15	syl2anc 596	. . . . 5 ⊢ (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) → ∃𝑡 ∈ 𝐽 ((𝐹‘𝑧) ∈ 𝑡 ∧ (𝑆‘𝑡) ≠ ∅))
17		n0 4303	. . . . . . . 8 ⊢ ((𝑆‘𝑡) ≠ ∅ ↔ ∃𝑤 𝑤 ∈ (𝑆‘𝑡))
18		inss2 4137	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥)) ⊆ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥)
19		resima2 6070	. . . . . . . . . . . . . . 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 2763	. . . . . . . . . . . . . . . . . . 19 ⊢ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥) = (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥)
26	14, 4, 25	cvmsiota 36222	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ (𝑤 ∈ (𝑆‘𝑡) ∧ 𝑧 ∈ 𝐵 ∧ (𝐹‘𝑧) ∈ 𝑡)) → ((℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥) ∈ 𝑤 ∧ 𝑧 ∈ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥)))
27	22, 21, 23, 24, 26	syl13anc 1400	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) ∧ ((𝐹‘𝑧) ∈ 𝑡 ∧ 𝑤 ∈ (𝑆‘𝑡))) → ((℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥) ∈ 𝑤 ∧ 𝑧 ∈ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥)))
28	27	simpld 500	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) ∧ ((𝐹‘𝑧) ∈ 𝑡 ∧ 𝑤 ∈ (𝑆‘𝑡))) → (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥) ∈ 𝑤)
29	14	cvmshmeo 36216	. . . . . . . . . . . . . . . 16 ⊢ ((𝑤 ∈ (𝑆‘𝑡) ∧ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥) ∈ 𝑤) → (𝐹 ↾ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥)) ∈ ((𝐶 ↾_t (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))Homeo(𝐽 ↾_t 𝑡)))
30	21, 28, 29	syl2anc 596	. . . . . . . . . . . . . . 15 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) ∧ ((𝐹‘𝑧) ∈ 𝑡 ∧ 𝑤 ∈ (𝑆‘𝑡))) → (𝐹 ↾ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥)) ∈ ((𝐶 ↾_t (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))Homeo(𝐽 ↾_t 𝑡)))
31		cvmtop1 36205	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐶 ∈ Top)
32	22, 31	syl 18	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) ∧ ((𝐹‘𝑧) ∈ 𝑡 ∧ 𝑤 ∈ (𝑆‘𝑡))) → 𝐶 ∈ Top)
33		simpllr 788	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) ∧ ((𝐹‘𝑧) ∈ 𝑡 ∧ 𝑤 ∈ (𝑆‘𝑡))) → 𝐴 ∈ 𝐶)
34		elrestr 17631	. . . . . . . . . . . . . . . 16 ⊢ ((𝐶 ∈ Top ∧ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥) ∈ 𝑤 ∧ 𝐴 ∈ 𝐶) → (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥)) ∈ (𝐶 ↾_t (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥)))
35	32, 28, 33, 34	syl3anc 1399	. . . . . . . . . . . . . . 15 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) ∧ ((𝐹‘𝑧) ∈ 𝑡 ∧ 𝑤 ∈ (𝑆‘𝑡))) → (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥)) ∈ (𝐶 ↾_t (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥)))
36		hmeoima 24117	. . . . . . . . . . . . . . 15 ⊢ (((𝐹 ↾ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥)) ∈ ((𝐶 ↾_t (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))Homeo(𝐽 ↾_t 𝑡)) ∧ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥)) ∈ (𝐶 ↾_t (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))) → ((𝐹 ↾ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥)) “ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))) ∈ (𝐽 ↾_t 𝑡))
37	30, 35, 36	syl2anc 596	. . . . . . . . . . . . . 14 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) ∧ ((𝐹‘𝑧) ∈ 𝑡 ∧ 𝑤 ∈ (𝑆‘𝑡))) → ((𝐹 ↾ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥)) “ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))) ∈ (𝐽 ↾_t 𝑡))
38	20, 37	eqeltrrid 2869	. . . . . . . . . . . . 13 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) ∧ ((𝐹‘𝑧) ∈ 𝑡 ∧ 𝑤 ∈ (𝑆‘𝑡))) → (𝐹 “ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))) ∈ (𝐽 ↾_t 𝑡))
39		cvmtop2 36206	. . . . . . . . . . . . . . . 16 ⊢ (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐽 ∈ Top)
40	39	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) → 𝐽 ∈ Top)
41	40	ad2antrr 739	. . . . . . . . . . . . . 14 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) ∧ ((𝐹‘𝑧) ∈ 𝑡 ∧ 𝑤 ∈ (𝑆‘𝑡))) → 𝐽 ∈ Top)
42	14	cvmsrcl 36209	. . . . . . . . . . . . . . 15 ⊢ (𝑤 ∈ (𝑆‘𝑡) → 𝑡 ∈ 𝐽)
43	42	ad2antll 742	. . . . . . . . . . . . . 14 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) ∧ ((𝐹‘𝑧) ∈ 𝑡 ∧ 𝑤 ∈ (𝑆‘𝑡))) → 𝑡 ∈ 𝐽)
44		restopn2 23528	. . . . . . . . . . . . . 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 6735	. . . . . . . . . . . . 13 ⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) → 𝐹 Fn 𝐵)
49	48	ad2antrr 739	. . . . . . . . . . . 12 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) ∧ ((𝐹‘𝑧) ∈ 𝑡 ∧ 𝑤 ∈ (𝑆‘𝑡))) → 𝐹 Fn 𝐵)
50		inss1 4136	. . . . . . . . . . . . 13 ⊢ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥)) ⊆ 𝐴
51	33, 10	syl 18	. . . . . . . . . . . . 13 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) ∧ ((𝐹‘𝑧) ∈ 𝑡 ∧ 𝑤 ∈ (𝑆‘𝑡))) → 𝐴 ⊆ 𝐵)
52	50, 51	sstrid 3924	. . . . . . . . . . . 12 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) ∧ ((𝐹‘𝑧) ∈ 𝑡 ∧ 𝑤 ∈ (𝑆‘𝑡))) → (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥)) ⊆ 𝐵)
53		simplr 781	. . . . . . . . . . . . 13 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) ∧ ((𝐹‘𝑧) ∈ 𝑡 ∧ 𝑤 ∈ (𝑆‘𝑡))) → 𝑧 ∈ 𝐴)
54	27	simprd 501	. . . . . . . . . . . . 13 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) ∧ ((𝐹‘𝑧) ∈ 𝑡 ∧ 𝑤 ∈ (𝑆‘𝑡))) → 𝑧 ∈ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))
55	53, 54	elind 4100	. . . . . . . . . . . 12 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) ∧ ((𝐹‘𝑧) ∈ 𝑡 ∧ 𝑤 ∈ (𝑆‘𝑡))) → 𝑧 ∈ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥)))
56		fnfvima 7265	. . . . . . . . . . . 12 ⊢ ((𝐹 Fn 𝐵 ∧ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥)) ⊆ 𝐵 ∧ 𝑧 ∈ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))) → (𝐹‘𝑧) ∈ (𝐹 “ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))))
57	49, 52, 55, 56	syl3anc 1399	. . . . . . . . . . 11 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) ∧ ((𝐹‘𝑧) ∈ 𝑡 ∧ 𝑤 ∈ (𝑆‘𝑡))) → (𝐹‘𝑧) ∈ (𝐹 “ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))))
58		imass2 6068	. . . . . . . . . . . 12 ⊢ ((𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥)) ⊆ 𝐴 → (𝐹 “ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))) ⊆ (𝐹 “ 𝐴))
59	50, 58	mp1i 14	. . . . . . . . . . 11 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) ∧ ((𝐹‘𝑧) ∈ 𝑡 ∧ 𝑤 ∈ (𝑆‘𝑡))) → (𝐹 “ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))) ⊆ (𝐹 “ 𝐴))
60		eleq2 2853	. . . . . . . . . . . . 13 ⊢ (𝑦 = (𝐹 “ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))) → ((𝐹‘𝑧) ∈ 𝑦 ↔ (𝐹‘𝑧) ∈ (𝐹 “ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥)))))
61		sseq1 3938	. . . . . . . . . . . . 13 ⊢ (𝑦 = (𝐹 “ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))) → (𝑦 ⊆ (𝐹 “ 𝐴) ↔ (𝐹 “ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))) ⊆ (𝐹 “ 𝐴)))
62	60, 61	anbi12d 644	. . . . . . . . . . . 12 ⊢ (𝑦 = (𝐹 “ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))) → (((𝐹‘𝑧) ∈ 𝑦 ∧ 𝑦 ⊆ (𝐹 “ 𝐴)) ↔ ((𝐹‘𝑧) ∈ (𝐹 “ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))) ∧ (𝐹 “ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))) ⊆ (𝐹 “ 𝐴))))
63	62	rspcev 3580	. . . . . . . . . . 11 ⊢ (((𝐹 “ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))) ∈ 𝐽 ∧ ((𝐹‘𝑧) ∈ (𝐹 “ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))) ∧ (𝐹 “ (𝐴 ∩ (℩𝑥 ∈ 𝑤 𝑧 ∈ 𝑥))) ⊆ (𝐹 “ 𝐴))) → ∃𝑦 ∈ 𝐽 ((𝐹‘𝑧) ∈ 𝑦 ∧ 𝑦 ⊆ (𝐹 “ 𝐴)))
64	47, 57, 59, 63	syl12anc 850	. . . . . . . . . 10 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) ∧ ((𝐹‘𝑧) ∈ 𝑡 ∧ 𝑤 ∈ (𝑆‘𝑡))) → ∃𝑦 ∈ 𝐽 ((𝐹‘𝑧) ∈ 𝑦 ∧ 𝑦 ⊆ (𝐹 “ 𝐴)))
65	64	expr 462	. . . . . . . . 9 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) ∧ (𝐹‘𝑧) ∈ 𝑡) → (𝑤 ∈ (𝑆‘𝑡) → ∃𝑦 ∈ 𝐽 ((𝐹‘𝑧) ∈ 𝑦 ∧ 𝑦 ⊆ (𝐹 “ 𝐴))))
66	65	exlimdv 1968	. . . . . . . 8 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) ∧ (𝐹‘𝑧) ∈ 𝑡) → (∃𝑤 𝑤 ∈ (𝑆‘𝑡) → ∃𝑦 ∈ 𝐽 ((𝐹‘𝑧) ∈ 𝑦 ∧ 𝑦 ⊆ (𝐹 “ 𝐴))))
67	17, 66	biimtrid 245	. . . . . . 7 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) ∧ (𝐹‘𝑧) ∈ 𝑡) → ((𝑆‘𝑡) ≠ ∅ → ∃𝑦 ∈ 𝐽 ((𝐹‘𝑧) ∈ 𝑦 ∧ 𝑦 ⊆ (𝐹 “ 𝐴))))
68	67	expimpd 459	. . . . . 6 ⊢ (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) → (((𝐹‘𝑧) ∈ 𝑡 ∧ (𝑆‘𝑡) ≠ ∅) → ∃𝑦 ∈ 𝐽 ((𝐹‘𝑧) ∈ 𝑦 ∧ 𝑦 ⊆ (𝐹 “ 𝐴))))
69	68	rexlimdvw 3172	. . . . 5 ⊢ (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) → (∃𝑡 ∈ 𝐽 ((𝐹‘𝑧) ∈ 𝑡 ∧ (𝑆‘𝑡) ≠ ∅) → ∃𝑦 ∈ 𝐽 ((𝐹‘𝑧) ∈ 𝑦 ∧ 𝑦 ⊆ (𝐹 “ 𝐴))))
70	16, 69	mpd 16	. . . 4 ⊢ (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) ∧ 𝑧 ∈ 𝐴) → ∃𝑦 ∈ 𝐽 ((𝐹‘𝑧) ∈ 𝑦 ∧ 𝑦 ⊆ (𝐹 “ 𝐴)))
71	70	ralrimiva 3158	. . 3 ⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) → ∀𝑧 ∈ 𝐴 ∃𝑦 ∈ 𝐽 ((𝐹‘𝑧) ∈ 𝑦 ∧ 𝑦 ⊆ (𝐹 “ 𝐴)))
72		eleq1 2852	. . . . . . 7 ⊢ (𝑥 = (𝐹‘𝑧) → (𝑥 ∈ 𝑦 ↔ (𝐹‘𝑧) ∈ 𝑦))
73	72	anbi1d 643	. . . . . 6 ⊢ (𝑥 = (𝐹‘𝑧) → ((𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ (𝐹 “ 𝐴)) ↔ ((𝐹‘𝑧) ∈ 𝑦 ∧ 𝑦 ⊆ (𝐹 “ 𝐴))))
74	73	rexbidv 3190	. . . . 5 ⊢ (𝑥 = (𝐹‘𝑧) → (∃𝑦 ∈ 𝐽 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ (𝐹 “ 𝐴)) ↔ ∃𝑦 ∈ 𝐽 ((𝐹‘𝑧) ∈ 𝑦 ∧ 𝑦 ⊆ (𝐹 “ 𝐴))))
75	74	ralima 7269	. . . 4 ⊢ ((𝐹 Fn 𝐵 ∧ 𝐴 ⊆ 𝐵) → (∀𝑥 ∈ (𝐹 “ 𝐴)∃𝑦 ∈ 𝐽 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ (𝐹 “ 𝐴)) ↔ ∀𝑧 ∈ 𝐴 ∃𝑦 ∈ 𝐽 ((𝐹‘𝑧) ∈ 𝑦 ∧ 𝑦 ⊆ (𝐹 “ 𝐴))))
76	48, 11, 75	syl2anc 596	. . 3 ⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) → (∀𝑥 ∈ (𝐹 “ 𝐴)∃𝑦 ∈ 𝐽 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ (𝐹 “ 𝐴)) ↔ ∀𝑧 ∈ 𝐴 ∃𝑦 ∈ 𝐽 ((𝐹‘𝑧) ∈ 𝑦 ∧ 𝑦 ⊆ (𝐹 “ 𝐴))))
77	71, 76	mpbird 260	. 2 ⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐴 ∈ 𝐶) → ∀𝑥 ∈ (𝐹 “ 𝐴)∃𝑦 ∈ 𝐽 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ (𝐹 “ 𝐴)))
78		eltop2 23326	. . 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 2147 ≠ wne 2959 ∀wral 3080 ∃wrex 3090 {crab 3416 ⊆ wss 3900 ∖ cdif 4048 ∩ cin 4092 ∅c0 4281 𝒫 cpw 4560 {csn 4588 ∪ cuni 4870 ↦ cmpt 5190 ^◡ccnv 5655 ↾ cres 5658 “ cima 5659 Fn wfn 6556 ⟶wf 6557 ‘cfv 6561 ℩crio 7402 (class class class)co 7446 ↾_t crest 17623 Topctop 23244 Cn ccn 23575 Homeochmeo 24105 CovMap ccvm 36200

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 1945 ax-6 2002 ax-7 2043 ax-8 2149 ax-9 2157 ax-10 2180 ax-11 2197 ax-12 2216 ax-ext 2735 ax-rep 5236 ax-sep 5253 ax-nul 5264 ax-pow 5332 ax-pr 5396 ax-un 7778

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 2102 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2839 df-nfc 2913 df-ne 2960 df-ral 3081 df-rex 3091 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3456 df-sbc 3743 df-csb 3852 df-ss 3901 df-pss 4017 df-dif 4050 df-in 4094 df-un 4154 df-nul 4282 df-if 4486 df-pw 4562 df-sn 4589 df-pr 4591 df-op 4839 df-uni 4871 df-int 4911 df-iun 4956 df-br 5107 df-opab 5172 df-mpt 5191 df-tr 5217 df-id 5551 df-eprel 5556 df-po 5564 df-so 5565 df-fr 5609 df-we 5611 df-xp 5662 df-rel 5663 df-cnv 5664 df-co 5665 df-dm 5666 df-rn 5667 df-res 5668 df-ima 5669 df-ord 6386 df-on 6387 df-lim 6388 df-suc 6389 df-iota 6515 df-fun 6563 df-fn 6564 df-f 6565 df-f1 6566 df-fo 6567 df-f1o 6568 df-fv 6569 df-riota 7403 df-ov 7449 df-oprab 7450 df-mpo 7451 df-om 7905 df-1st 8028 df-2nd 8029 df-map 8880 df-en 9005 df-fin 9008 df-fi 9433 df-rest 17625 df-topgen 17646 df-top 23245 df-topon 23262 df-bases 23297 df-cn 23578 df-hmeo 24107 df-cvm 36201

This theorem is used by: cvmopn 36225

W3C validator