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

Theorem cvmsss2 32418
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.
StepHypRef Expression
1 n0 4307 . 2 ((𝑆𝑈) ≠ ∅ ↔ ∃𝑥 𝑥 ∈ (𝑆𝑈))
2 simpl2 1184 . . . . . 6 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → 𝑉𝐽)
3 simpl1 1183 . . . . . . . . . . . 12 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → 𝐹 ∈ (𝐶 CovMap 𝐽))
4 cvmtop1 32404 . . . . . . . . . . . 12 (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐶 ∈ Top)
53, 4syl 17 . . . . . . . . . . 11 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → 𝐶 ∈ Top)
65adantr 481 . . . . . . . . . 10 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑦𝑥) → 𝐶 ∈ Top)
7 cvmcov.1 . . . . . . . . . . . . 13 𝑆 = (𝑘𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ ( 𝑠 = (𝐹𝑘) ∧ ∀𝑢𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢𝑣) = ∅ ∧ (𝐹𝑢) ∈ ((𝐶t 𝑢)Homeo(𝐽t 𝑘))))})
87cvmsss 32411 . . . . . . . . . . . 12 (𝑥 ∈ (𝑆𝑈) → 𝑥𝐶)
98adantl 482 . . . . . . . . . . 11 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → 𝑥𝐶)
109sselda 3964 . . . . . . . . . 10 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑦𝑥) → 𝑦𝐶)
11 cvmcn 32406 . . . . . . . . . . . . 13 (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐹 ∈ (𝐶 Cn 𝐽))
123, 11syl 17 . . . . . . . . . . . 12 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → 𝐹 ∈ (𝐶 Cn 𝐽))
13 cnima 21801 . . . . . . . . . . . 12 ((𝐹 ∈ (𝐶 Cn 𝐽) ∧ 𝑉𝐽) → (𝐹𝑉) ∈ 𝐶)
1412, 2, 13syl2anc 584 . . . . . . . . . . 11 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → (𝐹𝑉) ∈ 𝐶)
1514adantr 481 . . . . . . . . . 10 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑦𝑥) → (𝐹𝑉) ∈ 𝐶)
16 inopn 21435 . . . . . . . . . 10 ((𝐶 ∈ Top ∧ 𝑦𝐶 ∧ (𝐹𝑉) ∈ 𝐶) → (𝑦 ∩ (𝐹𝑉)) ∈ 𝐶)
176, 10, 15, 16syl3anc 1363 . . . . . . . . 9 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑦𝑥) → (𝑦 ∩ (𝐹𝑉)) ∈ 𝐶)
1817fmpttd 6871 . . . . . . . 8 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))):𝑥𝐶)
1918frnd 6514 . . . . . . 7 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ⊆ 𝐶)
207cvmsn0 32412 . . . . . . . . 9 (𝑥 ∈ (𝑆𝑈) → 𝑥 ≠ ∅)
2120adantl 482 . . . . . . . 8 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → 𝑥 ≠ ∅)
22 dmmptg 6089 . . . . . . . . . . . 12 (∀𝑦𝑥 (𝑦 ∩ (𝐹𝑉)) ∈ V → dom (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) = 𝑥)
23 inex1g 5214 . . . . . . . . . . . 12 (𝑦𝑥 → (𝑦 ∩ (𝐹𝑉)) ∈ V)
2422, 23mprg 3149 . . . . . . . . . . 11 dom (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) = 𝑥
2524eqeq1i 2823 . . . . . . . . . 10 (dom (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) = ∅ ↔ 𝑥 = ∅)
26 dm0rn0 5788 . . . . . . . . . 10 (dom (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) = ∅ ↔ ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) = ∅)
2725, 26bitr3i 278 . . . . . . . . 9 (𝑥 = ∅ ↔ ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) = ∅)
2827necon3bii 3065 . . . . . . . 8 (𝑥 ≠ ∅ ↔ ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ≠ ∅)
2921, 28sylib 219 . . . . . . 7 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ≠ ∅)
3019, 29jca 512 . . . . . 6 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → (ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ⊆ 𝐶 ∧ ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ≠ ∅))
31 inss2 4203 . . . . . . . . . . . 12 (𝑦 ∩ (𝐹𝑉)) ⊆ (𝐹𝑉)
32 elpw2g 5238 . . . . . . . . . . . . 13 ((𝐹𝑉) ∈ 𝐶 → ((𝑦 ∩ (𝐹𝑉)) ∈ 𝒫 (𝐹𝑉) ↔ (𝑦 ∩ (𝐹𝑉)) ⊆ (𝐹𝑉)))
3315, 32syl 17 . . . . . . . . . . . 12 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑦𝑥) → ((𝑦 ∩ (𝐹𝑉)) ∈ 𝒫 (𝐹𝑉) ↔ (𝑦 ∩ (𝐹𝑉)) ⊆ (𝐹𝑉)))
3431, 33mpbiri 259 . . . . . . . . . . 11 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑦𝑥) → (𝑦 ∩ (𝐹𝑉)) ∈ 𝒫 (𝐹𝑉))
3534fmpttd 6871 . . . . . . . . . 10 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))):𝑥⟶𝒫 (𝐹𝑉))
3635frnd 6514 . . . . . . . . 9 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ⊆ 𝒫 (𝐹𝑉))
37 sspwuni 5013 . . . . . . . . 9 (ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ⊆ 𝒫 (𝐹𝑉) ↔ ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ⊆ (𝐹𝑉))
3836, 37sylib 219 . . . . . . . 8 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ⊆ (𝐹𝑉))
39 simpl3 1185 . . . . . . . . . . . 12 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → 𝑉𝑈)
40 imass2 5958 . . . . . . . . . . . 12 (𝑉𝑈 → (𝐹𝑉) ⊆ (𝐹𝑈))
4139, 40syl 17 . . . . . . . . . . 11 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → (𝐹𝑉) ⊆ (𝐹𝑈))
427cvmsuni 32413 . . . . . . . . . . . 12 (𝑥 ∈ (𝑆𝑈) → 𝑥 = (𝐹𝑈))
4342adantl 482 . . . . . . . . . . 11 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → 𝑥 = (𝐹𝑈))
4441, 43sseqtrrd 4005 . . . . . . . . . 10 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → (𝐹𝑉) ⊆ 𝑥)
4544sselda 3964 . . . . . . . . 9 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑧 ∈ (𝐹𝑉)) → 𝑧 𝑥)
46 eqid 2818 . . . . . . . . . . . . . . 15 (𝑡 ∩ (𝐹𝑉)) = (𝑡 ∩ (𝐹𝑉))
47 ineq1 4178 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑡 → (𝑦 ∩ (𝐹𝑉)) = (𝑡 ∩ (𝐹𝑉)))
4847rspceeqv 3635 . . . . . . . . . . . . . . 15 ((𝑡𝑥 ∧ (𝑡 ∩ (𝐹𝑉)) = (𝑡 ∩ (𝐹𝑉))) → ∃𝑦𝑥 (𝑡 ∩ (𝐹𝑉)) = (𝑦 ∩ (𝐹𝑉)))
4946, 48mpan2 687 . . . . . . . . . . . . . 14 (𝑡𝑥 → ∃𝑦𝑥 (𝑡 ∩ (𝐹𝑉)) = (𝑦 ∩ (𝐹𝑉)))
5049ad2antrl 724 . . . . . . . . . . . . 13 (((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑧 ∈ (𝐹𝑉)) ∧ (𝑡𝑥𝑧𝑡)) → ∃𝑦𝑥 (𝑡 ∩ (𝐹𝑉)) = (𝑦 ∩ (𝐹𝑉)))
51 vex 3495 . . . . . . . . . . . . . . 15 𝑡 ∈ V
5251inex1 5212 . . . . . . . . . . . . . 14 (𝑡 ∩ (𝐹𝑉)) ∈ V
53 eqid 2818 . . . . . . . . . . . . . . 15 (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) = (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉)))
5453elrnmpt 5821 . . . . . . . . . . . . . 14 ((𝑡 ∩ (𝐹𝑉)) ∈ V → ((𝑡 ∩ (𝐹𝑉)) ∈ ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ↔ ∃𝑦𝑥 (𝑡 ∩ (𝐹𝑉)) = (𝑦 ∩ (𝐹𝑉))))
5552, 54ax-mp 5 . . . . . . . . . . . . 13 ((𝑡 ∩ (𝐹𝑉)) ∈ ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ↔ ∃𝑦𝑥 (𝑡 ∩ (𝐹𝑉)) = (𝑦 ∩ (𝐹𝑉)))
5650, 55sylibr 235 . . . . . . . . . . . 12 (((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑧 ∈ (𝐹𝑉)) ∧ (𝑡𝑥𝑧𝑡)) → (𝑡 ∩ (𝐹𝑉)) ∈ ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))))
57 simprr 769 . . . . . . . . . . . . 13 (((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑧 ∈ (𝐹𝑉)) ∧ (𝑡𝑥𝑧𝑡)) → 𝑧𝑡)
58 simplr 765 . . . . . . . . . . . . 13 (((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑧 ∈ (𝐹𝑉)) ∧ (𝑡𝑥𝑧𝑡)) → 𝑧 ∈ (𝐹𝑉))
5957, 58elind 4168 . . . . . . . . . . . 12 (((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑧 ∈ (𝐹𝑉)) ∧ (𝑡𝑥𝑧𝑡)) → 𝑧 ∈ (𝑡 ∩ (𝐹𝑉)))
60 eleq2 2898 . . . . . . . . . . . . 13 (𝑤 = (𝑡 ∩ (𝐹𝑉)) → (𝑧𝑤𝑧 ∈ (𝑡 ∩ (𝐹𝑉))))
6160rspcev 3620 . . . . . . . . . . . 12 (((𝑡 ∩ (𝐹𝑉)) ∈ ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ∧ 𝑧 ∈ (𝑡 ∩ (𝐹𝑉))) → ∃𝑤 ∈ ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉)))𝑧𝑤)
6256, 59, 61syl2anc 584 . . . . . . . . . . 11 (((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑧 ∈ (𝐹𝑉)) ∧ (𝑡𝑥𝑧𝑡)) → ∃𝑤 ∈ ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉)))𝑧𝑤)
6362rexlimdvaa 3282 . . . . . . . . . 10 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑧 ∈ (𝐹𝑉)) → (∃𝑡𝑥 𝑧𝑡 → ∃𝑤 ∈ ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉)))𝑧𝑤))
64 eluni2 4834 . . . . . . . . . 10 (𝑧 𝑥 ↔ ∃𝑡𝑥 𝑧𝑡)
65 eluni2 4834 . . . . . . . . . 10 (𝑧 ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ↔ ∃𝑤 ∈ ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉)))𝑧𝑤)
6663, 64, 653imtr4g 297 . . . . . . . . 9 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑧 ∈ (𝐹𝑉)) → (𝑧 𝑥𝑧 ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉)))))
6745, 66mpd 15 . . . . . . . 8 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑧 ∈ (𝐹𝑉)) → 𝑧 ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))))
6838, 67eqelssd 3985 . . . . . . 7 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) = (𝐹𝑉))
69 eldifsn 4711 . . . . . . . . . . . 12 (𝑧 ∈ (ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ∖ {(𝑡 ∩ (𝐹𝑉))}) ↔ (𝑧 ∈ ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ∧ 𝑧 ≠ (𝑡 ∩ (𝐹𝑉))))
70 vex 3495 . . . . . . . . . . . . . . 15 𝑧 ∈ V
7153elrnmpt 5821 . . . . . . . . . . . . . . 15 (𝑧 ∈ V → (𝑧 ∈ ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ↔ ∃𝑦𝑥 𝑧 = (𝑦 ∩ (𝐹𝑉))))
7270, 71ax-mp 5 . . . . . . . . . . . . . 14 (𝑧 ∈ ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ↔ ∃𝑦𝑥 𝑧 = (𝑦 ∩ (𝐹𝑉)))
7347equcoms 2018 . . . . . . . . . . . . . . . . . 18 (𝑡 = 𝑦 → (𝑦 ∩ (𝐹𝑉)) = (𝑡 ∩ (𝐹𝑉)))
7473necon3ai 3038 . . . . . . . . . . . . . . . . 17 ((𝑦 ∩ (𝐹𝑉)) ≠ (𝑡 ∩ (𝐹𝑉)) → ¬ 𝑡 = 𝑦)
75 simpllr 772 . . . . . . . . . . . . . . . . . . 19 (((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) ∧ 𝑦𝑥) → 𝑥 ∈ (𝑆𝑈))
76 simplr 765 . . . . . . . . . . . . . . . . . . 19 (((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) ∧ 𝑦𝑥) → 𝑡𝑥)
77 simpr 485 . . . . . . . . . . . . . . . . . . 19 (((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) ∧ 𝑦𝑥) → 𝑦𝑥)
787cvmsdisj 32414 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ (𝑆𝑈) ∧ 𝑡𝑥𝑦𝑥) → (𝑡 = 𝑦 ∨ (𝑡𝑦) = ∅))
7975, 76, 77, 78syl3anc 1363 . . . . . . . . . . . . . . . . . 18 (((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) ∧ 𝑦𝑥) → (𝑡 = 𝑦 ∨ (𝑡𝑦) = ∅))
8079ord 858 . . . . . . . . . . . . . . . . 17 (((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) ∧ 𝑦𝑥) → (¬ 𝑡 = 𝑦 → (𝑡𝑦) = ∅))
81 inss1 4202 . . . . . . . . . . . . . . . . . 18 ((𝑡𝑦) ∩ (𝐹𝑉)) ⊆ (𝑡𝑦)
82 sseq0 4350 . . . . . . . . . . . . . . . . . 18 ((((𝑡𝑦) ∩ (𝐹𝑉)) ⊆ (𝑡𝑦) ∧ (𝑡𝑦) = ∅) → ((𝑡𝑦) ∩ (𝐹𝑉)) = ∅)
8381, 82mpan 686 . . . . . . . . . . . . . . . . 17 ((𝑡𝑦) = ∅ → ((𝑡𝑦) ∩ (𝐹𝑉)) = ∅)
8474, 80, 83syl56 36 . . . . . . . . . . . . . . . 16 (((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) ∧ 𝑦𝑥) → ((𝑦 ∩ (𝐹𝑉)) ≠ (𝑡 ∩ (𝐹𝑉)) → ((𝑡𝑦) ∩ (𝐹𝑉)) = ∅))
85 neeq1 3075 . . . . . . . . . . . . . . . . 17 (𝑧 = (𝑦 ∩ (𝐹𝑉)) → (𝑧 ≠ (𝑡 ∩ (𝐹𝑉)) ↔ (𝑦 ∩ (𝐹𝑉)) ≠ (𝑡 ∩ (𝐹𝑉))))
86 ineq2 4180 . . . . . . . . . . . . . . . . . . 19 (𝑧 = (𝑦 ∩ (𝐹𝑉)) → ((𝑡 ∩ (𝐹𝑉)) ∩ 𝑧) = ((𝑡 ∩ (𝐹𝑉)) ∩ (𝑦 ∩ (𝐹𝑉))))
87 inindir 4201 . . . . . . . . . . . . . . . . . . 19 ((𝑡𝑦) ∩ (𝐹𝑉)) = ((𝑡 ∩ (𝐹𝑉)) ∩ (𝑦 ∩ (𝐹𝑉)))
8886, 87syl6eqr 2871 . . . . . . . . . . . . . . . . . 18 (𝑧 = (𝑦 ∩ (𝐹𝑉)) → ((𝑡 ∩ (𝐹𝑉)) ∩ 𝑧) = ((𝑡𝑦) ∩ (𝐹𝑉)))
8988eqeq1d 2820 . . . . . . . . . . . . . . . . 17 (𝑧 = (𝑦 ∩ (𝐹𝑉)) → (((𝑡 ∩ (𝐹𝑉)) ∩ 𝑧) = ∅ ↔ ((𝑡𝑦) ∩ (𝐹𝑉)) = ∅))
9085, 89imbi12d 346 . . . . . . . . . . . . . . . 16 (𝑧 = (𝑦 ∩ (𝐹𝑉)) → ((𝑧 ≠ (𝑡 ∩ (𝐹𝑉)) → ((𝑡 ∩ (𝐹𝑉)) ∩ 𝑧) = ∅) ↔ ((𝑦 ∩ (𝐹𝑉)) ≠ (𝑡 ∩ (𝐹𝑉)) → ((𝑡𝑦) ∩ (𝐹𝑉)) = ∅)))
9184, 90syl5ibrcom 248 . . . . . . . . . . . . . . 15 (((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) ∧ 𝑦𝑥) → (𝑧 = (𝑦 ∩ (𝐹𝑉)) → (𝑧 ≠ (𝑡 ∩ (𝐹𝑉)) → ((𝑡 ∩ (𝐹𝑉)) ∩ 𝑧) = ∅)))
9291rexlimdva 3281 . . . . . . . . . . . . . 14 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → (∃𝑦𝑥 𝑧 = (𝑦 ∩ (𝐹𝑉)) → (𝑧 ≠ (𝑡 ∩ (𝐹𝑉)) → ((𝑡 ∩ (𝐹𝑉)) ∩ 𝑧) = ∅)))
9372, 92syl5bi 243 . . . . . . . . . . . . 13 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → (𝑧 ∈ ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) → (𝑧 ≠ (𝑡 ∩ (𝐹𝑉)) → ((𝑡 ∩ (𝐹𝑉)) ∩ 𝑧) = ∅)))
9493impd 411 . . . . . . . . . . . 12 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → ((𝑧 ∈ ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ∧ 𝑧 ≠ (𝑡 ∩ (𝐹𝑉))) → ((𝑡 ∩ (𝐹𝑉)) ∩ 𝑧) = ∅))
9569, 94syl5bi 243 . . . . . . . . . . 11 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → (𝑧 ∈ (ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ∖ {(𝑡 ∩ (𝐹𝑉))}) → ((𝑡 ∩ (𝐹𝑉)) ∩ 𝑧) = ∅))
9695ralrimiv 3178 . . . . . . . . . 10 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → ∀𝑧 ∈ (ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ∖ {(𝑡 ∩ (𝐹𝑉))})((𝑡 ∩ (𝐹𝑉)) ∩ 𝑧) = ∅)
97 inss1 4202 . . . . . . . . . . . . 13 (𝑡 ∩ (𝐹𝑉)) ⊆ 𝑡
98 resabs1 5876 . . . . . . . . . . . . 13 ((𝑡 ∩ (𝐹𝑉)) ⊆ 𝑡 → ((𝐹𝑡) ↾ (𝑡 ∩ (𝐹𝑉))) = (𝐹 ↾ (𝑡 ∩ (𝐹𝑉))))
9997, 98ax-mp 5 . . . . . . . . . . . 12 ((𝐹𝑡) ↾ (𝑡 ∩ (𝐹𝑉))) = (𝐹 ↾ (𝑡 ∩ (𝐹𝑉)))
1007cvmshmeo 32415 . . . . . . . . . . . . . 14 ((𝑥 ∈ (𝑆𝑈) ∧ 𝑡𝑥) → (𝐹𝑡) ∈ ((𝐶t 𝑡)Homeo(𝐽t 𝑈)))
101100adantll 710 . . . . . . . . . . . . 13 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → (𝐹𝑡) ∈ ((𝐶t 𝑡)Homeo(𝐽t 𝑈)))
1025adantr 481 . . . . . . . . . . . . . . 15 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → 𝐶 ∈ Top)
1039sselda 3964 . . . . . . . . . . . . . . . 16 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → 𝑡𝐶)
104 elssuni 4859 . . . . . . . . . . . . . . . 16 (𝑡𝐶𝑡 𝐶)
105103, 104syl 17 . . . . . . . . . . . . . . 15 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → 𝑡 𝐶)
106 eqid 2818 . . . . . . . . . . . . . . . 16 𝐶 = 𝐶
107106restuni 21698 . . . . . . . . . . . . . . 15 ((𝐶 ∈ Top ∧ 𝑡 𝐶) → 𝑡 = (𝐶t 𝑡))
108102, 105, 107syl2anc 584 . . . . . . . . . . . . . 14 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → 𝑡 = (𝐶t 𝑡))
10997, 108sseqtrid 4016 . . . . . . . . . . . . 13 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → (𝑡 ∩ (𝐹𝑉)) ⊆ (𝐶t 𝑡))
110 eqid 2818 . . . . . . . . . . . . . 14 (𝐶t 𝑡) = (𝐶t 𝑡)
111110hmeores 22307 . . . . . . . . . . . . 13 (((𝐹𝑡) ∈ ((𝐶t 𝑡)Homeo(𝐽t 𝑈)) ∧ (𝑡 ∩ (𝐹𝑉)) ⊆ (𝐶t 𝑡)) → ((𝐹𝑡) ↾ (𝑡 ∩ (𝐹𝑉))) ∈ (((𝐶t 𝑡) ↾t (𝑡 ∩ (𝐹𝑉)))Homeo((𝐽t 𝑈) ↾t ((𝐹𝑡) “ (𝑡 ∩ (𝐹𝑉))))))
112101, 109, 111syl2anc 584 . . . . . . . . . . . 12 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → ((𝐹𝑡) ↾ (𝑡 ∩ (𝐹𝑉))) ∈ (((𝐶t 𝑡) ↾t (𝑡 ∩ (𝐹𝑉)))Homeo((𝐽t 𝑈) ↾t ((𝐹𝑡) “ (𝑡 ∩ (𝐹𝑉))))))
11399, 112eqeltrrid 2915 . . . . . . . . . . 11 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → (𝐹 ↾ (𝑡 ∩ (𝐹𝑉))) ∈ (((𝐶t 𝑡) ↾t (𝑡 ∩ (𝐹𝑉)))Homeo((𝐽t 𝑈) ↾t ((𝐹𝑡) “ (𝑡 ∩ (𝐹𝑉))))))
11497a1i 11 . . . . . . . . . . . . 13 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → (𝑡 ∩ (𝐹𝑉)) ⊆ 𝑡)
115 simpr 485 . . . . . . . . . . . . 13 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → 𝑡𝑥)
116 restabs 21701 . . . . . . . . . . . . 13 ((𝐶 ∈ Top ∧ (𝑡 ∩ (𝐹𝑉)) ⊆ 𝑡𝑡𝑥) → ((𝐶t 𝑡) ↾t (𝑡 ∩ (𝐹𝑉))) = (𝐶t (𝑡 ∩ (𝐹𝑉))))
117102, 114, 115, 116syl3anc 1363 . . . . . . . . . . . 12 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → ((𝐶t 𝑡) ↾t (𝑡 ∩ (𝐹𝑉))) = (𝐶t (𝑡 ∩ (𝐹𝑉))))
118 incom 4175 . . . . . . . . . . . . . . . . 17 (𝑡 ∩ (𝐹𝑉)) = ((𝐹𝑉) ∩ 𝑡)
119 cnvresima 6080 . . . . . . . . . . . . . . . . 17 ((𝐹𝑡) “ 𝑉) = ((𝐹𝑉) ∩ 𝑡)
120118, 119eqtr4i 2844 . . . . . . . . . . . . . . . 16 (𝑡 ∩ (𝐹𝑉)) = ((𝐹𝑡) “ 𝑉)
121120imaeq2i 5920 . . . . . . . . . . . . . . 15 ((𝐹𝑡) “ (𝑡 ∩ (𝐹𝑉))) = ((𝐹𝑡) “ ((𝐹𝑡) “ 𝑉))
1223adantr 481 . . . . . . . . . . . . . . . . . 18 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → 𝐹 ∈ (𝐶 CovMap 𝐽))
123 simplr 765 . . . . . . . . . . . . . . . . . 18 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → 𝑥 ∈ (𝑆𝑈))
1247cvmsf1o 32416 . . . . . . . . . . . . . . . . . 18 ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑥 ∈ (𝑆𝑈) ∧ 𝑡𝑥) → (𝐹𝑡):𝑡1-1-onto𝑈)
125122, 123, 115, 124syl3anc 1363 . . . . . . . . . . . . . . . . 17 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → (𝐹𝑡):𝑡1-1-onto𝑈)
126 f1ofo 6615 . . . . . . . . . . . . . . . . 17 ((𝐹𝑡):𝑡1-1-onto𝑈 → (𝐹𝑡):𝑡onto𝑈)
127125, 126syl 17 . . . . . . . . . . . . . . . 16 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → (𝐹𝑡):𝑡onto𝑈)
12839adantr 481 . . . . . . . . . . . . . . . 16 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → 𝑉𝑈)
129 foimacnv 6625 . . . . . . . . . . . . . . . 16 (((𝐹𝑡):𝑡onto𝑈𝑉𝑈) → ((𝐹𝑡) “ ((𝐹𝑡) “ 𝑉)) = 𝑉)
130127, 128, 129syl2anc 584 . . . . . . . . . . . . . . 15 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → ((𝐹𝑡) “ ((𝐹𝑡) “ 𝑉)) = 𝑉)
131121, 130syl5eq 2865 . . . . . . . . . . . . . 14 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → ((𝐹𝑡) “ (𝑡 ∩ (𝐹𝑉))) = 𝑉)
132131oveq2d 7161 . . . . . . . . . . . . 13 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → ((𝐽t 𝑈) ↾t ((𝐹𝑡) “ (𝑡 ∩ (𝐹𝑉)))) = ((𝐽t 𝑈) ↾t 𝑉))
133 cvmtop2 32405 . . . . . . . . . . . . . . . 16 (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐽 ∈ Top)
1343, 133syl 17 . . . . . . . . . . . . . . 15 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → 𝐽 ∈ Top)
1357cvmsrcl 32408 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (𝑆𝑈) → 𝑈𝐽)
136135adantl 482 . . . . . . . . . . . . . . 15 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → 𝑈𝐽)
137 restabs 21701 . . . . . . . . . . . . . . 15 ((𝐽 ∈ Top ∧ 𝑉𝑈𝑈𝐽) → ((𝐽t 𝑈) ↾t 𝑉) = (𝐽t 𝑉))
138134, 39, 136, 137syl3anc 1363 . . . . . . . . . . . . . 14 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → ((𝐽t 𝑈) ↾t 𝑉) = (𝐽t 𝑉))
139138adantr 481 . . . . . . . . . . . . 13 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → ((𝐽t 𝑈) ↾t 𝑉) = (𝐽t 𝑉))
140132, 139eqtrd 2853 . . . . . . . . . . . 12 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → ((𝐽t 𝑈) ↾t ((𝐹𝑡) “ (𝑡 ∩ (𝐹𝑉)))) = (𝐽t 𝑉))
141117, 140oveq12d 7163 . . . . . . . . . . 11 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → (((𝐶t 𝑡) ↾t (𝑡 ∩ (𝐹𝑉)))Homeo((𝐽t 𝑈) ↾t ((𝐹𝑡) “ (𝑡 ∩ (𝐹𝑉))))) = ((𝐶t (𝑡 ∩ (𝐹𝑉)))Homeo(𝐽t 𝑉)))
142113, 141eleqtrd 2912 . . . . . . . . . 10 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → (𝐹 ↾ (𝑡 ∩ (𝐹𝑉))) ∈ ((𝐶t (𝑡 ∩ (𝐹𝑉)))Homeo(𝐽t 𝑉)))
14396, 142jca 512 . . . . . . . . 9 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → (∀𝑧 ∈ (ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ∖ {(𝑡 ∩ (𝐹𝑉))})((𝑡 ∩ (𝐹𝑉)) ∩ 𝑧) = ∅ ∧ (𝐹 ↾ (𝑡 ∩ (𝐹𝑉))) ∈ ((𝐶t (𝑡 ∩ (𝐹𝑉)))Homeo(𝐽t 𝑉))))
144143ralrimiva 3179 . . . . . . . 8 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → ∀𝑡𝑥 (∀𝑧 ∈ (ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ∖ {(𝑡 ∩ (𝐹𝑉))})((𝑡 ∩ (𝐹𝑉)) ∩ 𝑧) = ∅ ∧ (𝐹 ↾ (𝑡 ∩ (𝐹𝑉))) ∈ ((𝐶t (𝑡 ∩ (𝐹𝑉)))Homeo(𝐽t 𝑉))))
14552rgenw 3147 . . . . . . . . 9 𝑡𝑥 (𝑡 ∩ (𝐹𝑉)) ∈ V
14647cbvmptv 5160 . . . . . . . . . 10 (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) = (𝑡𝑥 ↦ (𝑡 ∩ (𝐹𝑉)))
147 sneq 4567 . . . . . . . . . . . . 13 (𝑤 = (𝑡 ∩ (𝐹𝑉)) → {𝑤} = {(𝑡 ∩ (𝐹𝑉))})
148147difeq2d 4096 . . . . . . . . . . . 12 (𝑤 = (𝑡 ∩ (𝐹𝑉)) → (ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ∖ {𝑤}) = (ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ∖ {(𝑡 ∩ (𝐹𝑉))}))
149 ineq1 4178 . . . . . . . . . . . . 13 (𝑤 = (𝑡 ∩ (𝐹𝑉)) → (𝑤𝑧) = ((𝑡 ∩ (𝐹𝑉)) ∩ 𝑧))
150149eqeq1d 2820 . . . . . . . . . . . 12 (𝑤 = (𝑡 ∩ (𝐹𝑉)) → ((𝑤𝑧) = ∅ ↔ ((𝑡 ∩ (𝐹𝑉)) ∩ 𝑧) = ∅))
151148, 150raleqbidv 3399 . . . . . . . . . . 11 (𝑤 = (𝑡 ∩ (𝐹𝑉)) → (∀𝑧 ∈ (ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ∖ {𝑤})(𝑤𝑧) = ∅ ↔ ∀𝑧 ∈ (ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ∖ {(𝑡 ∩ (𝐹𝑉))})((𝑡 ∩ (𝐹𝑉)) ∩ 𝑧) = ∅))
152 reseq2 5841 . . . . . . . . . . . 12 (𝑤 = (𝑡 ∩ (𝐹𝑉)) → (𝐹𝑤) = (𝐹 ↾ (𝑡 ∩ (𝐹𝑉))))
153 oveq2 7153 . . . . . . . . . . . . 13 (𝑤 = (𝑡 ∩ (𝐹𝑉)) → (𝐶t 𝑤) = (𝐶t (𝑡 ∩ (𝐹𝑉))))
154153oveq1d 7160 . . . . . . . . . . . 12 (𝑤 = (𝑡 ∩ (𝐹𝑉)) → ((𝐶t 𝑤)Homeo(𝐽t 𝑉)) = ((𝐶t (𝑡 ∩ (𝐹𝑉)))Homeo(𝐽t 𝑉)))
155152, 154eleq12d 2904 . . . . . . . . . . 11 (𝑤 = (𝑡 ∩ (𝐹𝑉)) → ((𝐹𝑤) ∈ ((𝐶t 𝑤)Homeo(𝐽t 𝑉)) ↔ (𝐹 ↾ (𝑡 ∩ (𝐹𝑉))) ∈ ((𝐶t (𝑡 ∩ (𝐹𝑉)))Homeo(𝐽t 𝑉))))
156151, 155anbi12d 630 . . . . . . . . . 10 (𝑤 = (𝑡 ∩ (𝐹𝑉)) → ((∀𝑧 ∈ (ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ∖ {𝑤})(𝑤𝑧) = ∅ ∧ (𝐹𝑤) ∈ ((𝐶t 𝑤)Homeo(𝐽t 𝑉))) ↔ (∀𝑧 ∈ (ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ∖ {(𝑡 ∩ (𝐹𝑉))})((𝑡 ∩ (𝐹𝑉)) ∩ 𝑧) = ∅ ∧ (𝐹 ↾ (𝑡 ∩ (𝐹𝑉))) ∈ ((𝐶t (𝑡 ∩ (𝐹𝑉)))Homeo(𝐽t 𝑉)))))
157146, 156ralrnmptw 6852 . . . . . . . . 9 (∀𝑡𝑥 (𝑡 ∩ (𝐹𝑉)) ∈ V → (∀𝑤 ∈ ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉)))(∀𝑧 ∈ (ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ∖ {𝑤})(𝑤𝑧) = ∅ ∧ (𝐹𝑤) ∈ ((𝐶t 𝑤)Homeo(𝐽t 𝑉))) ↔ ∀𝑡𝑥 (∀𝑧 ∈ (ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ∖ {(𝑡 ∩ (𝐹𝑉))})((𝑡 ∩ (𝐹𝑉)) ∩ 𝑧) = ∅ ∧ (𝐹 ↾ (𝑡 ∩ (𝐹𝑉))) ∈ ((𝐶t (𝑡 ∩ (𝐹𝑉)))Homeo(𝐽t 𝑉)))))
158145, 157ax-mp 5 . . . . . . . 8 (∀𝑤 ∈ ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉)))(∀𝑧 ∈ (ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ∖ {𝑤})(𝑤𝑧) = ∅ ∧ (𝐹𝑤) ∈ ((𝐶t 𝑤)Homeo(𝐽t 𝑉))) ↔ ∀𝑡𝑥 (∀𝑧 ∈ (ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ∖ {(𝑡 ∩ (𝐹𝑉))})((𝑡 ∩ (𝐹𝑉)) ∩ 𝑧) = ∅ ∧ (𝐹 ↾ (𝑡 ∩ (𝐹𝑉))) ∈ ((𝐶t (𝑡 ∩ (𝐹𝑉)))Homeo(𝐽t 𝑉))))
159144, 158sylibr 235 . . . . . . 7 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → ∀𝑤 ∈ ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉)))(∀𝑧 ∈ (ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ∖ {𝑤})(𝑤𝑧) = ∅ ∧ (𝐹𝑤) ∈ ((𝐶t 𝑤)Homeo(𝐽t 𝑉))))
16068, 159jca 512 . . . . . 6 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → ( ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) = (𝐹𝑉) ∧ ∀𝑤 ∈ ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉)))(∀𝑧 ∈ (ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ∖ {𝑤})(𝑤𝑧) = ∅ ∧ (𝐹𝑤) ∈ ((𝐶t 𝑤)Homeo(𝐽t 𝑉)))))
1617cvmscbv 32402 . . . . . . . 8 𝑆 = (𝑎𝐽 ↦ {𝑏 ∈ (𝒫 𝐶 ∖ {∅}) ∣ ( 𝑏 = (𝐹𝑎) ∧ ∀𝑤𝑏 (∀𝑧 ∈ (𝑏 ∖ {𝑤})(𝑤𝑧) = ∅ ∧ (𝐹𝑤) ∈ ((𝐶t 𝑤)Homeo(𝐽t 𝑎))))})
162161cvmsval 32410 . . . . . . 7 (𝐶 ∈ Top → (ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ∈ (𝑆𝑉) ↔ (𝑉𝐽 ∧ (ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ⊆ 𝐶 ∧ ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ≠ ∅) ∧ ( ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) = (𝐹𝑉) ∧ ∀𝑤 ∈ ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉)))(∀𝑧 ∈ (ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ∖ {𝑤})(𝑤𝑧) = ∅ ∧ (𝐹𝑤) ∈ ((𝐶t 𝑤)Homeo(𝐽t 𝑉)))))))
1635, 162syl 17 . . . . . 6 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → (ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ∈ (𝑆𝑉) ↔ (𝑉𝐽 ∧ (ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ⊆ 𝐶 ∧ ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ≠ ∅) ∧ ( ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) = (𝐹𝑉) ∧ ∀𝑤 ∈ ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉)))(∀𝑧 ∈ (ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ∖ {𝑤})(𝑤𝑧) = ∅ ∧ (𝐹𝑤) ∈ ((𝐶t 𝑤)Homeo(𝐽t 𝑉)))))))
1642, 30, 160, 163mpbir3and 1334 . . . . 5 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ∈ (𝑆𝑉))
165164ne0d 4298 . . . 4 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → (𝑆𝑉) ≠ ∅)
166165ex 413 . . 3 ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) → (𝑥 ∈ (𝑆𝑈) → (𝑆𝑉) ≠ ∅))
167166exlimdv 1925 . 2 ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) → (∃𝑥 𝑥 ∈ (𝑆𝑈) → (𝑆𝑉) ≠ ∅))
1681, 167syl5bi 243 1 ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) → ((𝑆𝑈) ≠ ∅ → (𝑆𝑉) ≠ ∅))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207  wa 396  wo 841  w3a 1079   = wceq 1528  wex 1771  wcel 2105  wne 3013  wral 3135  wrex 3136  {crab 3139  Vcvv 3492  cdif 3930  cin 3932  wss 3933  c0 4288  𝒫 cpw 4535  {csn 4557   cuni 4830  cmpt 5137  ccnv 5547  dom cdm 5548  ran crn 5549  cres 5550  cima 5551  ontowfo 6346  1-1-ontowf1o 6347  cfv 6348  (class class class)co 7145  t crest 16682  Topctop 21429   Cn ccn 21760  Homeochmeo 22289   CovMap ccvm 32399
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-rep 5181  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7450
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ne 3014  df-ral 3140  df-rex 3141  df-reu 3142  df-rab 3144  df-v 3494  df-sbc 3770  df-csb 3881  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-pss 3951  df-nul 4289  df-if 4464  df-pw 4537  df-sn 4558  df-pr 4560  df-tp 4562  df-op 4564  df-uni 4831  df-int 4868  df-iun 4912  df-br 5058  df-opab 5120  df-mpt 5138  df-tr 5164  df-id 5453  df-eprel 5458  df-po 5467  df-so 5468  df-fr 5507  df-we 5509  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-pred 6141  df-ord 6187  df-on 6188  df-lim 6189  df-suc 6190  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-ov 7148  df-oprab 7149  df-mpo 7150  df-om 7570  df-1st 7678  df-2nd 7679  df-wrecs 7936  df-recs 7997  df-rdg 8035  df-oadd 8095  df-er 8278  df-map 8397  df-en 8498  df-fin 8501  df-fi 8863  df-rest 16684  df-topgen 16705  df-top 21430  df-topon 21447  df-bases 21482  df-cn 21763  df-hmeo 22291  df-cvm 32400
This theorem is referenced by:  cvmcov2  32419
  Copyright terms: Public domain W3C validator