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 31382
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 3964 . 2 ((𝑆𝑈) ≠ ∅ ↔ ∃𝑥 𝑥 ∈ (𝑆𝑈))
2 simpl2 1085 . . . . . 6 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → 𝑉𝐽)
3 simpl1 1084 . . . . . . . . . . . 12 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → 𝐹 ∈ (𝐶 CovMap 𝐽))
4 cvmtop1 31368 . . . . . . . . . . . 12 (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐶 ∈ Top)
53, 4syl 17 . . . . . . . . . . 11 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → 𝐶 ∈ Top)
65adantr 480 . . . . . . . . . 10 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑦𝑥) → 𝐶 ∈ Top)
7 cvmcov.1 . . . . . . . . . . . . 13 𝑆 = (𝑘𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ ( 𝑠 = (𝐹𝑘) ∧ ∀𝑢𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢𝑣) = ∅ ∧ (𝐹𝑢) ∈ ((𝐶t 𝑢)Homeo(𝐽t 𝑘))))})
87cvmsss 31375 . . . . . . . . . . . 12 (𝑥 ∈ (𝑆𝑈) → 𝑥𝐶)
98adantl 481 . . . . . . . . . . 11 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → 𝑥𝐶)
109sselda 3636 . . . . . . . . . 10 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑦𝑥) → 𝑦𝐶)
11 cvmcn 31370 . . . . . . . . . . . . 13 (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐹 ∈ (𝐶 Cn 𝐽))
123, 11syl 17 . . . . . . . . . . . 12 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → 𝐹 ∈ (𝐶 Cn 𝐽))
13 cnima 21117 . . . . . . . . . . . 12 ((𝐹 ∈ (𝐶 Cn 𝐽) ∧ 𝑉𝐽) → (𝐹𝑉) ∈ 𝐶)
1412, 2, 13syl2anc 694 . . . . . . . . . . 11 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → (𝐹𝑉) ∈ 𝐶)
1514adantr 480 . . . . . . . . . 10 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑦𝑥) → (𝐹𝑉) ∈ 𝐶)
16 inopn 20752 . . . . . . . . . 10 ((𝐶 ∈ Top ∧ 𝑦𝐶 ∧ (𝐹𝑉) ∈ 𝐶) → (𝑦 ∩ (𝐹𝑉)) ∈ 𝐶)
176, 10, 15, 16syl3anc 1366 . . . . . . . . 9 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑦𝑥) → (𝑦 ∩ (𝐹𝑉)) ∈ 𝐶)
18 eqid 2651 . . . . . . . . 9 (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) = (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉)))
1917, 18fmptd 6425 . . . . . . . 8 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))):𝑥𝐶)
20 frn 6091 . . . . . . . 8 ((𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))):𝑥𝐶 → ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ⊆ 𝐶)
2119, 20syl 17 . . . . . . 7 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ⊆ 𝐶)
227cvmsn0 31376 . . . . . . . . 9 (𝑥 ∈ (𝑆𝑈) → 𝑥 ≠ ∅)
2322adantl 481 . . . . . . . 8 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → 𝑥 ≠ ∅)
24 dmmptg 5670 . . . . . . . . . . . 12 (∀𝑦𝑥 (𝑦 ∩ (𝐹𝑉)) ∈ V → dom (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) = 𝑥)
25 inex1g 4834 . . . . . . . . . . . 12 (𝑦𝑥 → (𝑦 ∩ (𝐹𝑉)) ∈ V)
2624, 25mprg 2955 . . . . . . . . . . 11 dom (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) = 𝑥
2726eqeq1i 2656 . . . . . . . . . 10 (dom (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) = ∅ ↔ 𝑥 = ∅)
28 dm0rn0 5374 . . . . . . . . . 10 (dom (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) = ∅ ↔ ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) = ∅)
2927, 28bitr3i 266 . . . . . . . . 9 (𝑥 = ∅ ↔ ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) = ∅)
3029necon3bii 2875 . . . . . . . 8 (𝑥 ≠ ∅ ↔ ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ≠ ∅)
3123, 30sylib 208 . . . . . . 7 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ≠ ∅)
3221, 31jca 553 . . . . . 6 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → (ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ⊆ 𝐶 ∧ ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ≠ ∅))
33 inss2 3867 . . . . . . . . . . . 12 (𝑦 ∩ (𝐹𝑉)) ⊆ (𝐹𝑉)
34 elpw2g 4857 . . . . . . . . . . . . 13 ((𝐹𝑉) ∈ 𝐶 → ((𝑦 ∩ (𝐹𝑉)) ∈ 𝒫 (𝐹𝑉) ↔ (𝑦 ∩ (𝐹𝑉)) ⊆ (𝐹𝑉)))
3515, 34syl 17 . . . . . . . . . . . 12 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑦𝑥) → ((𝑦 ∩ (𝐹𝑉)) ∈ 𝒫 (𝐹𝑉) ↔ (𝑦 ∩ (𝐹𝑉)) ⊆ (𝐹𝑉)))
3633, 35mpbiri 248 . . . . . . . . . . 11 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑦𝑥) → (𝑦 ∩ (𝐹𝑉)) ∈ 𝒫 (𝐹𝑉))
3736, 18fmptd 6425 . . . . . . . . . 10 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))):𝑥⟶𝒫 (𝐹𝑉))
38 frn 6091 . . . . . . . . . 10 ((𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))):𝑥⟶𝒫 (𝐹𝑉) → ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ⊆ 𝒫 (𝐹𝑉))
3937, 38syl 17 . . . . . . . . 9 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ⊆ 𝒫 (𝐹𝑉))
40 sspwuni 4643 . . . . . . . . 9 (ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ⊆ 𝒫 (𝐹𝑉) ↔ ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ⊆ (𝐹𝑉))
4139, 40sylib 208 . . . . . . . 8 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ⊆ (𝐹𝑉))
42 simpl3 1086 . . . . . . . . . . . . . 14 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → 𝑉𝑈)
43 imass2 5536 . . . . . . . . . . . . . 14 (𝑉𝑈 → (𝐹𝑉) ⊆ (𝐹𝑈))
4442, 43syl 17 . . . . . . . . . . . . 13 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → (𝐹𝑉) ⊆ (𝐹𝑈))
457cvmsuni 31377 . . . . . . . . . . . . . 14 (𝑥 ∈ (𝑆𝑈) → 𝑥 = (𝐹𝑈))
4645adantl 481 . . . . . . . . . . . . 13 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → 𝑥 = (𝐹𝑈))
4744, 46sseqtr4d 3675 . . . . . . . . . . . 12 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → (𝐹𝑉) ⊆ 𝑥)
4847sselda 3636 . . . . . . . . . . 11 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑧 ∈ (𝐹𝑉)) → 𝑧 𝑥)
49 eqid 2651 . . . . . . . . . . . . . . . . 17 (𝑡 ∩ (𝐹𝑉)) = (𝑡 ∩ (𝐹𝑉))
50 ineq1 3840 . . . . . . . . . . . . . . . . . . 19 (𝑦 = 𝑡 → (𝑦 ∩ (𝐹𝑉)) = (𝑡 ∩ (𝐹𝑉)))
5150eqeq2d 2661 . . . . . . . . . . . . . . . . . 18 (𝑦 = 𝑡 → ((𝑡 ∩ (𝐹𝑉)) = (𝑦 ∩ (𝐹𝑉)) ↔ (𝑡 ∩ (𝐹𝑉)) = (𝑡 ∩ (𝐹𝑉))))
5251rspcev 3340 . . . . . . . . . . . . . . . . 17 ((𝑡𝑥 ∧ (𝑡 ∩ (𝐹𝑉)) = (𝑡 ∩ (𝐹𝑉))) → ∃𝑦𝑥 (𝑡 ∩ (𝐹𝑉)) = (𝑦 ∩ (𝐹𝑉)))
5349, 52mpan2 707 . . . . . . . . . . . . . . . 16 (𝑡𝑥 → ∃𝑦𝑥 (𝑡 ∩ (𝐹𝑉)) = (𝑦 ∩ (𝐹𝑉)))
5453ad2antrl 764 . . . . . . . . . . . . . . 15 (((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑧 ∈ (𝐹𝑉)) ∧ (𝑡𝑥𝑧𝑡)) → ∃𝑦𝑥 (𝑡 ∩ (𝐹𝑉)) = (𝑦 ∩ (𝐹𝑉)))
55 vex 3234 . . . . . . . . . . . . . . . . 17 𝑡 ∈ V
5655inex1 4832 . . . . . . . . . . . . . . . 16 (𝑡 ∩ (𝐹𝑉)) ∈ V
5718elrnmpt 5404 . . . . . . . . . . . . . . . 16 ((𝑡 ∩ (𝐹𝑉)) ∈ V → ((𝑡 ∩ (𝐹𝑉)) ∈ ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ↔ ∃𝑦𝑥 (𝑡 ∩ (𝐹𝑉)) = (𝑦 ∩ (𝐹𝑉))))
5856, 57ax-mp 5 . . . . . . . . . . . . . . 15 ((𝑡 ∩ (𝐹𝑉)) ∈ ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ↔ ∃𝑦𝑥 (𝑡 ∩ (𝐹𝑉)) = (𝑦 ∩ (𝐹𝑉)))
5954, 58sylibr 224 . . . . . . . . . . . . . 14 (((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑧 ∈ (𝐹𝑉)) ∧ (𝑡𝑥𝑧𝑡)) → (𝑡 ∩ (𝐹𝑉)) ∈ ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))))
60 simprr 811 . . . . . . . . . . . . . . 15 (((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑧 ∈ (𝐹𝑉)) ∧ (𝑡𝑥𝑧𝑡)) → 𝑧𝑡)
61 simplr 807 . . . . . . . . . . . . . . 15 (((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑧 ∈ (𝐹𝑉)) ∧ (𝑡𝑥𝑧𝑡)) → 𝑧 ∈ (𝐹𝑉))
6260, 61elind 3831 . . . . . . . . . . . . . 14 (((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑧 ∈ (𝐹𝑉)) ∧ (𝑡𝑥𝑧𝑡)) → 𝑧 ∈ (𝑡 ∩ (𝐹𝑉)))
63 eleq2 2719 . . . . . . . . . . . . . . 15 (𝑤 = (𝑡 ∩ (𝐹𝑉)) → (𝑧𝑤𝑧 ∈ (𝑡 ∩ (𝐹𝑉))))
6463rspcev 3340 . . . . . . . . . . . . . 14 (((𝑡 ∩ (𝐹𝑉)) ∈ ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ∧ 𝑧 ∈ (𝑡 ∩ (𝐹𝑉))) → ∃𝑤 ∈ ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉)))𝑧𝑤)
6559, 62, 64syl2anc 694 . . . . . . . . . . . . 13 (((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑧 ∈ (𝐹𝑉)) ∧ (𝑡𝑥𝑧𝑡)) → ∃𝑤 ∈ ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉)))𝑧𝑤)
6665rexlimdvaa 3061 . . . . . . . . . . . 12 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑧 ∈ (𝐹𝑉)) → (∃𝑡𝑥 𝑧𝑡 → ∃𝑤 ∈ ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉)))𝑧𝑤))
67 eluni2 4472 . . . . . . . . . . . 12 (𝑧 𝑥 ↔ ∃𝑡𝑥 𝑧𝑡)
68 eluni2 4472 . . . . . . . . . . . 12 (𝑧 ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ↔ ∃𝑤 ∈ ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉)))𝑧𝑤)
6966, 67, 683imtr4g 285 . . . . . . . . . . 11 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑧 ∈ (𝐹𝑉)) → (𝑧 𝑥𝑧 ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉)))))
7048, 69mpd 15 . . . . . . . . . 10 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑧 ∈ (𝐹𝑉)) → 𝑧 ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))))
7170ex 449 . . . . . . . . 9 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → (𝑧 ∈ (𝐹𝑉) → 𝑧 ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉)))))
7271ssrdv 3642 . . . . . . . 8 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → (𝐹𝑉) ⊆ ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))))
7341, 72eqssd 3653 . . . . . . 7 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) = (𝐹𝑉))
74 eldifsn 4350 . . . . . . . . . . . 12 (𝑧 ∈ (ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ∖ {(𝑡 ∩ (𝐹𝑉))}) ↔ (𝑧 ∈ ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ∧ 𝑧 ≠ (𝑡 ∩ (𝐹𝑉))))
75 vex 3234 . . . . . . . . . . . . . . 15 𝑧 ∈ V
7618elrnmpt 5404 . . . . . . . . . . . . . . 15 (𝑧 ∈ V → (𝑧 ∈ ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ↔ ∃𝑦𝑥 𝑧 = (𝑦 ∩ (𝐹𝑉))))
7775, 76ax-mp 5 . . . . . . . . . . . . . 14 (𝑧 ∈ ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ↔ ∃𝑦𝑥 𝑧 = (𝑦 ∩ (𝐹𝑉)))
7850equcoms 1993 . . . . . . . . . . . . . . . . . 18 (𝑡 = 𝑦 → (𝑦 ∩ (𝐹𝑉)) = (𝑡 ∩ (𝐹𝑉)))
7978necon3ai 2848 . . . . . . . . . . . . . . . . 17 ((𝑦 ∩ (𝐹𝑉)) ≠ (𝑡 ∩ (𝐹𝑉)) → ¬ 𝑡 = 𝑦)
80 simpllr 815 . . . . . . . . . . . . . . . . . . 19 (((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) ∧ 𝑦𝑥) → 𝑥 ∈ (𝑆𝑈))
81 simplr 807 . . . . . . . . . . . . . . . . . . 19 (((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) ∧ 𝑦𝑥) → 𝑡𝑥)
82 simpr 476 . . . . . . . . . . . . . . . . . . 19 (((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) ∧ 𝑦𝑥) → 𝑦𝑥)
837cvmsdisj 31378 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ (𝑆𝑈) ∧ 𝑡𝑥𝑦𝑥) → (𝑡 = 𝑦 ∨ (𝑡𝑦) = ∅))
8480, 81, 82, 83syl3anc 1366 . . . . . . . . . . . . . . . . . 18 (((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) ∧ 𝑦𝑥) → (𝑡 = 𝑦 ∨ (𝑡𝑦) = ∅))
8584ord 391 . . . . . . . . . . . . . . . . 17 (((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) ∧ 𝑦𝑥) → (¬ 𝑡 = 𝑦 → (𝑡𝑦) = ∅))
86 inss1 3866 . . . . . . . . . . . . . . . . . 18 ((𝑡𝑦) ∩ (𝐹𝑉)) ⊆ (𝑡𝑦)
87 sseq0 4008 . . . . . . . . . . . . . . . . . 18 ((((𝑡𝑦) ∩ (𝐹𝑉)) ⊆ (𝑡𝑦) ∧ (𝑡𝑦) = ∅) → ((𝑡𝑦) ∩ (𝐹𝑉)) = ∅)
8886, 87mpan 706 . . . . . . . . . . . . . . . . 17 ((𝑡𝑦) = ∅ → ((𝑡𝑦) ∩ (𝐹𝑉)) = ∅)
8979, 85, 88syl56 36 . . . . . . . . . . . . . . . 16 (((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) ∧ 𝑦𝑥) → ((𝑦 ∩ (𝐹𝑉)) ≠ (𝑡 ∩ (𝐹𝑉)) → ((𝑡𝑦) ∩ (𝐹𝑉)) = ∅))
90 neeq1 2885 . . . . . . . . . . . . . . . . 17 (𝑧 = (𝑦 ∩ (𝐹𝑉)) → (𝑧 ≠ (𝑡 ∩ (𝐹𝑉)) ↔ (𝑦 ∩ (𝐹𝑉)) ≠ (𝑡 ∩ (𝐹𝑉))))
91 ineq2 3841 . . . . . . . . . . . . . . . . . . 19 (𝑧 = (𝑦 ∩ (𝐹𝑉)) → ((𝑡 ∩ (𝐹𝑉)) ∩ 𝑧) = ((𝑡 ∩ (𝐹𝑉)) ∩ (𝑦 ∩ (𝐹𝑉))))
92 inindir 3864 . . . . . . . . . . . . . . . . . . 19 ((𝑡𝑦) ∩ (𝐹𝑉)) = ((𝑡 ∩ (𝐹𝑉)) ∩ (𝑦 ∩ (𝐹𝑉)))
9391, 92syl6eqr 2703 . . . . . . . . . . . . . . . . . 18 (𝑧 = (𝑦 ∩ (𝐹𝑉)) → ((𝑡 ∩ (𝐹𝑉)) ∩ 𝑧) = ((𝑡𝑦) ∩ (𝐹𝑉)))
9493eqeq1d 2653 . . . . . . . . . . . . . . . . 17 (𝑧 = (𝑦 ∩ (𝐹𝑉)) → (((𝑡 ∩ (𝐹𝑉)) ∩ 𝑧) = ∅ ↔ ((𝑡𝑦) ∩ (𝐹𝑉)) = ∅))
9590, 94imbi12d 333 . . . . . . . . . . . . . . . 16 (𝑧 = (𝑦 ∩ (𝐹𝑉)) → ((𝑧 ≠ (𝑡 ∩ (𝐹𝑉)) → ((𝑡 ∩ (𝐹𝑉)) ∩ 𝑧) = ∅) ↔ ((𝑦 ∩ (𝐹𝑉)) ≠ (𝑡 ∩ (𝐹𝑉)) → ((𝑡𝑦) ∩ (𝐹𝑉)) = ∅)))
9689, 95syl5ibrcom 237 . . . . . . . . . . . . . . 15 (((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) ∧ 𝑦𝑥) → (𝑧 = (𝑦 ∩ (𝐹𝑉)) → (𝑧 ≠ (𝑡 ∩ (𝐹𝑉)) → ((𝑡 ∩ (𝐹𝑉)) ∩ 𝑧) = ∅)))
9796rexlimdva 3060 . . . . . . . . . . . . . 14 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → (∃𝑦𝑥 𝑧 = (𝑦 ∩ (𝐹𝑉)) → (𝑧 ≠ (𝑡 ∩ (𝐹𝑉)) → ((𝑡 ∩ (𝐹𝑉)) ∩ 𝑧) = ∅)))
9877, 97syl5bi 232 . . . . . . . . . . . . 13 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → (𝑧 ∈ ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) → (𝑧 ≠ (𝑡 ∩ (𝐹𝑉)) → ((𝑡 ∩ (𝐹𝑉)) ∩ 𝑧) = ∅)))
9998impd 446 . . . . . . . . . . . 12 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → ((𝑧 ∈ ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ∧ 𝑧 ≠ (𝑡 ∩ (𝐹𝑉))) → ((𝑡 ∩ (𝐹𝑉)) ∩ 𝑧) = ∅))
10074, 99syl5bi 232 . . . . . . . . . . 11 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → (𝑧 ∈ (ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ∖ {(𝑡 ∩ (𝐹𝑉))}) → ((𝑡 ∩ (𝐹𝑉)) ∩ 𝑧) = ∅))
101100ralrimiv 2994 . . . . . . . . . 10 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → ∀𝑧 ∈ (ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ∖ {(𝑡 ∩ (𝐹𝑉))})((𝑡 ∩ (𝐹𝑉)) ∩ 𝑧) = ∅)
102 inss1 3866 . . . . . . . . . . . . 13 (𝑡 ∩ (𝐹𝑉)) ⊆ 𝑡
103 resabs1 5462 . . . . . . . . . . . . 13 ((𝑡 ∩ (𝐹𝑉)) ⊆ 𝑡 → ((𝐹𝑡) ↾ (𝑡 ∩ (𝐹𝑉))) = (𝐹 ↾ (𝑡 ∩ (𝐹𝑉))))
104102, 103ax-mp 5 . . . . . . . . . . . 12 ((𝐹𝑡) ↾ (𝑡 ∩ (𝐹𝑉))) = (𝐹 ↾ (𝑡 ∩ (𝐹𝑉)))
1057cvmshmeo 31379 . . . . . . . . . . . . . 14 ((𝑥 ∈ (𝑆𝑈) ∧ 𝑡𝑥) → (𝐹𝑡) ∈ ((𝐶t 𝑡)Homeo(𝐽t 𝑈)))
106105adantll 750 . . . . . . . . . . . . 13 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → (𝐹𝑡) ∈ ((𝐶t 𝑡)Homeo(𝐽t 𝑈)))
1075adantr 480 . . . . . . . . . . . . . . 15 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → 𝐶 ∈ Top)
1089sselda 3636 . . . . . . . . . . . . . . . 16 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → 𝑡𝐶)
109 elssuni 4499 . . . . . . . . . . . . . . . 16 (𝑡𝐶𝑡 𝐶)
110108, 109syl 17 . . . . . . . . . . . . . . 15 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → 𝑡 𝐶)
111 eqid 2651 . . . . . . . . . . . . . . . 16 𝐶 = 𝐶
112111restuni 21014 . . . . . . . . . . . . . . 15 ((𝐶 ∈ Top ∧ 𝑡 𝐶) → 𝑡 = (𝐶t 𝑡))
113107, 110, 112syl2anc 694 . . . . . . . . . . . . . 14 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → 𝑡 = (𝐶t 𝑡))
114102, 113syl5sseq 3686 . . . . . . . . . . . . 13 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → (𝑡 ∩ (𝐹𝑉)) ⊆ (𝐶t 𝑡))
115 eqid 2651 . . . . . . . . . . . . . 14 (𝐶t 𝑡) = (𝐶t 𝑡)
116115hmeores 21622 . . . . . . . . . . . . 13 (((𝐹𝑡) ∈ ((𝐶t 𝑡)Homeo(𝐽t 𝑈)) ∧ (𝑡 ∩ (𝐹𝑉)) ⊆ (𝐶t 𝑡)) → ((𝐹𝑡) ↾ (𝑡 ∩ (𝐹𝑉))) ∈ (((𝐶t 𝑡) ↾t (𝑡 ∩ (𝐹𝑉)))Homeo((𝐽t 𝑈) ↾t ((𝐹𝑡) “ (𝑡 ∩ (𝐹𝑉))))))
117106, 114, 116syl2anc 694 . . . . . . . . . . . 12 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → ((𝐹𝑡) ↾ (𝑡 ∩ (𝐹𝑉))) ∈ (((𝐶t 𝑡) ↾t (𝑡 ∩ (𝐹𝑉)))Homeo((𝐽t 𝑈) ↾t ((𝐹𝑡) “ (𝑡 ∩ (𝐹𝑉))))))
118104, 117syl5eqelr 2735 . . . . . . . . . . 11 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → (𝐹 ↾ (𝑡 ∩ (𝐹𝑉))) ∈ (((𝐶t 𝑡) ↾t (𝑡 ∩ (𝐹𝑉)))Homeo((𝐽t 𝑈) ↾t ((𝐹𝑡) “ (𝑡 ∩ (𝐹𝑉))))))
119102a1i 11 . . . . . . . . . . . . 13 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → (𝑡 ∩ (𝐹𝑉)) ⊆ 𝑡)
120 simpr 476 . . . . . . . . . . . . 13 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → 𝑡𝑥)
121 restabs 21017 . . . . . . . . . . . . 13 ((𝐶 ∈ Top ∧ (𝑡 ∩ (𝐹𝑉)) ⊆ 𝑡𝑡𝑥) → ((𝐶t 𝑡) ↾t (𝑡 ∩ (𝐹𝑉))) = (𝐶t (𝑡 ∩ (𝐹𝑉))))
122107, 119, 120, 121syl3anc 1366 . . . . . . . . . . . 12 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → ((𝐶t 𝑡) ↾t (𝑡 ∩ (𝐹𝑉))) = (𝐶t (𝑡 ∩ (𝐹𝑉))))
123 incom 3838 . . . . . . . . . . . . . . . . 17 (𝑡 ∩ (𝐹𝑉)) = ((𝐹𝑉) ∩ 𝑡)
124 cnvresima 5661 . . . . . . . . . . . . . . . . 17 ((𝐹𝑡) “ 𝑉) = ((𝐹𝑉) ∩ 𝑡)
125123, 124eqtr4i 2676 . . . . . . . . . . . . . . . 16 (𝑡 ∩ (𝐹𝑉)) = ((𝐹𝑡) “ 𝑉)
126125imaeq2i 5499 . . . . . . . . . . . . . . 15 ((𝐹𝑡) “ (𝑡 ∩ (𝐹𝑉))) = ((𝐹𝑡) “ ((𝐹𝑡) “ 𝑉))
1273adantr 480 . . . . . . . . . . . . . . . . . 18 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → 𝐹 ∈ (𝐶 CovMap 𝐽))
128 simplr 807 . . . . . . . . . . . . . . . . . 18 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → 𝑥 ∈ (𝑆𝑈))
1297cvmsf1o 31380 . . . . . . . . . . . . . . . . . 18 ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑥 ∈ (𝑆𝑈) ∧ 𝑡𝑥) → (𝐹𝑡):𝑡1-1-onto𝑈)
130127, 128, 120, 129syl3anc 1366 . . . . . . . . . . . . . . . . 17 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → (𝐹𝑡):𝑡1-1-onto𝑈)
131 f1ofo 6182 . . . . . . . . . . . . . . . . 17 ((𝐹𝑡):𝑡1-1-onto𝑈 → (𝐹𝑡):𝑡onto𝑈)
132130, 131syl 17 . . . . . . . . . . . . . . . 16 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → (𝐹𝑡):𝑡onto𝑈)
13342adantr 480 . . . . . . . . . . . . . . . 16 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → 𝑉𝑈)
134 foimacnv 6192 . . . . . . . . . . . . . . . 16 (((𝐹𝑡):𝑡onto𝑈𝑉𝑈) → ((𝐹𝑡) “ ((𝐹𝑡) “ 𝑉)) = 𝑉)
135132, 133, 134syl2anc 694 . . . . . . . . . . . . . . 15 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → ((𝐹𝑡) “ ((𝐹𝑡) “ 𝑉)) = 𝑉)
136126, 135syl5eq 2697 . . . . . . . . . . . . . 14 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → ((𝐹𝑡) “ (𝑡 ∩ (𝐹𝑉))) = 𝑉)
137136oveq2d 6706 . . . . . . . . . . . . 13 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → ((𝐽t 𝑈) ↾t ((𝐹𝑡) “ (𝑡 ∩ (𝐹𝑉)))) = ((𝐽t 𝑈) ↾t 𝑉))
138 cvmtop2 31369 . . . . . . . . . . . . . . . 16 (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐽 ∈ Top)
1393, 138syl 17 . . . . . . . . . . . . . . 15 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → 𝐽 ∈ Top)
1407cvmsrcl 31372 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (𝑆𝑈) → 𝑈𝐽)
141140adantl 481 . . . . . . . . . . . . . . 15 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → 𝑈𝐽)
142 restabs 21017 . . . . . . . . . . . . . . 15 ((𝐽 ∈ Top ∧ 𝑉𝑈𝑈𝐽) → ((𝐽t 𝑈) ↾t 𝑉) = (𝐽t 𝑉))
143139, 42, 141, 142syl3anc 1366 . . . . . . . . . . . . . 14 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → ((𝐽t 𝑈) ↾t 𝑉) = (𝐽t 𝑉))
144143adantr 480 . . . . . . . . . . . . 13 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → ((𝐽t 𝑈) ↾t 𝑉) = (𝐽t 𝑉))
145137, 144eqtrd 2685 . . . . . . . . . . . 12 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → ((𝐽t 𝑈) ↾t ((𝐹𝑡) “ (𝑡 ∩ (𝐹𝑉)))) = (𝐽t 𝑉))
146122, 145oveq12d 6708 . . . . . . . . . . 11 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → (((𝐶t 𝑡) ↾t (𝑡 ∩ (𝐹𝑉)))Homeo((𝐽t 𝑈) ↾t ((𝐹𝑡) “ (𝑡 ∩ (𝐹𝑉))))) = ((𝐶t (𝑡 ∩ (𝐹𝑉)))Homeo(𝐽t 𝑉)))
147118, 146eleqtrd 2732 . . . . . . . . . 10 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → (𝐹 ↾ (𝑡 ∩ (𝐹𝑉))) ∈ ((𝐶t (𝑡 ∩ (𝐹𝑉)))Homeo(𝐽t 𝑉)))
148101, 147jca 553 . . . . . . . . 9 ((((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) ∧ 𝑡𝑥) → (∀𝑧 ∈ (ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ∖ {(𝑡 ∩ (𝐹𝑉))})((𝑡 ∩ (𝐹𝑉)) ∩ 𝑧) = ∅ ∧ (𝐹 ↾ (𝑡 ∩ (𝐹𝑉))) ∈ ((𝐶t (𝑡 ∩ (𝐹𝑉)))Homeo(𝐽t 𝑉))))
149148ralrimiva 2995 . . . . . . . 8 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → ∀𝑡𝑥 (∀𝑧 ∈ (ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ∖ {(𝑡 ∩ (𝐹𝑉))})((𝑡 ∩ (𝐹𝑉)) ∩ 𝑧) = ∅ ∧ (𝐹 ↾ (𝑡 ∩ (𝐹𝑉))) ∈ ((𝐶t (𝑡 ∩ (𝐹𝑉)))Homeo(𝐽t 𝑉))))
15056rgenw 2953 . . . . . . . . 9 𝑡𝑥 (𝑡 ∩ (𝐹𝑉)) ∈ V
15150cbvmptv 4783 . . . . . . . . . 10 (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) = (𝑡𝑥 ↦ (𝑡 ∩ (𝐹𝑉)))
152 sneq 4220 . . . . . . . . . . . . 13 (𝑤 = (𝑡 ∩ (𝐹𝑉)) → {𝑤} = {(𝑡 ∩ (𝐹𝑉))})
153152difeq2d 3761 . . . . . . . . . . . 12 (𝑤 = (𝑡 ∩ (𝐹𝑉)) → (ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ∖ {𝑤}) = (ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ∖ {(𝑡 ∩ (𝐹𝑉))}))
154 ineq1 3840 . . . . . . . . . . . . 13 (𝑤 = (𝑡 ∩ (𝐹𝑉)) → (𝑤𝑧) = ((𝑡 ∩ (𝐹𝑉)) ∩ 𝑧))
155154eqeq1d 2653 . . . . . . . . . . . 12 (𝑤 = (𝑡 ∩ (𝐹𝑉)) → ((𝑤𝑧) = ∅ ↔ ((𝑡 ∩ (𝐹𝑉)) ∩ 𝑧) = ∅))
156153, 155raleqbidv 3182 . . . . . . . . . . 11 (𝑤 = (𝑡 ∩ (𝐹𝑉)) → (∀𝑧 ∈ (ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ∖ {𝑤})(𝑤𝑧) = ∅ ↔ ∀𝑧 ∈ (ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ∖ {(𝑡 ∩ (𝐹𝑉))})((𝑡 ∩ (𝐹𝑉)) ∩ 𝑧) = ∅))
157 reseq2 5423 . . . . . . . . . . . 12 (𝑤 = (𝑡 ∩ (𝐹𝑉)) → (𝐹𝑤) = (𝐹 ↾ (𝑡 ∩ (𝐹𝑉))))
158 oveq2 6698 . . . . . . . . . . . . 13 (𝑤 = (𝑡 ∩ (𝐹𝑉)) → (𝐶t 𝑤) = (𝐶t (𝑡 ∩ (𝐹𝑉))))
159158oveq1d 6705 . . . . . . . . . . . 12 (𝑤 = (𝑡 ∩ (𝐹𝑉)) → ((𝐶t 𝑤)Homeo(𝐽t 𝑉)) = ((𝐶t (𝑡 ∩ (𝐹𝑉)))Homeo(𝐽t 𝑉)))
160157, 159eleq12d 2724 . . . . . . . . . . 11 (𝑤 = (𝑡 ∩ (𝐹𝑉)) → ((𝐹𝑤) ∈ ((𝐶t 𝑤)Homeo(𝐽t 𝑉)) ↔ (𝐹 ↾ (𝑡 ∩ (𝐹𝑉))) ∈ ((𝐶t (𝑡 ∩ (𝐹𝑉)))Homeo(𝐽t 𝑉))))
161156, 160anbi12d 747 . . . . . . . . . 10 (𝑤 = (𝑡 ∩ (𝐹𝑉)) → ((∀𝑧 ∈ (ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ∖ {𝑤})(𝑤𝑧) = ∅ ∧ (𝐹𝑤) ∈ ((𝐶t 𝑤)Homeo(𝐽t 𝑉))) ↔ (∀𝑧 ∈ (ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ∖ {(𝑡 ∩ (𝐹𝑉))})((𝑡 ∩ (𝐹𝑉)) ∩ 𝑧) = ∅ ∧ (𝐹 ↾ (𝑡 ∩ (𝐹𝑉))) ∈ ((𝐶t (𝑡 ∩ (𝐹𝑉)))Homeo(𝐽t 𝑉)))))
162151, 161ralrnmpt 6408 . . . . . . . . 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 224 . . . . . . 7 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → ∀𝑤 ∈ ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉)))(∀𝑧 ∈ (ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ∖ {𝑤})(𝑤𝑧) = ∅ ∧ (𝐹𝑤) ∈ ((𝐶t 𝑤)Homeo(𝐽t 𝑉))))
16573, 164jca 553 . . . . . 6 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → ( ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) = (𝐹𝑉) ∧ ∀𝑤 ∈ ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉)))(∀𝑧 ∈ (ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ∖ {𝑤})(𝑤𝑧) = ∅ ∧ (𝐹𝑤) ∈ ((𝐶t 𝑤)Homeo(𝐽t 𝑉)))))
1667cvmscbv 31366 . . . . . . . 8 𝑆 = (𝑎𝐽 ↦ {𝑏 ∈ (𝒫 𝐶 ∖ {∅}) ∣ ( 𝑏 = (𝐹𝑎) ∧ ∀𝑤𝑏 (∀𝑧 ∈ (𝑏 ∖ {𝑤})(𝑤𝑧) = ∅ ∧ (𝐹𝑤) ∈ ((𝐶t 𝑤)Homeo(𝐽t 𝑎))))})
167166cvmsval 31374 . . . . . . 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 1264 . . . . 5 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ∈ (𝑆𝑉))
170 ne0i 3954 . . . . 5 (ran (𝑦𝑥 ↦ (𝑦 ∩ (𝐹𝑉))) ∈ (𝑆𝑉) → (𝑆𝑉) ≠ ∅)
171169, 170syl 17 . . . 4 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) ∧ 𝑥 ∈ (𝑆𝑈)) → (𝑆𝑉) ≠ ∅)
172171ex 449 . . 3 ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) → (𝑥 ∈ (𝑆𝑈) → (𝑆𝑉) ≠ ∅))
173172exlimdv 1901 . 2 ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) → (∃𝑥 𝑥 ∈ (𝑆𝑈) → (𝑆𝑉) ≠ ∅))
1741, 173syl5bi 232 1 ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑉𝐽𝑉𝑈) → ((𝑆𝑈) ≠ ∅ → (𝑆𝑉) ≠ ∅))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wo 382  wa 383  w3a 1054   = wceq 1523  wex 1744  wcel 2030  wne 2823  wral 2941  wrex 2942  {crab 2945  Vcvv 3231  cdif 3604  cin 3606  wss 3607  c0 3948  𝒫 cpw 4191  {csn 4210   cuni 4468  cmpt 4762  ccnv 5142  dom cdm 5143  ran crn 5144  cres 5145  cima 5146  wf 5922  ontowfo 5924  1-1-ontowf1o 5925  cfv 5926  (class class class)co 6690  t crest 16128  Topctop 20746   Cn ccn 21076  Homeochmeo 21604   CovMap ccvm 31363
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rex 2947  df-reu 2948  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-om 7108  df-1st 7210  df-2nd 7211  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-oadd 7609  df-er 7787  df-map 7901  df-en 7998  df-fin 8001  df-fi 8358  df-rest 16130  df-topgen 16151  df-top 20747  df-topon 20764  df-bases 20798  df-cn 21079  df-hmeo 21606  df-cvm 31364
This theorem is referenced by:  cvmcov2  31383
  Copyright terms: Public domain W3C validator