| Step | Hyp | Ref
| Expression |
| 1 | | heibor.7 |
. . . . . . . 8
⊢ (𝜑 → 𝐹:ℕ0⟶(𝒫 𝑋 ∩ Fin)) |
| 2 | | 0nn0 12541 |
. . . . . . . 8
⊢ 0 ∈
ℕ0 |
| 3 | | inss2 4238 |
. . . . . . . . 9
⊢
(𝒫 𝑋 ∩
Fin) ⊆ Fin |
| 4 | | ffvelcdm 7101 |
. . . . . . . . 9
⊢ ((𝐹:ℕ0⟶(𝒫 𝑋 ∩ Fin) ∧ 0 ∈
ℕ0) → (𝐹‘0) ∈ (𝒫 𝑋 ∩ Fin)) |
| 5 | 3, 4 | sselid 3981 |
. . . . . . . 8
⊢ ((𝐹:ℕ0⟶(𝒫 𝑋 ∩ Fin) ∧ 0 ∈
ℕ0) → (𝐹‘0) ∈ Fin) |
| 6 | 1, 2, 5 | sylancl 586 |
. . . . . . 7
⊢ (𝜑 → (𝐹‘0) ∈ Fin) |
| 7 | | heibor.8 |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑛 ∈ ℕ0 𝑋 = ∪ 𝑦 ∈ (𝐹‘𝑛)(𝑦𝐵𝑛)) |
| 8 | | fveq2 6906 |
. . . . . . . . . . . 12
⊢ (𝑛 = 0 → (𝐹‘𝑛) = (𝐹‘0)) |
| 9 | | oveq2 7439 |
. . . . . . . . . . . 12
⊢ (𝑛 = 0 → (𝑦𝐵𝑛) = (𝑦𝐵0)) |
| 10 | 8, 9 | iuneq12d 5021 |
. . . . . . . . . . 11
⊢ (𝑛 = 0 → ∪ 𝑦 ∈ (𝐹‘𝑛)(𝑦𝐵𝑛) = ∪ 𝑦 ∈ (𝐹‘0)(𝑦𝐵0)) |
| 11 | 10 | eqeq2d 2748 |
. . . . . . . . . 10
⊢ (𝑛 = 0 → (𝑋 = ∪ 𝑦 ∈ (𝐹‘𝑛)(𝑦𝐵𝑛) ↔ 𝑋 = ∪ 𝑦 ∈ (𝐹‘0)(𝑦𝐵0))) |
| 12 | 11 | rspccva 3621 |
. . . . . . . . 9
⊢
((∀𝑛 ∈
ℕ0 𝑋 =
∪ 𝑦 ∈ (𝐹‘𝑛)(𝑦𝐵𝑛) ∧ 0 ∈ ℕ0) →
𝑋 = ∪ 𝑦 ∈ (𝐹‘0)(𝑦𝐵0)) |
| 13 | 7, 2, 12 | sylancl 586 |
. . . . . . . 8
⊢ (𝜑 → 𝑋 = ∪ 𝑦 ∈ (𝐹‘0)(𝑦𝐵0)) |
| 14 | | eqimss 4042 |
. . . . . . . 8
⊢ (𝑋 = ∪ 𝑦 ∈ (𝐹‘0)(𝑦𝐵0) → 𝑋 ⊆ ∪
𝑦 ∈ (𝐹‘0)(𝑦𝐵0)) |
| 15 | 13, 14 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑋 ⊆ ∪
𝑦 ∈ (𝐹‘0)(𝑦𝐵0)) |
| 16 | | heibor.1 |
. . . . . . . . . 10
⊢ 𝐽 = (MetOpen‘𝐷) |
| 17 | | heibor.3 |
. . . . . . . . . 10
⊢ 𝐾 = {𝑢 ∣ ¬ ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)𝑢 ⊆ ∪ 𝑣} |
| 18 | | ovex 7464 |
. . . . . . . . . 10
⊢ (𝑦𝐵0) ∈ V |
| 19 | 16, 17, 18 | heiborlem1 37818 |
. . . . . . . . 9
⊢ (((𝐹‘0) ∈ Fin ∧ 𝑋 ⊆ ∪ 𝑦 ∈ (𝐹‘0)(𝑦𝐵0) ∧ 𝑋 ∈ 𝐾) → ∃𝑦 ∈ (𝐹‘0)(𝑦𝐵0) ∈ 𝐾) |
| 20 | | oveq1 7438 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑥 → (𝑦𝐵0) = (𝑥𝐵0)) |
| 21 | 20 | eleq1d 2826 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑥 → ((𝑦𝐵0) ∈ 𝐾 ↔ (𝑥𝐵0) ∈ 𝐾)) |
| 22 | 21 | cbvrexvw 3238 |
. . . . . . . . 9
⊢
(∃𝑦 ∈
(𝐹‘0)(𝑦𝐵0) ∈ 𝐾 ↔ ∃𝑥 ∈ (𝐹‘0)(𝑥𝐵0) ∈ 𝐾) |
| 23 | 19, 22 | sylib 218 |
. . . . . . . 8
⊢ (((𝐹‘0) ∈ Fin ∧ 𝑋 ⊆ ∪ 𝑦 ∈ (𝐹‘0)(𝑦𝐵0) ∧ 𝑋 ∈ 𝐾) → ∃𝑥 ∈ (𝐹‘0)(𝑥𝐵0) ∈ 𝐾) |
| 24 | 23 | 3expia 1122 |
. . . . . . 7
⊢ (((𝐹‘0) ∈ Fin ∧ 𝑋 ⊆ ∪ 𝑦 ∈ (𝐹‘0)(𝑦𝐵0)) → (𝑋 ∈ 𝐾 → ∃𝑥 ∈ (𝐹‘0)(𝑥𝐵0) ∈ 𝐾)) |
| 25 | 6, 15, 24 | syl2anc 584 |
. . . . . 6
⊢ (𝜑 → (𝑋 ∈ 𝐾 → ∃𝑥 ∈ (𝐹‘0)(𝑥𝐵0) ∈ 𝐾)) |
| 26 | 25 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (𝑈 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪
𝑈)) → (𝑋 ∈ 𝐾 → ∃𝑥 ∈ (𝐹‘0)(𝑥𝐵0) ∈ 𝐾)) |
| 27 | | heibor.4 |
. . . . . . . . . 10
⊢ 𝐺 = {〈𝑦, 𝑛〉 ∣ (𝑛 ∈ ℕ0 ∧ 𝑦 ∈ (𝐹‘𝑛) ∧ (𝑦𝐵𝑛) ∈ 𝐾)} |
| 28 | | vex 3484 |
. . . . . . . . . 10
⊢ 𝑥 ∈ V |
| 29 | | c0ex 11255 |
. . . . . . . . . 10
⊢ 0 ∈
V |
| 30 | 16, 17, 27, 28, 29 | heiborlem2 37819 |
. . . . . . . . 9
⊢ (𝑥𝐺0 ↔ (0 ∈ ℕ0 ∧
𝑥 ∈ (𝐹‘0) ∧ (𝑥𝐵0) ∈ 𝐾)) |
| 31 | | heibor.5 |
. . . . . . . . . . . 12
⊢ 𝐵 = (𝑧 ∈ 𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚)))) |
| 32 | | heibor.6 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐷 ∈ (CMet‘𝑋)) |
| 33 | 16, 17, 27, 31, 32, 1, 7 | heiborlem3 37820 |
. . . . . . . . . . 11
⊢ (𝜑 → ∃𝑔∀𝑥 ∈ 𝐺 ((𝑔‘𝑥)𝐺((2nd ‘𝑥) + 1) ∧ ((𝐵‘𝑥) ∩ ((𝑔‘𝑥)𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾)) |
| 34 | 33 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑈 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪
𝑈)) ∧ 𝑥𝐺0) → ∃𝑔∀𝑥 ∈ 𝐺 ((𝑔‘𝑥)𝐺((2nd ‘𝑥) + 1) ∧ ((𝐵‘𝑥) ∩ ((𝑔‘𝑥)𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾)) |
| 35 | 32 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑈 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪
𝑈)) ∧ (𝑥𝐺0 ∧ ∀𝑥 ∈ 𝐺 ((𝑔‘𝑥)𝐺((2nd ‘𝑥) + 1) ∧ ((𝐵‘𝑥) ∩ ((𝑔‘𝑥)𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾))) → 𝐷 ∈ (CMet‘𝑋)) |
| 36 | 1 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑈 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪
𝑈)) ∧ (𝑥𝐺0 ∧ ∀𝑥 ∈ 𝐺 ((𝑔‘𝑥)𝐺((2nd ‘𝑥) + 1) ∧ ((𝐵‘𝑥) ∩ ((𝑔‘𝑥)𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾))) → 𝐹:ℕ0⟶(𝒫 𝑋 ∩ Fin)) |
| 37 | 7 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑈 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪
𝑈)) ∧ (𝑥𝐺0 ∧ ∀𝑥 ∈ 𝐺 ((𝑔‘𝑥)𝐺((2nd ‘𝑥) + 1) ∧ ((𝐵‘𝑥) ∩ ((𝑔‘𝑥)𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾))) → ∀𝑛 ∈ ℕ0 𝑋 = ∪ 𝑦 ∈ (𝐹‘𝑛)(𝑦𝐵𝑛)) |
| 38 | | simprr 773 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑈 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪
𝑈)) ∧ (𝑥𝐺0 ∧ ∀𝑥 ∈ 𝐺 ((𝑔‘𝑥)𝐺((2nd ‘𝑥) + 1) ∧ ((𝐵‘𝑥) ∩ ((𝑔‘𝑥)𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾))) → ∀𝑥 ∈ 𝐺 ((𝑔‘𝑥)𝐺((2nd ‘𝑥) + 1) ∧ ((𝐵‘𝑥) ∩ ((𝑔‘𝑥)𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾)) |
| 39 | | fveq2 6906 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑡 → (𝑔‘𝑥) = (𝑔‘𝑡)) |
| 40 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑡 → (2nd ‘𝑥) = (2nd ‘𝑡)) |
| 41 | 40 | oveq1d 7446 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑡 → ((2nd ‘𝑥) + 1) = ((2nd
‘𝑡) +
1)) |
| 42 | 39, 41 | breq12d 5156 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑡 → ((𝑔‘𝑥)𝐺((2nd ‘𝑥) + 1) ↔ (𝑔‘𝑡)𝐺((2nd ‘𝑡) + 1))) |
| 43 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑡 → (𝐵‘𝑥) = (𝐵‘𝑡)) |
| 44 | 39, 41 | oveq12d 7449 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑡 → ((𝑔‘𝑥)𝐵((2nd ‘𝑥) + 1)) = ((𝑔‘𝑡)𝐵((2nd ‘𝑡) + 1))) |
| 45 | 43, 44 | ineq12d 4221 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑡 → ((𝐵‘𝑥) ∩ ((𝑔‘𝑥)𝐵((2nd ‘𝑥) + 1))) = ((𝐵‘𝑡) ∩ ((𝑔‘𝑡)𝐵((2nd ‘𝑡) + 1)))) |
| 46 | 45 | eleq1d 2826 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑡 → (((𝐵‘𝑥) ∩ ((𝑔‘𝑥)𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾 ↔ ((𝐵‘𝑡) ∩ ((𝑔‘𝑡)𝐵((2nd ‘𝑡) + 1))) ∈ 𝐾)) |
| 47 | 42, 46 | anbi12d 632 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑡 → (((𝑔‘𝑥)𝐺((2nd ‘𝑥) + 1) ∧ ((𝐵‘𝑥) ∩ ((𝑔‘𝑥)𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾) ↔ ((𝑔‘𝑡)𝐺((2nd ‘𝑡) + 1) ∧ ((𝐵‘𝑡) ∩ ((𝑔‘𝑡)𝐵((2nd ‘𝑡) + 1))) ∈ 𝐾))) |
| 48 | 47 | cbvralvw 3237 |
. . . . . . . . . . . . . 14
⊢
(∀𝑥 ∈
𝐺 ((𝑔‘𝑥)𝐺((2nd ‘𝑥) + 1) ∧ ((𝐵‘𝑥) ∩ ((𝑔‘𝑥)𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾) ↔ ∀𝑡 ∈ 𝐺 ((𝑔‘𝑡)𝐺((2nd ‘𝑡) + 1) ∧ ((𝐵‘𝑡) ∩ ((𝑔‘𝑡)𝐵((2nd ‘𝑡) + 1))) ∈ 𝐾)) |
| 49 | 38, 48 | sylib 218 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑈 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪
𝑈)) ∧ (𝑥𝐺0 ∧ ∀𝑥 ∈ 𝐺 ((𝑔‘𝑥)𝐺((2nd ‘𝑥) + 1) ∧ ((𝐵‘𝑥) ∩ ((𝑔‘𝑥)𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾))) → ∀𝑡 ∈ 𝐺 ((𝑔‘𝑡)𝐺((2nd ‘𝑡) + 1) ∧ ((𝐵‘𝑡) ∩ ((𝑔‘𝑡)𝐵((2nd ‘𝑡) + 1))) ∈ 𝐾)) |
| 50 | | simprl 771 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑈 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪
𝑈)) ∧ (𝑥𝐺0 ∧ ∀𝑥 ∈ 𝐺 ((𝑔‘𝑥)𝐺((2nd ‘𝑥) + 1) ∧ ((𝐵‘𝑥) ∩ ((𝑔‘𝑥)𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾))) → 𝑥𝐺0) |
| 51 | | eqeq1 2741 |
. . . . . . . . . . . . . . . 16
⊢ (𝑔 = 𝑚 → (𝑔 = 0 ↔ 𝑚 = 0)) |
| 52 | | oveq1 7438 |
. . . . . . . . . . . . . . . 16
⊢ (𝑔 = 𝑚 → (𝑔 − 1) = (𝑚 − 1)) |
| 53 | 51, 52 | ifbieq2d 4552 |
. . . . . . . . . . . . . . 15
⊢ (𝑔 = 𝑚 → if(𝑔 = 0, 𝑥, (𝑔 − 1)) = if(𝑚 = 0, 𝑥, (𝑚 − 1))) |
| 54 | 53 | cbvmptv 5255 |
. . . . . . . . . . . . . 14
⊢ (𝑔 ∈ ℕ0
↦ if(𝑔 = 0, 𝑥, (𝑔 − 1))) = (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝑥, (𝑚 − 1))) |
| 55 | | seqeq3 14047 |
. . . . . . . . . . . . . 14
⊢ ((𝑔 ∈ ℕ0
↦ if(𝑔 = 0, 𝑥, (𝑔 − 1))) = (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝑥, (𝑚 − 1))) → seq0(𝑔, (𝑔 ∈ ℕ0 ↦ if(𝑔 = 0, 𝑥, (𝑔 − 1)))) = seq0(𝑔, (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝑥, (𝑚 − 1))))) |
| 56 | 54, 55 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢
seq0(𝑔, (𝑔 ∈ ℕ0
↦ if(𝑔 = 0, 𝑥, (𝑔 − 1)))) = seq0(𝑔, (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝑥, (𝑚 − 1)))) |
| 57 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ ↦
〈(seq0(𝑔, (𝑔 ∈ ℕ0
↦ if(𝑔 = 0, 𝑥, (𝑔 − 1))))‘𝑛), (3 / (2↑𝑛))〉) = (𝑛 ∈ ℕ ↦ 〈(seq0(𝑔, (𝑔 ∈ ℕ0 ↦ if(𝑔 = 0, 𝑥, (𝑔 − 1))))‘𝑛), (3 / (2↑𝑛))〉) |
| 58 | | simplrl 777 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑈 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪
𝑈)) ∧ (𝑥𝐺0 ∧ ∀𝑥 ∈ 𝐺 ((𝑔‘𝑥)𝐺((2nd ‘𝑥) + 1) ∧ ((𝐵‘𝑥) ∩ ((𝑔‘𝑥)𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾))) → 𝑈 ⊆ 𝐽) |
| 59 | | cmetmet 25320 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐷 ∈ (CMet‘𝑋) → 𝐷 ∈ (Met‘𝑋)) |
| 60 | | metxmet 24344 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐷 ∈ (Met‘𝑋) → 𝐷 ∈ (∞Met‘𝑋)) |
| 61 | 16 | mopnuni 24451 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝑋 = ∪ 𝐽) |
| 62 | 32, 59, 60, 61 | 4syl 19 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑋 = ∪ 𝐽) |
| 63 | 62 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑈 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪
𝑈)) → 𝑋 = ∪
𝐽) |
| 64 | | simprr 773 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑈 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪
𝑈)) → ∪ 𝐽 =
∪ 𝑈) |
| 65 | 63, 64 | eqtr2d 2778 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑈 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪
𝑈)) → ∪ 𝑈 =
𝑋) |
| 66 | 65 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑈 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪
𝑈)) ∧ (𝑥𝐺0 ∧ ∀𝑥 ∈ 𝐺 ((𝑔‘𝑥)𝐺((2nd ‘𝑥) + 1) ∧ ((𝐵‘𝑥) ∩ ((𝑔‘𝑥)𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾))) → ∪
𝑈 = 𝑋) |
| 67 | 16, 17, 27, 31, 35, 36, 37, 49, 50, 56, 57, 58, 66 | heiborlem9 37826 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑈 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪
𝑈)) ∧ (𝑥𝐺0 ∧ ∀𝑥 ∈ 𝐺 ((𝑔‘𝑥)𝐺((2nd ‘𝑥) + 1) ∧ ((𝐵‘𝑥) ∩ ((𝑔‘𝑥)𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾))) → ¬ 𝑋 ∈ 𝐾) |
| 68 | 67 | expr 456 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑈 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪
𝑈)) ∧ 𝑥𝐺0) → (∀𝑥 ∈ 𝐺 ((𝑔‘𝑥)𝐺((2nd ‘𝑥) + 1) ∧ ((𝐵‘𝑥) ∩ ((𝑔‘𝑥)𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾) → ¬ 𝑋 ∈ 𝐾)) |
| 69 | 68 | exlimdv 1933 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑈 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪
𝑈)) ∧ 𝑥𝐺0) → (∃𝑔∀𝑥 ∈ 𝐺 ((𝑔‘𝑥)𝐺((2nd ‘𝑥) + 1) ∧ ((𝐵‘𝑥) ∩ ((𝑔‘𝑥)𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾) → ¬ 𝑋 ∈ 𝐾)) |
| 70 | 34, 69 | mpd 15 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑈 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪
𝑈)) ∧ 𝑥𝐺0) → ¬ 𝑋 ∈ 𝐾) |
| 71 | 30, 70 | sylan2br 595 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑈 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪
𝑈)) ∧ (0 ∈
ℕ0 ∧ 𝑥
∈ (𝐹‘0) ∧
(𝑥𝐵0) ∈ 𝐾)) → ¬ 𝑋 ∈ 𝐾) |
| 72 | 71 | 3exp2 1355 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑈 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪
𝑈)) → (0 ∈
ℕ0 → (𝑥 ∈ (𝐹‘0) → ((𝑥𝐵0) ∈ 𝐾 → ¬ 𝑋 ∈ 𝐾)))) |
| 73 | 2, 72 | mpi 20 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑈 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪
𝑈)) → (𝑥 ∈ (𝐹‘0) → ((𝑥𝐵0) ∈ 𝐾 → ¬ 𝑋 ∈ 𝐾))) |
| 74 | 73 | rexlimdv 3153 |
. . . . 5
⊢ ((𝜑 ∧ (𝑈 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪
𝑈)) → (∃𝑥 ∈ (𝐹‘0)(𝑥𝐵0) ∈ 𝐾 → ¬ 𝑋 ∈ 𝐾)) |
| 75 | 26, 74 | syld 47 |
. . . 4
⊢ ((𝜑 ∧ (𝑈 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪
𝑈)) → (𝑋 ∈ 𝐾 → ¬ 𝑋 ∈ 𝐾)) |
| 76 | 75 | pm2.01d 190 |
. . 3
⊢ ((𝜑 ∧ (𝑈 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪
𝑈)) → ¬ 𝑋 ∈ 𝐾) |
| 77 | | elfvdm 6943 |
. . . . . 6
⊢ (𝐷 ∈ (CMet‘𝑋) → 𝑋 ∈ dom CMet) |
| 78 | | sseq1 4009 |
. . . . . . . . 9
⊢ (𝑢 = 𝑋 → (𝑢 ⊆ ∪ 𝑣 ↔ 𝑋 ⊆ ∪ 𝑣)) |
| 79 | 78 | rexbidv 3179 |
. . . . . . . 8
⊢ (𝑢 = 𝑋 → (∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)𝑢 ⊆ ∪ 𝑣 ↔ ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)𝑋 ⊆ ∪ 𝑣)) |
| 80 | 79 | notbid 318 |
. . . . . . 7
⊢ (𝑢 = 𝑋 → (¬ ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)𝑢 ⊆ ∪ 𝑣 ↔ ¬ ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)𝑋 ⊆ ∪ 𝑣)) |
| 81 | 80, 17 | elab2g 3680 |
. . . . . 6
⊢ (𝑋 ∈ dom CMet → (𝑋 ∈ 𝐾 ↔ ¬ ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)𝑋 ⊆ ∪ 𝑣)) |
| 82 | 32, 77, 81 | 3syl 18 |
. . . . 5
⊢ (𝜑 → (𝑋 ∈ 𝐾 ↔ ¬ ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)𝑋 ⊆ ∪ 𝑣)) |
| 83 | 82 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ (𝑈 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪
𝑈)) → (𝑋 ∈ 𝐾 ↔ ¬ ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)𝑋 ⊆ ∪ 𝑣)) |
| 84 | 83 | con2bid 354 |
. . 3
⊢ ((𝜑 ∧ (𝑈 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪
𝑈)) → (∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)𝑋 ⊆ ∪ 𝑣 ↔ ¬ 𝑋 ∈ 𝐾)) |
| 85 | 76, 84 | mpbird 257 |
. 2
⊢ ((𝜑 ∧ (𝑈 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪
𝑈)) → ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)𝑋 ⊆ ∪ 𝑣) |
| 86 | 62 | ad2antrr 726 |
. . . . 5
⊢ (((𝜑 ∧ (𝑈 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪
𝑈)) ∧ 𝑣 ∈ (𝒫 𝑈 ∩ Fin)) → 𝑋 = ∪
𝐽) |
| 87 | 86 | sseq1d 4015 |
. . . 4
⊢ (((𝜑 ∧ (𝑈 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪
𝑈)) ∧ 𝑣 ∈ (𝒫 𝑈 ∩ Fin)) → (𝑋 ⊆ ∪ 𝑣
↔ ∪ 𝐽 ⊆ ∪ 𝑣)) |
| 88 | | inss1 4237 |
. . . . . . . . 9
⊢
(𝒫 𝑈 ∩
Fin) ⊆ 𝒫 𝑈 |
| 89 | 88 | sseli 3979 |
. . . . . . . 8
⊢ (𝑣 ∈ (𝒫 𝑈 ∩ Fin) → 𝑣 ∈ 𝒫 𝑈) |
| 90 | 89 | elpwid 4609 |
. . . . . . 7
⊢ (𝑣 ∈ (𝒫 𝑈 ∩ Fin) → 𝑣 ⊆ 𝑈) |
| 91 | | simprl 771 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑈 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪
𝑈)) → 𝑈 ⊆ 𝐽) |
| 92 | | sstr 3992 |
. . . . . . . 8
⊢ ((𝑣 ⊆ 𝑈 ∧ 𝑈 ⊆ 𝐽) → 𝑣 ⊆ 𝐽) |
| 93 | 92 | unissd 4917 |
. . . . . . 7
⊢ ((𝑣 ⊆ 𝑈 ∧ 𝑈 ⊆ 𝐽) → ∪ 𝑣 ⊆ ∪ 𝐽) |
| 94 | 90, 91, 93 | syl2anr 597 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑈 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪
𝑈)) ∧ 𝑣 ∈ (𝒫 𝑈 ∩ Fin)) → ∪ 𝑣
⊆ ∪ 𝐽) |
| 95 | 94 | biantrud 531 |
. . . . 5
⊢ (((𝜑 ∧ (𝑈 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪
𝑈)) ∧ 𝑣 ∈ (𝒫 𝑈 ∩ Fin)) → (∪ 𝐽
⊆ ∪ 𝑣 ↔ (∪ 𝐽 ⊆ ∪ 𝑣
∧ ∪ 𝑣 ⊆ ∪ 𝐽))) |
| 96 | | eqss 3999 |
. . . . 5
⊢ (∪ 𝐽 =
∪ 𝑣 ↔ (∪ 𝐽 ⊆ ∪ 𝑣
∧ ∪ 𝑣 ⊆ ∪ 𝐽)) |
| 97 | 95, 96 | bitr4di 289 |
. . . 4
⊢ (((𝜑 ∧ (𝑈 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪
𝑈)) ∧ 𝑣 ∈ (𝒫 𝑈 ∩ Fin)) → (∪ 𝐽
⊆ ∪ 𝑣 ↔ ∪ 𝐽 = ∪
𝑣)) |
| 98 | 87, 97 | bitrd 279 |
. . 3
⊢ (((𝜑 ∧ (𝑈 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪
𝑈)) ∧ 𝑣 ∈ (𝒫 𝑈 ∩ Fin)) → (𝑋 ⊆ ∪ 𝑣
↔ ∪ 𝐽 = ∪ 𝑣)) |
| 99 | 98 | rexbidva 3177 |
. 2
⊢ ((𝜑 ∧ (𝑈 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪
𝑈)) → (∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)𝑋 ⊆ ∪ 𝑣 ↔ ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)∪ 𝐽 =
∪ 𝑣)) |
| 100 | 85, 99 | mpbid 232 |
1
⊢ ((𝜑 ∧ (𝑈 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪
𝑈)) → ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)∪ 𝐽 =
∪ 𝑣) |