cvmsss2 - Mathbox for Mario Carneiro

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

Theorem cvmsss2 34253

Description: An open subset of an evenly covered set is evenly covered. (Contributed by Mario Carneiro, 7-Jul-2015.)

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

**Assertion**
Ref	Expression
cvmsss2	⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈) → ((𝑆‘𝑈) ≠ ∅ → (𝑆‘𝑉) ≠ ∅))

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

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

Step	Hyp	Ref	Expression
1		n0 4345	. 2 ⊢ ((𝑆‘𝑈) ≠ ∅ ↔ ∃𝑥 𝑥 ∈ (𝑆‘𝑈))
2		simpl2 1192	. . . . . 6 ⊢ (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈) ∧ 𝑥 ∈ (𝑆‘𝑈)) → 𝑉 ∈ 𝐽)
3		simpl1 1191	. . . . . . . . . . . 12 ⊢ (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈) ∧ 𝑥 ∈ (𝑆‘𝑈)) → 𝐹 ∈ (𝐶 CovMap 𝐽))
4		cvmtop1 34239	. . . . . . . . . . . 12 ⊢ (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐶 ∈ Top)
5	3, 4	syl 17	. . . . . . . . . . 11 ⊢ (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈) ∧ 𝑥 ∈ (𝑆‘𝑈)) → 𝐶 ∈ Top)
6	5	adantr 481	. . . . . . . . . 10 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈) ∧ 𝑥 ∈ (𝑆‘𝑈)) ∧ 𝑦 ∈ 𝑥) → 𝐶 ∈ Top)
7		cvmcov.1	. . . . . . . . . . . . 13 ⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (^◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾_t 𝑢)Homeo(𝐽 ↾_t 𝑘))))})
8	7	cvmsss 34246	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (𝑆‘𝑈) → 𝑥 ⊆ 𝐶)
9	8	adantl 482	. . . . . . . . . . 11 ⊢ (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈) ∧ 𝑥 ∈ (𝑆‘𝑈)) → 𝑥 ⊆ 𝐶)
10	9	sselda 3981	. . . . . . . . . 10 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈) ∧ 𝑥 ∈ (𝑆‘𝑈)) ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ 𝐶)
11		cvmcn 34241	. . . . . . . . . . . . 13 ⊢ (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐹 ∈ (𝐶 Cn 𝐽))
12	3, 11	syl 17	. . . . . . . . . . . 12 ⊢ (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈) ∧ 𝑥 ∈ (𝑆‘𝑈)) → 𝐹 ∈ (𝐶 Cn 𝐽))
13		cnima 22760	. . . . . . . . . . . 12 ⊢ ((𝐹 ∈ (𝐶 Cn 𝐽) ∧ 𝑉 ∈ 𝐽) → (^◡𝐹 “ 𝑉) ∈ 𝐶)
14	12, 2, 13	syl2anc 584	. . . . . . . . . . 11 ⊢ (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈) ∧ 𝑥 ∈ (𝑆‘𝑈)) → (^◡𝐹 “ 𝑉) ∈ 𝐶)
15	14	adantr 481	. . . . . . . . . 10 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈) ∧ 𝑥 ∈ (𝑆‘𝑈)) ∧ 𝑦 ∈ 𝑥) → (^◡𝐹 “ 𝑉) ∈ 𝐶)
16		inopn 22392	. . . . . . . . . 10 ⊢ ((𝐶 ∈ Top ∧ 𝑦 ∈ 𝐶 ∧ (^◡𝐹 “ 𝑉) ∈ 𝐶) → (𝑦 ∩ (^◡𝐹 “ 𝑉)) ∈ 𝐶)
17	6, 10, 15, 16	syl3anc 1371	. . . . . . . . 9 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈) ∧ 𝑥 ∈ (𝑆‘𝑈)) ∧ 𝑦 ∈ 𝑥) → (𝑦 ∩ (^◡𝐹 “ 𝑉)) ∈ 𝐶)
18	17	fmpttd 7111	. . . . . . . 8 ⊢ (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈) ∧ 𝑥 ∈ (𝑆‘𝑈)) → (𝑦 ∈ 𝑥 ↦ (𝑦 ∩ (^◡𝐹 “ 𝑉))):𝑥⟶𝐶)
19	18	frnd 6722	. . . . . . 7 ⊢ (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈) ∧ 𝑥 ∈ (𝑆‘𝑈)) → ran (𝑦 ∈ 𝑥 ↦ (𝑦 ∩ (^◡𝐹 “ 𝑉))) ⊆ 𝐶)
20	7	cvmsn0 34247	. . . . . . . . 9 ⊢ (𝑥 ∈ (𝑆‘𝑈) → 𝑥 ≠ ∅)
21	20	adantl 482	. . . . . . . 8 ⊢ (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈) ∧ 𝑥 ∈ (𝑆‘𝑈)) → 𝑥 ≠ ∅)
22		dmmptg 6238	. . . . . . . . . . . 12 ⊢ (∀𝑦 ∈ 𝑥 (𝑦 ∩ (^◡𝐹 “ 𝑉)) ∈ V → dom (𝑦 ∈ 𝑥 ↦ (𝑦 ∩ (^◡𝐹 “ 𝑉))) = 𝑥)
23		inex1g 5318	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ 𝑥 → (𝑦 ∩ (^◡𝐹 “ 𝑉)) ∈ V)
24	22, 23	mprg 3067	. . . . . . . . . . 11 ⊢ dom (𝑦 ∈ 𝑥 ↦ (𝑦 ∩ (^◡𝐹 “ 𝑉))) = 𝑥
25	24	eqeq1i 2737	. . . . . . . . . 10 ⊢ (dom (𝑦 ∈ 𝑥 ↦ (𝑦 ∩ (^◡𝐹 “ 𝑉))) = ∅ ↔ 𝑥 = ∅)
26		dm0rn0 5922	. . . . . . . . . 10 ⊢ (dom (𝑦 ∈ 𝑥 ↦ (𝑦 ∩ (^◡𝐹 “ 𝑉))) = ∅ ↔ ran (𝑦 ∈ 𝑥 ↦ (𝑦 ∩ (^◡𝐹 “ 𝑉))) = ∅)
27	25, 26	bitr3i 276	. . . . . . . . 9 ⊢ (𝑥 = ∅ ↔ ran (𝑦 ∈ 𝑥 ↦ (𝑦 ∩ (^◡𝐹 “ 𝑉))) = ∅)
28	27	necon3bii 2993	. . . . . . . 8 ⊢ (𝑥 ≠ ∅ ↔ ran (𝑦 ∈ 𝑥 ↦ (𝑦 ∩ (^◡𝐹 “ 𝑉))) ≠ ∅)
29	21, 28	sylib 217	. . . . . . 7 ⊢ (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈) ∧ 𝑥 ∈ (𝑆‘𝑈)) → ran (𝑦 ∈ 𝑥 ↦ (𝑦 ∩ (^◡𝐹 “ 𝑉))) ≠ ∅)
30	19, 29	jca 512	. . . . . 6 ⊢ (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈) ∧ 𝑥 ∈ (𝑆‘𝑈)) → (ran (𝑦 ∈ 𝑥 ↦ (𝑦 ∩ (^◡𝐹 “ 𝑉))) ⊆ 𝐶 ∧ ran (𝑦 ∈ 𝑥 ↦ (𝑦 ∩ (^◡𝐹 “ 𝑉))) ≠ ∅))
31		inss2 4228	. . . . . . . . . . . 12 ⊢ (𝑦 ∩ (^◡𝐹 “ 𝑉)) ⊆ (^◡𝐹 “ 𝑉)
32		elpw2g 5343	. . . . . . . . . . . . 13 ⊢ ((^◡𝐹 “ 𝑉) ∈ 𝐶 → ((𝑦 ∩ (^◡𝐹 “ 𝑉)) ∈ 𝒫 (^◡𝐹 “ 𝑉) ↔ (𝑦 ∩ (^◡𝐹 “ 𝑉)) ⊆ (^◡𝐹 “ 𝑉)))
33	15, 32	syl 17	. . . . . . . . . . . 12 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈) ∧ 𝑥 ∈ (𝑆‘𝑈)) ∧ 𝑦 ∈ 𝑥) → ((𝑦 ∩ (^◡𝐹 “ 𝑉)) ∈ 𝒫 (^◡𝐹 “ 𝑉) ↔ (𝑦 ∩ (^◡𝐹 “ 𝑉)) ⊆ (^◡𝐹 “ 𝑉)))
34	31, 33	mpbiri 257	. . . . . . . . . . 11 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈) ∧ 𝑥 ∈ (𝑆‘𝑈)) ∧ 𝑦 ∈ 𝑥) → (𝑦 ∩ (^◡𝐹 “ 𝑉)) ∈ 𝒫 (^◡𝐹 “ 𝑉))
35	34	fmpttd 7111	. . . . . . . . . 10 ⊢ (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈) ∧ 𝑥 ∈ (𝑆‘𝑈)) → (𝑦 ∈ 𝑥 ↦ (𝑦 ∩ (^◡𝐹 “ 𝑉))):𝑥⟶𝒫 (^◡𝐹 “ 𝑉))
36	35	frnd 6722	. . . . . . . . 9 ⊢ (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈) ∧ 𝑥 ∈ (𝑆‘𝑈)) → ran (𝑦 ∈ 𝑥 ↦ (𝑦 ∩ (^◡𝐹 “ 𝑉))) ⊆ 𝒫 (^◡𝐹 “ 𝑉))
37		sspwuni 5102	. . . . . . . . 9 ⊢ (ran (𝑦 ∈ 𝑥 ↦ (𝑦 ∩ (^◡𝐹 “ 𝑉))) ⊆ 𝒫 (^◡𝐹 “ 𝑉) ↔ ∪ ran (𝑦 ∈ 𝑥 ↦ (𝑦 ∩ (^◡𝐹 “ 𝑉))) ⊆ (^◡𝐹 “ 𝑉))
38	36, 37	sylib 217	. . . . . . . 8 ⊢ (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈) ∧ 𝑥 ∈ (𝑆‘𝑈)) → ∪ ran (𝑦 ∈ 𝑥 ↦ (𝑦 ∩ (^◡𝐹 “ 𝑉))) ⊆ (^◡𝐹 “ 𝑉))
39		simpl3 1193	. . . . . . . . . . . 12 ⊢ (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈) ∧ 𝑥 ∈ (𝑆‘𝑈)) → 𝑉 ⊆ 𝑈)
40		imass2 6098	. . . . . . . . . . . 12 ⊢ (𝑉 ⊆ 𝑈 → (^◡𝐹 “ 𝑉) ⊆ (^◡𝐹 “ 𝑈))
41	39, 40	syl 17	. . . . . . . . . . 11 ⊢ (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈) ∧ 𝑥 ∈ (𝑆‘𝑈)) → (^◡𝐹 “ 𝑉) ⊆ (^◡𝐹 “ 𝑈))
42	7	cvmsuni 34248	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (𝑆‘𝑈) → ∪ 𝑥 = (^◡𝐹 “ 𝑈))
43	42	adantl 482	. . . . . . . . . . 11 ⊢ (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈) ∧ 𝑥 ∈ (𝑆‘𝑈)) → ∪ 𝑥 = (^◡𝐹 “ 𝑈))
44	41, 43	sseqtrrd 4022	. . . . . . . . . 10 ⊢ (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈) ∧ 𝑥 ∈ (𝑆‘𝑈)) → (^◡𝐹 “ 𝑉) ⊆ ∪ 𝑥)
45	44	sselda 3981	. . . . . . . . 9 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈) ∧ 𝑥 ∈ (𝑆‘𝑈)) ∧ 𝑧 ∈ (^◡𝐹 “ 𝑉)) → 𝑧 ∈ ∪ 𝑥)
46		eqid 2732	. . . . . . . . . . . . . . 15 ⊢ (𝑡 ∩ (^◡𝐹 “ 𝑉)) = (𝑡 ∩ (^◡𝐹 “ 𝑉))
47		ineq1 4204	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑡 → (𝑦 ∩ (^◡𝐹 “ 𝑉)) = (𝑡 ∩ (^◡𝐹 “ 𝑉)))
48	47	rspceeqv 3632	. . . . . . . . . . . . . . 15 ⊢ ((𝑡 ∈ 𝑥 ∧ (𝑡 ∩ (^◡𝐹 “ 𝑉)) = (𝑡 ∩ (^◡𝐹 “ 𝑉))) → ∃𝑦 ∈ 𝑥 (𝑡 ∩ (^◡𝐹 “ 𝑉)) = (𝑦 ∩ (^◡𝐹 “ 𝑉)))
49	46, 48	mpan2 689	. . . . . . . . . . . . . 14 ⊢ (𝑡 ∈ 𝑥 → ∃𝑦 ∈ 𝑥 (𝑡 ∩ (^◡𝐹 “ 𝑉)) = (𝑦 ∩ (^◡𝐹 “ 𝑉)))
50	49	ad2antrl 726	. . . . . . . . . . . . 13 ⊢ (((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈) ∧ 𝑥 ∈ (𝑆‘𝑈)) ∧ 𝑧 ∈ (^◡𝐹 “ 𝑉)) ∧ (𝑡 ∈ 𝑥 ∧ 𝑧 ∈ 𝑡)) → ∃𝑦 ∈ 𝑥 (𝑡 ∩ (^◡𝐹 “ 𝑉)) = (𝑦 ∩ (^◡𝐹 “ 𝑉)))
51		vex 3478	. . . . . . . . . . . . . . 15 ⊢ 𝑡 ∈ V
52	51	inex1 5316	. . . . . . . . . . . . . 14 ⊢ (𝑡 ∩ (^◡𝐹 “ 𝑉)) ∈ V
53		eqid 2732	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ 𝑥 ↦ (𝑦 ∩ (^◡𝐹 “ 𝑉))) = (𝑦 ∈ 𝑥 ↦ (𝑦 ∩ (^◡𝐹 “ 𝑉)))
54	53	elrnmpt 5953	. . . . . . . . . . . . . 14 ⊢ ((𝑡 ∩ (^◡𝐹 “ 𝑉)) ∈ V → ((𝑡 ∩ (^◡𝐹 “ 𝑉)) ∈ ran (𝑦 ∈ 𝑥 ↦ (𝑦 ∩ (^◡𝐹 “ 𝑉))) ↔ ∃𝑦 ∈ 𝑥 (𝑡 ∩ (^◡𝐹 “ 𝑉)) = (𝑦 ∩ (^◡𝐹 “ 𝑉))))
55	52, 54	ax-mp 5	. . . . . . . . . . . . 13 ⊢ ((𝑡 ∩ (^◡𝐹 “ 𝑉)) ∈ ran (𝑦 ∈ 𝑥 ↦ (𝑦 ∩ (^◡𝐹 “ 𝑉))) ↔ ∃𝑦 ∈ 𝑥 (𝑡 ∩ (^◡𝐹 “ 𝑉)) = (𝑦 ∩ (^◡𝐹 “ 𝑉)))
56	50, 55	sylibr 233	. . . . . . . . . . . 12 ⊢ (((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈) ∧ 𝑥 ∈ (𝑆‘𝑈)) ∧ 𝑧 ∈ (^◡𝐹 “ 𝑉)) ∧ (𝑡 ∈ 𝑥 ∧ 𝑧 ∈ 𝑡)) → (𝑡 ∩ (^◡𝐹 “ 𝑉)) ∈ ran (𝑦 ∈ 𝑥 ↦ (𝑦 ∩ (^◡𝐹 “ 𝑉))))
57		simprr 771	. . . . . . . . . . . . 13 ⊢ (((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈) ∧ 𝑥 ∈ (𝑆‘𝑈)) ∧ 𝑧 ∈ (^◡𝐹 “ 𝑉)) ∧ (𝑡 ∈ 𝑥 ∧ 𝑧 ∈ 𝑡)) → 𝑧 ∈ 𝑡)
58		simplr 767	. . . . . . . . . . . . 13 ⊢ (((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈) ∧ 𝑥 ∈ (𝑆‘𝑈)) ∧ 𝑧 ∈ (^◡𝐹 “ 𝑉)) ∧ (𝑡 ∈ 𝑥 ∧ 𝑧 ∈ 𝑡)) → 𝑧 ∈ (^◡𝐹 “ 𝑉))
59	57, 58	elind 4193	. . . . . . . . . . . 12 ⊢ (((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈) ∧ 𝑥 ∈ (𝑆‘𝑈)) ∧ 𝑧 ∈ (^◡𝐹 “ 𝑉)) ∧ (𝑡 ∈ 𝑥 ∧ 𝑧 ∈ 𝑡)) → 𝑧 ∈ (𝑡 ∩ (^◡𝐹 “ 𝑉)))
60		eleq2 2822	. . . . . . . . . . . . 13 ⊢ (𝑤 = (𝑡 ∩ (^◡𝐹 “ 𝑉)) → (𝑧 ∈ 𝑤 ↔ 𝑧 ∈ (𝑡 ∩ (^◡𝐹 “ 𝑉))))
61	60	rspcev 3612	. . . . . . . . . . . 12 ⊢ (((𝑡 ∩ (^◡𝐹 “ 𝑉)) ∈ ran (𝑦 ∈ 𝑥 ↦ (𝑦 ∩ (^◡𝐹 “ 𝑉))) ∧ 𝑧 ∈ (𝑡 ∩ (^◡𝐹 “ 𝑉))) → ∃𝑤 ∈ ran (𝑦 ∈ 𝑥 ↦ (𝑦 ∩ (^◡𝐹 “ 𝑉)))𝑧 ∈ 𝑤)
62	56, 59, 61	syl2anc 584	. . . . . . . . . . 11 ⊢ (((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈) ∧ 𝑥 ∈ (𝑆‘𝑈)) ∧ 𝑧 ∈ (^◡𝐹 “ 𝑉)) ∧ (𝑡 ∈ 𝑥 ∧ 𝑧 ∈ 𝑡)) → ∃𝑤 ∈ ran (𝑦 ∈ 𝑥 ↦ (𝑦 ∩ (^◡𝐹 “ 𝑉)))𝑧 ∈ 𝑤)
63	62	rexlimdvaa 3156	. . . . . . . . . 10 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈) ∧ 𝑥 ∈ (𝑆‘𝑈)) ∧ 𝑧 ∈ (^◡𝐹 “ 𝑉)) → (∃𝑡 ∈ 𝑥 𝑧 ∈ 𝑡 → ∃𝑤 ∈ ran (𝑦 ∈ 𝑥 ↦ (𝑦 ∩ (^◡𝐹 “ 𝑉)))𝑧 ∈ 𝑤))
64		eluni2 4911	. . . . . . . . . 10 ⊢ (𝑧 ∈ ∪ 𝑥 ↔ ∃𝑡 ∈ 𝑥 𝑧 ∈ 𝑡)
65		eluni2 4911	. . . . . . . . . 10 ⊢ (𝑧 ∈ ∪ ran (𝑦 ∈ 𝑥 ↦ (𝑦 ∩ (^◡𝐹 “ 𝑉))) ↔ ∃𝑤 ∈ ran (𝑦 ∈ 𝑥 ↦ (𝑦 ∩ (^◡𝐹 “ 𝑉)))𝑧 ∈ 𝑤)
66	63, 64, 65	3imtr4g 295	. . . . . . . . 9 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈) ∧ 𝑥 ∈ (𝑆‘𝑈)) ∧ 𝑧 ∈ (^◡𝐹 “ 𝑉)) → (𝑧 ∈ ∪ 𝑥 → 𝑧 ∈ ∪ ran (𝑦 ∈ 𝑥 ↦ (𝑦 ∩ (^◡𝐹 “ 𝑉)))))
67	45, 66	mpd 15	. . . . . . . 8 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈) ∧ 𝑥 ∈ (𝑆‘𝑈)) ∧ 𝑧 ∈ (^◡𝐹 “ 𝑉)) → 𝑧 ∈ ∪ ran (𝑦 ∈ 𝑥 ↦ (𝑦 ∩ (^◡𝐹 “ 𝑉))))
68	38, 67	eqelssd 4002	. . . . . . 7 ⊢ (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈) ∧ 𝑥 ∈ (𝑆‘𝑈)) → ∪ ran (𝑦 ∈ 𝑥 ↦ (𝑦 ∩ (^◡𝐹 “ 𝑉))) = (^◡𝐹 “ 𝑉))
69		eldifsn 4789	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ (ran (𝑦 ∈ 𝑥 ↦ (𝑦 ∩ (^◡𝐹 “ 𝑉))) ∖ {(𝑡 ∩ (^◡𝐹 “ 𝑉))}) ↔ (𝑧 ∈ ran (𝑦 ∈ 𝑥 ↦ (𝑦 ∩ (^◡𝐹 “ 𝑉))) ∧ 𝑧 ≠ (𝑡 ∩ (^◡𝐹 “ 𝑉))))
70		vex 3478	. . . . . . . . . . . . . . 15 ⊢ 𝑧 ∈ V
71	53	elrnmpt 5953	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ∈ V → (𝑧 ∈ ran (𝑦 ∈ 𝑥 ↦ (𝑦 ∩ (^◡𝐹 “ 𝑉))) ↔ ∃𝑦 ∈ 𝑥 𝑧 = (𝑦 ∩ (^◡𝐹 “ 𝑉))))
72	70, 71	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ (𝑧 ∈ ran (𝑦 ∈ 𝑥 ↦ (𝑦 ∩ (^◡𝐹 “ 𝑉))) ↔ ∃𝑦 ∈ 𝑥 𝑧 = (𝑦 ∩ (^◡𝐹 “ 𝑉)))
73	47	equcoms 2023	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 = 𝑦 → (𝑦 ∩ (^◡𝐹 “ 𝑉)) = (𝑡 ∩ (^◡𝐹 “ 𝑉)))
74	73	necon3ai 2965	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑦 ∩ (^◡𝐹 “ 𝑉)) ≠ (𝑡 ∩ (^◡𝐹 “ 𝑉)) → ¬ 𝑡 = 𝑦)
75		simpllr 774	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈) ∧ 𝑥 ∈ (𝑆‘𝑈)) ∧ 𝑡 ∈ 𝑥) ∧ 𝑦 ∈ 𝑥) → 𝑥 ∈ (𝑆‘𝑈))
76		simplr 767	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈) ∧ 𝑥 ∈ (𝑆‘𝑈)) ∧ 𝑡 ∈ 𝑥) ∧ 𝑦 ∈ 𝑥) → 𝑡 ∈ 𝑥)
77		simpr 485	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈) ∧ 𝑥 ∈ (𝑆‘𝑈)) ∧ 𝑡 ∈ 𝑥) ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ 𝑥)
78	7	cvmsdisj 34249	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ (𝑆‘𝑈) ∧ 𝑡 ∈ 𝑥 ∧ 𝑦 ∈ 𝑥) → (𝑡 = 𝑦 ∨ (𝑡 ∩ 𝑦) = ∅))
79	75, 76, 77, 78	syl3anc 1371	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈) ∧ 𝑥 ∈ (𝑆‘𝑈)) ∧ 𝑡 ∈ 𝑥) ∧ 𝑦 ∈ 𝑥) → (𝑡 = 𝑦 ∨ (𝑡 ∩ 𝑦) = ∅))
80	79	ord 862	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈) ∧ 𝑥 ∈ (𝑆‘𝑈)) ∧ 𝑡 ∈ 𝑥) ∧ 𝑦 ∈ 𝑥) → (¬ 𝑡 = 𝑦 → (𝑡 ∩ 𝑦) = ∅))
81		inss1 4227	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑡 ∩ 𝑦) ∩ (^◡𝐹 “ 𝑉)) ⊆ (𝑡 ∩ 𝑦)
82		sseq0 4398	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑡 ∩ 𝑦) ∩ (^◡𝐹 “ 𝑉)) ⊆ (𝑡 ∩ 𝑦) ∧ (𝑡 ∩ 𝑦) = ∅) → ((𝑡 ∩ 𝑦) ∩ (^◡𝐹 “ 𝑉)) = ∅)
83	81, 82	mpan 688	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑡 ∩ 𝑦) = ∅ → ((𝑡 ∩ 𝑦) ∩ (^◡𝐹 “ 𝑉)) = ∅)
84	74, 80, 83	syl56 36	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈) ∧ 𝑥 ∈ (𝑆‘𝑈)) ∧ 𝑡 ∈ 𝑥) ∧ 𝑦 ∈ 𝑥) → ((𝑦 ∩ (^◡𝐹 “ 𝑉)) ≠ (𝑡 ∩ (^◡𝐹 “ 𝑉)) → ((𝑡 ∩ 𝑦) ∩ (^◡𝐹 “ 𝑉)) = ∅))
85		neeq1 3003	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = (𝑦 ∩ (^◡𝐹 “ 𝑉)) → (𝑧 ≠ (𝑡 ∩ (^◡𝐹 “ 𝑉)) ↔ (𝑦 ∩ (^◡𝐹 “ 𝑉)) ≠ (𝑡 ∩ (^◡𝐹 “ 𝑉))))
86		ineq2 4205	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = (𝑦 ∩ (^◡𝐹 “ 𝑉)) → ((𝑡 ∩ (^◡𝐹 “ 𝑉)) ∩ 𝑧) = ((𝑡 ∩ (^◡𝐹 “ 𝑉)) ∩ (𝑦 ∩ (^◡𝐹 “ 𝑉))))
87		inindir 4226	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑡 ∩ 𝑦) ∩ (^◡𝐹 “ 𝑉)) = ((𝑡 ∩ (^◡𝐹 “ 𝑉)) ∩ (𝑦 ∩ (^◡𝐹 “ 𝑉)))
88	86, 87	eqtr4di 2790	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = (𝑦 ∩ (^◡𝐹 “ 𝑉)) → ((𝑡 ∩ (^◡𝐹 “ 𝑉)) ∩ 𝑧) = ((𝑡 ∩ 𝑦) ∩ (^◡𝐹 “ 𝑉)))
89	88	eqeq1d 2734	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = (𝑦 ∩ (^◡𝐹 “ 𝑉)) → (((𝑡 ∩ (^◡𝐹 “ 𝑉)) ∩ 𝑧) = ∅ ↔ ((𝑡 ∩ 𝑦) ∩ (^◡𝐹 “ 𝑉)) = ∅))
90	85, 89	imbi12d 344	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = (𝑦 ∩ (^◡𝐹 “ 𝑉)) → ((𝑧 ≠ (𝑡 ∩ (^◡𝐹 “ 𝑉)) → ((𝑡 ∩ (^◡𝐹 “ 𝑉)) ∩ 𝑧) = ∅) ↔ ((𝑦 ∩ (^◡𝐹 “ 𝑉)) ≠ (𝑡 ∩ (^◡𝐹 “ 𝑉)) → ((𝑡 ∩ 𝑦) ∩ (^◡𝐹 “ 𝑉)) = ∅)))
91	84, 90	syl5ibrcom 246	. . . . . . . . . . . . . . 15 ⊢ (((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈) ∧ 𝑥 ∈ (𝑆‘𝑈)) ∧ 𝑡 ∈ 𝑥) ∧ 𝑦 ∈ 𝑥) → (𝑧 = (𝑦 ∩ (^◡𝐹 “ 𝑉)) → (𝑧 ≠ (𝑡 ∩ (^◡𝐹 “ 𝑉)) → ((𝑡 ∩ (^◡𝐹 “ 𝑉)) ∩ 𝑧) = ∅)))
92	91	rexlimdva 3155	. . . . . . . . . . . . . 14 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈) ∧ 𝑥 ∈ (𝑆‘𝑈)) ∧ 𝑡 ∈ 𝑥) → (∃𝑦 ∈ 𝑥 𝑧 = (𝑦 ∩ (^◡𝐹 “ 𝑉)) → (𝑧 ≠ (𝑡 ∩ (^◡𝐹 “ 𝑉)) → ((𝑡 ∩ (^◡𝐹 “ 𝑉)) ∩ 𝑧) = ∅)))
93	72, 92	biimtrid 241	. . . . . . . . . . . . 13 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈) ∧ 𝑥 ∈ (𝑆‘𝑈)) ∧ 𝑡 ∈ 𝑥) → (𝑧 ∈ ran (𝑦 ∈ 𝑥 ↦ (𝑦 ∩ (^◡𝐹 “ 𝑉))) → (𝑧 ≠ (𝑡 ∩ (^◡𝐹 “ 𝑉)) → ((𝑡 ∩ (^◡𝐹 “ 𝑉)) ∩ 𝑧) = ∅)))
94	93	impd 411	. . . . . . . . . . . 12 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈) ∧ 𝑥 ∈ (𝑆‘𝑈)) ∧ 𝑡 ∈ 𝑥) → ((𝑧 ∈ ran (𝑦 ∈ 𝑥 ↦ (𝑦 ∩ (^◡𝐹 “ 𝑉))) ∧ 𝑧 ≠ (𝑡 ∩ (^◡𝐹 “ 𝑉))) → ((𝑡 ∩ (^◡𝐹 “ 𝑉)) ∩ 𝑧) = ∅))
95	69, 94	biimtrid 241	. . . . . . . . . . 11 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈) ∧ 𝑥 ∈ (𝑆‘𝑈)) ∧ 𝑡 ∈ 𝑥) → (𝑧 ∈ (ran (𝑦 ∈ 𝑥 ↦ (𝑦 ∩ (^◡𝐹 “ 𝑉))) ∖ {(𝑡 ∩ (^◡𝐹 “ 𝑉))}) → ((𝑡 ∩ (^◡𝐹 “ 𝑉)) ∩ 𝑧) = ∅))
96	95	ralrimiv 3145	. . . . . . . . . 10 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈) ∧ 𝑥 ∈ (𝑆‘𝑈)) ∧ 𝑡 ∈ 𝑥) → ∀𝑧 ∈ (ran (𝑦 ∈ 𝑥 ↦ (𝑦 ∩ (^◡𝐹 “ 𝑉))) ∖ {(𝑡 ∩ (^◡𝐹 “ 𝑉))})((𝑡 ∩ (^◡𝐹 “ 𝑉)) ∩ 𝑧) = ∅)
97		inss1 4227	. . . . . . . . . . . . 13 ⊢ (𝑡 ∩ (^◡𝐹 “ 𝑉)) ⊆ 𝑡
98		resabs1 6009	. . . . . . . . . . . . 13 ⊢ ((𝑡 ∩ (^◡𝐹 “ 𝑉)) ⊆ 𝑡 → ((𝐹 ↾ 𝑡) ↾ (𝑡 ∩ (^◡𝐹 “ 𝑉))) = (𝐹 ↾ (𝑡 ∩ (^◡𝐹 “ 𝑉))))
99	97, 98	ax-mp 5	. . . . . . . . . . . 12 ⊢ ((𝐹 ↾ 𝑡) ↾ (𝑡 ∩ (^◡𝐹 “ 𝑉))) = (𝐹 ↾ (𝑡 ∩ (^◡𝐹 “ 𝑉)))
100	7	cvmshmeo 34250	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ (𝑆‘𝑈) ∧ 𝑡 ∈ 𝑥) → (𝐹 ↾ 𝑡) ∈ ((𝐶 ↾_t 𝑡)Homeo(𝐽 ↾_t 𝑈)))
101	100	adantll 712	. . . . . . . . . . . . 13 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈) ∧ 𝑥 ∈ (𝑆‘𝑈)) ∧ 𝑡 ∈ 𝑥) → (𝐹 ↾ 𝑡) ∈ ((𝐶 ↾_t 𝑡)Homeo(𝐽 ↾_t 𝑈)))
102	5	adantr 481	. . . . . . . . . . . . . . 15 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈) ∧ 𝑥 ∈ (𝑆‘𝑈)) ∧ 𝑡 ∈ 𝑥) → 𝐶 ∈ Top)
103	9	sselda 3981	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈) ∧ 𝑥 ∈ (𝑆‘𝑈)) ∧ 𝑡 ∈ 𝑥) → 𝑡 ∈ 𝐶)
104		elssuni 4940	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 ∈ 𝐶 → 𝑡 ⊆ ∪ 𝐶)
105	103, 104	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈) ∧ 𝑥 ∈ (𝑆‘𝑈)) ∧ 𝑡 ∈ 𝑥) → 𝑡 ⊆ ∪ 𝐶)
106		eqid 2732	. . . . . . . . . . . . . . . 16 ⊢ ∪ 𝐶 = ∪ 𝐶
107	106	restuni 22657	. . . . . . . . . . . . . . 15 ⊢ ((𝐶 ∈ Top ∧ 𝑡 ⊆ ∪ 𝐶) → 𝑡 = ∪ (𝐶 ↾_t 𝑡))
108	102, 105, 107	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈) ∧ 𝑥 ∈ (𝑆‘𝑈)) ∧ 𝑡 ∈ 𝑥) → 𝑡 = ∪ (𝐶 ↾_t 𝑡))
109	97, 108	sseqtrid 4033	. . . . . . . . . . . . 13 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈) ∧ 𝑥 ∈ (𝑆‘𝑈)) ∧ 𝑡 ∈ 𝑥) → (𝑡 ∩ (^◡𝐹 “ 𝑉)) ⊆ ∪ (𝐶 ↾_t 𝑡))
110		eqid 2732	. . . . . . . . . . . . . 14 ⊢ ∪ (𝐶 ↾_t 𝑡) = ∪ (𝐶 ↾_t 𝑡)
111	110	hmeores 23266	. . . . . . . . . . . . 13 ⊢ (((𝐹 ↾ 𝑡) ∈ ((𝐶 ↾_t 𝑡)Homeo(𝐽 ↾_t 𝑈)) ∧ (𝑡 ∩ (^◡𝐹 “ 𝑉)) ⊆ ∪ (𝐶 ↾_t 𝑡)) → ((𝐹 ↾ 𝑡) ↾ (𝑡 ∩ (^◡𝐹 “ 𝑉))) ∈ (((𝐶 ↾_t 𝑡) ↾_t (𝑡 ∩ (^◡𝐹 “ 𝑉)))Homeo((𝐽 ↾_t 𝑈) ↾_t ((𝐹 ↾ 𝑡) “ (𝑡 ∩ (^◡𝐹 “ 𝑉))))))
112	101, 109, 111	syl2anc 584	. . . . . . . . . . . 12 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈) ∧ 𝑥 ∈ (𝑆‘𝑈)) ∧ 𝑡 ∈ 𝑥) → ((𝐹 ↾ 𝑡) ↾ (𝑡 ∩ (^◡𝐹 “ 𝑉))) ∈ (((𝐶 ↾_t 𝑡) ↾_t (𝑡 ∩ (^◡𝐹 “ 𝑉)))Homeo((𝐽 ↾_t 𝑈) ↾_t ((𝐹 ↾ 𝑡) “ (𝑡 ∩ (^◡𝐹 “ 𝑉))))))
113	99, 112	eqeltrrid 2838	. . . . . . . . . . 11 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈) ∧ 𝑥 ∈ (𝑆‘𝑈)) ∧ 𝑡 ∈ 𝑥) → (𝐹 ↾ (𝑡 ∩ (^◡𝐹 “ 𝑉))) ∈ (((𝐶 ↾_t 𝑡) ↾_t (𝑡 ∩ (^◡𝐹 “ 𝑉)))Homeo((𝐽 ↾_t 𝑈) ↾_t ((𝐹 ↾ 𝑡) “ (𝑡 ∩ (^◡𝐹 “ 𝑉))))))
114	97	a1i 11	. . . . . . . . . . . . 13 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈) ∧ 𝑥 ∈ (𝑆‘𝑈)) ∧ 𝑡 ∈ 𝑥) → (𝑡 ∩ (^◡𝐹 “ 𝑉)) ⊆ 𝑡)
115		simpr 485	. . . . . . . . . . . . 13 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈) ∧ 𝑥 ∈ (𝑆‘𝑈)) ∧ 𝑡 ∈ 𝑥) → 𝑡 ∈ 𝑥)
116		restabs 22660	. . . . . . . . . . . . 13 ⊢ ((𝐶 ∈ Top ∧ (𝑡 ∩ (^◡𝐹 “ 𝑉)) ⊆ 𝑡 ∧ 𝑡 ∈ 𝑥) → ((𝐶 ↾_t 𝑡) ↾_t (𝑡 ∩ (^◡𝐹 “ 𝑉))) = (𝐶 ↾_t (𝑡 ∩ (^◡𝐹 “ 𝑉))))
117	102, 114, 115, 116	syl3anc 1371	. . . . . . . . . . . 12 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈) ∧ 𝑥 ∈ (𝑆‘𝑈)) ∧ 𝑡 ∈ 𝑥) → ((𝐶 ↾_t 𝑡) ↾_t (𝑡 ∩ (^◡𝐹 “ 𝑉))) = (𝐶 ↾_t (𝑡 ∩ (^◡𝐹 “ 𝑉))))
118		incom 4200	. . . . . . . . . . . . . . . . 17 ⊢ (𝑡 ∩ (^◡𝐹 “ 𝑉)) = ((^◡𝐹 “ 𝑉) ∩ 𝑡)
119		cnvresima 6226	. . . . . . . . . . . . . . . . 17 ⊢ (^◡(𝐹 ↾ 𝑡) “ 𝑉) = ((^◡𝐹 “ 𝑉) ∩ 𝑡)
120	118, 119	eqtr4i 2763	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 ∩ (^◡𝐹 “ 𝑉)) = (^◡(𝐹 ↾ 𝑡) “ 𝑉)
121	120	imaeq2i 6055	. . . . . . . . . . . . . . 15 ⊢ ((𝐹 ↾ 𝑡) “ (𝑡 ∩ (^◡𝐹 “ 𝑉))) = ((𝐹 ↾ 𝑡) “ (^◡(𝐹 ↾ 𝑡) “ 𝑉))
122	3	adantr 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈) ∧ 𝑥 ∈ (𝑆‘𝑈)) ∧ 𝑡 ∈ 𝑥) → 𝐹 ∈ (𝐶 CovMap 𝐽))
123		simplr 767	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈) ∧ 𝑥 ∈ (𝑆‘𝑈)) ∧ 𝑡 ∈ 𝑥) → 𝑥 ∈ (𝑆‘𝑈))
124	7	cvmsf1o 34251	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑥 ∈ (𝑆‘𝑈) ∧ 𝑡 ∈ 𝑥) → (𝐹 ↾ 𝑡):𝑡–1-1-onto→𝑈)
125	122, 123, 115, 124	syl3anc 1371	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈) ∧ 𝑥 ∈ (𝑆‘𝑈)) ∧ 𝑡 ∈ 𝑥) → (𝐹 ↾ 𝑡):𝑡–1-1-onto→𝑈)
126		f1ofo 6837	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹 ↾ 𝑡):𝑡–1-1-onto→𝑈 → (𝐹 ↾ 𝑡):𝑡–onto→𝑈)
127	125, 126	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈) ∧ 𝑥 ∈ (𝑆‘𝑈)) ∧ 𝑡 ∈ 𝑥) → (𝐹 ↾ 𝑡):𝑡–onto→𝑈)
128	39	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈) ∧ 𝑥 ∈ (𝑆‘𝑈)) ∧ 𝑡 ∈ 𝑥) → 𝑉 ⊆ 𝑈)
129		foimacnv 6847	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹 ↾ 𝑡):𝑡–onto→𝑈 ∧ 𝑉 ⊆ 𝑈) → ((𝐹 ↾ 𝑡) “ (^◡(𝐹 ↾ 𝑡) “ 𝑉)) = 𝑉)
130	127, 128, 129	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈) ∧ 𝑥 ∈ (𝑆‘𝑈)) ∧ 𝑡 ∈ 𝑥) → ((𝐹 ↾ 𝑡) “ (^◡(𝐹 ↾ 𝑡) “ 𝑉)) = 𝑉)
131	121, 130	eqtrid 2784	. . . . . . . . . . . . . 14 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈) ∧ 𝑥 ∈ (𝑆‘𝑈)) ∧ 𝑡 ∈ 𝑥) → ((𝐹 ↾ 𝑡) “ (𝑡 ∩ (^◡𝐹 “ 𝑉))) = 𝑉)
132	131	oveq2d 7421	. . . . . . . . . . . . 13 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈) ∧ 𝑥 ∈ (𝑆‘𝑈)) ∧ 𝑡 ∈ 𝑥) → ((𝐽 ↾_t 𝑈) ↾_t ((𝐹 ↾ 𝑡) “ (𝑡 ∩ (^◡𝐹 “ 𝑉)))) = ((𝐽 ↾_t 𝑈) ↾_t 𝑉))
133		cvmtop2 34240	. . . . . . . . . . . . . . . 16 ⊢ (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐽 ∈ Top)
134	3, 133	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈) ∧ 𝑥 ∈ (𝑆‘𝑈)) → 𝐽 ∈ Top)
135	7	cvmsrcl 34243	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (𝑆‘𝑈) → 𝑈 ∈ 𝐽)
136	135	adantl 482	. . . . . . . . . . . . . . 15 ⊢ (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈) ∧ 𝑥 ∈ (𝑆‘𝑈)) → 𝑈 ∈ 𝐽)
137		restabs 22660	. . . . . . . . . . . . . . 15 ⊢ ((𝐽 ∈ Top ∧ 𝑉 ⊆ 𝑈 ∧ 𝑈 ∈ 𝐽) → ((𝐽 ↾_t 𝑈) ↾_t 𝑉) = (𝐽 ↾_t 𝑉))
138	134, 39, 136, 137	syl3anc 1371	. . . . . . . . . . . . . 14 ⊢ (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈) ∧ 𝑥 ∈ (𝑆‘𝑈)) → ((𝐽 ↾_t 𝑈) ↾_t 𝑉) = (𝐽 ↾_t 𝑉))
139	138	adantr 481	. . . . . . . . . . . . 13 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈) ∧ 𝑥 ∈ (𝑆‘𝑈)) ∧ 𝑡 ∈ 𝑥) → ((𝐽 ↾_t 𝑈) ↾_t 𝑉) = (𝐽 ↾_t 𝑉))
140	132, 139	eqtrd 2772	. . . . . . . . . . . 12 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈) ∧ 𝑥 ∈ (𝑆‘𝑈)) ∧ 𝑡 ∈ 𝑥) → ((𝐽 ↾_t 𝑈) ↾_t ((𝐹 ↾ 𝑡) “ (𝑡 ∩ (^◡𝐹 “ 𝑉)))) = (𝐽 ↾_t 𝑉))
141	117, 140	oveq12d 7423	. . . . . . . . . . 11 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈) ∧ 𝑥 ∈ (𝑆‘𝑈)) ∧ 𝑡 ∈ 𝑥) → (((𝐶 ↾_t 𝑡) ↾_t (𝑡 ∩ (^◡𝐹 “ 𝑉)))Homeo((𝐽 ↾_t 𝑈) ↾_t ((𝐹 ↾ 𝑡) “ (𝑡 ∩ (^◡𝐹 “ 𝑉))))) = ((𝐶 ↾_t (𝑡 ∩ (^◡𝐹 “ 𝑉)))Homeo(𝐽 ↾_t 𝑉)))
142	113, 141	eleqtrd 2835	. . . . . . . . . 10 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈) ∧ 𝑥 ∈ (𝑆‘𝑈)) ∧ 𝑡 ∈ 𝑥) → (𝐹 ↾ (𝑡 ∩ (^◡𝐹 “ 𝑉))) ∈ ((𝐶 ↾_t (𝑡 ∩ (^◡𝐹 “ 𝑉)))Homeo(𝐽 ↾_t 𝑉)))
143	96, 142	jca 512	. . . . . . . . 9 ⊢ ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈) ∧ 𝑥 ∈ (𝑆‘𝑈)) ∧ 𝑡 ∈ 𝑥) → (∀𝑧 ∈ (ran (𝑦 ∈ 𝑥 ↦ (𝑦 ∩ (^◡𝐹 “ 𝑉))) ∖ {(𝑡 ∩ (^◡𝐹 “ 𝑉))})((𝑡 ∩ (^◡𝐹 “ 𝑉)) ∩ 𝑧) = ∅ ∧ (𝐹 ↾ (𝑡 ∩ (^◡𝐹 “ 𝑉))) ∈ ((𝐶 ↾_t (𝑡 ∩ (^◡𝐹 “ 𝑉)))Homeo(𝐽 ↾_t 𝑉))))
144	143	ralrimiva 3146	. . . . . . . 8 ⊢ (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈) ∧ 𝑥 ∈ (𝑆‘𝑈)) → ∀𝑡 ∈ 𝑥 (∀𝑧 ∈ (ran (𝑦 ∈ 𝑥 ↦ (𝑦 ∩ (^◡𝐹 “ 𝑉))) ∖ {(𝑡 ∩ (^◡𝐹 “ 𝑉))})((𝑡 ∩ (^◡𝐹 “ 𝑉)) ∩ 𝑧) = ∅ ∧ (𝐹 ↾ (𝑡 ∩ (^◡𝐹 “ 𝑉))) ∈ ((𝐶 ↾_t (𝑡 ∩ (^◡𝐹 “ 𝑉)))Homeo(𝐽 ↾_t 𝑉))))
145	52	rgenw 3065	. . . . . . . . 9 ⊢ ∀𝑡 ∈ 𝑥 (𝑡 ∩ (^◡𝐹 “ 𝑉)) ∈ V
146	47	cbvmptv 5260	. . . . . . . . . 10 ⊢ (𝑦 ∈ 𝑥 ↦ (𝑦 ∩ (^◡𝐹 “ 𝑉))) = (𝑡 ∈ 𝑥 ↦ (𝑡 ∩ (^◡𝐹 “ 𝑉)))
147		sneq 4637	. . . . . . . . . . . . 13 ⊢ (𝑤 = (𝑡 ∩ (^◡𝐹 “ 𝑉)) → {𝑤} = {(𝑡 ∩ (^◡𝐹 “ 𝑉))})
148	147	difeq2d 4121	. . . . . . . . . . . 12 ⊢ (𝑤 = (𝑡 ∩ (^◡𝐹 “ 𝑉)) → (ran (𝑦 ∈ 𝑥 ↦ (𝑦 ∩ (^◡𝐹 “ 𝑉))) ∖ {𝑤}) = (ran (𝑦 ∈ 𝑥 ↦ (𝑦 ∩ (^◡𝐹 “ 𝑉))) ∖ {(𝑡 ∩ (^◡𝐹 “ 𝑉))}))
149		ineq1 4204	. . . . . . . . . . . . 13 ⊢ (𝑤 = (𝑡 ∩ (^◡𝐹 “ 𝑉)) → (𝑤 ∩ 𝑧) = ((𝑡 ∩ (^◡𝐹 “ 𝑉)) ∩ 𝑧))
150	149	eqeq1d 2734	. . . . . . . . . . . 12 ⊢ (𝑤 = (𝑡 ∩ (^◡𝐹 “ 𝑉)) → ((𝑤 ∩ 𝑧) = ∅ ↔ ((𝑡 ∩ (^◡𝐹 “ 𝑉)) ∩ 𝑧) = ∅))
151	148, 150	raleqbidv 3342	. . . . . . . . . . 11 ⊢ (𝑤 = (𝑡 ∩ (^◡𝐹 “ 𝑉)) → (∀𝑧 ∈ (ran (𝑦 ∈ 𝑥 ↦ (𝑦 ∩ (^◡𝐹 “ 𝑉))) ∖ {𝑤})(𝑤 ∩ 𝑧) = ∅ ↔ ∀𝑧 ∈ (ran (𝑦 ∈ 𝑥 ↦ (𝑦 ∩ (^◡𝐹 “ 𝑉))) ∖ {(𝑡 ∩ (^◡𝐹 “ 𝑉))})((𝑡 ∩ (^◡𝐹 “ 𝑉)) ∩ 𝑧) = ∅))
152		reseq2 5974	. . . . . . . . . . . 12 ⊢ (𝑤 = (𝑡 ∩ (^◡𝐹 “ 𝑉)) → (𝐹 ↾ 𝑤) = (𝐹 ↾ (𝑡 ∩ (^◡𝐹 “ 𝑉))))
153		oveq2 7413	. . . . . . . . . . . . 13 ⊢ (𝑤 = (𝑡 ∩ (^◡𝐹 “ 𝑉)) → (𝐶 ↾_t 𝑤) = (𝐶 ↾_t (𝑡 ∩ (^◡𝐹 “ 𝑉))))
154	153	oveq1d 7420	. . . . . . . . . . . 12 ⊢ (𝑤 = (𝑡 ∩ (^◡𝐹 “ 𝑉)) → ((𝐶 ↾_t 𝑤)Homeo(𝐽 ↾_t 𝑉)) = ((𝐶 ↾_t (𝑡 ∩ (^◡𝐹 “ 𝑉)))Homeo(𝐽 ↾_t 𝑉)))
155	152, 154	eleq12d 2827	. . . . . . . . . . 11 ⊢ (𝑤 = (𝑡 ∩ (^◡𝐹 “ 𝑉)) → ((𝐹 ↾ 𝑤) ∈ ((𝐶 ↾_t 𝑤)Homeo(𝐽 ↾_t 𝑉)) ↔ (𝐹 ↾ (𝑡 ∩ (^◡𝐹 “ 𝑉))) ∈ ((𝐶 ↾_t (𝑡 ∩ (^◡𝐹 “ 𝑉)))Homeo(𝐽 ↾_t 𝑉))))
156	151, 155	anbi12d 631	. . . . . . . . . 10 ⊢ (𝑤 = (𝑡 ∩ (^◡𝐹 “ 𝑉)) → ((∀𝑧 ∈ (ran (𝑦 ∈ 𝑥 ↦ (𝑦 ∩ (^◡𝐹 “ 𝑉))) ∖ {𝑤})(𝑤 ∩ 𝑧) = ∅ ∧ (𝐹 ↾ 𝑤) ∈ ((𝐶 ↾_t 𝑤)Homeo(𝐽 ↾_t 𝑉))) ↔ (∀𝑧 ∈ (ran (𝑦 ∈ 𝑥 ↦ (𝑦 ∩ (^◡𝐹 “ 𝑉))) ∖ {(𝑡 ∩ (^◡𝐹 “ 𝑉))})((𝑡 ∩ (^◡𝐹 “ 𝑉)) ∩ 𝑧) = ∅ ∧ (𝐹 ↾ (𝑡 ∩ (^◡𝐹 “ 𝑉))) ∈ ((𝐶 ↾_t (𝑡 ∩ (^◡𝐹 “ 𝑉)))Homeo(𝐽 ↾_t 𝑉)))))
157	146, 156	ralrnmptw 7092	. . . . . . . . 9 ⊢ (∀𝑡 ∈ 𝑥 (𝑡 ∩ (^◡𝐹 “ 𝑉)) ∈ V → (∀𝑤 ∈ ran (𝑦 ∈ 𝑥 ↦ (𝑦 ∩ (^◡𝐹 “ 𝑉)))(∀𝑧 ∈ (ran (𝑦 ∈ 𝑥 ↦ (𝑦 ∩ (^◡𝐹 “ 𝑉))) ∖ {𝑤})(𝑤 ∩ 𝑧) = ∅ ∧ (𝐹 ↾ 𝑤) ∈ ((𝐶 ↾_t 𝑤)Homeo(𝐽 ↾_t 𝑉))) ↔ ∀𝑡 ∈ 𝑥 (∀𝑧 ∈ (ran (𝑦 ∈ 𝑥 ↦ (𝑦 ∩ (^◡𝐹 “ 𝑉))) ∖ {(𝑡 ∩ (^◡𝐹 “ 𝑉))})((𝑡 ∩ (^◡𝐹 “ 𝑉)) ∩ 𝑧) = ∅ ∧ (𝐹 ↾ (𝑡 ∩ (^◡𝐹 “ 𝑉))) ∈ ((𝐶 ↾_t (𝑡 ∩ (^◡𝐹 “ 𝑉)))Homeo(𝐽 ↾_t 𝑉)))))
158	145, 157	ax-mp 5	. . . . . . . 8 ⊢ (∀𝑤 ∈ ran (𝑦 ∈ 𝑥 ↦ (𝑦 ∩ (^◡𝐹 “ 𝑉)))(∀𝑧 ∈ (ran (𝑦 ∈ 𝑥 ↦ (𝑦 ∩ (^◡𝐹 “ 𝑉))) ∖ {𝑤})(𝑤 ∩ 𝑧) = ∅ ∧ (𝐹 ↾ 𝑤) ∈ ((𝐶 ↾_t 𝑤)Homeo(𝐽 ↾_t 𝑉))) ↔ ∀𝑡 ∈ 𝑥 (∀𝑧 ∈ (ran (𝑦 ∈ 𝑥 ↦ (𝑦 ∩ (^◡𝐹 “ 𝑉))) ∖ {(𝑡 ∩ (^◡𝐹 “ 𝑉))})((𝑡 ∩ (^◡𝐹 “ 𝑉)) ∩ 𝑧) = ∅ ∧ (𝐹 ↾ (𝑡 ∩ (^◡𝐹 “ 𝑉))) ∈ ((𝐶 ↾_t (𝑡 ∩ (^◡𝐹 “ 𝑉)))Homeo(𝐽 ↾_t 𝑉))))
159	144, 158	sylibr 233	. . . . . . 7 ⊢ (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈) ∧ 𝑥 ∈ (𝑆‘𝑈)) → ∀𝑤 ∈ ran (𝑦 ∈ 𝑥 ↦ (𝑦 ∩ (^◡𝐹 “ 𝑉)))(∀𝑧 ∈ (ran (𝑦 ∈ 𝑥 ↦ (𝑦 ∩ (^◡𝐹 “ 𝑉))) ∖ {𝑤})(𝑤 ∩ 𝑧) = ∅ ∧ (𝐹 ↾ 𝑤) ∈ ((𝐶 ↾_t 𝑤)Homeo(𝐽 ↾_t 𝑉))))
160	68, 159	jca 512	. . . . . 6 ⊢ (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈) ∧ 𝑥 ∈ (𝑆‘𝑈)) → (∪ ran (𝑦 ∈ 𝑥 ↦ (𝑦 ∩ (^◡𝐹 “ 𝑉))) = (^◡𝐹 “ 𝑉) ∧ ∀𝑤 ∈ ran (𝑦 ∈ 𝑥 ↦ (𝑦 ∩ (^◡𝐹 “ 𝑉)))(∀𝑧 ∈ (ran (𝑦 ∈ 𝑥 ↦ (𝑦 ∩ (^◡𝐹 “ 𝑉))) ∖ {𝑤})(𝑤 ∩ 𝑧) = ∅ ∧ (𝐹 ↾ 𝑤) ∈ ((𝐶 ↾_t 𝑤)Homeo(𝐽 ↾_t 𝑉)))))
161	7	cvmscbv 34237	. . . . . . . 8 ⊢ 𝑆 = (𝑎 ∈ 𝐽 ↦ {𝑏 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑏 = (^◡𝐹 “ 𝑎) ∧ ∀𝑤 ∈ 𝑏 (∀𝑧 ∈ (𝑏 ∖ {𝑤})(𝑤 ∩ 𝑧) = ∅ ∧ (𝐹 ↾ 𝑤) ∈ ((𝐶 ↾_t 𝑤)Homeo(𝐽 ↾_t 𝑎))))})
162	161	cvmsval 34245	. . . . . . 7 ⊢ (𝐶 ∈ Top → (ran (𝑦 ∈ 𝑥 ↦ (𝑦 ∩ (^◡𝐹 “ 𝑉))) ∈ (𝑆‘𝑉) ↔ (𝑉 ∈ 𝐽 ∧ (ran (𝑦 ∈ 𝑥 ↦ (𝑦 ∩ (^◡𝐹 “ 𝑉))) ⊆ 𝐶 ∧ ran (𝑦 ∈ 𝑥 ↦ (𝑦 ∩ (^◡𝐹 “ 𝑉))) ≠ ∅) ∧ (∪ ran (𝑦 ∈ 𝑥 ↦ (𝑦 ∩ (^◡𝐹 “ 𝑉))) = (^◡𝐹 “ 𝑉) ∧ ∀𝑤 ∈ ran (𝑦 ∈ 𝑥 ↦ (𝑦 ∩ (^◡𝐹 “ 𝑉)))(∀𝑧 ∈ (ran (𝑦 ∈ 𝑥 ↦ (𝑦 ∩ (^◡𝐹 “ 𝑉))) ∖ {𝑤})(𝑤 ∩ 𝑧) = ∅ ∧ (𝐹 ↾ 𝑤) ∈ ((𝐶 ↾_t 𝑤)Homeo(𝐽 ↾_t 𝑉)))))))
163	5, 162	syl 17	. . . . . 6 ⊢ (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈) ∧ 𝑥 ∈ (𝑆‘𝑈)) → (ran (𝑦 ∈ 𝑥 ↦ (𝑦 ∩ (^◡𝐹 “ 𝑉))) ∈ (𝑆‘𝑉) ↔ (𝑉 ∈ 𝐽 ∧ (ran (𝑦 ∈ 𝑥 ↦ (𝑦 ∩ (^◡𝐹 “ 𝑉))) ⊆ 𝐶 ∧ ran (𝑦 ∈ 𝑥 ↦ (𝑦 ∩ (^◡𝐹 “ 𝑉))) ≠ ∅) ∧ (∪ ran (𝑦 ∈ 𝑥 ↦ (𝑦 ∩ (^◡𝐹 “ 𝑉))) = (^◡𝐹 “ 𝑉) ∧ ∀𝑤 ∈ ran (𝑦 ∈ 𝑥 ↦ (𝑦 ∩ (^◡𝐹 “ 𝑉)))(∀𝑧 ∈ (ran (𝑦 ∈ 𝑥 ↦ (𝑦 ∩ (^◡𝐹 “ 𝑉))) ∖ {𝑤})(𝑤 ∩ 𝑧) = ∅ ∧ (𝐹 ↾ 𝑤) ∈ ((𝐶 ↾_t 𝑤)Homeo(𝐽 ↾_t 𝑉)))))))
164	2, 30, 160, 163	mpbir3and 1342	. . . . 5 ⊢ (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈) ∧ 𝑥 ∈ (𝑆‘𝑈)) → ran (𝑦 ∈ 𝑥 ↦ (𝑦 ∩ (^◡𝐹 “ 𝑉))) ∈ (𝑆‘𝑉))
165	164	ne0d 4334	. . . 4 ⊢ (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈) ∧ 𝑥 ∈ (𝑆‘𝑈)) → (𝑆‘𝑉) ≠ ∅)
166	165	ex 413	. . 3 ⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈) → (𝑥 ∈ (𝑆‘𝑈) → (𝑆‘𝑉) ≠ ∅))
167	166	exlimdv 1936	. 2 ⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈) → (∃𝑥 𝑥 ∈ (𝑆‘𝑈) → (𝑆‘𝑉) ≠ ∅))
168	1, 167	biimtrid 241	1 ⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈) → ((𝑆‘𝑈) ≠ ∅ → (𝑆‘𝑉) ≠ ∅))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 396 ∨ wo 845 ∧ w3a 1087 = wceq 1541 ∃wex 1781 ∈ wcel 2106 ≠ wne 2940 ∀wral 3061 ∃wrex 3070 {crab 3432 Vcvv 3474 ∖ cdif 3944 ∩ cin 3946 ⊆ wss 3947 ∅c0 4321 𝒫 cpw 4601 {csn 4627 ∪ cuni 4907 ↦ cmpt 5230 ^◡ccnv 5674 dom cdm 5675 ran crn 5676 ↾ cres 5677 “ cima 5678 –onto→wfo 6538 –1-1-onto→wf1o 6539 ‘cfv 6540 (class class class)co 7405 ↾_t crest 17362 Topctop 22386 Cn ccn 22719 Homeochmeo 23248 CovMap ccvm 34234

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 5284 ax-sep 5298 ax-nul 5305 ax-pow 5362 ax-pr 5426 ax-un 7721

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-reu 3377 df-rab 3433 df-v 3476 df-sbc 3777 df-csb 3893 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-pss 3966 df-nul 4322 df-if 4528 df-pw 4603 df-sn 4628 df-pr 4630 df-op 4634 df-uni 4908 df-int 4950 df-iun 4998 df-br 5148 df-opab 5210 df-mpt 5231 df-tr 5265 df-id 5573 df-eprel 5579 df-po 5587 df-so 5588 df-fr 5630 df-we 5632 df-xp 5681 df-rel 5682 df-cnv 5683 df-co 5684 df-dm 5685 df-rn 5686 df-res 5687 df-ima 5688 df-ord 6364 df-on 6365 df-lim 6366 df-suc 6367 df-iota 6492 df-fun 6542 df-fn 6543 df-f 6544 df-f1 6545 df-fo 6546 df-f1o 6547 df-fv 6548 df-ov 7408 df-oprab 7409 df-mpo 7410 df-om 7852 df-1st 7971 df-2nd 7972 df-map 8818 df-en 8936 df-fin 8939 df-fi 9402 df-rest 17364 df-topgen 17385 df-top 22387 df-topon 22404 df-bases 22440 df-cn 22722 df-hmeo 23250 df-cvm 34235

This theorem is referenced by: cvmcov2 34254

W3C validator