| Step | Hyp | Ref
| Expression |
| 1 | | simpr2 1196 |
. . . . 5
⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ (𝑇 ∈ (𝑆‘𝑈) ∧ 𝐴 ∈ 𝐵 ∧ (𝐹‘𝐴) ∈ 𝑈)) → 𝐴 ∈ 𝐵) |
| 2 | | simpr3 1197 |
. . . . 5
⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ (𝑇 ∈ (𝑆‘𝑈) ∧ 𝐴 ∈ 𝐵 ∧ (𝐹‘𝐴) ∈ 𝑈)) → (𝐹‘𝐴) ∈ 𝑈) |
| 3 | | cvmcn 35267 |
. . . . . . 7
⊢ (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐹 ∈ (𝐶 Cn 𝐽)) |
| 4 | 3 | adantr 480 |
. . . . . 6
⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ (𝑇 ∈ (𝑆‘𝑈) ∧ 𝐴 ∈ 𝐵 ∧ (𝐹‘𝐴) ∈ 𝑈)) → 𝐹 ∈ (𝐶 Cn 𝐽)) |
| 5 | | cvmseu.1 |
. . . . . . 7
⊢ 𝐵 = ∪
𝐶 |
| 6 | | eqid 2737 |
. . . . . . 7
⊢ ∪ 𝐽 =
∪ 𝐽 |
| 7 | 5, 6 | cnf 23254 |
. . . . . 6
⊢ (𝐹 ∈ (𝐶 Cn 𝐽) → 𝐹:𝐵⟶∪ 𝐽) |
| 8 | | ffn 6736 |
. . . . . 6
⊢ (𝐹:𝐵⟶∪ 𝐽 → 𝐹 Fn 𝐵) |
| 9 | | elpreima 7078 |
. . . . . 6
⊢ (𝐹 Fn 𝐵 → (𝐴 ∈ (◡𝐹 “ 𝑈) ↔ (𝐴 ∈ 𝐵 ∧ (𝐹‘𝐴) ∈ 𝑈))) |
| 10 | 4, 7, 8, 9 | 4syl 19 |
. . . . 5
⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ (𝑇 ∈ (𝑆‘𝑈) ∧ 𝐴 ∈ 𝐵 ∧ (𝐹‘𝐴) ∈ 𝑈)) → (𝐴 ∈ (◡𝐹 “ 𝑈) ↔ (𝐴 ∈ 𝐵 ∧ (𝐹‘𝐴) ∈ 𝑈))) |
| 11 | 1, 2, 10 | mpbir2and 713 |
. . . 4
⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ (𝑇 ∈ (𝑆‘𝑈) ∧ 𝐴 ∈ 𝐵 ∧ (𝐹‘𝐴) ∈ 𝑈)) → 𝐴 ∈ (◡𝐹 “ 𝑈)) |
| 12 | | simpr1 1195 |
. . . . 5
⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ (𝑇 ∈ (𝑆‘𝑈) ∧ 𝐴 ∈ 𝐵 ∧ (𝐹‘𝐴) ∈ 𝑈)) → 𝑇 ∈ (𝑆‘𝑈)) |
| 13 | | cvmcov.1 |
. . . . . 6
⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 =
(◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))}) |
| 14 | 13 | cvmsuni 35274 |
. . . . 5
⊢ (𝑇 ∈ (𝑆‘𝑈) → ∪ 𝑇 = (◡𝐹 “ 𝑈)) |
| 15 | 12, 14 | syl 17 |
. . . 4
⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ (𝑇 ∈ (𝑆‘𝑈) ∧ 𝐴 ∈ 𝐵 ∧ (𝐹‘𝐴) ∈ 𝑈)) → ∪ 𝑇 = (◡𝐹 “ 𝑈)) |
| 16 | 11, 15 | eleqtrrd 2844 |
. . 3
⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ (𝑇 ∈ (𝑆‘𝑈) ∧ 𝐴 ∈ 𝐵 ∧ (𝐹‘𝐴) ∈ 𝑈)) → 𝐴 ∈ ∪ 𝑇) |
| 17 | | eluni2 4911 |
. . 3
⊢ (𝐴 ∈ ∪ 𝑇
↔ ∃𝑥 ∈
𝑇 𝐴 ∈ 𝑥) |
| 18 | 16, 17 | sylib 218 |
. 2
⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ (𝑇 ∈ (𝑆‘𝑈) ∧ 𝐴 ∈ 𝐵 ∧ (𝐹‘𝐴) ∈ 𝑈)) → ∃𝑥 ∈ 𝑇 𝐴 ∈ 𝑥) |
| 19 | | inelcm 4465 |
. . . 4
⊢ ((𝐴 ∈ 𝑥 ∧ 𝐴 ∈ 𝑧) → (𝑥 ∩ 𝑧) ≠ ∅) |
| 20 | 13 | cvmsdisj 35275 |
. . . . . . . 8
⊢ ((𝑇 ∈ (𝑆‘𝑈) ∧ 𝑥 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇) → (𝑥 = 𝑧 ∨ (𝑥 ∩ 𝑧) = ∅)) |
| 21 | 20 | 3expb 1121 |
. . . . . . 7
⊢ ((𝑇 ∈ (𝑆‘𝑈) ∧ (𝑥 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (𝑥 = 𝑧 ∨ (𝑥 ∩ 𝑧) = ∅)) |
| 22 | 12, 21 | sylan 580 |
. . . . . 6
⊢ (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ (𝑇 ∈ (𝑆‘𝑈) ∧ 𝐴 ∈ 𝐵 ∧ (𝐹‘𝐴) ∈ 𝑈)) ∧ (𝑥 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (𝑥 = 𝑧 ∨ (𝑥 ∩ 𝑧) = ∅)) |
| 23 | 22 | ord 865 |
. . . . 5
⊢ (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ (𝑇 ∈ (𝑆‘𝑈) ∧ 𝐴 ∈ 𝐵 ∧ (𝐹‘𝐴) ∈ 𝑈)) ∧ (𝑥 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (¬ 𝑥 = 𝑧 → (𝑥 ∩ 𝑧) = ∅)) |
| 24 | 23 | necon1ad 2957 |
. . . 4
⊢ (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ (𝑇 ∈ (𝑆‘𝑈) ∧ 𝐴 ∈ 𝐵 ∧ (𝐹‘𝐴) ∈ 𝑈)) ∧ (𝑥 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → ((𝑥 ∩ 𝑧) ≠ ∅ → 𝑥 = 𝑧)) |
| 25 | 19, 24 | syl5 34 |
. . 3
⊢ (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ (𝑇 ∈ (𝑆‘𝑈) ∧ 𝐴 ∈ 𝐵 ∧ (𝐹‘𝐴) ∈ 𝑈)) ∧ (𝑥 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → ((𝐴 ∈ 𝑥 ∧ 𝐴 ∈ 𝑧) → 𝑥 = 𝑧)) |
| 26 | 25 | ralrimivva 3202 |
. 2
⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ (𝑇 ∈ (𝑆‘𝑈) ∧ 𝐴 ∈ 𝐵 ∧ (𝐹‘𝐴) ∈ 𝑈)) → ∀𝑥 ∈ 𝑇 ∀𝑧 ∈ 𝑇 ((𝐴 ∈ 𝑥 ∧ 𝐴 ∈ 𝑧) → 𝑥 = 𝑧)) |
| 27 | | eleq2w 2825 |
. . 3
⊢ (𝑥 = 𝑧 → (𝐴 ∈ 𝑥 ↔ 𝐴 ∈ 𝑧)) |
| 28 | 27 | reu4 3737 |
. 2
⊢
(∃!𝑥 ∈
𝑇 𝐴 ∈ 𝑥 ↔ (∃𝑥 ∈ 𝑇 𝐴 ∈ 𝑥 ∧ ∀𝑥 ∈ 𝑇 ∀𝑧 ∈ 𝑇 ((𝐴 ∈ 𝑥 ∧ 𝐴 ∈ 𝑧) → 𝑥 = 𝑧))) |
| 29 | 18, 26, 28 | sylanbrc 583 |
1
⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ (𝑇 ∈ (𝑆‘𝑈) ∧ 𝐴 ∈ 𝐵 ∧ (𝐹‘𝐴) ∈ 𝑈)) → ∃!𝑥 ∈ 𝑇 𝐴 ∈ 𝑥) |