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 33868
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 4306 . 2 ((𝑆𝑈) ≠ ∅ ↔ ∃𝑥 𝑥 ∈ (𝑆𝑈))
2 simpl2 1192 . . . . . 6 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → 𝑉𝐽)
3 simpl1 1191 . . . . . . . . . . . 12 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → 𝐹 ∈ (𝐶 CovMap 𝐽))
4 cvmtop1 33854 . . . . . . . . . . . 12 (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐶 ∈ Top)
53, 4syl 17 . . . . . . . . . . 11 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → 𝐶 ∈ Top)
65adantr 481 . . . . . . . . . 10 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑦𝑥) → 𝐶 ∈ Top)
7 cvmcov.1 . . . . . . . . . . . . 13 𝑆 = (𝑘𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ ( 𝑠 = (𝐹𝑘) ∧ ∀𝑢𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢𝑣) = ∅ ∧ (𝐹𝑢) ∈ ((𝐶t 𝑢)Homeo(𝐽t 𝑘))))})
87cvmsss 33861 . . . . . . . . . . . 12 (𝑥 ∈ (𝑆𝑈) → 𝑥𝐶)
98adantl 482 . . . . . . . . . . 11 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → 𝑥𝐶)
109sselda 3944 . . . . . . . . . 10 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑦𝑥) → 𝑦𝐶)
11 cvmcn 33856 . . . . . . . . . . . . 13 (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐹 ∈ (𝐶 Cn 𝐽))
123, 11syl 17 . . . . . . . . . . . 12 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → 𝐹 ∈ (𝐶 Cn 𝐽))
13 cnima 22616 . . . . . . . . . . . 12 ((𝐹 ∈ (𝐶 Cn 𝐽) ∧ 𝑉𝐽) → (𝐹𝑉) ∈ 𝐶)
1412, 2, 13syl2anc 584 . . . . . . . . . . 11 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → (𝐹𝑉) ∈ 𝐶)
1514adantr 481 . . . . . . . . . 10 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑦𝑥) → (𝐹𝑉) ∈ 𝐶)
16 inopn 22248 . . . . . . . . . 10 ((𝐶 ∈ Top ∧ 𝑦𝐶 ∧ (𝐹𝑉) ∈ 𝐶) → (𝑦 ∩ (𝐹𝑉)) ∈ 𝐶)
176, 10, 15, 16syl3anc 1371 . . . . . . . . 9 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑦𝑥) → (𝑦 ∩ (𝐹𝑉)) ∈ 𝐶)
1817fmpttd 7063 . . . . . . . 8 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))):𝑥𝐶)
1918frnd 6676 . . . . . . 7 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ⊆ 𝐶)
207cvmsn0 33862 . . . . . . . . 9 (𝑥 ∈ (𝑆𝑈) → 𝑥 ≠ ∅)
2120adantl 482 . . . . . . . 8 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → 𝑥 ≠ ∅)
22 dmmptg 6194 . . . . . . . . . . . 12 (∀𝑦𝑥 (𝑦 ∩ (𝐹𝑉)) ∈ V → dom (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) = 𝑥)
23 inex1g 5276 . . . . . . . . . . . 12 (𝑦𝑥 → (𝑦 ∩ (𝐹𝑉)) ∈ V)
2422, 23mprg 3070 . . . . . . . . . . 11 dom (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) = 𝑥
2524eqeq1i 2741 . . . . . . . . . 10 (dom (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) = ∅ ↔ 𝑥 = ∅)
26 dm0rn0 5880 . . . . . . . . . 10 (dom (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) = ∅ ↔ ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) = ∅)
2725, 26bitr3i 276 . . . . . . . . 9 (𝑥 = ∅ ↔ ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) = ∅)
2827necon3bii 2996 . . . . . . . 8 (𝑥 ≠ ∅ ↔ ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ≠ ∅)
2921, 28sylib 217 . . . . . . 7 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ≠ ∅)
3019, 29jca 512 . . . . . 6 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → (ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ⊆ 𝐶 ∧ ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ≠ ∅))
31 inss2 4189 . . . . . . . . . . . 12 (𝑦 ∩ (𝐹𝑉)) ⊆ (𝐹𝑉)
32 elpw2g 5301 . . . . . . . . . . . . 13 ((𝐹𝑉) ∈ 𝐶 → ((𝑦 ∩ (𝐹𝑉)) ∈ 𝒫 (𝐹𝑉) ↔ (𝑦 ∩ (𝐹𝑉)) ⊆ (𝐹𝑉)))
3315, 32syl 17 . . . . . . . . . . . 12 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑦𝑥) → ((𝑦 ∩ (𝐹𝑉)) ∈ 𝒫 (𝐹𝑉) ↔ (𝑦 ∩ (𝐹𝑉)) ⊆ (𝐹𝑉)))
3431, 33mpbiri 257 . . . . . . . . . . 11 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑦𝑥) → (𝑦 ∩ (𝐹𝑉)) ∈ 𝒫 (𝐹𝑉))
3534fmpttd 7063 . . . . . . . . . 10 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))):𝑥⟶𝒫 (𝐹𝑉))
3635frnd 6676 . . . . . . . . 9 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ⊆ 𝒫 (𝐹𝑉))
37 sspwuni 5060 . . . . . . . . 9 (ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ⊆ 𝒫 (𝐹𝑉) ↔ ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ⊆ (𝐹𝑉))
3836, 37sylib 217 . . . . . . . 8 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ⊆ (𝐹𝑉))
39 simpl3 1193 . . . . . . . . . . . 12 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → 𝑉𝑈)
40 imass2 6054 . . . . . . . . . . . 12 (𝑉𝑈 → (𝐹𝑉) ⊆ (𝐹𝑈))
4139, 40syl 17 . . . . . . . . . . 11 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → (𝐹𝑉) ⊆ (𝐹𝑈))
427cvmsuni 33863 . . . . . . . . . . . 12 (𝑥 ∈ (𝑆𝑈) → 𝑥 = (𝐹𝑈))
4342adantl 482 . . . . . . . . . . 11 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → 𝑥 = (𝐹𝑈))
4441, 43sseqtrrd 3985 . . . . . . . . . 10 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → (𝐹𝑉) ⊆ 𝑥)
4544sselda 3944 . . . . . . . . 9 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑧 ∈ (𝐹𝑉)) → 𝑧 𝑥)
46 eqid 2736 . . . . . . . . . . . . . . 15 (𝑡 ∩ (𝐹𝑉)) = (𝑡 ∩ (𝐹𝑉))
47 ineq1 4165 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑡 → (𝑦 ∩ (𝐹𝑉)) = (𝑡 ∩ (𝐹𝑉)))
4847rspceeqv 3595 . . . . . . . . . . . . . . 15 ((𝑡𝑥 ∧ (𝑡 ∩ (𝐹𝑉)) = (𝑡 ∩ (𝐹𝑉))) → ∃𝑦𝑥 (𝑡 ∩ (𝐹𝑉)) = (𝑦 ∩ (𝐹𝑉)))
4946, 48mpan2 689 . . . . . . . . . . . . . 14 (𝑡𝑥 → ∃𝑦𝑥 (𝑡 ∩ (𝐹𝑉)) = (𝑦 ∩ (𝐹𝑉)))
5049ad2antrl 726 . . . . . . . . . . . . 13 (((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑧 ∈ (𝐹𝑉)) ∧ (𝑡𝑥𝑧𝑡)) → ∃𝑦𝑥 (𝑡 ∩ (𝐹𝑉)) = (𝑦 ∩ (𝐹𝑉)))
51 vex 3449 . . . . . . . . . . . . . . 15 𝑡 ∈ V
5251inex1 5274 . . . . . . . . . . . . . 14 (𝑡 ∩ (𝐹𝑉)) ∈ V
53 eqid 2736 . . . . . . . . . . . . . . 15 (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) = (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉)))
5453elrnmpt 5911 . . . . . . . . . . . . . 14 ((𝑡 ∩ (𝐹𝑉)) ∈ V → ((𝑡 ∩ (𝐹𝑉)) ∈ ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ↔ ∃𝑦𝑥 (𝑡 ∩ (𝐹𝑉)) = (𝑦 ∩ (𝐹𝑉))))
5552, 54ax-mp 5 . . . . . . . . . . . . 13 ((𝑡 ∩ (𝐹𝑉)) ∈ ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ↔ ∃𝑦𝑥 (𝑡 ∩ (𝐹𝑉)) = (𝑦 ∩ (𝐹𝑉)))
5650, 55sylibr 233 . . . . . . . . . . . 12 (((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑧 ∈ (𝐹𝑉)) ∧ (𝑡𝑥𝑧𝑡)) → (𝑡 ∩ (𝐹𝑉)) ∈ ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))))
57 simprr 771 . . . . . . . . . . . . 13 (((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑧 ∈ (𝐹𝑉)) ∧ (𝑡𝑥𝑧𝑡)) → 𝑧𝑡)
58 simplr 767 . . . . . . . . . . . . 13 (((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑧 ∈ (𝐹𝑉)) ∧ (𝑡𝑥𝑧𝑡)) → 𝑧 ∈ (𝐹𝑉))
5957, 58elind 4154 . . . . . . . . . . . 12 (((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑧 ∈ (𝐹𝑉)) ∧ (𝑡𝑥𝑧𝑡)) → 𝑧 ∈ (𝑡 ∩ (𝐹𝑉)))
60 eleq2 2826 . . . . . . . . . . . . 13 (𝑤 = (𝑡 ∩ (𝐹𝑉)) → (𝑧𝑤𝑧 ∈ (𝑡 ∩ (𝐹𝑉))))
6160rspcev 3581 . . . . . . . . . . . 12 (((𝑡 ∩ (𝐹𝑉)) ∈ ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ∧ 𝑧 ∈ (𝑡 ∩ (𝐹𝑉))) → ∃𝑤 ∈ ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉)))𝑧𝑤)
6256, 59, 61syl2anc 584 . . . . . . . . . . 11 (((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑧 ∈ (𝐹𝑉)) ∧ (𝑡𝑥𝑧𝑡)) → ∃𝑤 ∈ ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉)))𝑧𝑤)
6362rexlimdvaa 3153 . . . . . . . . . 10 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑧 ∈ (𝐹𝑉)) → (∃𝑡𝑥 𝑧𝑡 → ∃𝑤 ∈ ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉)))𝑧𝑤))
64 eluni2 4869 . . . . . . . . . 10 (𝑧 𝑥 ↔ ∃𝑡𝑥 𝑧𝑡)
65 eluni2 4869 . . . . . . . . . 10 (𝑧 ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ↔ ∃𝑤 ∈ ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉)))𝑧𝑤)
6663, 64, 653imtr4g 295 . . . . . . . . 9 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑧 ∈ (𝐹𝑉)) → (𝑧 𝑥𝑧 ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉)))))
6745, 66mpd 15 . . . . . . . 8 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑧 ∈ (𝐹𝑉)) → 𝑧 ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))))
6838, 67eqelssd 3965 . . . . . . 7 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) = (𝐹𝑉))
69 eldifsn 4747 . . . . . . . . . . . 12 (𝑧 ∈ (ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ∖ {(𝑡 ∩ (𝐹𝑉))}) ↔ (𝑧 ∈ ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ∧ 𝑧 ≠ (𝑡 ∩ (𝐹𝑉))))
70 vex 3449 . . . . . . . . . . . . . . 15 𝑧 ∈ V
7153elrnmpt 5911 . . . . . . . . . . . . . . 15 (𝑧 ∈ V → (𝑧 ∈ ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ↔ ∃𝑦𝑥 𝑧 = (𝑦 ∩ (𝐹𝑉))))
7270, 71ax-mp 5 . . . . . . . . . . . . . 14 (𝑧 ∈ ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ↔ ∃𝑦𝑥 𝑧 = (𝑦 ∩ (𝐹𝑉)))
7347equcoms 2023 . . . . . . . . . . . . . . . . . 18 (𝑡 = 𝑦 → (𝑦 ∩ (𝐹𝑉)) = (𝑡 ∩ (𝐹𝑉)))
7473necon3ai 2968 . . . . . . . . . . . . . . . . 17 ((𝑦 ∩ (𝐹𝑉)) ≠ (𝑡 ∩ (𝐹𝑉)) → ¬ 𝑡 = 𝑦)
75 simpllr 774 . . . . . . . . . . . . . . . . . . 19 (((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) ∧ 𝑦𝑥) → 𝑥 ∈ (𝑆𝑈))
76 simplr 767 . . . . . . . . . . . . . . . . . . 19 (((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) ∧ 𝑦𝑥) → 𝑡𝑥)
77 simpr 485 . . . . . . . . . . . . . . . . . . 19 (((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) ∧ 𝑦𝑥) → 𝑦𝑥)
787cvmsdisj 33864 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ (𝑆𝑈) ∧ 𝑡𝑥𝑦𝑥) → (𝑡 = 𝑦 ∨ (𝑡𝑦) = ∅))
7975, 76, 77, 78syl3anc 1371 . . . . . . . . . . . . . . . . . 18 (((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) ∧ 𝑦𝑥) → (𝑡 = 𝑦 ∨ (𝑡𝑦) = ∅))
8079ord 862 . . . . . . . . . . . . . . . . 17 (((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) ∧ 𝑦𝑥) → (¬ 𝑡 = 𝑦 → (𝑡𝑦) = ∅))
81 inss1 4188 . . . . . . . . . . . . . . . . . 18 ((𝑡𝑦) ∩ (𝐹𝑉)) ⊆ (𝑡𝑦)
82 sseq0 4359 . . . . . . . . . . . . . . . . . 18 ((((𝑡𝑦) ∩ (𝐹𝑉)) ⊆ (𝑡𝑦) ∧ (𝑡𝑦) = ∅) → ((𝑡𝑦) ∩ (𝐹𝑉)) = ∅)
8381, 82mpan 688 . . . . . . . . . . . . . . . . 17 ((𝑡𝑦) = ∅ → ((𝑡𝑦) ∩ (𝐹𝑉)) = ∅)
8474, 80, 83syl56 36 . . . . . . . . . . . . . . . 16 (((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) ∧ 𝑦𝑥) → ((𝑦 ∩ (𝐹𝑉)) ≠ (𝑡 ∩ (𝐹𝑉)) → ((𝑡𝑦) ∩ (𝐹𝑉)) = ∅))
85 neeq1 3006 . . . . . . . . . . . . . . . . 17 (𝑧 = (𝑦 ∩ (𝐹𝑉)) → (𝑧 ≠ (𝑡 ∩ (𝐹𝑉)) ↔ (𝑦 ∩ (𝐹𝑉)) ≠ (𝑡 ∩ (𝐹𝑉))))
86 ineq2 4166 . . . . . . . . . . . . . . . . . . 19 (𝑧 = (𝑦 ∩ (𝐹𝑉)) → ((𝑡 ∩ (𝐹𝑉)) ∩ 𝑧) = ((𝑡 ∩ (𝐹𝑉)) ∩ (𝑦 ∩ (𝐹𝑉))))
87 inindir 4187 . . . . . . . . . . . . . . . . . . 19 ((𝑡𝑦) ∩ (𝐹𝑉)) = ((𝑡 ∩ (𝐹𝑉)) ∩ (𝑦 ∩ (𝐹𝑉)))
8886, 87eqtr4di 2794 . . . . . . . . . . . . . . . . . 18 (𝑧 = (𝑦 ∩ (𝐹𝑉)) → ((𝑡 ∩ (𝐹𝑉)) ∩ 𝑧) = ((𝑡𝑦) ∩ (𝐹𝑉)))
8988eqeq1d 2738 . . . . . . . . . . . . . . . . 17 (𝑧 = (𝑦 ∩ (𝐹𝑉)) → (((𝑡 ∩ (𝐹𝑉)) ∩ 𝑧) = ∅ ↔ ((𝑡𝑦) ∩ (𝐹𝑉)) = ∅))
9085, 89imbi12d 344 . . . . . . . . . . . . . . . 16 (𝑧 = (𝑦 ∩ (𝐹𝑉)) → ((𝑧 ≠ (𝑡 ∩ (𝐹𝑉)) → ((𝑡 ∩ (𝐹𝑉)) ∩ 𝑧) = ∅) ↔ ((𝑦 ∩ (𝐹𝑉)) ≠ (𝑡 ∩ (𝐹𝑉)) → ((𝑡𝑦) ∩ (𝐹𝑉)) = ∅)))
9184, 90syl5ibrcom 246 . . . . . . . . . . . . . . 15 (((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) ∧ 𝑦𝑥) → (𝑧 = (𝑦 ∩ (𝐹𝑉)) → (𝑧 ≠ (𝑡 ∩ (𝐹𝑉)) → ((𝑡 ∩ (𝐹𝑉)) ∩ 𝑧) = ∅)))
9291rexlimdva 3152 . . . . . . . . . . . . . 14 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → (∃𝑦𝑥 𝑧 = (𝑦 ∩ (𝐹𝑉)) → (𝑧 ≠ (𝑡 ∩ (𝐹𝑉)) → ((𝑡 ∩ (𝐹𝑉)) ∩ 𝑧) = ∅)))
9372, 92biimtrid 241 . . . . . . . . . . . . 13 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → (𝑧 ∈ ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) → (𝑧 ≠ (𝑡 ∩ (𝐹𝑉)) → ((𝑡 ∩ (𝐹𝑉)) ∩ 𝑧) = ∅)))
9493impd 411 . . . . . . . . . . . 12 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → ((𝑧 ∈ ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ∧ 𝑧 ≠ (𝑡 ∩ (𝐹𝑉))) → ((𝑡 ∩ (𝐹𝑉)) ∩ 𝑧) = ∅))
9569, 94biimtrid 241 . . . . . . . . . . 11 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → (𝑧 ∈ (ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ∖ {(𝑡 ∩ (𝐹𝑉))}) → ((𝑡 ∩ (𝐹𝑉)) ∩ 𝑧) = ∅))
9695ralrimiv 3142 . . . . . . . . . 10 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → ∀𝑧 ∈ (ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ∖ {(𝑡 ∩ (𝐹𝑉))})((𝑡 ∩ (𝐹𝑉)) ∩ 𝑧) = ∅)
97 inss1 4188 . . . . . . . . . . . . 13 (𝑡 ∩ (𝐹𝑉)) ⊆ 𝑡
98 resabs1 5967 . . . . . . . . . . . . 13 ((𝑡 ∩ (𝐹𝑉)) ⊆ 𝑡 → ((𝐹𝑡) ↾ (𝑡 ∩ (𝐹𝑉))) = (𝐹 ↾ (𝑡 ∩ (𝐹𝑉))))
9997, 98ax-mp 5 . . . . . . . . . . . 12 ((𝐹𝑡) ↾ (𝑡 ∩ (𝐹𝑉))) = (𝐹 ↾ (𝑡 ∩ (𝐹𝑉)))
1007cvmshmeo 33865 . . . . . . . . . . . . . 14 ((𝑥 ∈ (𝑆𝑈) ∧ 𝑡𝑥) → (𝐹𝑡) ∈ ((𝐶t 𝑡)Homeo(𝐽t 𝑈)))
101100adantll 712 . . . . . . . . . . . . 13 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → (𝐹𝑡) ∈ ((𝐶t 𝑡)Homeo(𝐽t 𝑈)))
1025adantr 481 . . . . . . . . . . . . . . 15 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → 𝐶 ∈ Top)
1039sselda 3944 . . . . . . . . . . . . . . . 16 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → 𝑡𝐶)
104 elssuni 4898 . . . . . . . . . . . . . . . 16 (𝑡𝐶𝑡 𝐶)
105103, 104syl 17 . . . . . . . . . . . . . . 15 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → 𝑡 𝐶)
106 eqid 2736 . . . . . . . . . . . . . . . 16 𝐶 = 𝐶
107106restuni 22513 . . . . . . . . . . . . . . 15 ((𝐶 ∈ Top ∧ 𝑡 𝐶) → 𝑡 = (𝐶t 𝑡))
108102, 105, 107syl2anc 584 . . . . . . . . . . . . . 14 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → 𝑡 = (𝐶t 𝑡))
10997, 108sseqtrid 3996 . . . . . . . . . . . . 13 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → (𝑡 ∩ (𝐹𝑉)) ⊆ (𝐶t 𝑡))
110 eqid 2736 . . . . . . . . . . . . . 14 (𝐶t 𝑡) = (𝐶t 𝑡)
111110hmeores 23122 . . . . . . . . . . . . 13 (((𝐹𝑡) ∈ ((𝐶t 𝑡)Homeo(𝐽t 𝑈)) ∧ (𝑡 ∩ (𝐹𝑉)) ⊆ (𝐶t 𝑡)) → ((𝐹𝑡) ↾ (𝑡 ∩ (𝐹𝑉))) ∈ (((𝐶t 𝑡) ↾t (𝑡 ∩ (𝐹𝑉)))Homeo((𝐽t 𝑈) ↾t ((𝐹𝑡) “ (𝑡 ∩ (𝐹𝑉))))))
112101, 109, 111syl2anc 584 . . . . . . . . . . . 12 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → ((𝐹𝑡) ↾ (𝑡 ∩ (𝐹𝑉))) ∈ (((𝐶t 𝑡) ↾t (𝑡 ∩ (𝐹𝑉)))Homeo((𝐽t 𝑈) ↾t ((𝐹𝑡) “ (𝑡 ∩ (𝐹𝑉))))))
11399, 112eqeltrrid 2843 . . . . . . . . . . 11 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → (𝐹 ↾ (𝑡 ∩ (𝐹𝑉))) ∈ (((𝐶t 𝑡) ↾t (𝑡 ∩ (𝐹𝑉)))Homeo((𝐽t 𝑈) ↾t ((𝐹𝑡) “ (𝑡 ∩ (𝐹𝑉))))))
11497a1i 11 . . . . . . . . . . . . 13 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → (𝑡 ∩ (𝐹𝑉)) ⊆ 𝑡)
115 simpr 485 . . . . . . . . . . . . 13 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → 𝑡𝑥)
116 restabs 22516 . . . . . . . . . . . . 13 ((𝐶 ∈ Top ∧ (𝑡 ∩ (𝐹𝑉)) ⊆ 𝑡𝑡𝑥) → ((𝐶t 𝑡) ↾t (𝑡 ∩ (𝐹𝑉))) = (𝐶t (𝑡 ∩ (𝐹𝑉))))
117102, 114, 115, 116syl3anc 1371 . . . . . . . . . . . 12 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → ((𝐶t 𝑡) ↾t (𝑡 ∩ (𝐹𝑉))) = (𝐶t (𝑡 ∩ (𝐹𝑉))))
118 incom 4161 . . . . . . . . . . . . . . . . 17 (𝑡 ∩ (𝐹𝑉)) = ((𝐹𝑉) ∩ 𝑡)
119 cnvresima 6182 . . . . . . . . . . . . . . . . 17 ((𝐹𝑡) “ 𝑉) = ((𝐹𝑉) ∩ 𝑡)
120118, 119eqtr4i 2767 . . . . . . . . . . . . . . . 16 (𝑡 ∩ (𝐹𝑉)) = ((𝐹𝑡) “ 𝑉)
121120imaeq2i 6011 . . . . . . . . . . . . . . 15 ((𝐹𝑡) “ (𝑡 ∩ (𝐹𝑉))) = ((𝐹𝑡) “ ((𝐹𝑡) “ 𝑉))
1223adantr 481 . . . . . . . . . . . . . . . . . 18 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → 𝐹 ∈ (𝐶 CovMap 𝐽))
123 simplr 767 . . . . . . . . . . . . . . . . . 18 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → 𝑥 ∈ (𝑆𝑈))
1247cvmsf1o 33866 . . . . . . . . . . . . . . . . . 18 ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑥 ∈ (𝑆𝑈) ∧ 𝑡𝑥) → (𝐹𝑡):𝑡1-1-onto𝑈)
125122, 123, 115, 124syl3anc 1371 . . . . . . . . . . . . . . . . 17 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → (𝐹𝑡):𝑡1-1-onto𝑈)
126 f1ofo 6791 . . . . . . . . . . . . . . . . 17 ((𝐹𝑡):𝑡1-1-onto𝑈 → (𝐹𝑡):𝑡onto𝑈)
127125, 126syl 17 . . . . . . . . . . . . . . . 16 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → (𝐹𝑡):𝑡onto𝑈)
12839adantr 481 . . . . . . . . . . . . . . . 16 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → 𝑉𝑈)
129 foimacnv 6801 . . . . . . . . . . . . . . . 16 (((𝐹𝑡):𝑡onto𝑈𝑉𝑈) → ((𝐹𝑡) “ ((𝐹𝑡) “ 𝑉)) = 𝑉)
130127, 128, 129syl2anc 584 . . . . . . . . . . . . . . 15 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → ((𝐹𝑡) “ ((𝐹𝑡) “ 𝑉)) = 𝑉)
131121, 130eqtrid 2788 . . . . . . . . . . . . . 14 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → ((𝐹𝑡) “ (𝑡 ∩ (𝐹𝑉))) = 𝑉)
132131oveq2d 7373 . . . . . . . . . . . . 13 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → ((𝐽t 𝑈) ↾t ((𝐹𝑡) “ (𝑡 ∩ (𝐹𝑉)))) = ((𝐽t 𝑈) ↾t 𝑉))
133 cvmtop2 33855 . . . . . . . . . . . . . . . 16 (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐽 ∈ Top)
1343, 133syl 17 . . . . . . . . . . . . . . 15 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → 𝐽 ∈ Top)
1357cvmsrcl 33858 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (𝑆𝑈) → 𝑈𝐽)
136135adantl 482 . . . . . . . . . . . . . . 15 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → 𝑈𝐽)
137 restabs 22516 . . . . . . . . . . . . . . 15 ((𝐽 ∈ Top ∧ 𝑉𝑈𝑈𝐽) → ((𝐽t 𝑈) ↾t 𝑉) = (𝐽t 𝑉))
138134, 39, 136, 137syl3anc 1371 . . . . . . . . . . . . . 14 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → ((𝐽t 𝑈) ↾t 𝑉) = (𝐽t 𝑉))
139138adantr 481 . . . . . . . . . . . . 13 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → ((𝐽t 𝑈) ↾t 𝑉) = (𝐽t 𝑉))
140132, 139eqtrd 2776 . . . . . . . . . . . 12 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → ((𝐽t 𝑈) ↾t ((𝐹𝑡) “ (𝑡 ∩ (𝐹𝑉)))) = (𝐽t 𝑉))
141117, 140oveq12d 7375 . . . . . . . . . . 11 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → (((𝐶t 𝑡) ↾t (𝑡 ∩ (𝐹𝑉)))Homeo((𝐽t 𝑈) ↾t ((𝐹𝑡) “ (𝑡 ∩ (𝐹𝑉))))) = ((𝐶t (𝑡 ∩ (𝐹𝑉)))Homeo(𝐽t 𝑉)))
142113, 141eleqtrd 2840 . . . . . . . . . 10 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → (𝐹 ↾ (𝑡 ∩ (𝐹𝑉))) ∈ ((𝐶t (𝑡 ∩ (𝐹𝑉)))Homeo(𝐽t 𝑉)))
14396, 142jca 512 . . . . . . . . 9 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → (∀𝑧 ∈ (ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ∖ {(𝑡 ∩ (𝐹𝑉))})((𝑡 ∩ (𝐹𝑉)) ∩ 𝑧) = ∅ ∧ (𝐹 ↾ (𝑡 ∩ (𝐹𝑉))) ∈ ((𝐶t (𝑡 ∩ (𝐹𝑉)))Homeo(𝐽t 𝑉))))
144143ralrimiva 3143 . . . . . . . 8 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → ∀𝑡𝑥 (∀𝑧 ∈ (ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ∖ {(𝑡 ∩ (𝐹𝑉))})((𝑡 ∩ (𝐹𝑉)) ∩ 𝑧) = ∅ ∧ (𝐹 ↾ (𝑡 ∩ (𝐹𝑉))) ∈ ((𝐶t (𝑡 ∩ (𝐹𝑉)))Homeo(𝐽t 𝑉))))
14552rgenw 3068 . . . . . . . . 9 𝑡𝑥 (𝑡 ∩ (𝐹𝑉)) ∈ V
14647cbvmptv 5218 . . . . . . . . . 10 (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) = (𝑡𝑥 ↦ (𝑡 ∩ (𝐹𝑉)))
147 sneq 4596 . . . . . . . . . . . . 13 (𝑤 = (𝑡 ∩ (𝐹𝑉)) → {𝑤} = {(𝑡 ∩ (𝐹𝑉))})
148147difeq2d 4082 . . . . . . . . . . . 12 (𝑤 = (𝑡 ∩ (𝐹𝑉)) → (ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ∖ {𝑤}) = (ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ∖ {(𝑡 ∩ (𝐹𝑉))}))
149 ineq1 4165 . . . . . . . . . . . . 13 (𝑤 = (𝑡 ∩ (𝐹𝑉)) → (𝑤𝑧) = ((𝑡 ∩ (𝐹𝑉)) ∩ 𝑧))
150149eqeq1d 2738 . . . . . . . . . . . 12 (𝑤 = (𝑡 ∩ (𝐹𝑉)) → ((𝑤𝑧) = ∅ ↔ ((𝑡 ∩ (𝐹𝑉)) ∩ 𝑧) = ∅))
151148, 150raleqbidv 3319 . . . . . . . . . . 11 (𝑤 = (𝑡 ∩ (𝐹𝑉)) → (∀𝑧 ∈ (ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ∖ {𝑤})(𝑤𝑧) = ∅ ↔ ∀𝑧 ∈ (ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ∖ {(𝑡 ∩ (𝐹𝑉))})((𝑡 ∩ (𝐹𝑉)) ∩ 𝑧) = ∅))
152 reseq2 5932 . . . . . . . . . . . 12 (𝑤 = (𝑡 ∩ (𝐹𝑉)) → (𝐹𝑤) = (𝐹 ↾ (𝑡 ∩ (𝐹𝑉))))
153 oveq2 7365 . . . . . . . . . . . . 13 (𝑤 = (𝑡 ∩ (𝐹𝑉)) → (𝐶t 𝑤) = (𝐶t (𝑡 ∩ (𝐹𝑉))))
154153oveq1d 7372 . . . . . . . . . . . 12 (𝑤 = (𝑡 ∩ (𝐹𝑉)) → ((𝐶t 𝑤)Homeo(𝐽t 𝑉)) = ((𝐶t (𝑡 ∩ (𝐹𝑉)))Homeo(𝐽t 𝑉)))
155152, 154eleq12d 2832 . . . . . . . . . . 11 (𝑤 = (𝑡 ∩ (𝐹𝑉)) → ((𝐹𝑤) ∈ ((𝐶t 𝑤)Homeo(𝐽t 𝑉)) ↔ (𝐹 ↾ (𝑡 ∩ (𝐹𝑉))) ∈ ((𝐶t (𝑡 ∩ (𝐹𝑉)))Homeo(𝐽t 𝑉))))
156151, 155anbi12d 631 . . . . . . . . . 10 (𝑤 = (𝑡 ∩ (𝐹𝑉)) → ((∀𝑧 ∈ (ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ∖ {𝑤})(𝑤𝑧) = ∅ ∧ (𝐹𝑤) ∈ ((𝐶t 𝑤)Homeo(𝐽t 𝑉))) ↔ (∀𝑧 ∈ (ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ∖ {(𝑡 ∩ (𝐹𝑉))})((𝑡 ∩ (𝐹𝑉)) ∩ 𝑧) = ∅ ∧ (𝐹 ↾ (𝑡 ∩ (𝐹𝑉))) ∈ ((𝐶t (𝑡 ∩ (𝐹𝑉)))Homeo(𝐽t 𝑉)))))
157146, 156ralrnmptw 7044 . . . . . . . . 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 233 . . . . . . 7 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → ∀𝑤 ∈ ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉)))(∀𝑧 ∈ (ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ∖ {𝑤})(𝑤𝑧) = ∅ ∧ (𝐹𝑤) ∈ ((𝐶t 𝑤)Homeo(𝐽t 𝑉))))
16068, 159jca 512 . . . . . 6 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → ( ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) = (𝐹𝑉) ∧ ∀𝑤 ∈ ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉)))(∀𝑧 ∈ (ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ∖ {𝑤})(𝑤𝑧) = ∅ ∧ (𝐹𝑤) ∈ ((𝐶t 𝑤)Homeo(𝐽t 𝑉)))))
1617cvmscbv 33852 . . . . . . . 8 𝑆 = (𝑎𝐽 ↦ {𝑏 ∈ (𝒫 𝐶 ∖ {∅}) ∣ ( 𝑏 = (𝐹𝑎) ∧ ∀𝑤𝑏 (∀𝑧 ∈ (𝑏 ∖ {𝑤})(𝑤𝑧) = ∅ ∧ (𝐹𝑤) ∈ ((𝐶t 𝑤)Homeo(𝐽t 𝑎))))})
162161cvmsval 33860 . . . . . . 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 1342 . . . . 5 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ∈ (𝑆𝑉))
165164ne0d 4295 . . . 4 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → (𝑆𝑉) ≠ ∅)
166165ex 413 . . 3 ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) → (𝑥 ∈ (𝑆𝑈) → (𝑆𝑉) ≠ ∅))
167166exlimdv 1936 . 2 ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) → (∃𝑥 𝑥 ∈ (𝑆𝑈) → (𝑆𝑉) ≠ ∅))
1681, 167biimtrid 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 2943  wral 3064  wrex 3073  {crab 3407  Vcvv 3445  cdif 3907  cin 3909  wss 3910  c0 4282  𝒫 cpw 4560  {csn 4586   cuni 4865  cmpt 5188  ccnv 5632  dom cdm 5633  ran crn 5634  cres 5635  cima 5636  ontowfo 6494  1-1-ontowf1o 6495  cfv 6496  (class class class)co 7357  t crest 17302  Topctop 22242   Cn ccn 22575  Homeochmeo 23104   CovMap ccvm 33849
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 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672
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 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-ral 3065  df-rex 3074  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-int 4908  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-ov 7360  df-oprab 7361  df-mpo 7362  df-om 7803  df-1st 7921  df-2nd 7922  df-map 8767  df-en 8884  df-fin 8887  df-fi 9347  df-rest 17304  df-topgen 17325  df-top 22243  df-topon 22260  df-bases 22296  df-cn 22578  df-hmeo 23106  df-cvm 33850
This theorem is referenced by:  cvmcov2  33869
  Copyright terms: Public domain W3C validator