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

Theorem cvmsss2 30510
 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 3890 . 2 ((𝑆𝑈) ≠ ∅ ↔ ∃𝑥 𝑥 ∈ (𝑆𝑈))
2 simpl2 1058 . . . . . 6 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → 𝑉𝐽)
3 simpl1 1057 . . . . . . . . . . . 12 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → 𝐹 ∈ (𝐶 CovMap 𝐽))
4 cvmtop1 30496 . . . . . . . . . . . 12 (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐶 ∈ Top)
53, 4syl 17 . . . . . . . . . . 11 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → 𝐶 ∈ Top)
65adantr 480 . . . . . . . . . 10 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑦𝑥) → 𝐶 ∈ Top)
7 cvmcov.1 . . . . . . . . . . . . 13 𝑆 = (𝑘𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ ( 𝑠 = (𝐹𝑘) ∧ ∀𝑢𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢𝑣) = ∅ ∧ (𝐹𝑢) ∈ ((𝐶t 𝑢)Homeo(𝐽t 𝑘))))})
87cvmsss 30503 . . . . . . . . . . . 12 (𝑥 ∈ (𝑆𝑈) → 𝑥𝐶)
98adantl 481 . . . . . . . . . . 11 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → 𝑥𝐶)
109sselda 3568 . . . . . . . . . 10 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑦𝑥) → 𝑦𝐶)
11 cvmcn 30498 . . . . . . . . . . . . 13 (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐹 ∈ (𝐶 Cn 𝐽))
123, 11syl 17 . . . . . . . . . . . 12 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → 𝐹 ∈ (𝐶 Cn 𝐽))
13 cnima 20879 . . . . . . . . . . . 12 ((𝐹 ∈ (𝐶 Cn 𝐽) ∧ 𝑉𝐽) → (𝐹𝑉) ∈ 𝐶)
1412, 2, 13syl2anc 691 . . . . . . . . . . 11 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → (𝐹𝑉) ∈ 𝐶)
1514adantr 480 . . . . . . . . . 10 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑦𝑥) → (𝐹𝑉) ∈ 𝐶)
16 inopn 20529 . . . . . . . . . 10 ((𝐶 ∈ Top ∧ 𝑦𝐶 ∧ (𝐹𝑉) ∈ 𝐶) → (𝑦 ∩ (𝐹𝑉)) ∈ 𝐶)
176, 10, 15, 16syl3anc 1318 . . . . . . . . 9 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑦𝑥) → (𝑦 ∩ (𝐹𝑉)) ∈ 𝐶)
18 eqid 2610 . . . . . . . . 9 (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) = (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉)))
1917, 18fmptd 6292 . . . . . . . 8 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))):𝑥𝐶)
20 frn 5966 . . . . . . . 8 ((𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))):𝑥𝐶 → ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ⊆ 𝐶)
2119, 20syl 17 . . . . . . 7 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ⊆ 𝐶)
227cvmsn0 30504 . . . . . . . . 9 (𝑥 ∈ (𝑆𝑈) → 𝑥 ≠ ∅)
2322adantl 481 . . . . . . . 8 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → 𝑥 ≠ ∅)
24 dmmptg 5549 . . . . . . . . . . . 12 (∀𝑦𝑥 (𝑦 ∩ (𝐹𝑉)) ∈ V → dom (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) = 𝑥)
25 inex1g 4729 . . . . . . . . . . . 12 (𝑦𝑥 → (𝑦 ∩ (𝐹𝑉)) ∈ V)
2624, 25mprg 2910 . . . . . . . . . . 11 dom (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) = 𝑥
2726eqeq1i 2615 . . . . . . . . . 10 (dom (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) = ∅ ↔ 𝑥 = ∅)
28 dm0rn0 5263 . . . . . . . . . 10 (dom (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) = ∅ ↔ ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) = ∅)
2927, 28bitr3i 265 . . . . . . . . 9 (𝑥 = ∅ ↔ ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) = ∅)
3029necon3bii 2834 . . . . . . . 8 (𝑥 ≠ ∅ ↔ ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ≠ ∅)
3123, 30sylib 207 . . . . . . 7 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ≠ ∅)
3221, 31jca 553 . . . . . 6 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → (ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ⊆ 𝐶 ∧ ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ≠ ∅))
33 inss2 3796 . . . . . . . . . . . 12 (𝑦 ∩ (𝐹𝑉)) ⊆ (𝐹𝑉)
34 elpw2g 4754 . . . . . . . . . . . . 13 ((𝐹𝑉) ∈ 𝐶 → ((𝑦 ∩ (𝐹𝑉)) ∈ 𝒫 (𝐹𝑉) ↔ (𝑦 ∩ (𝐹𝑉)) ⊆ (𝐹𝑉)))
3515, 34syl 17 . . . . . . . . . . . 12 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑦𝑥) → ((𝑦 ∩ (𝐹𝑉)) ∈ 𝒫 (𝐹𝑉) ↔ (𝑦 ∩ (𝐹𝑉)) ⊆ (𝐹𝑉)))
3633, 35mpbiri 247 . . . . . . . . . . 11 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑦𝑥) → (𝑦 ∩ (𝐹𝑉)) ∈ 𝒫 (𝐹𝑉))
3736, 18fmptd 6292 . . . . . . . . . 10 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))):𝑥⟶𝒫 (𝐹𝑉))
38 frn 5966 . . . . . . . . . 10 ((𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))):𝑥⟶𝒫 (𝐹𝑉) → ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ⊆ 𝒫 (𝐹𝑉))
3937, 38syl 17 . . . . . . . . 9 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ⊆ 𝒫 (𝐹𝑉))
40 sspwuni 4547 . . . . . . . . 9 (ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ⊆ 𝒫 (𝐹𝑉) ↔ ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ⊆ (𝐹𝑉))
4139, 40sylib 207 . . . . . . . 8 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ⊆ (𝐹𝑉))
42 simpl3 1059 . . . . . . . . . . . . . 14 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → 𝑉𝑈)
43 imass2 5420 . . . . . . . . . . . . . 14 (𝑉𝑈 → (𝐹𝑉) ⊆ (𝐹𝑈))
4442, 43syl 17 . . . . . . . . . . . . 13 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → (𝐹𝑉) ⊆ (𝐹𝑈))
457cvmsuni 30505 . . . . . . . . . . . . . 14 (𝑥 ∈ (𝑆𝑈) → 𝑥 = (𝐹𝑈))
4645adantl 481 . . . . . . . . . . . . 13 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → 𝑥 = (𝐹𝑈))
4744, 46sseqtr4d 3605 . . . . . . . . . . . 12 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → (𝐹𝑉) ⊆ 𝑥)
4847sselda 3568 . . . . . . . . . . 11 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑧 ∈ (𝐹𝑉)) → 𝑧 𝑥)
49 eqid 2610 . . . . . . . . . . . . . . . . 17 (𝑡 ∩ (𝐹𝑉)) = (𝑡 ∩ (𝐹𝑉))
50 ineq1 3769 . . . . . . . . . . . . . . . . . . 19 (𝑦 = 𝑡 → (𝑦 ∩ (𝐹𝑉)) = (𝑡 ∩ (𝐹𝑉)))
5150eqeq2d 2620 . . . . . . . . . . . . . . . . . 18 (𝑦 = 𝑡 → ((𝑡 ∩ (𝐹𝑉)) = (𝑦 ∩ (𝐹𝑉)) ↔ (𝑡 ∩ (𝐹𝑉)) = (𝑡 ∩ (𝐹𝑉))))
5251rspcev 3282 . . . . . . . . . . . . . . . . 17 ((𝑡𝑥 ∧ (𝑡 ∩ (𝐹𝑉)) = (𝑡 ∩ (𝐹𝑉))) → ∃𝑦𝑥 (𝑡 ∩ (𝐹𝑉)) = (𝑦 ∩ (𝐹𝑉)))
5349, 52mpan2 703 . . . . . . . . . . . . . . . 16 (𝑡𝑥 → ∃𝑦𝑥 (𝑡 ∩ (𝐹𝑉)) = (𝑦 ∩ (𝐹𝑉)))
5453ad2antrl 760 . . . . . . . . . . . . . . 15 (((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑧 ∈ (𝐹𝑉)) ∧ (𝑡𝑥𝑧𝑡)) → ∃𝑦𝑥 (𝑡 ∩ (𝐹𝑉)) = (𝑦 ∩ (𝐹𝑉)))
55 vex 3176 . . . . . . . . . . . . . . . . 17 𝑡 ∈ V
5655inex1 4727 . . . . . . . . . . . . . . . 16 (𝑡 ∩ (𝐹𝑉)) ∈ V
5718elrnmpt 5293 . . . . . . . . . . . . . . . 16 ((𝑡 ∩ (𝐹𝑉)) ∈ V → ((𝑡 ∩ (𝐹𝑉)) ∈ ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ↔ ∃𝑦𝑥 (𝑡 ∩ (𝐹𝑉)) = (𝑦 ∩ (𝐹𝑉))))
5856, 57ax-mp 5 . . . . . . . . . . . . . . 15 ((𝑡 ∩ (𝐹𝑉)) ∈ ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ↔ ∃𝑦𝑥 (𝑡 ∩ (𝐹𝑉)) = (𝑦 ∩ (𝐹𝑉)))
5954, 58sylibr 223 . . . . . . . . . . . . . 14 (((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑧 ∈ (𝐹𝑉)) ∧ (𝑡𝑥𝑧𝑡)) → (𝑡 ∩ (𝐹𝑉)) ∈ ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))))
60 simprr 792 . . . . . . . . . . . . . . 15 (((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑧 ∈ (𝐹𝑉)) ∧ (𝑡𝑥𝑧𝑡)) → 𝑧𝑡)
61 simplr 788 . . . . . . . . . . . . . . 15 (((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑧 ∈ (𝐹𝑉)) ∧ (𝑡𝑥𝑧𝑡)) → 𝑧 ∈ (𝐹𝑉))
6260, 61elind 3760 . . . . . . . . . . . . . 14 (((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑧 ∈ (𝐹𝑉)) ∧ (𝑡𝑥𝑧𝑡)) → 𝑧 ∈ (𝑡 ∩ (𝐹𝑉)))
63 eleq2 2677 . . . . . . . . . . . . . . 15 (𝑤 = (𝑡 ∩ (𝐹𝑉)) → (𝑧𝑤𝑧 ∈ (𝑡 ∩ (𝐹𝑉))))
6463rspcev 3282 . . . . . . . . . . . . . 14 (((𝑡 ∩ (𝐹𝑉)) ∈ ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ∧ 𝑧 ∈ (𝑡 ∩ (𝐹𝑉))) → ∃𝑤 ∈ ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉)))𝑧𝑤)
6559, 62, 64syl2anc 691 . . . . . . . . . . . . 13 (((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑧 ∈ (𝐹𝑉)) ∧ (𝑡𝑥𝑧𝑡)) → ∃𝑤 ∈ ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉)))𝑧𝑤)
6665rexlimdvaa 3014 . . . . . . . . . . . 12 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑧 ∈ (𝐹𝑉)) → (∃𝑡𝑥 𝑧𝑡 → ∃𝑤 ∈ ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉)))𝑧𝑤))
67 eluni2 4376 . . . . . . . . . . . 12 (𝑧 𝑥 ↔ ∃𝑡𝑥 𝑧𝑡)
68 eluni2 4376 . . . . . . . . . . . 12 (𝑧 ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ↔ ∃𝑤 ∈ ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉)))𝑧𝑤)
6966, 67, 683imtr4g 284 . . . . . . . . . . 11 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑧 ∈ (𝐹𝑉)) → (𝑧 𝑥𝑧 ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉)))))
7048, 69mpd 15 . . . . . . . . . 10 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑧 ∈ (𝐹𝑉)) → 𝑧 ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))))
7170ex 449 . . . . . . . . 9 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → (𝑧 ∈ (𝐹𝑉) → 𝑧 ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉)))))
7271ssrdv 3574 . . . . . . . 8 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → (𝐹𝑉) ⊆ ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))))
7341, 72eqssd 3585 . . . . . . 7 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) = (𝐹𝑉))
74 eldifsn 4260 . . . . . . . . . . . 12 (𝑧 ∈ (ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ∖ {(𝑡 ∩ (𝐹𝑉))}) ↔ (𝑧 ∈ ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ∧ 𝑧 ≠ (𝑡 ∩ (𝐹𝑉))))
75 vex 3176 . . . . . . . . . . . . . . 15 𝑧 ∈ V
7618elrnmpt 5293 . . . . . . . . . . . . . . 15 (𝑧 ∈ V → (𝑧 ∈ ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ↔ ∃𝑦𝑥 𝑧 = (𝑦 ∩ (𝐹𝑉))))
7775, 76ax-mp 5 . . . . . . . . . . . . . 14 (𝑧 ∈ ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ↔ ∃𝑦𝑥 𝑧 = (𝑦 ∩ (𝐹𝑉)))
7850equcoms 1934 . . . . . . . . . . . . . . . . . 18 (𝑡 = 𝑦 → (𝑦 ∩ (𝐹𝑉)) = (𝑡 ∩ (𝐹𝑉)))
7978necon3ai 2807 . . . . . . . . . . . . . . . . 17 ((𝑦 ∩ (𝐹𝑉)) ≠ (𝑡 ∩ (𝐹𝑉)) → ¬ 𝑡 = 𝑦)
80 simpllr 795 . . . . . . . . . . . . . . . . . . 19 (((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) ∧ 𝑦𝑥) → 𝑥 ∈ (𝑆𝑈))
81 simplr 788 . . . . . . . . . . . . . . . . . . 19 (((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) ∧ 𝑦𝑥) → 𝑡𝑥)
82 simpr 476 . . . . . . . . . . . . . . . . . . 19 (((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) ∧ 𝑦𝑥) → 𝑦𝑥)
837cvmsdisj 30506 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ (𝑆𝑈) ∧ 𝑡𝑥𝑦𝑥) → (𝑡 = 𝑦 ∨ (𝑡𝑦) = ∅))
8480, 81, 82, 83syl3anc 1318 . . . . . . . . . . . . . . . . . 18 (((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) ∧ 𝑦𝑥) → (𝑡 = 𝑦 ∨ (𝑡𝑦) = ∅))
8584ord 391 . . . . . . . . . . . . . . . . 17 (((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) ∧ 𝑦𝑥) → (¬ 𝑡 = 𝑦 → (𝑡𝑦) = ∅))
86 inss1 3795 . . . . . . . . . . . . . . . . . 18 ((𝑡𝑦) ∩ (𝐹𝑉)) ⊆ (𝑡𝑦)
87 sseq0 3927 . . . . . . . . . . . . . . . . . 18 ((((𝑡𝑦) ∩ (𝐹𝑉)) ⊆ (𝑡𝑦) ∧ (𝑡𝑦) = ∅) → ((𝑡𝑦) ∩ (𝐹𝑉)) = ∅)
8886, 87mpan 702 . . . . . . . . . . . . . . . . 17 ((𝑡𝑦) = ∅ → ((𝑡𝑦) ∩ (𝐹𝑉)) = ∅)
8979, 85, 88syl56 35 . . . . . . . . . . . . . . . 16 (((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) ∧ 𝑦𝑥) → ((𝑦 ∩ (𝐹𝑉)) ≠ (𝑡 ∩ (𝐹𝑉)) → ((𝑡𝑦) ∩ (𝐹𝑉)) = ∅))
90 neeq1 2844 . . . . . . . . . . . . . . . . 17 (𝑧 = (𝑦 ∩ (𝐹𝑉)) → (𝑧 ≠ (𝑡 ∩ (𝐹𝑉)) ↔ (𝑦 ∩ (𝐹𝑉)) ≠ (𝑡 ∩ (𝐹𝑉))))
91 ineq2 3770 . . . . . . . . . . . . . . . . . . 19 (𝑧 = (𝑦 ∩ (𝐹𝑉)) → ((𝑡 ∩ (𝐹𝑉)) ∩ 𝑧) = ((𝑡 ∩ (𝐹𝑉)) ∩ (𝑦 ∩ (𝐹𝑉))))
92 inindir 3793 . . . . . . . . . . . . . . . . . . 19 ((𝑡𝑦) ∩ (𝐹𝑉)) = ((𝑡 ∩ (𝐹𝑉)) ∩ (𝑦 ∩ (𝐹𝑉)))
9391, 92syl6eqr 2662 . . . . . . . . . . . . . . . . . 18 (𝑧 = (𝑦 ∩ (𝐹𝑉)) → ((𝑡 ∩ (𝐹𝑉)) ∩ 𝑧) = ((𝑡𝑦) ∩ (𝐹𝑉)))
9493eqeq1d 2612 . . . . . . . . . . . . . . . . 17 (𝑧 = (𝑦 ∩ (𝐹𝑉)) → (((𝑡 ∩ (𝐹𝑉)) ∩ 𝑧) = ∅ ↔ ((𝑡𝑦) ∩ (𝐹𝑉)) = ∅))
9590, 94imbi12d 333 . . . . . . . . . . . . . . . 16 (𝑧 = (𝑦 ∩ (𝐹𝑉)) → ((𝑧 ≠ (𝑡 ∩ (𝐹𝑉)) → ((𝑡 ∩ (𝐹𝑉)) ∩ 𝑧) = ∅) ↔ ((𝑦 ∩ (𝐹𝑉)) ≠ (𝑡 ∩ (𝐹𝑉)) → ((𝑡𝑦) ∩ (𝐹𝑉)) = ∅)))
9689, 95syl5ibrcom 236 . . . . . . . . . . . . . . 15 (((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) ∧ 𝑦𝑥) → (𝑧 = (𝑦 ∩ (𝐹𝑉)) → (𝑧 ≠ (𝑡 ∩ (𝐹𝑉)) → ((𝑡 ∩ (𝐹𝑉)) ∩ 𝑧) = ∅)))
9796rexlimdva 3013 . . . . . . . . . . . . . 14 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → (∃𝑦𝑥 𝑧 = (𝑦 ∩ (𝐹𝑉)) → (𝑧 ≠ (𝑡 ∩ (𝐹𝑉)) → ((𝑡 ∩ (𝐹𝑉)) ∩ 𝑧) = ∅)))
9877, 97syl5bi 231 . . . . . . . . . . . . 13 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → (𝑧 ∈ ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) → (𝑧 ≠ (𝑡 ∩ (𝐹𝑉)) → ((𝑡 ∩ (𝐹𝑉)) ∩ 𝑧) = ∅)))
9998impd 446 . . . . . . . . . . . 12 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → ((𝑧 ∈ ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ∧ 𝑧 ≠ (𝑡 ∩ (𝐹𝑉))) → ((𝑡 ∩ (𝐹𝑉)) ∩ 𝑧) = ∅))
10074, 99syl5bi 231 . . . . . . . . . . 11 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → (𝑧 ∈ (ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ∖ {(𝑡 ∩ (𝐹𝑉))}) → ((𝑡 ∩ (𝐹𝑉)) ∩ 𝑧) = ∅))
101100ralrimiv 2948 . . . . . . . . . 10 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → ∀𝑧 ∈ (ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ∖ {(𝑡 ∩ (𝐹𝑉))})((𝑡 ∩ (𝐹𝑉)) ∩ 𝑧) = ∅)
102 inss1 3795 . . . . . . . . . . . . 13 (𝑡 ∩ (𝐹𝑉)) ⊆ 𝑡
103 resabs1 5347 . . . . . . . . . . . . 13 ((𝑡 ∩ (𝐹𝑉)) ⊆ 𝑡 → ((𝐹𝑡) ↾ (𝑡 ∩ (𝐹𝑉))) = (𝐹 ↾ (𝑡 ∩ (𝐹𝑉))))
104102, 103ax-mp 5 . . . . . . . . . . . 12 ((𝐹𝑡) ↾ (𝑡 ∩ (𝐹𝑉))) = (𝐹 ↾ (𝑡 ∩ (𝐹𝑉)))
1057cvmshmeo 30507 . . . . . . . . . . . . . 14 ((𝑥 ∈ (𝑆𝑈) ∧ 𝑡𝑥) → (𝐹𝑡) ∈ ((𝐶t 𝑡)Homeo(𝐽t 𝑈)))
106105adantll 746 . . . . . . . . . . . . 13 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → (𝐹𝑡) ∈ ((𝐶t 𝑡)Homeo(𝐽t 𝑈)))
1075adantr 480 . . . . . . . . . . . . . . 15 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → 𝐶 ∈ Top)
1089sselda 3568 . . . . . . . . . . . . . . . 16 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → 𝑡𝐶)
109 elssuni 4403 . . . . . . . . . . . . . . . 16 (𝑡𝐶𝑡 𝐶)
110108, 109syl 17 . . . . . . . . . . . . . . 15 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → 𝑡 𝐶)
111 eqid 2610 . . . . . . . . . . . . . . . 16 𝐶 = 𝐶
112111restuni 20776 . . . . . . . . . . . . . . 15 ((𝐶 ∈ Top ∧ 𝑡 𝐶) → 𝑡 = (𝐶t 𝑡))
113107, 110, 112syl2anc 691 . . . . . . . . . . . . . 14 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → 𝑡 = (𝐶t 𝑡))
114102, 113syl5sseq 3616 . . . . . . . . . . . . 13 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → (𝑡 ∩ (𝐹𝑉)) ⊆ (𝐶t 𝑡))
115 eqid 2610 . . . . . . . . . . . . . 14 (𝐶t 𝑡) = (𝐶t 𝑡)
116115hmeores 21384 . . . . . . . . . . . . 13 (((𝐹𝑡) ∈ ((𝐶t 𝑡)Homeo(𝐽t 𝑈)) ∧ (𝑡 ∩ (𝐹𝑉)) ⊆ (𝐶t 𝑡)) → ((𝐹𝑡) ↾ (𝑡 ∩ (𝐹𝑉))) ∈ (((𝐶t 𝑡) ↾t (𝑡 ∩ (𝐹𝑉)))Homeo((𝐽t 𝑈) ↾t ((𝐹𝑡) “ (𝑡 ∩ (𝐹𝑉))))))
117106, 114, 116syl2anc 691 . . . . . . . . . . . 12 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → ((𝐹𝑡) ↾ (𝑡 ∩ (𝐹𝑉))) ∈ (((𝐶t 𝑡) ↾t (𝑡 ∩ (𝐹𝑉)))Homeo((𝐽t 𝑈) ↾t ((𝐹𝑡) “ (𝑡 ∩ (𝐹𝑉))))))
118104, 117syl5eqelr 2693 . . . . . . . . . . 11 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → (𝐹 ↾ (𝑡 ∩ (𝐹𝑉))) ∈ (((𝐶t 𝑡) ↾t (𝑡 ∩ (𝐹𝑉)))Homeo((𝐽t 𝑈) ↾t ((𝐹𝑡) “ (𝑡 ∩ (𝐹𝑉))))))
119102a1i 11 . . . . . . . . . . . . 13 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → (𝑡 ∩ (𝐹𝑉)) ⊆ 𝑡)
120 simpr 476 . . . . . . . . . . . . 13 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → 𝑡𝑥)
121 restabs 20779 . . . . . . . . . . . . 13 ((𝐶 ∈ Top ∧ (𝑡 ∩ (𝐹𝑉)) ⊆ 𝑡𝑡𝑥) → ((𝐶t 𝑡) ↾t (𝑡 ∩ (𝐹𝑉))) = (𝐶t (𝑡 ∩ (𝐹𝑉))))
122107, 119, 120, 121syl3anc 1318 . . . . . . . . . . . 12 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → ((𝐶t 𝑡) ↾t (𝑡 ∩ (𝐹𝑉))) = (𝐶t (𝑡 ∩ (𝐹𝑉))))
123 incom 3767 . . . . . . . . . . . . . . . . 17 (𝑡 ∩ (𝐹𝑉)) = ((𝐹𝑉) ∩ 𝑡)
124 cnvresima 5541 . . . . . . . . . . . . . . . . 17 ((𝐹𝑡) “ 𝑉) = ((𝐹𝑉) ∩ 𝑡)
125123, 124eqtr4i 2635 . . . . . . . . . . . . . . . 16 (𝑡 ∩ (𝐹𝑉)) = ((𝐹𝑡) “ 𝑉)
126125imaeq2i 5383 . . . . . . . . . . . . . . 15 ((𝐹𝑡) “ (𝑡 ∩ (𝐹𝑉))) = ((𝐹𝑡) “ ((𝐹𝑡) “ 𝑉))
1273adantr 480 . . . . . . . . . . . . . . . . . 18 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → 𝐹 ∈ (𝐶 CovMap 𝐽))
128 simplr 788 . . . . . . . . . . . . . . . . . 18 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → 𝑥 ∈ (𝑆𝑈))
1297cvmsf1o 30508 . . . . . . . . . . . . . . . . . 18 ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑥 ∈ (𝑆𝑈) ∧ 𝑡𝑥) → (𝐹𝑡):𝑡1-1-onto𝑈)
130127, 128, 120, 129syl3anc 1318 . . . . . . . . . . . . . . . . 17 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → (𝐹𝑡):𝑡1-1-onto𝑈)
131 f1ofo 6057 . . . . . . . . . . . . . . . . 17 ((𝐹𝑡):𝑡1-1-onto𝑈 → (𝐹𝑡):𝑡onto𝑈)
132130, 131syl 17 . . . . . . . . . . . . . . . 16 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → (𝐹𝑡):𝑡onto𝑈)
13342adantr 480 . . . . . . . . . . . . . . . 16 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → 𝑉𝑈)
134 foimacnv 6067 . . . . . . . . . . . . . . . 16 (((𝐹𝑡):𝑡onto𝑈𝑉𝑈) → ((𝐹𝑡) “ ((𝐹𝑡) “ 𝑉)) = 𝑉)
135132, 133, 134syl2anc 691 . . . . . . . . . . . . . . 15 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → ((𝐹𝑡) “ ((𝐹𝑡) “ 𝑉)) = 𝑉)
136126, 135syl5eq 2656 . . . . . . . . . . . . . 14 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → ((𝐹𝑡) “ (𝑡 ∩ (𝐹𝑉))) = 𝑉)
137136oveq2d 6565 . . . . . . . . . . . . 13 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → ((𝐽t 𝑈) ↾t ((𝐹𝑡) “ (𝑡 ∩ (𝐹𝑉)))) = ((𝐽t 𝑈) ↾t 𝑉))
138 cvmtop2 30497 . . . . . . . . . . . . . . . 16 (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐽 ∈ Top)
1393, 138syl 17 . . . . . . . . . . . . . . 15 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → 𝐽 ∈ Top)
1407cvmsrcl 30500 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (𝑆𝑈) → 𝑈𝐽)
141140adantl 481 . . . . . . . . . . . . . . 15 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → 𝑈𝐽)
142 restabs 20779 . . . . . . . . . . . . . . 15 ((𝐽 ∈ Top ∧ 𝑉𝑈𝑈𝐽) → ((𝐽t 𝑈) ↾t 𝑉) = (𝐽t 𝑉))
143139, 42, 141, 142syl3anc 1318 . . . . . . . . . . . . . 14 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → ((𝐽t 𝑈) ↾t 𝑉) = (𝐽t 𝑉))
144143adantr 480 . . . . . . . . . . . . 13 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → ((𝐽t 𝑈) ↾t 𝑉) = (𝐽t 𝑉))
145137, 144eqtrd 2644 . . . . . . . . . . . 12 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → ((𝐽t 𝑈) ↾t ((𝐹𝑡) “ (𝑡 ∩ (𝐹𝑉)))) = (𝐽t 𝑉))
146122, 145oveq12d 6567 . . . . . . . . . . 11 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → (((𝐶t 𝑡) ↾t (𝑡 ∩ (𝐹𝑉)))Homeo((𝐽t 𝑈) ↾t ((𝐹𝑡) “ (𝑡 ∩ (𝐹𝑉))))) = ((𝐶t (𝑡 ∩ (𝐹𝑉)))Homeo(𝐽t 𝑉)))
147118, 146eleqtrd 2690 . . . . . . . . . 10 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → (𝐹 ↾ (𝑡 ∩ (𝐹𝑉))) ∈ ((𝐶t (𝑡 ∩ (𝐹𝑉)))Homeo(𝐽t 𝑉)))
148101, 147jca 553 . . . . . . . . 9 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → (∀𝑧 ∈ (ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ∖ {(𝑡 ∩ (𝐹𝑉))})((𝑡 ∩ (𝐹𝑉)) ∩ 𝑧) = ∅ ∧ (𝐹 ↾ (𝑡 ∩ (𝐹𝑉))) ∈ ((𝐶t (𝑡 ∩ (𝐹𝑉)))Homeo(𝐽t 𝑉))))
149148ralrimiva 2949 . . . . . . . 8 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → ∀𝑡𝑥 (∀𝑧 ∈ (ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ∖ {(𝑡 ∩ (𝐹𝑉))})((𝑡 ∩ (𝐹𝑉)) ∩ 𝑧) = ∅ ∧ (𝐹 ↾ (𝑡 ∩ (𝐹𝑉))) ∈ ((𝐶t (𝑡 ∩ (𝐹𝑉)))Homeo(𝐽t 𝑉))))
15056rgenw 2908 . . . . . . . . 9 𝑡𝑥 (𝑡 ∩ (𝐹𝑉)) ∈ V
15150cbvmptv 4678 . . . . . . . . . 10 (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) = (𝑡𝑥 ↦ (𝑡 ∩ (𝐹𝑉)))
152 sneq 4135 . . . . . . . . . . . . 13 (𝑤 = (𝑡 ∩ (𝐹𝑉)) → {𝑤} = {(𝑡 ∩ (𝐹𝑉))})
153152difeq2d 3690 . . . . . . . . . . . 12 (𝑤 = (𝑡 ∩ (𝐹𝑉)) → (ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ∖ {𝑤}) = (ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ∖ {(𝑡 ∩ (𝐹𝑉))}))
154 ineq1 3769 . . . . . . . . . . . . 13 (𝑤 = (𝑡 ∩ (𝐹𝑉)) → (𝑤𝑧) = ((𝑡 ∩ (𝐹𝑉)) ∩ 𝑧))
155154eqeq1d 2612 . . . . . . . . . . . 12 (𝑤 = (𝑡 ∩ (𝐹𝑉)) → ((𝑤𝑧) = ∅ ↔ ((𝑡 ∩ (𝐹𝑉)) ∩ 𝑧) = ∅))
156153, 155raleqbidv 3129 . . . . . . . . . . 11 (𝑤 = (𝑡 ∩ (𝐹𝑉)) → (∀𝑧 ∈ (ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ∖ {𝑤})(𝑤𝑧) = ∅ ↔ ∀𝑧 ∈ (ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ∖ {(𝑡 ∩ (𝐹𝑉))})((𝑡 ∩ (𝐹𝑉)) ∩ 𝑧) = ∅))
157 reseq2 5312 . . . . . . . . . . . 12 (𝑤 = (𝑡 ∩ (𝐹𝑉)) → (𝐹𝑤) = (𝐹 ↾ (𝑡 ∩ (𝐹𝑉))))
158 oveq2 6557 . . . . . . . . . . . . 13 (𝑤 = (𝑡 ∩ (𝐹𝑉)) → (𝐶t 𝑤) = (𝐶t (𝑡 ∩ (𝐹𝑉))))
159158oveq1d 6564 . . . . . . . . . . . 12 (𝑤 = (𝑡 ∩ (𝐹𝑉)) → ((𝐶t 𝑤)Homeo(𝐽t 𝑉)) = ((𝐶t (𝑡 ∩ (𝐹𝑉)))Homeo(𝐽t 𝑉)))
160157, 159eleq12d 2682 . . . . . . . . . . 11 (𝑤 = (𝑡 ∩ (𝐹𝑉)) → ((𝐹𝑤) ∈ ((𝐶t 𝑤)Homeo(𝐽t 𝑉)) ↔ (𝐹 ↾ (𝑡 ∩ (𝐹𝑉))) ∈ ((𝐶t (𝑡 ∩ (𝐹𝑉)))Homeo(𝐽t 𝑉))))
161156, 160anbi12d 743 . . . . . . . . . 10 (𝑤 = (𝑡 ∩ (𝐹𝑉)) → ((∀𝑧 ∈ (ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ∖ {𝑤})(𝑤𝑧) = ∅ ∧ (𝐹𝑤) ∈ ((𝐶t 𝑤)Homeo(𝐽t 𝑉))) ↔ (∀𝑧 ∈ (ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ∖ {(𝑡 ∩ (𝐹𝑉))})((𝑡 ∩ (𝐹𝑉)) ∩ 𝑧) = ∅ ∧ (𝐹 ↾ (𝑡 ∩ (𝐹𝑉))) ∈ ((𝐶t (𝑡 ∩ (𝐹𝑉)))Homeo(𝐽t 𝑉)))))
162151, 161ralrnmpt 6276 . . . . . . . . 9 (∀𝑡𝑥 (𝑡 ∩ (𝐹𝑉)) ∈ V → (∀𝑤 ∈ ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉)))(∀𝑧 ∈ (ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ∖ {𝑤})(𝑤𝑧) = ∅ ∧ (𝐹𝑤) ∈ ((𝐶t 𝑤)Homeo(𝐽t 𝑉))) ↔ ∀𝑡𝑥 (∀𝑧 ∈ (ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ∖ {(𝑡 ∩ (𝐹𝑉))})((𝑡 ∩ (𝐹𝑉)) ∩ 𝑧) = ∅ ∧ (𝐹 ↾ (𝑡 ∩ (𝐹𝑉))) ∈ ((𝐶t (𝑡 ∩ (𝐹𝑉)))Homeo(𝐽t 𝑉)))))
163150, 162ax-mp 5 . . . . . . . 8 (∀𝑤 ∈ ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉)))(∀𝑧 ∈ (ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ∖ {𝑤})(𝑤𝑧) = ∅ ∧ (𝐹𝑤) ∈ ((𝐶t 𝑤)Homeo(𝐽t 𝑉))) ↔ ∀𝑡𝑥 (∀𝑧 ∈ (ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ∖ {(𝑡 ∩ (𝐹𝑉))})((𝑡 ∩ (𝐹𝑉)) ∩ 𝑧) = ∅ ∧ (𝐹 ↾ (𝑡 ∩ (𝐹𝑉))) ∈ ((𝐶t (𝑡 ∩ (𝐹𝑉)))Homeo(𝐽t 𝑉))))
164149, 163sylibr 223 . . . . . . 7 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → ∀𝑤 ∈ ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉)))(∀𝑧 ∈ (ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ∖ {𝑤})(𝑤𝑧) = ∅ ∧ (𝐹𝑤) ∈ ((𝐶t 𝑤)Homeo(𝐽t 𝑉))))
16573, 164jca 553 . . . . . 6 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → ( ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) = (𝐹𝑉) ∧ ∀𝑤 ∈ ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉)))(∀𝑧 ∈ (ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ∖ {𝑤})(𝑤𝑧) = ∅ ∧ (𝐹𝑤) ∈ ((𝐶t 𝑤)Homeo(𝐽t 𝑉)))))
1667cvmscbv 30494 . . . . . . . 8 𝑆 = (𝑎𝐽 ↦ {𝑏 ∈ (𝒫 𝐶 ∖ {∅}) ∣ ( 𝑏 = (𝐹𝑎) ∧ ∀𝑤𝑏 (∀𝑧 ∈ (𝑏 ∖ {𝑤})(𝑤𝑧) = ∅ ∧ (𝐹𝑤) ∈ ((𝐶t 𝑤)Homeo(𝐽t 𝑎))))})
167166cvmsval 30502 . . . . . . 7 (𝐶 ∈ Top → (ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ∈ (𝑆𝑉) ↔ (𝑉𝐽 ∧ (ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ⊆ 𝐶 ∧ ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ≠ ∅) ∧ ( ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) = (𝐹𝑉) ∧ ∀𝑤 ∈ ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉)))(∀𝑧 ∈ (ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ∖ {𝑤})(𝑤𝑧) = ∅ ∧ (𝐹𝑤) ∈ ((𝐶t 𝑤)Homeo(𝐽t 𝑉)))))))
1685, 167syl 17 . . . . . 6 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → (ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ∈ (𝑆𝑉) ↔ (𝑉𝐽 ∧ (ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ⊆ 𝐶 ∧ ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ≠ ∅) ∧ ( ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) = (𝐹𝑉) ∧ ∀𝑤 ∈ ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉)))(∀𝑧 ∈ (ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ∖ {𝑤})(𝑤𝑧) = ∅ ∧ (𝐹𝑤) ∈ ((𝐶t 𝑤)Homeo(𝐽t 𝑉)))))))
1692, 32, 165, 168mpbir3and 1238 . . . . 5 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ∈ (𝑆𝑉))
170 ne0i 3880 . . . . 5 (ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ∈ (𝑆𝑉) → (𝑆𝑉) ≠ ∅)
171169, 170syl 17 . . . 4 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → (𝑆𝑉) ≠ ∅)
172171ex 449 . . 3 ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) → (𝑥 ∈ (𝑆𝑈) → (𝑆𝑉) ≠ ∅))
173172exlimdv 1848 . 2 ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) → (∃𝑥 𝑥 ∈ (𝑆𝑈) → (𝑆𝑉) ≠ ∅))
1741, 173syl5bi 231 1 ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) → ((𝑆𝑈) ≠ ∅ → (𝑆𝑉) ≠ ∅))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∨ wo 382   ∧ wa 383   ∧ w3a 1031   = wceq 1475  ∃wex 1695   ∈ wcel 1977   ≠ wne 2780  ∀wral 2896  ∃wrex 2897  {crab 2900  Vcvv 3173   ∖ cdif 3537   ∩ cin 3539   ⊆ wss 3540  ∅c0 3874  𝒫 cpw 4108  {csn 4125  ∪ cuni 4372   ↦ cmpt 4643  ◡ccnv 5037  dom cdm 5038  ran crn 5039   ↾ cres 5040   “ cima 5041  ⟶wf 5800  –onto→wfo 5802  –1-1-onto→wf1o 5803  ‘cfv 5804  (class class class)co 6549   ↾t crest 15904  Topctop 20517   Cn ccn 20838  Homeochmeo 21366   CovMap ccvm 30491 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-reu 2903  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-1st 7059  df-2nd 7060  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-oadd 7451  df-er 7629  df-map 7746  df-en 7842  df-fin 7845  df-fi 8200  df-rest 15906  df-topgen 15927  df-top 20521  df-bases 20522  df-topon 20523  df-cn 20841  df-hmeo 21368  df-cvm 30492 This theorem is referenced by:  cvmcov2  30511
 Copyright terms: Public domain W3C validator