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 35259
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 4359 . 2 ((𝑆𝑈) ≠ ∅ ↔ ∃𝑥 𝑥 ∈ (𝑆𝑈))
2 simpl2 1191 . . . . . 6 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → 𝑉𝐽)
3 simpl1 1190 . . . . . . . . . . . 12 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → 𝐹 ∈ (𝐶 CovMap 𝐽))
4 cvmtop1 35245 . . . . . . . . . . . 12 (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐶 ∈ Top)
53, 4syl 17 . . . . . . . . . . 11 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → 𝐶 ∈ Top)
65adantr 480 . . . . . . . . . 10 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑦𝑥) → 𝐶 ∈ Top)
7 cvmcov.1 . . . . . . . . . . . . 13 𝑆 = (𝑘𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ ( 𝑠 = (𝐹𝑘) ∧ ∀𝑢𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢𝑣) = ∅ ∧ (𝐹𝑢) ∈ ((𝐶t 𝑢)Homeo(𝐽t 𝑘))))})
87cvmsss 35252 . . . . . . . . . . . 12 (𝑥 ∈ (𝑆𝑈) → 𝑥𝐶)
98adantl 481 . . . . . . . . . . 11 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → 𝑥𝐶)
109sselda 3995 . . . . . . . . . 10 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑦𝑥) → 𝑦𝐶)
11 cvmcn 35247 . . . . . . . . . . . . 13 (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐹 ∈ (𝐶 Cn 𝐽))
123, 11syl 17 . . . . . . . . . . . 12 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → 𝐹 ∈ (𝐶 Cn 𝐽))
13 cnima 23289 . . . . . . . . . . . 12 ((𝐹 ∈ (𝐶 Cn 𝐽) ∧ 𝑉𝐽) → (𝐹𝑉) ∈ 𝐶)
1412, 2, 13syl2anc 584 . . . . . . . . . . 11 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → (𝐹𝑉) ∈ 𝐶)
1514adantr 480 . . . . . . . . . 10 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑦𝑥) → (𝐹𝑉) ∈ 𝐶)
16 inopn 22921 . . . . . . . . . 10 ((𝐶 ∈ Top ∧ 𝑦𝐶 ∧ (𝐹𝑉) ∈ 𝐶) → (𝑦 ∩ (𝐹𝑉)) ∈ 𝐶)
176, 10, 15, 16syl3anc 1370 . . . . . . . . 9 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑦𝑥) → (𝑦 ∩ (𝐹𝑉)) ∈ 𝐶)
1817fmpttd 7135 . . . . . . . 8 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))):𝑥𝐶)
1918frnd 6745 . . . . . . 7 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ⊆ 𝐶)
207cvmsn0 35253 . . . . . . . . 9 (𝑥 ∈ (𝑆𝑈) → 𝑥 ≠ ∅)
2120adantl 481 . . . . . . . 8 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → 𝑥 ≠ ∅)
22 dmmptg 6264 . . . . . . . . . . . 12 (∀𝑦𝑥 (𝑦 ∩ (𝐹𝑉)) ∈ V → dom (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) = 𝑥)
23 inex1g 5325 . . . . . . . . . . . 12 (𝑦𝑥 → (𝑦 ∩ (𝐹𝑉)) ∈ V)
2422, 23mprg 3065 . . . . . . . . . . 11 dom (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) = 𝑥
2524eqeq1i 2740 . . . . . . . . . 10 (dom (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) = ∅ ↔ 𝑥 = ∅)
26 dm0rn0 5938 . . . . . . . . . 10 (dom (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) = ∅ ↔ ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) = ∅)
2725, 26bitr3i 277 . . . . . . . . 9 (𝑥 = ∅ ↔ ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) = ∅)
2827necon3bii 2991 . . . . . . . 8 (𝑥 ≠ ∅ ↔ ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ≠ ∅)
2921, 28sylib 218 . . . . . . 7 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ≠ ∅)
3019, 29jca 511 . . . . . 6 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → (ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ⊆ 𝐶 ∧ ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ≠ ∅))
31 inss2 4246 . . . . . . . . . . . 12 (𝑦 ∩ (𝐹𝑉)) ⊆ (𝐹𝑉)
32 elpw2g 5339 . . . . . . . . . . . . 13 ((𝐹𝑉) ∈ 𝐶 → ((𝑦 ∩ (𝐹𝑉)) ∈ 𝒫 (𝐹𝑉) ↔ (𝑦 ∩ (𝐹𝑉)) ⊆ (𝐹𝑉)))
3315, 32syl 17 . . . . . . . . . . . 12 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑦𝑥) → ((𝑦 ∩ (𝐹𝑉)) ∈ 𝒫 (𝐹𝑉) ↔ (𝑦 ∩ (𝐹𝑉)) ⊆ (𝐹𝑉)))
3431, 33mpbiri 258 . . . . . . . . . . 11 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑦𝑥) → (𝑦 ∩ (𝐹𝑉)) ∈ 𝒫 (𝐹𝑉))
3534fmpttd 7135 . . . . . . . . . 10 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))):𝑥⟶𝒫 (𝐹𝑉))
3635frnd 6745 . . . . . . . . 9 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ⊆ 𝒫 (𝐹𝑉))
37 sspwuni 5105 . . . . . . . . 9 (ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ⊆ 𝒫 (𝐹𝑉) ↔ ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ⊆ (𝐹𝑉))
3836, 37sylib 218 . . . . . . . 8 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ⊆ (𝐹𝑉))
39 simpl3 1192 . . . . . . . . . . . 12 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → 𝑉𝑈)
40 imass2 6123 . . . . . . . . . . . 12 (𝑉𝑈 → (𝐹𝑉) ⊆ (𝐹𝑈))
4139, 40syl 17 . . . . . . . . . . 11 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → (𝐹𝑉) ⊆ (𝐹𝑈))
427cvmsuni 35254 . . . . . . . . . . . 12 (𝑥 ∈ (𝑆𝑈) → 𝑥 = (𝐹𝑈))
4342adantl 481 . . . . . . . . . . 11 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → 𝑥 = (𝐹𝑈))
4441, 43sseqtrrd 4037 . . . . . . . . . 10 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → (𝐹𝑉) ⊆ 𝑥)
4544sselda 3995 . . . . . . . . 9 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑧 ∈ (𝐹𝑉)) → 𝑧 𝑥)
46 eqid 2735 . . . . . . . . . . . . . . 15 (𝑡 ∩ (𝐹𝑉)) = (𝑡 ∩ (𝐹𝑉))
47 ineq1 4221 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑡 → (𝑦 ∩ (𝐹𝑉)) = (𝑡 ∩ (𝐹𝑉)))
4847rspceeqv 3645 . . . . . . . . . . . . . . 15 ((𝑡𝑥 ∧ (𝑡 ∩ (𝐹𝑉)) = (𝑡 ∩ (𝐹𝑉))) → ∃𝑦𝑥 (𝑡 ∩ (𝐹𝑉)) = (𝑦 ∩ (𝐹𝑉)))
4946, 48mpan2 691 . . . . . . . . . . . . . 14 (𝑡𝑥 → ∃𝑦𝑥 (𝑡 ∩ (𝐹𝑉)) = (𝑦 ∩ (𝐹𝑉)))
5049ad2antrl 728 . . . . . . . . . . . . 13 (((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑧 ∈ (𝐹𝑉)) ∧ (𝑡𝑥𝑧𝑡)) → ∃𝑦𝑥 (𝑡 ∩ (𝐹𝑉)) = (𝑦 ∩ (𝐹𝑉)))
51 vex 3482 . . . . . . . . . . . . . . 15 𝑡 ∈ V
5251inex1 5323 . . . . . . . . . . . . . 14 (𝑡 ∩ (𝐹𝑉)) ∈ V
53 eqid 2735 . . . . . . . . . . . . . . 15 (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) = (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉)))
5453elrnmpt 5972 . . . . . . . . . . . . . 14 ((𝑡 ∩ (𝐹𝑉)) ∈ V → ((𝑡 ∩ (𝐹𝑉)) ∈ ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ↔ ∃𝑦𝑥 (𝑡 ∩ (𝐹𝑉)) = (𝑦 ∩ (𝐹𝑉))))
5552, 54ax-mp 5 . . . . . . . . . . . . 13 ((𝑡 ∩ (𝐹𝑉)) ∈ ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ↔ ∃𝑦𝑥 (𝑡 ∩ (𝐹𝑉)) = (𝑦 ∩ (𝐹𝑉)))
5650, 55sylibr 234 . . . . . . . . . . . 12 (((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑧 ∈ (𝐹𝑉)) ∧ (𝑡𝑥𝑧𝑡)) → (𝑡 ∩ (𝐹𝑉)) ∈ ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))))
57 simprr 773 . . . . . . . . . . . . 13 (((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑧 ∈ (𝐹𝑉)) ∧ (𝑡𝑥𝑧𝑡)) → 𝑧𝑡)
58 simplr 769 . . . . . . . . . . . . 13 (((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑧 ∈ (𝐹𝑉)) ∧ (𝑡𝑥𝑧𝑡)) → 𝑧 ∈ (𝐹𝑉))
5957, 58elind 4210 . . . . . . . . . . . 12 (((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑧 ∈ (𝐹𝑉)) ∧ (𝑡𝑥𝑧𝑡)) → 𝑧 ∈ (𝑡 ∩ (𝐹𝑉)))
60 eleq2 2828 . . . . . . . . . . . . 13 (𝑤 = (𝑡 ∩ (𝐹𝑉)) → (𝑧𝑤𝑧 ∈ (𝑡 ∩ (𝐹𝑉))))
6160rspcev 3622 . . . . . . . . . . . 12 (((𝑡 ∩ (𝐹𝑉)) ∈ ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ∧ 𝑧 ∈ (𝑡 ∩ (𝐹𝑉))) → ∃𝑤 ∈ ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉)))𝑧𝑤)
6256, 59, 61syl2anc 584 . . . . . . . . . . 11 (((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑧 ∈ (𝐹𝑉)) ∧ (𝑡𝑥𝑧𝑡)) → ∃𝑤 ∈ ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉)))𝑧𝑤)
6362rexlimdvaa 3154 . . . . . . . . . 10 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑧 ∈ (𝐹𝑉)) → (∃𝑡𝑥 𝑧𝑡 → ∃𝑤 ∈ ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉)))𝑧𝑤))
64 eluni2 4916 . . . . . . . . . 10 (𝑧 𝑥 ↔ ∃𝑡𝑥 𝑧𝑡)
65 eluni2 4916 . . . . . . . . . 10 (𝑧 ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ↔ ∃𝑤 ∈ ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉)))𝑧𝑤)
6663, 64, 653imtr4g 296 . . . . . . . . 9 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑧 ∈ (𝐹𝑉)) → (𝑧 𝑥𝑧 ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉)))))
6745, 66mpd 15 . . . . . . . 8 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑧 ∈ (𝐹𝑉)) → 𝑧 ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))))
6838, 67eqelssd 4017 . . . . . . 7 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) = (𝐹𝑉))
69 eldifsn 4791 . . . . . . . . . . . 12 (𝑧 ∈ (ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ∖ {(𝑡 ∩ (𝐹𝑉))}) ↔ (𝑧 ∈ ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ∧ 𝑧 ≠ (𝑡 ∩ (𝐹𝑉))))
70 vex 3482 . . . . . . . . . . . . . . 15 𝑧 ∈ V
7153elrnmpt 5972 . . . . . . . . . . . . . . 15 (𝑧 ∈ V → (𝑧 ∈ ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ↔ ∃𝑦𝑥 𝑧 = (𝑦 ∩ (𝐹𝑉))))
7270, 71ax-mp 5 . . . . . . . . . . . . . 14 (𝑧 ∈ ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ↔ ∃𝑦𝑥 𝑧 = (𝑦 ∩ (𝐹𝑉)))
7347equcoms 2017 . . . . . . . . . . . . . . . . . 18 (𝑡 = 𝑦 → (𝑦 ∩ (𝐹𝑉)) = (𝑡 ∩ (𝐹𝑉)))
7473necon3ai 2963 . . . . . . . . . . . . . . . . 17 ((𝑦 ∩ (𝐹𝑉)) ≠ (𝑡 ∩ (𝐹𝑉)) → ¬ 𝑡 = 𝑦)
75 simpllr 776 . . . . . . . . . . . . . . . . . . 19 (((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) ∧ 𝑦𝑥) → 𝑥 ∈ (𝑆𝑈))
76 simplr 769 . . . . . . . . . . . . . . . . . . 19 (((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) ∧ 𝑦𝑥) → 𝑡𝑥)
77 simpr 484 . . . . . . . . . . . . . . . . . . 19 (((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) ∧ 𝑦𝑥) → 𝑦𝑥)
787cvmsdisj 35255 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ (𝑆𝑈) ∧ 𝑡𝑥𝑦𝑥) → (𝑡 = 𝑦 ∨ (𝑡𝑦) = ∅))
7975, 76, 77, 78syl3anc 1370 . . . . . . . . . . . . . . . . . 18 (((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) ∧ 𝑦𝑥) → (𝑡 = 𝑦 ∨ (𝑡𝑦) = ∅))
8079ord 864 . . . . . . . . . . . . . . . . 17 (((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) ∧ 𝑦𝑥) → (¬ 𝑡 = 𝑦 → (𝑡𝑦) = ∅))
81 inss1 4245 . . . . . . . . . . . . . . . . . 18 ((𝑡𝑦) ∩ (𝐹𝑉)) ⊆ (𝑡𝑦)
82 sseq0 4409 . . . . . . . . . . . . . . . . . 18 ((((𝑡𝑦) ∩ (𝐹𝑉)) ⊆ (𝑡𝑦) ∧ (𝑡𝑦) = ∅) → ((𝑡𝑦) ∩ (𝐹𝑉)) = ∅)
8381, 82mpan 690 . . . . . . . . . . . . . . . . 17 ((𝑡𝑦) = ∅ → ((𝑡𝑦) ∩ (𝐹𝑉)) = ∅)
8474, 80, 83syl56 36 . . . . . . . . . . . . . . . 16 (((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) ∧ 𝑦𝑥) → ((𝑦 ∩ (𝐹𝑉)) ≠ (𝑡 ∩ (𝐹𝑉)) → ((𝑡𝑦) ∩ (𝐹𝑉)) = ∅))
85 neeq1 3001 . . . . . . . . . . . . . . . . 17 (𝑧 = (𝑦 ∩ (𝐹𝑉)) → (𝑧 ≠ (𝑡 ∩ (𝐹𝑉)) ↔ (𝑦 ∩ (𝐹𝑉)) ≠ (𝑡 ∩ (𝐹𝑉))))
86 ineq2 4222 . . . . . . . . . . . . . . . . . . 19 (𝑧 = (𝑦 ∩ (𝐹𝑉)) → ((𝑡 ∩ (𝐹𝑉)) ∩ 𝑧) = ((𝑡 ∩ (𝐹𝑉)) ∩ (𝑦 ∩ (𝐹𝑉))))
87 inindir 4244 . . . . . . . . . . . . . . . . . . 19 ((𝑡𝑦) ∩ (𝐹𝑉)) = ((𝑡 ∩ (𝐹𝑉)) ∩ (𝑦 ∩ (𝐹𝑉)))
8886, 87eqtr4di 2793 . . . . . . . . . . . . . . . . . 18 (𝑧 = (𝑦 ∩ (𝐹𝑉)) → ((𝑡 ∩ (𝐹𝑉)) ∩ 𝑧) = ((𝑡𝑦) ∩ (𝐹𝑉)))
8988eqeq1d 2737 . . . . . . . . . . . . . . . . 17 (𝑧 = (𝑦 ∩ (𝐹𝑉)) → (((𝑡 ∩ (𝐹𝑉)) ∩ 𝑧) = ∅ ↔ ((𝑡𝑦) ∩ (𝐹𝑉)) = ∅))
9085, 89imbi12d 344 . . . . . . . . . . . . . . . 16 (𝑧 = (𝑦 ∩ (𝐹𝑉)) → ((𝑧 ≠ (𝑡 ∩ (𝐹𝑉)) → ((𝑡 ∩ (𝐹𝑉)) ∩ 𝑧) = ∅) ↔ ((𝑦 ∩ (𝐹𝑉)) ≠ (𝑡 ∩ (𝐹𝑉)) → ((𝑡𝑦) ∩ (𝐹𝑉)) = ∅)))
9184, 90syl5ibrcom 247 . . . . . . . . . . . . . . 15 (((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) ∧ 𝑦𝑥) → (𝑧 = (𝑦 ∩ (𝐹𝑉)) → (𝑧 ≠ (𝑡 ∩ (𝐹𝑉)) → ((𝑡 ∩ (𝐹𝑉)) ∩ 𝑧) = ∅)))
9291rexlimdva 3153 . . . . . . . . . . . . . 14 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → (∃𝑦𝑥 𝑧 = (𝑦 ∩ (𝐹𝑉)) → (𝑧 ≠ (𝑡 ∩ (𝐹𝑉)) → ((𝑡 ∩ (𝐹𝑉)) ∩ 𝑧) = ∅)))
9372, 92biimtrid 242 . . . . . . . . . . . . 13 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → (𝑧 ∈ ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) → (𝑧 ≠ (𝑡 ∩ (𝐹𝑉)) → ((𝑡 ∩ (𝐹𝑉)) ∩ 𝑧) = ∅)))
9493impd 410 . . . . . . . . . . . 12 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → ((𝑧 ∈ ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ∧ 𝑧 ≠ (𝑡 ∩ (𝐹𝑉))) → ((𝑡 ∩ (𝐹𝑉)) ∩ 𝑧) = ∅))
9569, 94biimtrid 242 . . . . . . . . . . 11 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → (𝑧 ∈ (ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ∖ {(𝑡 ∩ (𝐹𝑉))}) → ((𝑡 ∩ (𝐹𝑉)) ∩ 𝑧) = ∅))
9695ralrimiv 3143 . . . . . . . . . 10 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → ∀𝑧 ∈ (ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ∖ {(𝑡 ∩ (𝐹𝑉))})((𝑡 ∩ (𝐹𝑉)) ∩ 𝑧) = ∅)
97 inss1 4245 . . . . . . . . . . . . 13 (𝑡 ∩ (𝐹𝑉)) ⊆ 𝑡
98 resabs1 6027 . . . . . . . . . . . . 13 ((𝑡 ∩ (𝐹𝑉)) ⊆ 𝑡 → ((𝐹𝑡) ↾ (𝑡 ∩ (𝐹𝑉))) = (𝐹 ↾ (𝑡 ∩ (𝐹𝑉))))
9997, 98ax-mp 5 . . . . . . . . . . . 12 ((𝐹𝑡) ↾ (𝑡 ∩ (𝐹𝑉))) = (𝐹 ↾ (𝑡 ∩ (𝐹𝑉)))
1007cvmshmeo 35256 . . . . . . . . . . . . . 14 ((𝑥 ∈ (𝑆𝑈) ∧ 𝑡𝑥) → (𝐹𝑡) ∈ ((𝐶t 𝑡)Homeo(𝐽t 𝑈)))
101100adantll 714 . . . . . . . . . . . . 13 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → (𝐹𝑡) ∈ ((𝐶t 𝑡)Homeo(𝐽t 𝑈)))
1025adantr 480 . . . . . . . . . . . . . . 15 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → 𝐶 ∈ Top)
1039sselda 3995 . . . . . . . . . . . . . . . 16 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → 𝑡𝐶)
104 elssuni 4942 . . . . . . . . . . . . . . . 16 (𝑡𝐶𝑡 𝐶)
105103, 104syl 17 . . . . . . . . . . . . . . 15 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → 𝑡 𝐶)
106 eqid 2735 . . . . . . . . . . . . . . . 16 𝐶 = 𝐶
107106restuni 23186 . . . . . . . . . . . . . . 15 ((𝐶 ∈ Top ∧ 𝑡 𝐶) → 𝑡 = (𝐶t 𝑡))
108102, 105, 107syl2anc 584 . . . . . . . . . . . . . 14 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → 𝑡 = (𝐶t 𝑡))
10997, 108sseqtrid 4048 . . . . . . . . . . . . 13 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → (𝑡 ∩ (𝐹𝑉)) ⊆ (𝐶t 𝑡))
110 eqid 2735 . . . . . . . . . . . . . 14 (𝐶t 𝑡) = (𝐶t 𝑡)
111110hmeores 23795 . . . . . . . . . . . . 13 (((𝐹𝑡) ∈ ((𝐶t 𝑡)Homeo(𝐽t 𝑈)) ∧ (𝑡 ∩ (𝐹𝑉)) ⊆ (𝐶t 𝑡)) → ((𝐹𝑡) ↾ (𝑡 ∩ (𝐹𝑉))) ∈ (((𝐶t 𝑡) ↾t (𝑡 ∩ (𝐹𝑉)))Homeo((𝐽t 𝑈) ↾t ((𝐹𝑡) “ (𝑡 ∩ (𝐹𝑉))))))
112101, 109, 111syl2anc 584 . . . . . . . . . . . 12 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → ((𝐹𝑡) ↾ (𝑡 ∩ (𝐹𝑉))) ∈ (((𝐶t 𝑡) ↾t (𝑡 ∩ (𝐹𝑉)))Homeo((𝐽t 𝑈) ↾t ((𝐹𝑡) “ (𝑡 ∩ (𝐹𝑉))))))
11399, 112eqeltrrid 2844 . . . . . . . . . . 11 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → (𝐹 ↾ (𝑡 ∩ (𝐹𝑉))) ∈ (((𝐶t 𝑡) ↾t (𝑡 ∩ (𝐹𝑉)))Homeo((𝐽t 𝑈) ↾t ((𝐹𝑡) “ (𝑡 ∩ (𝐹𝑉))))))
11497a1i 11 . . . . . . . . . . . . 13 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → (𝑡 ∩ (𝐹𝑉)) ⊆ 𝑡)
115 simpr 484 . . . . . . . . . . . . 13 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → 𝑡𝑥)
116 restabs 23189 . . . . . . . . . . . . 13 ((𝐶 ∈ Top ∧ (𝑡 ∩ (𝐹𝑉)) ⊆ 𝑡𝑡𝑥) → ((𝐶t 𝑡) ↾t (𝑡 ∩ (𝐹𝑉))) = (𝐶t (𝑡 ∩ (𝐹𝑉))))
117102, 114, 115, 116syl3anc 1370 . . . . . . . . . . . 12 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → ((𝐶t 𝑡) ↾t (𝑡 ∩ (𝐹𝑉))) = (𝐶t (𝑡 ∩ (𝐹𝑉))))
118 incom 4217 . . . . . . . . . . . . . . . . 17 (𝑡 ∩ (𝐹𝑉)) = ((𝐹𝑉) ∩ 𝑡)
119 cnvresima 6252 . . . . . . . . . . . . . . . . 17 ((𝐹𝑡) “ 𝑉) = ((𝐹𝑉) ∩ 𝑡)
120118, 119eqtr4i 2766 . . . . . . . . . . . . . . . 16 (𝑡 ∩ (𝐹𝑉)) = ((𝐹𝑡) “ 𝑉)
121120imaeq2i 6078 . . . . . . . . . . . . . . 15 ((𝐹𝑡) “ (𝑡 ∩ (𝐹𝑉))) = ((𝐹𝑡) “ ((𝐹𝑡) “ 𝑉))
1223adantr 480 . . . . . . . . . . . . . . . . . 18 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → 𝐹 ∈ (𝐶 CovMap 𝐽))
123 simplr 769 . . . . . . . . . . . . . . . . . 18 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → 𝑥 ∈ (𝑆𝑈))
1247cvmsf1o 35257 . . . . . . . . . . . . . . . . . 18 ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑥 ∈ (𝑆𝑈) ∧ 𝑡𝑥) → (𝐹𝑡):𝑡1-1-onto𝑈)
125122, 123, 115, 124syl3anc 1370 . . . . . . . . . . . . . . . . 17 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → (𝐹𝑡):𝑡1-1-onto𝑈)
126 f1ofo 6856 . . . . . . . . . . . . . . . . 17 ((𝐹𝑡):𝑡1-1-onto𝑈 → (𝐹𝑡):𝑡onto𝑈)
127125, 126syl 17 . . . . . . . . . . . . . . . 16 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → (𝐹𝑡):𝑡onto𝑈)
12839adantr 480 . . . . . . . . . . . . . . . 16 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → 𝑉𝑈)
129 foimacnv 6866 . . . . . . . . . . . . . . . 16 (((𝐹𝑡):𝑡onto𝑈𝑉𝑈) → ((𝐹𝑡) “ ((𝐹𝑡) “ 𝑉)) = 𝑉)
130127, 128, 129syl2anc 584 . . . . . . . . . . . . . . 15 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → ((𝐹𝑡) “ ((𝐹𝑡) “ 𝑉)) = 𝑉)
131121, 130eqtrid 2787 . . . . . . . . . . . . . 14 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → ((𝐹𝑡) “ (𝑡 ∩ (𝐹𝑉))) = 𝑉)
132131oveq2d 7447 . . . . . . . . . . . . 13 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → ((𝐽t 𝑈) ↾t ((𝐹𝑡) “ (𝑡 ∩ (𝐹𝑉)))) = ((𝐽t 𝑈) ↾t 𝑉))
133 cvmtop2 35246 . . . . . . . . . . . . . . . 16 (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐽 ∈ Top)
1343, 133syl 17 . . . . . . . . . . . . . . 15 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → 𝐽 ∈ Top)
1357cvmsrcl 35249 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (𝑆𝑈) → 𝑈𝐽)
136135adantl 481 . . . . . . . . . . . . . . 15 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → 𝑈𝐽)
137 restabs 23189 . . . . . . . . . . . . . . 15 ((𝐽 ∈ Top ∧ 𝑉𝑈𝑈𝐽) → ((𝐽t 𝑈) ↾t 𝑉) = (𝐽t 𝑉))
138134, 39, 136, 137syl3anc 1370 . . . . . . . . . . . . . 14 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → ((𝐽t 𝑈) ↾t 𝑉) = (𝐽t 𝑉))
139138adantr 480 . . . . . . . . . . . . 13 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → ((𝐽t 𝑈) ↾t 𝑉) = (𝐽t 𝑉))
140132, 139eqtrd 2775 . . . . . . . . . . . 12 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → ((𝐽t 𝑈) ↾t ((𝐹𝑡) “ (𝑡 ∩ (𝐹𝑉)))) = (𝐽t 𝑉))
141117, 140oveq12d 7449 . . . . . . . . . . 11 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → (((𝐶t 𝑡) ↾t (𝑡 ∩ (𝐹𝑉)))Homeo((𝐽t 𝑈) ↾t ((𝐹𝑡) “ (𝑡 ∩ (𝐹𝑉))))) = ((𝐶t (𝑡 ∩ (𝐹𝑉)))Homeo(𝐽t 𝑉)))
142113, 141eleqtrd 2841 . . . . . . . . . 10 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → (𝐹 ↾ (𝑡 ∩ (𝐹𝑉))) ∈ ((𝐶t (𝑡 ∩ (𝐹𝑉)))Homeo(𝐽t 𝑉)))
14396, 142jca 511 . . . . . . . . 9 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → (∀𝑧 ∈ (ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ∖ {(𝑡 ∩ (𝐹𝑉))})((𝑡 ∩ (𝐹𝑉)) ∩ 𝑧) = ∅ ∧ (𝐹 ↾ (𝑡 ∩ (𝐹𝑉))) ∈ ((𝐶t (𝑡 ∩ (𝐹𝑉)))Homeo(𝐽t 𝑉))))
144143ralrimiva 3144 . . . . . . . 8 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → ∀𝑡𝑥 (∀𝑧 ∈ (ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ∖ {(𝑡 ∩ (𝐹𝑉))})((𝑡 ∩ (𝐹𝑉)) ∩ 𝑧) = ∅ ∧ (𝐹 ↾ (𝑡 ∩ (𝐹𝑉))) ∈ ((𝐶t (𝑡 ∩ (𝐹𝑉)))Homeo(𝐽t 𝑉))))
14552rgenw 3063 . . . . . . . . 9 𝑡𝑥 (𝑡 ∩ (𝐹𝑉)) ∈ V
14647cbvmptv 5261 . . . . . . . . . 10 (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) = (𝑡𝑥 ↦ (𝑡 ∩ (𝐹𝑉)))
147 sneq 4641 . . . . . . . . . . . . 13 (𝑤 = (𝑡 ∩ (𝐹𝑉)) → {𝑤} = {(𝑡 ∩ (𝐹𝑉))})
148147difeq2d 4136 . . . . . . . . . . . 12 (𝑤 = (𝑡 ∩ (𝐹𝑉)) → (ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ∖ {𝑤}) = (ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ∖ {(𝑡 ∩ (𝐹𝑉))}))
149 ineq1 4221 . . . . . . . . . . . . 13 (𝑤 = (𝑡 ∩ (𝐹𝑉)) → (𝑤𝑧) = ((𝑡 ∩ (𝐹𝑉)) ∩ 𝑧))
150149eqeq1d 2737 . . . . . . . . . . . 12 (𝑤 = (𝑡 ∩ (𝐹𝑉)) → ((𝑤𝑧) = ∅ ↔ ((𝑡 ∩ (𝐹𝑉)) ∩ 𝑧) = ∅))
151148, 150raleqbidv 3344 . . . . . . . . . . 11 (𝑤 = (𝑡 ∩ (𝐹𝑉)) → (∀𝑧 ∈ (ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ∖ {𝑤})(𝑤𝑧) = ∅ ↔ ∀𝑧 ∈ (ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ∖ {(𝑡 ∩ (𝐹𝑉))})((𝑡 ∩ (𝐹𝑉)) ∩ 𝑧) = ∅))
152 reseq2 5995 . . . . . . . . . . . 12 (𝑤 = (𝑡 ∩ (𝐹𝑉)) → (𝐹𝑤) = (𝐹 ↾ (𝑡 ∩ (𝐹𝑉))))
153 oveq2 7439 . . . . . . . . . . . . 13 (𝑤 = (𝑡 ∩ (𝐹𝑉)) → (𝐶t 𝑤) = (𝐶t (𝑡 ∩ (𝐹𝑉))))
154153oveq1d 7446 . . . . . . . . . . . 12 (𝑤 = (𝑡 ∩ (𝐹𝑉)) → ((𝐶t 𝑤)Homeo(𝐽t 𝑉)) = ((𝐶t (𝑡 ∩ (𝐹𝑉)))Homeo(𝐽t 𝑉)))
155152, 154eleq12d 2833 . . . . . . . . . . 11 (𝑤 = (𝑡 ∩ (𝐹𝑉)) → ((𝐹𝑤) ∈ ((𝐶t 𝑤)Homeo(𝐽t 𝑉)) ↔ (𝐹 ↾ (𝑡 ∩ (𝐹𝑉))) ∈ ((𝐶t (𝑡 ∩ (𝐹𝑉)))Homeo(𝐽t 𝑉))))
156151, 155anbi12d 632 . . . . . . . . . 10 (𝑤 = (𝑡 ∩ (𝐹𝑉)) → ((∀𝑧 ∈ (ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ∖ {𝑤})(𝑤𝑧) = ∅ ∧ (𝐹𝑤) ∈ ((𝐶t 𝑤)Homeo(𝐽t 𝑉))) ↔ (∀𝑧 ∈ (ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ∖ {(𝑡 ∩ (𝐹𝑉))})((𝑡 ∩ (𝐹𝑉)) ∩ 𝑧) = ∅ ∧ (𝐹 ↾ (𝑡 ∩ (𝐹𝑉))) ∈ ((𝐶t (𝑡 ∩ (𝐹𝑉)))Homeo(𝐽t 𝑉)))))
157146, 156ralrnmptw 7114 . . . . . . . . 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 234 . . . . . . 7 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → ∀𝑤 ∈ ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉)))(∀𝑧 ∈ (ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ∖ {𝑤})(𝑤𝑧) = ∅ ∧ (𝐹𝑤) ∈ ((𝐶t 𝑤)Homeo(𝐽t 𝑉))))
16068, 159jca 511 . . . . . 6 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → ( ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) = (𝐹𝑉) ∧ ∀𝑤 ∈ ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉)))(∀𝑧 ∈ (ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ∖ {𝑤})(𝑤𝑧) = ∅ ∧ (𝐹𝑤) ∈ ((𝐶t 𝑤)Homeo(𝐽t 𝑉)))))
1617cvmscbv 35243 . . . . . . . 8 𝑆 = (𝑎𝐽 ↦ {𝑏 ∈ (𝒫 𝐶 ∖ {∅}) ∣ ( 𝑏 = (𝐹𝑎) ∧ ∀𝑤𝑏 (∀𝑧 ∈ (𝑏 ∖ {𝑤})(𝑤𝑧) = ∅ ∧ (𝐹𝑤) ∈ ((𝐶t 𝑤)Homeo(𝐽t 𝑎))))})
162161cvmsval 35251 . . . . . . 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 1341 . . . . 5 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ∈ (𝑆𝑉))
165164ne0d 4348 . . . 4 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → (𝑆𝑉) ≠ ∅)
166165ex 412 . . 3 ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) → (𝑥 ∈ (𝑆𝑈) → (𝑆𝑉) ≠ ∅))
167166exlimdv 1931 . 2 ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) → (∃𝑥 𝑥 ∈ (𝑆𝑈) → (𝑆𝑉) ≠ ∅))
1681, 167biimtrid 242 1 ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) → ((𝑆𝑈) ≠ ∅ → (𝑆𝑉) ≠ ∅))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  wo 847  w3a 1086   = wceq 1537  wex 1776  wcel 2106  wne 2938  wral 3059  wrex 3068  {crab 3433  Vcvv 3478  cdif 3960  cin 3962  wss 3963  c0 4339  𝒫 cpw 4605  {csn 4631   cuni 4912  cmpt 5231  ccnv 5688  dom cdm 5689  ran crn 5690  cres 5691  cima 5692  ontowfo 6561  1-1-ontowf1o 6562  cfv 6563  (class class class)co 7431  t crest 17467  Topctop 22915   Cn ccn 23248  Homeochmeo 23777   CovMap ccvm 35240
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-rep 5285  ax-sep 5302  ax-nul 5312  ax-pow 5371  ax-pr 5438  ax-un 7754
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-ral 3060  df-rex 3069  df-reu 3379  df-rab 3434  df-v 3480  df-sbc 3792  df-csb 3909  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-pss 3983  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-int 4952  df-iun 4998  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5583  df-eprel 5589  df-po 5597  df-so 5598  df-fr 5641  df-we 5643  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-ord 6389  df-on 6390  df-lim 6391  df-suc 6392  df-iota 6516  df-fun 6565  df-fn 6566  df-f 6567  df-f1 6568  df-fo 6569  df-f1o 6570  df-fv 6571  df-ov 7434  df-oprab 7435  df-mpo 7436  df-om 7888  df-1st 8013  df-2nd 8014  df-map 8867  df-en 8985  df-fin 8988  df-fi 9449  df-rest 17469  df-topgen 17490  df-top 22916  df-topon 22933  df-bases 22969  df-cn 23251  df-hmeo 23779  df-cvm 35241
This theorem is referenced by:  cvmcov2  35260
  Copyright terms: Public domain W3C validator