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 33908
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 4311 . 2 ((π‘†β€˜π‘ˆ) β‰  βˆ… ↔ βˆƒπ‘₯ π‘₯ ∈ (π‘†β€˜π‘ˆ))
2 simpl2 1193 . . . . . 6 (((𝐹 ∈ (𝐢 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 βŠ† π‘ˆ) ∧ π‘₯ ∈ (π‘†β€˜π‘ˆ)) β†’ 𝑉 ∈ 𝐽)
3 simpl1 1192 . . . . . . . . . . . 12 (((𝐹 ∈ (𝐢 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 βŠ† π‘ˆ) ∧ π‘₯ ∈ (π‘†β€˜π‘ˆ)) β†’ 𝐹 ∈ (𝐢 CovMap 𝐽))
4 cvmtop1 33894 . . . . . . . . . . . 12 (𝐹 ∈ (𝐢 CovMap 𝐽) β†’ 𝐢 ∈ Top)
53, 4syl 17 . . . . . . . . . . 11 (((𝐹 ∈ (𝐢 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 βŠ† π‘ˆ) ∧ π‘₯ ∈ (π‘†β€˜π‘ˆ)) β†’ 𝐢 ∈ Top)
65adantr 482 . . . . . . . . . 10 ((((𝐹 ∈ (𝐢 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 βŠ† π‘ˆ) ∧ π‘₯ ∈ (π‘†β€˜π‘ˆ)) ∧ 𝑦 ∈ π‘₯) β†’ 𝐢 ∈ Top)
7 cvmcov.1 . . . . . . . . . . . . 13 𝑆 = (π‘˜ ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐢 βˆ– {βˆ…}) ∣ (βˆͺ 𝑠 = (◑𝐹 β€œ π‘˜) ∧ βˆ€π‘’ ∈ 𝑠 (βˆ€π‘£ ∈ (𝑠 βˆ– {𝑒})(𝑒 ∩ 𝑣) = βˆ… ∧ (𝐹 β†Ύ 𝑒) ∈ ((𝐢 β†Ύt 𝑒)Homeo(𝐽 β†Ύt π‘˜))))})
87cvmsss 33901 . . . . . . . . . . . 12 (π‘₯ ∈ (π‘†β€˜π‘ˆ) β†’ π‘₯ βŠ† 𝐢)
98adantl 483 . . . . . . . . . . 11 (((𝐹 ∈ (𝐢 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 βŠ† π‘ˆ) ∧ π‘₯ ∈ (π‘†β€˜π‘ˆ)) β†’ π‘₯ βŠ† 𝐢)
109sselda 3949 . . . . . . . . . 10 ((((𝐹 ∈ (𝐢 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 βŠ† π‘ˆ) ∧ π‘₯ ∈ (π‘†β€˜π‘ˆ)) ∧ 𝑦 ∈ π‘₯) β†’ 𝑦 ∈ 𝐢)
11 cvmcn 33896 . . . . . . . . . . . . 13 (𝐹 ∈ (𝐢 CovMap 𝐽) β†’ 𝐹 ∈ (𝐢 Cn 𝐽))
123, 11syl 17 . . . . . . . . . . . 12 (((𝐹 ∈ (𝐢 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 βŠ† π‘ˆ) ∧ π‘₯ ∈ (π‘†β€˜π‘ˆ)) β†’ 𝐹 ∈ (𝐢 Cn 𝐽))
13 cnima 22632 . . . . . . . . . . . 12 ((𝐹 ∈ (𝐢 Cn 𝐽) ∧ 𝑉 ∈ 𝐽) β†’ (◑𝐹 β€œ 𝑉) ∈ 𝐢)
1412, 2, 13syl2anc 585 . . . . . . . . . . 11 (((𝐹 ∈ (𝐢 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 βŠ† π‘ˆ) ∧ π‘₯ ∈ (π‘†β€˜π‘ˆ)) β†’ (◑𝐹 β€œ 𝑉) ∈ 𝐢)
1514adantr 482 . . . . . . . . . 10 ((((𝐹 ∈ (𝐢 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 βŠ† π‘ˆ) ∧ π‘₯ ∈ (π‘†β€˜π‘ˆ)) ∧ 𝑦 ∈ π‘₯) β†’ (◑𝐹 β€œ 𝑉) ∈ 𝐢)
16 inopn 22264 . . . . . . . . . 10 ((𝐢 ∈ Top ∧ 𝑦 ∈ 𝐢 ∧ (◑𝐹 β€œ 𝑉) ∈ 𝐢) β†’ (𝑦 ∩ (◑𝐹 β€œ 𝑉)) ∈ 𝐢)
176, 10, 15, 16syl3anc 1372 . . . . . . . . 9 ((((𝐹 ∈ (𝐢 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 βŠ† π‘ˆ) ∧ π‘₯ ∈ (π‘†β€˜π‘ˆ)) ∧ 𝑦 ∈ π‘₯) β†’ (𝑦 ∩ (◑𝐹 β€œ 𝑉)) ∈ 𝐢)
1817fmpttd 7068 . . . . . . . 8 (((𝐹 ∈ (𝐢 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 βŠ† π‘ˆ) ∧ π‘₯ ∈ (π‘†β€˜π‘ˆ)) β†’ (𝑦 ∈ π‘₯ ↦ (𝑦 ∩ (◑𝐹 β€œ 𝑉))):π‘₯⟢𝐢)
1918frnd 6681 . . . . . . 7 (((𝐹 ∈ (𝐢 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 βŠ† π‘ˆ) ∧ π‘₯ ∈ (π‘†β€˜π‘ˆ)) β†’ ran (𝑦 ∈ π‘₯ ↦ (𝑦 ∩ (◑𝐹 β€œ 𝑉))) βŠ† 𝐢)
207cvmsn0 33902 . . . . . . . . 9 (π‘₯ ∈ (π‘†β€˜π‘ˆ) β†’ π‘₯ β‰  βˆ…)
2120adantl 483 . . . . . . . 8 (((𝐹 ∈ (𝐢 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 βŠ† π‘ˆ) ∧ π‘₯ ∈ (π‘†β€˜π‘ˆ)) β†’ π‘₯ β‰  βˆ…)
22 dmmptg 6199 . . . . . . . . . . . 12 (βˆ€π‘¦ ∈ π‘₯ (𝑦 ∩ (◑𝐹 β€œ 𝑉)) ∈ V β†’ dom (𝑦 ∈ π‘₯ ↦ (𝑦 ∩ (◑𝐹 β€œ 𝑉))) = π‘₯)
23 inex1g 5281 . . . . . . . . . . . 12 (𝑦 ∈ π‘₯ β†’ (𝑦 ∩ (◑𝐹 β€œ 𝑉)) ∈ V)
2422, 23mprg 3071 . . . . . . . . . . 11 dom (𝑦 ∈ π‘₯ ↦ (𝑦 ∩ (◑𝐹 β€œ 𝑉))) = π‘₯
2524eqeq1i 2742 . . . . . . . . . 10 (dom (𝑦 ∈ π‘₯ ↦ (𝑦 ∩ (◑𝐹 β€œ 𝑉))) = βˆ… ↔ π‘₯ = βˆ…)
26 dm0rn0 5885 . . . . . . . . . 10 (dom (𝑦 ∈ π‘₯ ↦ (𝑦 ∩ (◑𝐹 β€œ 𝑉))) = βˆ… ↔ ran (𝑦 ∈ π‘₯ ↦ (𝑦 ∩ (◑𝐹 β€œ 𝑉))) = βˆ…)
2725, 26bitr3i 277 . . . . . . . . 9 (π‘₯ = βˆ… ↔ ran (𝑦 ∈ π‘₯ ↦ (𝑦 ∩ (◑𝐹 β€œ 𝑉))) = βˆ…)
2827necon3bii 2997 . . . . . . . 8 (π‘₯ β‰  βˆ… ↔ ran (𝑦 ∈ π‘₯ ↦ (𝑦 ∩ (◑𝐹 β€œ 𝑉))) β‰  βˆ…)
2921, 28sylib 217 . . . . . . 7 (((𝐹 ∈ (𝐢 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 βŠ† π‘ˆ) ∧ π‘₯ ∈ (π‘†β€˜π‘ˆ)) β†’ ran (𝑦 ∈ π‘₯ ↦ (𝑦 ∩ (◑𝐹 β€œ 𝑉))) β‰  βˆ…)
3019, 29jca 513 . . . . . 6 (((𝐹 ∈ (𝐢 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 βŠ† π‘ˆ) ∧ π‘₯ ∈ (π‘†β€˜π‘ˆ)) β†’ (ran (𝑦 ∈ π‘₯ ↦ (𝑦 ∩ (◑𝐹 β€œ 𝑉))) βŠ† 𝐢 ∧ ran (𝑦 ∈ π‘₯ ↦ (𝑦 ∩ (◑𝐹 β€œ 𝑉))) β‰  βˆ…))
31 inss2 4194 . . . . . . . . . . . 12 (𝑦 ∩ (◑𝐹 β€œ 𝑉)) βŠ† (◑𝐹 β€œ 𝑉)
32 elpw2g 5306 . . . . . . . . . . . . 13 ((◑𝐹 β€œ 𝑉) ∈ 𝐢 β†’ ((𝑦 ∩ (◑𝐹 β€œ 𝑉)) ∈ 𝒫 (◑𝐹 β€œ 𝑉) ↔ (𝑦 ∩ (◑𝐹 β€œ 𝑉)) βŠ† (◑𝐹 β€œ 𝑉)))
3315, 32syl 17 . . . . . . . . . . . 12 ((((𝐹 ∈ (𝐢 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 βŠ† π‘ˆ) ∧ π‘₯ ∈ (π‘†β€˜π‘ˆ)) ∧ 𝑦 ∈ π‘₯) β†’ ((𝑦 ∩ (◑𝐹 β€œ 𝑉)) ∈ 𝒫 (◑𝐹 β€œ 𝑉) ↔ (𝑦 ∩ (◑𝐹 β€œ 𝑉)) βŠ† (◑𝐹 β€œ 𝑉)))
3431, 33mpbiri 258 . . . . . . . . . . 11 ((((𝐹 ∈ (𝐢 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 βŠ† π‘ˆ) ∧ π‘₯ ∈ (π‘†β€˜π‘ˆ)) ∧ 𝑦 ∈ π‘₯) β†’ (𝑦 ∩ (◑𝐹 β€œ 𝑉)) ∈ 𝒫 (◑𝐹 β€œ 𝑉))
3534fmpttd 7068 . . . . . . . . . 10 (((𝐹 ∈ (𝐢 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 βŠ† π‘ˆ) ∧ π‘₯ ∈ (π‘†β€˜π‘ˆ)) β†’ (𝑦 ∈ π‘₯ ↦ (𝑦 ∩ (◑𝐹 β€œ 𝑉))):π‘₯βŸΆπ’« (◑𝐹 β€œ 𝑉))
3635frnd 6681 . . . . . . . . 9 (((𝐹 ∈ (𝐢 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 βŠ† π‘ˆ) ∧ π‘₯ ∈ (π‘†β€˜π‘ˆ)) β†’ ran (𝑦 ∈ π‘₯ ↦ (𝑦 ∩ (◑𝐹 β€œ 𝑉))) βŠ† 𝒫 (◑𝐹 β€œ 𝑉))
37 sspwuni 5065 . . . . . . . . 9 (ran (𝑦 ∈ π‘₯ ↦ (𝑦 ∩ (◑𝐹 β€œ 𝑉))) βŠ† 𝒫 (◑𝐹 β€œ 𝑉) ↔ βˆͺ ran (𝑦 ∈ π‘₯ ↦ (𝑦 ∩ (◑𝐹 β€œ 𝑉))) βŠ† (◑𝐹 β€œ 𝑉))
3836, 37sylib 217 . . . . . . . 8 (((𝐹 ∈ (𝐢 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 βŠ† π‘ˆ) ∧ π‘₯ ∈ (π‘†β€˜π‘ˆ)) β†’ βˆͺ ran (𝑦 ∈ π‘₯ ↦ (𝑦 ∩ (◑𝐹 β€œ 𝑉))) βŠ† (◑𝐹 β€œ 𝑉))
39 simpl3 1194 . . . . . . . . . . . 12 (((𝐹 ∈ (𝐢 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 βŠ† π‘ˆ) ∧ π‘₯ ∈ (π‘†β€˜π‘ˆ)) β†’ 𝑉 βŠ† π‘ˆ)
40 imass2 6059 . . . . . . . . . . . 12 (𝑉 βŠ† π‘ˆ β†’ (◑𝐹 β€œ 𝑉) βŠ† (◑𝐹 β€œ π‘ˆ))
4139, 40syl 17 . . . . . . . . . . 11 (((𝐹 ∈ (𝐢 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 βŠ† π‘ˆ) ∧ π‘₯ ∈ (π‘†β€˜π‘ˆ)) β†’ (◑𝐹 β€œ 𝑉) βŠ† (◑𝐹 β€œ π‘ˆ))
427cvmsuni 33903 . . . . . . . . . . . 12 (π‘₯ ∈ (π‘†β€˜π‘ˆ) β†’ βˆͺ π‘₯ = (◑𝐹 β€œ π‘ˆ))
4342adantl 483 . . . . . . . . . . 11 (((𝐹 ∈ (𝐢 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 βŠ† π‘ˆ) ∧ π‘₯ ∈ (π‘†β€˜π‘ˆ)) β†’ βˆͺ π‘₯ = (◑𝐹 β€œ π‘ˆ))
4441, 43sseqtrrd 3990 . . . . . . . . . 10 (((𝐹 ∈ (𝐢 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 βŠ† π‘ˆ) ∧ π‘₯ ∈ (π‘†β€˜π‘ˆ)) β†’ (◑𝐹 β€œ 𝑉) βŠ† βˆͺ π‘₯)
4544sselda 3949 . . . . . . . . 9 ((((𝐹 ∈ (𝐢 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 βŠ† π‘ˆ) ∧ π‘₯ ∈ (π‘†β€˜π‘ˆ)) ∧ 𝑧 ∈ (◑𝐹 β€œ 𝑉)) β†’ 𝑧 ∈ βˆͺ π‘₯)
46 eqid 2737 . . . . . . . . . . . . . . 15 (𝑑 ∩ (◑𝐹 β€œ 𝑉)) = (𝑑 ∩ (◑𝐹 β€œ 𝑉))
47 ineq1 4170 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑑 β†’ (𝑦 ∩ (◑𝐹 β€œ 𝑉)) = (𝑑 ∩ (◑𝐹 β€œ 𝑉)))
4847rspceeqv 3600 . . . . . . . . . . . . . . 15 ((𝑑 ∈ π‘₯ ∧ (𝑑 ∩ (◑𝐹 β€œ 𝑉)) = (𝑑 ∩ (◑𝐹 β€œ 𝑉))) β†’ βˆƒπ‘¦ ∈ π‘₯ (𝑑 ∩ (◑𝐹 β€œ 𝑉)) = (𝑦 ∩ (◑𝐹 β€œ 𝑉)))
4946, 48mpan2 690 . . . . . . . . . . . . . 14 (𝑑 ∈ π‘₯ β†’ βˆƒπ‘¦ ∈ π‘₯ (𝑑 ∩ (◑𝐹 β€œ 𝑉)) = (𝑦 ∩ (◑𝐹 β€œ 𝑉)))
5049ad2antrl 727 . . . . . . . . . . . . 13 (((((𝐹 ∈ (𝐢 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 βŠ† π‘ˆ) ∧ π‘₯ ∈ (π‘†β€˜π‘ˆ)) ∧ 𝑧 ∈ (◑𝐹 β€œ 𝑉)) ∧ (𝑑 ∈ π‘₯ ∧ 𝑧 ∈ 𝑑)) β†’ βˆƒπ‘¦ ∈ π‘₯ (𝑑 ∩ (◑𝐹 β€œ 𝑉)) = (𝑦 ∩ (◑𝐹 β€œ 𝑉)))
51 vex 3452 . . . . . . . . . . . . . . 15 𝑑 ∈ V
5251inex1 5279 . . . . . . . . . . . . . 14 (𝑑 ∩ (◑𝐹 β€œ 𝑉)) ∈ V
53 eqid 2737 . . . . . . . . . . . . . . 15 (𝑦 ∈ π‘₯ ↦ (𝑦 ∩ (◑𝐹 β€œ 𝑉))) = (𝑦 ∈ π‘₯ ↦ (𝑦 ∩ (◑𝐹 β€œ 𝑉)))
5453elrnmpt 5916 . . . . . . . . . . . . . 14 ((𝑑 ∩ (◑𝐹 β€œ 𝑉)) ∈ V β†’ ((𝑑 ∩ (◑𝐹 β€œ 𝑉)) ∈ ran (𝑦 ∈ π‘₯ ↦ (𝑦 ∩ (◑𝐹 β€œ 𝑉))) ↔ βˆƒπ‘¦ ∈ π‘₯ (𝑑 ∩ (◑𝐹 β€œ 𝑉)) = (𝑦 ∩ (◑𝐹 β€œ 𝑉))))
5552, 54ax-mp 5 . . . . . . . . . . . . 13 ((𝑑 ∩ (◑𝐹 β€œ 𝑉)) ∈ ran (𝑦 ∈ π‘₯ ↦ (𝑦 ∩ (◑𝐹 β€œ 𝑉))) ↔ βˆƒπ‘¦ ∈ π‘₯ (𝑑 ∩ (◑𝐹 β€œ 𝑉)) = (𝑦 ∩ (◑𝐹 β€œ 𝑉)))
5650, 55sylibr 233 . . . . . . . . . . . 12 (((((𝐹 ∈ (𝐢 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 βŠ† π‘ˆ) ∧ π‘₯ ∈ (π‘†β€˜π‘ˆ)) ∧ 𝑧 ∈ (◑𝐹 β€œ 𝑉)) ∧ (𝑑 ∈ π‘₯ ∧ 𝑧 ∈ 𝑑)) β†’ (𝑑 ∩ (◑𝐹 β€œ 𝑉)) ∈ ran (𝑦 ∈ π‘₯ ↦ (𝑦 ∩ (◑𝐹 β€œ 𝑉))))
57 simprr 772 . . . . . . . . . . . . 13 (((((𝐹 ∈ (𝐢 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 βŠ† π‘ˆ) ∧ π‘₯ ∈ (π‘†β€˜π‘ˆ)) ∧ 𝑧 ∈ (◑𝐹 β€œ 𝑉)) ∧ (𝑑 ∈ π‘₯ ∧ 𝑧 ∈ 𝑑)) β†’ 𝑧 ∈ 𝑑)
58 simplr 768 . . . . . . . . . . . . 13 (((((𝐹 ∈ (𝐢 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 βŠ† π‘ˆ) ∧ π‘₯ ∈ (π‘†β€˜π‘ˆ)) ∧ 𝑧 ∈ (◑𝐹 β€œ 𝑉)) ∧ (𝑑 ∈ π‘₯ ∧ 𝑧 ∈ 𝑑)) β†’ 𝑧 ∈ (◑𝐹 β€œ 𝑉))
5957, 58elind 4159 . . . . . . . . . . . 12 (((((𝐹 ∈ (𝐢 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 βŠ† π‘ˆ) ∧ π‘₯ ∈ (π‘†β€˜π‘ˆ)) ∧ 𝑧 ∈ (◑𝐹 β€œ 𝑉)) ∧ (𝑑 ∈ π‘₯ ∧ 𝑧 ∈ 𝑑)) β†’ 𝑧 ∈ (𝑑 ∩ (◑𝐹 β€œ 𝑉)))
60 eleq2 2827 . . . . . . . . . . . . 13 (𝑀 = (𝑑 ∩ (◑𝐹 β€œ 𝑉)) β†’ (𝑧 ∈ 𝑀 ↔ 𝑧 ∈ (𝑑 ∩ (◑𝐹 β€œ 𝑉))))
6160rspcev 3584 . . . . . . . . . . . 12 (((𝑑 ∩ (◑𝐹 β€œ 𝑉)) ∈ ran (𝑦 ∈ π‘₯ ↦ (𝑦 ∩ (◑𝐹 β€œ 𝑉))) ∧ 𝑧 ∈ (𝑑 ∩ (◑𝐹 β€œ 𝑉))) β†’ βˆƒπ‘€ ∈ ran (𝑦 ∈ π‘₯ ↦ (𝑦 ∩ (◑𝐹 β€œ 𝑉)))𝑧 ∈ 𝑀)
6256, 59, 61syl2anc 585 . . . . . . . . . . 11 (((((𝐹 ∈ (𝐢 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 βŠ† π‘ˆ) ∧ π‘₯ ∈ (π‘†β€˜π‘ˆ)) ∧ 𝑧 ∈ (◑𝐹 β€œ 𝑉)) ∧ (𝑑 ∈ π‘₯ ∧ 𝑧 ∈ 𝑑)) β†’ βˆƒπ‘€ ∈ ran (𝑦 ∈ π‘₯ ↦ (𝑦 ∩ (◑𝐹 β€œ 𝑉)))𝑧 ∈ 𝑀)
6362rexlimdvaa 3154 . . . . . . . . . 10 ((((𝐹 ∈ (𝐢 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 βŠ† π‘ˆ) ∧ π‘₯ ∈ (π‘†β€˜π‘ˆ)) ∧ 𝑧 ∈ (◑𝐹 β€œ 𝑉)) β†’ (βˆƒπ‘‘ ∈ π‘₯ 𝑧 ∈ 𝑑 β†’ βˆƒπ‘€ ∈ ran (𝑦 ∈ π‘₯ ↦ (𝑦 ∩ (◑𝐹 β€œ 𝑉)))𝑧 ∈ 𝑀))
64 eluni2 4874 . . . . . . . . . 10 (𝑧 ∈ βˆͺ π‘₯ ↔ βˆƒπ‘‘ ∈ π‘₯ 𝑧 ∈ 𝑑)
65 eluni2 4874 . . . . . . . . . 10 (𝑧 ∈ βˆͺ ran (𝑦 ∈ π‘₯ ↦ (𝑦 ∩ (◑𝐹 β€œ 𝑉))) ↔ βˆƒπ‘€ ∈ ran (𝑦 ∈ π‘₯ ↦ (𝑦 ∩ (◑𝐹 β€œ 𝑉)))𝑧 ∈ 𝑀)
6663, 64, 653imtr4g 296 . . . . . . . . 9 ((((𝐹 ∈ (𝐢 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 βŠ† π‘ˆ) ∧ π‘₯ ∈ (π‘†β€˜π‘ˆ)) ∧ 𝑧 ∈ (◑𝐹 β€œ 𝑉)) β†’ (𝑧 ∈ βˆͺ π‘₯ β†’ 𝑧 ∈ βˆͺ ran (𝑦 ∈ π‘₯ ↦ (𝑦 ∩ (◑𝐹 β€œ 𝑉)))))
6745, 66mpd 15 . . . . . . . 8 ((((𝐹 ∈ (𝐢 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 βŠ† π‘ˆ) ∧ π‘₯ ∈ (π‘†β€˜π‘ˆ)) ∧ 𝑧 ∈ (◑𝐹 β€œ 𝑉)) β†’ 𝑧 ∈ βˆͺ ran (𝑦 ∈ π‘₯ ↦ (𝑦 ∩ (◑𝐹 β€œ 𝑉))))
6838, 67eqelssd 3970 . . . . . . 7 (((𝐹 ∈ (𝐢 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 βŠ† π‘ˆ) ∧ π‘₯ ∈ (π‘†β€˜π‘ˆ)) β†’ βˆͺ ran (𝑦 ∈ π‘₯ ↦ (𝑦 ∩ (◑𝐹 β€œ 𝑉))) = (◑𝐹 β€œ 𝑉))
69 eldifsn 4752 . . . . . . . . . . . 12 (𝑧 ∈ (ran (𝑦 ∈ π‘₯ ↦ (𝑦 ∩ (◑𝐹 β€œ 𝑉))) βˆ– {(𝑑 ∩ (◑𝐹 β€œ 𝑉))}) ↔ (𝑧 ∈ ran (𝑦 ∈ π‘₯ ↦ (𝑦 ∩ (◑𝐹 β€œ 𝑉))) ∧ 𝑧 β‰  (𝑑 ∩ (◑𝐹 β€œ 𝑉))))
70 vex 3452 . . . . . . . . . . . . . . 15 𝑧 ∈ V
7153elrnmpt 5916 . . . . . . . . . . . . . . 15 (𝑧 ∈ V β†’ (𝑧 ∈ ran (𝑦 ∈ π‘₯ ↦ (𝑦 ∩ (◑𝐹 β€œ 𝑉))) ↔ βˆƒπ‘¦ ∈ π‘₯ 𝑧 = (𝑦 ∩ (◑𝐹 β€œ 𝑉))))
7270, 71ax-mp 5 . . . . . . . . . . . . . 14 (𝑧 ∈ ran (𝑦 ∈ π‘₯ ↦ (𝑦 ∩ (◑𝐹 β€œ 𝑉))) ↔ βˆƒπ‘¦ ∈ π‘₯ 𝑧 = (𝑦 ∩ (◑𝐹 β€œ 𝑉)))
7347equcoms 2024 . . . . . . . . . . . . . . . . . 18 (𝑑 = 𝑦 β†’ (𝑦 ∩ (◑𝐹 β€œ 𝑉)) = (𝑑 ∩ (◑𝐹 β€œ 𝑉)))
7473necon3ai 2969 . . . . . . . . . . . . . . . . 17 ((𝑦 ∩ (◑𝐹 β€œ 𝑉)) β‰  (𝑑 ∩ (◑𝐹 β€œ 𝑉)) β†’ Β¬ 𝑑 = 𝑦)
75 simpllr 775 . . . . . . . . . . . . . . . . . . 19 (((((𝐹 ∈ (𝐢 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 βŠ† π‘ˆ) ∧ π‘₯ ∈ (π‘†β€˜π‘ˆ)) ∧ 𝑑 ∈ π‘₯) ∧ 𝑦 ∈ π‘₯) β†’ π‘₯ ∈ (π‘†β€˜π‘ˆ))
76 simplr 768 . . . . . . . . . . . . . . . . . . 19 (((((𝐹 ∈ (𝐢 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 βŠ† π‘ˆ) ∧ π‘₯ ∈ (π‘†β€˜π‘ˆ)) ∧ 𝑑 ∈ π‘₯) ∧ 𝑦 ∈ π‘₯) β†’ 𝑑 ∈ π‘₯)
77 simpr 486 . . . . . . . . . . . . . . . . . . 19 (((((𝐹 ∈ (𝐢 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 βŠ† π‘ˆ) ∧ π‘₯ ∈ (π‘†β€˜π‘ˆ)) ∧ 𝑑 ∈ π‘₯) ∧ 𝑦 ∈ π‘₯) β†’ 𝑦 ∈ π‘₯)
787cvmsdisj 33904 . . . . . . . . . . . . . . . . . . 19 ((π‘₯ ∈ (π‘†β€˜π‘ˆ) ∧ 𝑑 ∈ π‘₯ ∧ 𝑦 ∈ π‘₯) β†’ (𝑑 = 𝑦 ∨ (𝑑 ∩ 𝑦) = βˆ…))
7975, 76, 77, 78syl3anc 1372 . . . . . . . . . . . . . . . . . 18 (((((𝐹 ∈ (𝐢 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 βŠ† π‘ˆ) ∧ π‘₯ ∈ (π‘†β€˜π‘ˆ)) ∧ 𝑑 ∈ π‘₯) ∧ 𝑦 ∈ π‘₯) β†’ (𝑑 = 𝑦 ∨ (𝑑 ∩ 𝑦) = βˆ…))
8079ord 863 . . . . . . . . . . . . . . . . 17 (((((𝐹 ∈ (𝐢 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 βŠ† π‘ˆ) ∧ π‘₯ ∈ (π‘†β€˜π‘ˆ)) ∧ 𝑑 ∈ π‘₯) ∧ 𝑦 ∈ π‘₯) β†’ (Β¬ 𝑑 = 𝑦 β†’ (𝑑 ∩ 𝑦) = βˆ…))
81 inss1 4193 . . . . . . . . . . . . . . . . . 18 ((𝑑 ∩ 𝑦) ∩ (◑𝐹 β€œ 𝑉)) βŠ† (𝑑 ∩ 𝑦)
82 sseq0 4364 . . . . . . . . . . . . . . . . . 18 ((((𝑑 ∩ 𝑦) ∩ (◑𝐹 β€œ 𝑉)) βŠ† (𝑑 ∩ 𝑦) ∧ (𝑑 ∩ 𝑦) = βˆ…) β†’ ((𝑑 ∩ 𝑦) ∩ (◑𝐹 β€œ 𝑉)) = βˆ…)
8381, 82mpan 689 . . . . . . . . . . . . . . . . 17 ((𝑑 ∩ 𝑦) = βˆ… β†’ ((𝑑 ∩ 𝑦) ∩ (◑𝐹 β€œ 𝑉)) = βˆ…)
8474, 80, 83syl56 36 . . . . . . . . . . . . . . . 16 (((((𝐹 ∈ (𝐢 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 βŠ† π‘ˆ) ∧ π‘₯ ∈ (π‘†β€˜π‘ˆ)) ∧ 𝑑 ∈ π‘₯) ∧ 𝑦 ∈ π‘₯) β†’ ((𝑦 ∩ (◑𝐹 β€œ 𝑉)) β‰  (𝑑 ∩ (◑𝐹 β€œ 𝑉)) β†’ ((𝑑 ∩ 𝑦) ∩ (◑𝐹 β€œ 𝑉)) = βˆ…))
85 neeq1 3007 . . . . . . . . . . . . . . . . 17 (𝑧 = (𝑦 ∩ (◑𝐹 β€œ 𝑉)) β†’ (𝑧 β‰  (𝑑 ∩ (◑𝐹 β€œ 𝑉)) ↔ (𝑦 ∩ (◑𝐹 β€œ 𝑉)) β‰  (𝑑 ∩ (◑𝐹 β€œ 𝑉))))
86 ineq2 4171 . . . . . . . . . . . . . . . . . . 19 (𝑧 = (𝑦 ∩ (◑𝐹 β€œ 𝑉)) β†’ ((𝑑 ∩ (◑𝐹 β€œ 𝑉)) ∩ 𝑧) = ((𝑑 ∩ (◑𝐹 β€œ 𝑉)) ∩ (𝑦 ∩ (◑𝐹 β€œ 𝑉))))
87 inindir 4192 . . . . . . . . . . . . . . . . . . 19 ((𝑑 ∩ 𝑦) ∩ (◑𝐹 β€œ 𝑉)) = ((𝑑 ∩ (◑𝐹 β€œ 𝑉)) ∩ (𝑦 ∩ (◑𝐹 β€œ 𝑉)))
8886, 87eqtr4di 2795 . . . . . . . . . . . . . . . . . 18 (𝑧 = (𝑦 ∩ (◑𝐹 β€œ 𝑉)) β†’ ((𝑑 ∩ (◑𝐹 β€œ 𝑉)) ∩ 𝑧) = ((𝑑 ∩ 𝑦) ∩ (◑𝐹 β€œ 𝑉)))
8988eqeq1d 2739 . . . . . . . . . . . . . . . . 17 (𝑧 = (𝑦 ∩ (◑𝐹 β€œ 𝑉)) β†’ (((𝑑 ∩ (◑𝐹 β€œ 𝑉)) ∩ 𝑧) = βˆ… ↔ ((𝑑 ∩ 𝑦) ∩ (◑𝐹 β€œ 𝑉)) = βˆ…))
9085, 89imbi12d 345 . . . . . . . . . . . . . . . 16 (𝑧 = (𝑦 ∩ (◑𝐹 β€œ 𝑉)) β†’ ((𝑧 β‰  (𝑑 ∩ (◑𝐹 β€œ 𝑉)) β†’ ((𝑑 ∩ (◑𝐹 β€œ 𝑉)) ∩ 𝑧) = βˆ…) ↔ ((𝑦 ∩ (◑𝐹 β€œ 𝑉)) β‰  (𝑑 ∩ (◑𝐹 β€œ 𝑉)) β†’ ((𝑑 ∩ 𝑦) ∩ (◑𝐹 β€œ 𝑉)) = βˆ…)))
9184, 90syl5ibrcom 247 . . . . . . . . . . . . . . 15 (((((𝐹 ∈ (𝐢 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 βŠ† π‘ˆ) ∧ π‘₯ ∈ (π‘†β€˜π‘ˆ)) ∧ 𝑑 ∈ π‘₯) ∧ 𝑦 ∈ π‘₯) β†’ (𝑧 = (𝑦 ∩ (◑𝐹 β€œ 𝑉)) β†’ (𝑧 β‰  (𝑑 ∩ (◑𝐹 β€œ 𝑉)) β†’ ((𝑑 ∩ (◑𝐹 β€œ 𝑉)) ∩ 𝑧) = βˆ…)))
9291rexlimdva 3153 . . . . . . . . . . . . . 14 ((((𝐹 ∈ (𝐢 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 βŠ† π‘ˆ) ∧ π‘₯ ∈ (π‘†β€˜π‘ˆ)) ∧ 𝑑 ∈ π‘₯) β†’ (βˆƒπ‘¦ ∈ π‘₯ 𝑧 = (𝑦 ∩ (◑𝐹 β€œ 𝑉)) β†’ (𝑧 β‰  (𝑑 ∩ (◑𝐹 β€œ 𝑉)) β†’ ((𝑑 ∩ (◑𝐹 β€œ 𝑉)) ∩ 𝑧) = βˆ…)))
9372, 92biimtrid 241 . . . . . . . . . . . . 13 ((((𝐹 ∈ (𝐢 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 βŠ† π‘ˆ) ∧ π‘₯ ∈ (π‘†β€˜π‘ˆ)) ∧ 𝑑 ∈ π‘₯) β†’ (𝑧 ∈ ran (𝑦 ∈ π‘₯ ↦ (𝑦 ∩ (◑𝐹 β€œ 𝑉))) β†’ (𝑧 β‰  (𝑑 ∩ (◑𝐹 β€œ 𝑉)) β†’ ((𝑑 ∩ (◑𝐹 β€œ 𝑉)) ∩ 𝑧) = βˆ…)))
9493impd 412 . . . . . . . . . . . 12 ((((𝐹 ∈ (𝐢 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 βŠ† π‘ˆ) ∧ π‘₯ ∈ (π‘†β€˜π‘ˆ)) ∧ 𝑑 ∈ π‘₯) β†’ ((𝑧 ∈ ran (𝑦 ∈ π‘₯ ↦ (𝑦 ∩ (◑𝐹 β€œ 𝑉))) ∧ 𝑧 β‰  (𝑑 ∩ (◑𝐹 β€œ 𝑉))) β†’ ((𝑑 ∩ (◑𝐹 β€œ 𝑉)) ∩ 𝑧) = βˆ…))
9569, 94biimtrid 241 . . . . . . . . . . 11 ((((𝐹 ∈ (𝐢 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 βŠ† π‘ˆ) ∧ π‘₯ ∈ (π‘†β€˜π‘ˆ)) ∧ 𝑑 ∈ π‘₯) β†’ (𝑧 ∈ (ran (𝑦 ∈ π‘₯ ↦ (𝑦 ∩ (◑𝐹 β€œ 𝑉))) βˆ– {(𝑑 ∩ (◑𝐹 β€œ 𝑉))}) β†’ ((𝑑 ∩ (◑𝐹 β€œ 𝑉)) ∩ 𝑧) = βˆ…))
9695ralrimiv 3143 . . . . . . . . . 10 ((((𝐹 ∈ (𝐢 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 βŠ† π‘ˆ) ∧ π‘₯ ∈ (π‘†β€˜π‘ˆ)) ∧ 𝑑 ∈ π‘₯) β†’ βˆ€π‘§ ∈ (ran (𝑦 ∈ π‘₯ ↦ (𝑦 ∩ (◑𝐹 β€œ 𝑉))) βˆ– {(𝑑 ∩ (◑𝐹 β€œ 𝑉))})((𝑑 ∩ (◑𝐹 β€œ 𝑉)) ∩ 𝑧) = βˆ…)
97 inss1 4193 . . . . . . . . . . . . 13 (𝑑 ∩ (◑𝐹 β€œ 𝑉)) βŠ† 𝑑
98 resabs1 5972 . . . . . . . . . . . . 13 ((𝑑 ∩ (◑𝐹 β€œ 𝑉)) βŠ† 𝑑 β†’ ((𝐹 β†Ύ 𝑑) β†Ύ (𝑑 ∩ (◑𝐹 β€œ 𝑉))) = (𝐹 β†Ύ (𝑑 ∩ (◑𝐹 β€œ 𝑉))))
9997, 98ax-mp 5 . . . . . . . . . . . 12 ((𝐹 β†Ύ 𝑑) β†Ύ (𝑑 ∩ (◑𝐹 β€œ 𝑉))) = (𝐹 β†Ύ (𝑑 ∩ (◑𝐹 β€œ 𝑉)))
1007cvmshmeo 33905 . . . . . . . . . . . . . 14 ((π‘₯ ∈ (π‘†β€˜π‘ˆ) ∧ 𝑑 ∈ π‘₯) β†’ (𝐹 β†Ύ 𝑑) ∈ ((𝐢 β†Ύt 𝑑)Homeo(𝐽 β†Ύt π‘ˆ)))
101100adantll 713 . . . . . . . . . . . . 13 ((((𝐹 ∈ (𝐢 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 βŠ† π‘ˆ) ∧ π‘₯ ∈ (π‘†β€˜π‘ˆ)) ∧ 𝑑 ∈ π‘₯) β†’ (𝐹 β†Ύ 𝑑) ∈ ((𝐢 β†Ύt 𝑑)Homeo(𝐽 β†Ύt π‘ˆ)))
1025adantr 482 . . . . . . . . . . . . . . 15 ((((𝐹 ∈ (𝐢 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 βŠ† π‘ˆ) ∧ π‘₯ ∈ (π‘†β€˜π‘ˆ)) ∧ 𝑑 ∈ π‘₯) β†’ 𝐢 ∈ Top)
1039sselda 3949 . . . . . . . . . . . . . . . 16 ((((𝐹 ∈ (𝐢 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 βŠ† π‘ˆ) ∧ π‘₯ ∈ (π‘†β€˜π‘ˆ)) ∧ 𝑑 ∈ π‘₯) β†’ 𝑑 ∈ 𝐢)
104 elssuni 4903 . . . . . . . . . . . . . . . 16 (𝑑 ∈ 𝐢 β†’ 𝑑 βŠ† βˆͺ 𝐢)
105103, 104syl 17 . . . . . . . . . . . . . . 15 ((((𝐹 ∈ (𝐢 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 βŠ† π‘ˆ) ∧ π‘₯ ∈ (π‘†β€˜π‘ˆ)) ∧ 𝑑 ∈ π‘₯) β†’ 𝑑 βŠ† βˆͺ 𝐢)
106 eqid 2737 . . . . . . . . . . . . . . . 16 βˆͺ 𝐢 = βˆͺ 𝐢
107106restuni 22529 . . . . . . . . . . . . . . 15 ((𝐢 ∈ Top ∧ 𝑑 βŠ† βˆͺ 𝐢) β†’ 𝑑 = βˆͺ (𝐢 β†Ύt 𝑑))
108102, 105, 107syl2anc 585 . . . . . . . . . . . . . 14 ((((𝐹 ∈ (𝐢 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 βŠ† π‘ˆ) ∧ π‘₯ ∈ (π‘†β€˜π‘ˆ)) ∧ 𝑑 ∈ π‘₯) β†’ 𝑑 = βˆͺ (𝐢 β†Ύt 𝑑))
10997, 108sseqtrid 4001 . . . . . . . . . . . . 13 ((((𝐹 ∈ (𝐢 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 βŠ† π‘ˆ) ∧ π‘₯ ∈ (π‘†β€˜π‘ˆ)) ∧ 𝑑 ∈ π‘₯) β†’ (𝑑 ∩ (◑𝐹 β€œ 𝑉)) βŠ† βˆͺ (𝐢 β†Ύt 𝑑))
110 eqid 2737 . . . . . . . . . . . . . 14 βˆͺ (𝐢 β†Ύt 𝑑) = βˆͺ (𝐢 β†Ύt 𝑑)
111110hmeores 23138 . . . . . . . . . . . . 13 (((𝐹 β†Ύ 𝑑) ∈ ((𝐢 β†Ύt 𝑑)Homeo(𝐽 β†Ύt π‘ˆ)) ∧ (𝑑 ∩ (◑𝐹 β€œ 𝑉)) βŠ† βˆͺ (𝐢 β†Ύt 𝑑)) β†’ ((𝐹 β†Ύ 𝑑) β†Ύ (𝑑 ∩ (◑𝐹 β€œ 𝑉))) ∈ (((𝐢 β†Ύt 𝑑) β†Ύt (𝑑 ∩ (◑𝐹 β€œ 𝑉)))Homeo((𝐽 β†Ύt π‘ˆ) β†Ύt ((𝐹 β†Ύ 𝑑) β€œ (𝑑 ∩ (◑𝐹 β€œ 𝑉))))))
112101, 109, 111syl2anc 585 . . . . . . . . . . . 12 ((((𝐹 ∈ (𝐢 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 βŠ† π‘ˆ) ∧ π‘₯ ∈ (π‘†β€˜π‘ˆ)) ∧ 𝑑 ∈ π‘₯) β†’ ((𝐹 β†Ύ 𝑑) β†Ύ (𝑑 ∩ (◑𝐹 β€œ 𝑉))) ∈ (((𝐢 β†Ύt 𝑑) β†Ύt (𝑑 ∩ (◑𝐹 β€œ 𝑉)))Homeo((𝐽 β†Ύt π‘ˆ) β†Ύt ((𝐹 β†Ύ 𝑑) β€œ (𝑑 ∩ (◑𝐹 β€œ 𝑉))))))
11399, 112eqeltrrid 2843 . . . . . . . . . . 11 ((((𝐹 ∈ (𝐢 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 βŠ† π‘ˆ) ∧ π‘₯ ∈ (π‘†β€˜π‘ˆ)) ∧ 𝑑 ∈ π‘₯) β†’ (𝐹 β†Ύ (𝑑 ∩ (◑𝐹 β€œ 𝑉))) ∈ (((𝐢 β†Ύt 𝑑) β†Ύt (𝑑 ∩ (◑𝐹 β€œ 𝑉)))Homeo((𝐽 β†Ύt π‘ˆ) β†Ύt ((𝐹 β†Ύ 𝑑) β€œ (𝑑 ∩ (◑𝐹 β€œ 𝑉))))))
11497a1i 11 . . . . . . . . . . . . 13 ((((𝐹 ∈ (𝐢 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 βŠ† π‘ˆ) ∧ π‘₯ ∈ (π‘†β€˜π‘ˆ)) ∧ 𝑑 ∈ π‘₯) β†’ (𝑑 ∩ (◑𝐹 β€œ 𝑉)) βŠ† 𝑑)
115 simpr 486 . . . . . . . . . . . . 13 ((((𝐹 ∈ (𝐢 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 βŠ† π‘ˆ) ∧ π‘₯ ∈ (π‘†β€˜π‘ˆ)) ∧ 𝑑 ∈ π‘₯) β†’ 𝑑 ∈ π‘₯)
116 restabs 22532 . . . . . . . . . . . . 13 ((𝐢 ∈ Top ∧ (𝑑 ∩ (◑𝐹 β€œ 𝑉)) βŠ† 𝑑 ∧ 𝑑 ∈ π‘₯) β†’ ((𝐢 β†Ύt 𝑑) β†Ύt (𝑑 ∩ (◑𝐹 β€œ 𝑉))) = (𝐢 β†Ύt (𝑑 ∩ (◑𝐹 β€œ 𝑉))))
117102, 114, 115, 116syl3anc 1372 . . . . . . . . . . . 12 ((((𝐹 ∈ (𝐢 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 βŠ† π‘ˆ) ∧ π‘₯ ∈ (π‘†β€˜π‘ˆ)) ∧ 𝑑 ∈ π‘₯) β†’ ((𝐢 β†Ύt 𝑑) β†Ύt (𝑑 ∩ (◑𝐹 β€œ 𝑉))) = (𝐢 β†Ύt (𝑑 ∩ (◑𝐹 β€œ 𝑉))))
118 incom 4166 . . . . . . . . . . . . . . . . 17 (𝑑 ∩ (◑𝐹 β€œ 𝑉)) = ((◑𝐹 β€œ 𝑉) ∩ 𝑑)
119 cnvresima 6187 . . . . . . . . . . . . . . . . 17 (β—‘(𝐹 β†Ύ 𝑑) β€œ 𝑉) = ((◑𝐹 β€œ 𝑉) ∩ 𝑑)
120118, 119eqtr4i 2768 . . . . . . . . . . . . . . . 16 (𝑑 ∩ (◑𝐹 β€œ 𝑉)) = (β—‘(𝐹 β†Ύ 𝑑) β€œ 𝑉)
121120imaeq2i 6016 . . . . . . . . . . . . . . 15 ((𝐹 β†Ύ 𝑑) β€œ (𝑑 ∩ (◑𝐹 β€œ 𝑉))) = ((𝐹 β†Ύ 𝑑) β€œ (β—‘(𝐹 β†Ύ 𝑑) β€œ 𝑉))
1223adantr 482 . . . . . . . . . . . . . . . . . 18 ((((𝐹 ∈ (𝐢 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 βŠ† π‘ˆ) ∧ π‘₯ ∈ (π‘†β€˜π‘ˆ)) ∧ 𝑑 ∈ π‘₯) β†’ 𝐹 ∈ (𝐢 CovMap 𝐽))
123 simplr 768 . . . . . . . . . . . . . . . . . 18 ((((𝐹 ∈ (𝐢 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 βŠ† π‘ˆ) ∧ π‘₯ ∈ (π‘†β€˜π‘ˆ)) ∧ 𝑑 ∈ π‘₯) β†’ π‘₯ ∈ (π‘†β€˜π‘ˆ))
1247cvmsf1o 33906 . . . . . . . . . . . . . . . . . 18 ((𝐹 ∈ (𝐢 CovMap 𝐽) ∧ π‘₯ ∈ (π‘†β€˜π‘ˆ) ∧ 𝑑 ∈ π‘₯) β†’ (𝐹 β†Ύ 𝑑):𝑑–1-1-ontoβ†’π‘ˆ)
125122, 123, 115, 124syl3anc 1372 . . . . . . . . . . . . . . . . 17 ((((𝐹 ∈ (𝐢 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 βŠ† π‘ˆ) ∧ π‘₯ ∈ (π‘†β€˜π‘ˆ)) ∧ 𝑑 ∈ π‘₯) β†’ (𝐹 β†Ύ 𝑑):𝑑–1-1-ontoβ†’π‘ˆ)
126 f1ofo 6796 . . . . . . . . . . . . . . . . 17 ((𝐹 β†Ύ 𝑑):𝑑–1-1-ontoβ†’π‘ˆ β†’ (𝐹 β†Ύ 𝑑):𝑑–ontoβ†’π‘ˆ)
127125, 126syl 17 . . . . . . . . . . . . . . . 16 ((((𝐹 ∈ (𝐢 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 βŠ† π‘ˆ) ∧ π‘₯ ∈ (π‘†β€˜π‘ˆ)) ∧ 𝑑 ∈ π‘₯) β†’ (𝐹 β†Ύ 𝑑):𝑑–ontoβ†’π‘ˆ)
12839adantr 482 . . . . . . . . . . . . . . . 16 ((((𝐹 ∈ (𝐢 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 βŠ† π‘ˆ) ∧ π‘₯ ∈ (π‘†β€˜π‘ˆ)) ∧ 𝑑 ∈ π‘₯) β†’ 𝑉 βŠ† π‘ˆ)
129 foimacnv 6806 . . . . . . . . . . . . . . . 16 (((𝐹 β†Ύ 𝑑):𝑑–ontoβ†’π‘ˆ ∧ 𝑉 βŠ† π‘ˆ) β†’ ((𝐹 β†Ύ 𝑑) β€œ (β—‘(𝐹 β†Ύ 𝑑) β€œ 𝑉)) = 𝑉)
130127, 128, 129syl2anc 585 . . . . . . . . . . . . . . 15 ((((𝐹 ∈ (𝐢 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 βŠ† π‘ˆ) ∧ π‘₯ ∈ (π‘†β€˜π‘ˆ)) ∧ 𝑑 ∈ π‘₯) β†’ ((𝐹 β†Ύ 𝑑) β€œ (β—‘(𝐹 β†Ύ 𝑑) β€œ 𝑉)) = 𝑉)
131121, 130eqtrid 2789 . . . . . . . . . . . . . 14 ((((𝐹 ∈ (𝐢 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 βŠ† π‘ˆ) ∧ π‘₯ ∈ (π‘†β€˜π‘ˆ)) ∧ 𝑑 ∈ π‘₯) β†’ ((𝐹 β†Ύ 𝑑) β€œ (𝑑 ∩ (◑𝐹 β€œ 𝑉))) = 𝑉)
132131oveq2d 7378 . . . . . . . . . . . . 13 ((((𝐹 ∈ (𝐢 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 βŠ† π‘ˆ) ∧ π‘₯ ∈ (π‘†β€˜π‘ˆ)) ∧ 𝑑 ∈ π‘₯) β†’ ((𝐽 β†Ύt π‘ˆ) β†Ύt ((𝐹 β†Ύ 𝑑) β€œ (𝑑 ∩ (◑𝐹 β€œ 𝑉)))) = ((𝐽 β†Ύt π‘ˆ) β†Ύt 𝑉))
133 cvmtop2 33895 . . . . . . . . . . . . . . . 16 (𝐹 ∈ (𝐢 CovMap 𝐽) β†’ 𝐽 ∈ Top)
1343, 133syl 17 . . . . . . . . . . . . . . 15 (((𝐹 ∈ (𝐢 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 βŠ† π‘ˆ) ∧ π‘₯ ∈ (π‘†β€˜π‘ˆ)) β†’ 𝐽 ∈ Top)
1357cvmsrcl 33898 . . . . . . . . . . . . . . . 16 (π‘₯ ∈ (π‘†β€˜π‘ˆ) β†’ π‘ˆ ∈ 𝐽)
136135adantl 483 . . . . . . . . . . . . . . 15 (((𝐹 ∈ (𝐢 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 βŠ† π‘ˆ) ∧ π‘₯ ∈ (π‘†β€˜π‘ˆ)) β†’ π‘ˆ ∈ 𝐽)
137 restabs 22532 . . . . . . . . . . . . . . 15 ((𝐽 ∈ Top ∧ 𝑉 βŠ† π‘ˆ ∧ π‘ˆ ∈ 𝐽) β†’ ((𝐽 β†Ύt π‘ˆ) β†Ύt 𝑉) = (𝐽 β†Ύt 𝑉))
138134, 39, 136, 137syl3anc 1372 . . . . . . . . . . . . . 14 (((𝐹 ∈ (𝐢 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 βŠ† π‘ˆ) ∧ π‘₯ ∈ (π‘†β€˜π‘ˆ)) β†’ ((𝐽 β†Ύt π‘ˆ) β†Ύt 𝑉) = (𝐽 β†Ύt 𝑉))
139138adantr 482 . . . . . . . . . . . . 13 ((((𝐹 ∈ (𝐢 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 βŠ† π‘ˆ) ∧ π‘₯ ∈ (π‘†β€˜π‘ˆ)) ∧ 𝑑 ∈ π‘₯) β†’ ((𝐽 β†Ύt π‘ˆ) β†Ύt 𝑉) = (𝐽 β†Ύt 𝑉))
140132, 139eqtrd 2777 . . . . . . . . . . . 12 ((((𝐹 ∈ (𝐢 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 βŠ† π‘ˆ) ∧ π‘₯ ∈ (π‘†β€˜π‘ˆ)) ∧ 𝑑 ∈ π‘₯) β†’ ((𝐽 β†Ύt π‘ˆ) β†Ύt ((𝐹 β†Ύ 𝑑) β€œ (𝑑 ∩ (◑𝐹 β€œ 𝑉)))) = (𝐽 β†Ύt 𝑉))
141117, 140oveq12d 7380 . . . . . . . . . . 11 ((((𝐹 ∈ (𝐢 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 βŠ† π‘ˆ) ∧ π‘₯ ∈ (π‘†β€˜π‘ˆ)) ∧ 𝑑 ∈ π‘₯) β†’ (((𝐢 β†Ύt 𝑑) β†Ύt (𝑑 ∩ (◑𝐹 β€œ 𝑉)))Homeo((𝐽 β†Ύt π‘ˆ) β†Ύt ((𝐹 β†Ύ 𝑑) β€œ (𝑑 ∩ (◑𝐹 β€œ 𝑉))))) = ((𝐢 β†Ύt (𝑑 ∩ (◑𝐹 β€œ 𝑉)))Homeo(𝐽 β†Ύt 𝑉)))
142113, 141eleqtrd 2840 . . . . . . . . . 10 ((((𝐹 ∈ (𝐢 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 βŠ† π‘ˆ) ∧ π‘₯ ∈ (π‘†β€˜π‘ˆ)) ∧ 𝑑 ∈ π‘₯) β†’ (𝐹 β†Ύ (𝑑 ∩ (◑𝐹 β€œ 𝑉))) ∈ ((𝐢 β†Ύt (𝑑 ∩ (◑𝐹 β€œ 𝑉)))Homeo(𝐽 β†Ύt 𝑉)))
14396, 142jca 513 . . . . . . . . 9 ((((𝐹 ∈ (𝐢 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 βŠ† π‘ˆ) ∧ π‘₯ ∈ (π‘†β€˜π‘ˆ)) ∧ 𝑑 ∈ π‘₯) β†’ (βˆ€π‘§ ∈ (ran (𝑦 ∈ π‘₯ ↦ (𝑦 ∩ (◑𝐹 β€œ 𝑉))) βˆ– {(𝑑 ∩ (◑𝐹 β€œ 𝑉))})((𝑑 ∩ (◑𝐹 β€œ 𝑉)) ∩ 𝑧) = βˆ… ∧ (𝐹 β†Ύ (𝑑 ∩ (◑𝐹 β€œ 𝑉))) ∈ ((𝐢 β†Ύt (𝑑 ∩ (◑𝐹 β€œ 𝑉)))Homeo(𝐽 β†Ύt 𝑉))))
144143ralrimiva 3144 . . . . . . . 8 (((𝐹 ∈ (𝐢 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 βŠ† π‘ˆ) ∧ π‘₯ ∈ (π‘†β€˜π‘ˆ)) β†’ βˆ€π‘‘ ∈ π‘₯ (βˆ€π‘§ ∈ (ran (𝑦 ∈ π‘₯ ↦ (𝑦 ∩ (◑𝐹 β€œ 𝑉))) βˆ– {(𝑑 ∩ (◑𝐹 β€œ 𝑉))})((𝑑 ∩ (◑𝐹 β€œ 𝑉)) ∩ 𝑧) = βˆ… ∧ (𝐹 β†Ύ (𝑑 ∩ (◑𝐹 β€œ 𝑉))) ∈ ((𝐢 β†Ύt (𝑑 ∩ (◑𝐹 β€œ 𝑉)))Homeo(𝐽 β†Ύt 𝑉))))
14552rgenw 3069 . . . . . . . . 9 βˆ€π‘‘ ∈ π‘₯ (𝑑 ∩ (◑𝐹 β€œ 𝑉)) ∈ V
14647cbvmptv 5223 . . . . . . . . . 10 (𝑦 ∈ π‘₯ ↦ (𝑦 ∩ (◑𝐹 β€œ 𝑉))) = (𝑑 ∈ π‘₯ ↦ (𝑑 ∩ (◑𝐹 β€œ 𝑉)))
147 sneq 4601 . . . . . . . . . . . . 13 (𝑀 = (𝑑 ∩ (◑𝐹 β€œ 𝑉)) β†’ {𝑀} = {(𝑑 ∩ (◑𝐹 β€œ 𝑉))})
148147difeq2d 4087 . . . . . . . . . . . 12 (𝑀 = (𝑑 ∩ (◑𝐹 β€œ 𝑉)) β†’ (ran (𝑦 ∈ π‘₯ ↦ (𝑦 ∩ (◑𝐹 β€œ 𝑉))) βˆ– {𝑀}) = (ran (𝑦 ∈ π‘₯ ↦ (𝑦 ∩ (◑𝐹 β€œ 𝑉))) βˆ– {(𝑑 ∩ (◑𝐹 β€œ 𝑉))}))
149 ineq1 4170 . . . . . . . . . . . . 13 (𝑀 = (𝑑 ∩ (◑𝐹 β€œ 𝑉)) β†’ (𝑀 ∩ 𝑧) = ((𝑑 ∩ (◑𝐹 β€œ 𝑉)) ∩ 𝑧))
150149eqeq1d 2739 . . . . . . . . . . . 12 (𝑀 = (𝑑 ∩ (◑𝐹 β€œ 𝑉)) β†’ ((𝑀 ∩ 𝑧) = βˆ… ↔ ((𝑑 ∩ (◑𝐹 β€œ 𝑉)) ∩ 𝑧) = βˆ…))
151148, 150raleqbidv 3322 . . . . . . . . . . 11 (𝑀 = (𝑑 ∩ (◑𝐹 β€œ 𝑉)) β†’ (βˆ€π‘§ ∈ (ran (𝑦 ∈ π‘₯ ↦ (𝑦 ∩ (◑𝐹 β€œ 𝑉))) βˆ– {𝑀})(𝑀 ∩ 𝑧) = βˆ… ↔ βˆ€π‘§ ∈ (ran (𝑦 ∈ π‘₯ ↦ (𝑦 ∩ (◑𝐹 β€œ 𝑉))) βˆ– {(𝑑 ∩ (◑𝐹 β€œ 𝑉))})((𝑑 ∩ (◑𝐹 β€œ 𝑉)) ∩ 𝑧) = βˆ…))
152 reseq2 5937 . . . . . . . . . . . 12 (𝑀 = (𝑑 ∩ (◑𝐹 β€œ 𝑉)) β†’ (𝐹 β†Ύ 𝑀) = (𝐹 β†Ύ (𝑑 ∩ (◑𝐹 β€œ 𝑉))))
153 oveq2 7370 . . . . . . . . . . . . 13 (𝑀 = (𝑑 ∩ (◑𝐹 β€œ 𝑉)) β†’ (𝐢 β†Ύt 𝑀) = (𝐢 β†Ύt (𝑑 ∩ (◑𝐹 β€œ 𝑉))))
154153oveq1d 7377 . . . . . . . . . . . 12 (𝑀 = (𝑑 ∩ (◑𝐹 β€œ 𝑉)) β†’ ((𝐢 β†Ύt 𝑀)Homeo(𝐽 β†Ύt 𝑉)) = ((𝐢 β†Ύt (𝑑 ∩ (◑𝐹 β€œ 𝑉)))Homeo(𝐽 β†Ύt 𝑉)))
155152, 154eleq12d 2832 . . . . . . . . . . 11 (𝑀 = (𝑑 ∩ (◑𝐹 β€œ 𝑉)) β†’ ((𝐹 β†Ύ 𝑀) ∈ ((𝐢 β†Ύt 𝑀)Homeo(𝐽 β†Ύt 𝑉)) ↔ (𝐹 β†Ύ (𝑑 ∩ (◑𝐹 β€œ 𝑉))) ∈ ((𝐢 β†Ύt (𝑑 ∩ (◑𝐹 β€œ 𝑉)))Homeo(𝐽 β†Ύt 𝑉))))
156151, 155anbi12d 632 . . . . . . . . . 10 (𝑀 = (𝑑 ∩ (◑𝐹 β€œ 𝑉)) β†’ ((βˆ€π‘§ ∈ (ran (𝑦 ∈ π‘₯ ↦ (𝑦 ∩ (◑𝐹 β€œ 𝑉))) βˆ– {𝑀})(𝑀 ∩ 𝑧) = βˆ… ∧ (𝐹 β†Ύ 𝑀) ∈ ((𝐢 β†Ύt 𝑀)Homeo(𝐽 β†Ύt 𝑉))) ↔ (βˆ€π‘§ ∈ (ran (𝑦 ∈ π‘₯ ↦ (𝑦 ∩ (◑𝐹 β€œ 𝑉))) βˆ– {(𝑑 ∩ (◑𝐹 β€œ 𝑉))})((𝑑 ∩ (◑𝐹 β€œ 𝑉)) ∩ 𝑧) = βˆ… ∧ (𝐹 β†Ύ (𝑑 ∩ (◑𝐹 β€œ 𝑉))) ∈ ((𝐢 β†Ύt (𝑑 ∩ (◑𝐹 β€œ 𝑉)))Homeo(𝐽 β†Ύt 𝑉)))))
157146, 156ralrnmptw 7049 . . . . . . . . 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 513 . . . . . 6 (((𝐹 ∈ (𝐢 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 βŠ† π‘ˆ) ∧ π‘₯ ∈ (π‘†β€˜π‘ˆ)) β†’ (βˆͺ ran (𝑦 ∈ π‘₯ ↦ (𝑦 ∩ (◑𝐹 β€œ 𝑉))) = (◑𝐹 β€œ 𝑉) ∧ βˆ€π‘€ ∈ ran (𝑦 ∈ π‘₯ ↦ (𝑦 ∩ (◑𝐹 β€œ 𝑉)))(βˆ€π‘§ ∈ (ran (𝑦 ∈ π‘₯ ↦ (𝑦 ∩ (◑𝐹 β€œ 𝑉))) βˆ– {𝑀})(𝑀 ∩ 𝑧) = βˆ… ∧ (𝐹 β†Ύ 𝑀) ∈ ((𝐢 β†Ύt 𝑀)Homeo(𝐽 β†Ύt 𝑉)))))
1617cvmscbv 33892 . . . . . . . 8 𝑆 = (π‘Ž ∈ 𝐽 ↦ {𝑏 ∈ (𝒫 𝐢 βˆ– {βˆ…}) ∣ (βˆͺ 𝑏 = (◑𝐹 β€œ π‘Ž) ∧ βˆ€π‘€ ∈ 𝑏 (βˆ€π‘§ ∈ (𝑏 βˆ– {𝑀})(𝑀 ∩ 𝑧) = βˆ… ∧ (𝐹 β†Ύ 𝑀) ∈ ((𝐢 β†Ύt 𝑀)Homeo(𝐽 β†Ύt π‘Ž))))})
162161cvmsval 33900 . . . . . . 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 1343 . . . . 5 (((𝐹 ∈ (𝐢 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 βŠ† π‘ˆ) ∧ π‘₯ ∈ (π‘†β€˜π‘ˆ)) β†’ ran (𝑦 ∈ π‘₯ ↦ (𝑦 ∩ (◑𝐹 β€œ 𝑉))) ∈ (π‘†β€˜π‘‰))
165164ne0d 4300 . . . 4 (((𝐹 ∈ (𝐢 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 βŠ† π‘ˆ) ∧ π‘₯ ∈ (π‘†β€˜π‘ˆ)) β†’ (π‘†β€˜π‘‰) β‰  βˆ…)
166165ex 414 . . 3 ((𝐹 ∈ (𝐢 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 βŠ† π‘ˆ) β†’ (π‘₯ ∈ (π‘†β€˜π‘ˆ) β†’ (π‘†β€˜π‘‰) β‰  βˆ…))
167166exlimdv 1937 . 2 ((𝐹 ∈ (𝐢 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 βŠ† π‘ˆ) β†’ (βˆƒπ‘₯ π‘₯ ∈ (π‘†β€˜π‘ˆ) β†’ (π‘†β€˜π‘‰) β‰  βˆ…))
1681, 167biimtrid 241 1 ((𝐹 ∈ (𝐢 CovMap 𝐽) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 βŠ† π‘ˆ) β†’ ((π‘†β€˜π‘ˆ) β‰  βˆ… β†’ (π‘†β€˜π‘‰) β‰  βˆ…))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 397   ∨ wo 846   ∧ w3a 1088   = wceq 1542  βˆƒwex 1782   ∈ wcel 2107   β‰  wne 2944  βˆ€wral 3065  βˆƒwrex 3074  {crab 3410  Vcvv 3448   βˆ– cdif 3912   ∩ cin 3914   βŠ† wss 3915  βˆ…c0 4287  π’« cpw 4565  {csn 4591  βˆͺ cuni 4870   ↦ cmpt 5193  β—‘ccnv 5637  dom cdm 5638  ran crn 5639   β†Ύ cres 5640   β€œ cima 5641  β€“ontoβ†’wfo 6499  β€“1-1-ontoβ†’wf1o 6500  β€˜cfv 6501  (class class class)co 7362   β†Ύt crest 17309  Topctop 22258   Cn ccn 22591  Homeochmeo 23120   CovMap ccvm 33889
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-rep 5247  ax-sep 5261  ax-nul 5268  ax-pow 5325  ax-pr 5389  ax-un 7677
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-ral 3066  df-rex 3075  df-reu 3357  df-rab 3411  df-v 3450  df-sbc 3745  df-csb 3861  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-pss 3934  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-int 4913  df-iun 4961  df-br 5111  df-opab 5173  df-mpt 5194  df-tr 5228  df-id 5536  df-eprel 5542  df-po 5550  df-so 5551  df-fr 5593  df-we 5595  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-ord 6325  df-on 6326  df-lim 6327  df-suc 6328  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508  df-fv 6509  df-ov 7365  df-oprab 7366  df-mpo 7367  df-om 7808  df-1st 7926  df-2nd 7927  df-map 8774  df-en 8891  df-fin 8894  df-fi 9354  df-rest 17311  df-topgen 17332  df-top 22259  df-topon 22276  df-bases 22312  df-cn 22594  df-hmeo 23122  df-cvm 33890
This theorem is referenced by:  cvmcov2  33909
  Copyright terms: Public domain W3C validator