Step | Hyp | Ref
| Expression |
1 | | heibor.7 |
. . . . . . . 8
⊢ (𝜑 → 𝐹:ℕ0⟶(𝒫 𝑋 ∩ Fin)) |
2 | | 0nn0 12257 |
. . . . . . . 8
⊢ 0 ∈
ℕ0 |
3 | | inss2 4164 |
. . . . . . . . 9
⊢
(𝒫 𝑋 ∩
Fin) ⊆ Fin |
4 | | ffvelrn 6968 |
. . . . . . . . 9
⊢ ((𝐹:ℕ0⟶(𝒫 𝑋 ∩ Fin) ∧ 0 ∈
ℕ0) → (𝐹‘0) ∈ (𝒫 𝑋 ∩ Fin)) |
5 | 3, 4 | sselid 3920 |
. . . . . . . 8
⊢ ((𝐹:ℕ0⟶(𝒫 𝑋 ∩ Fin) ∧ 0 ∈
ℕ0) → (𝐹‘0) ∈ Fin) |
6 | 1, 2, 5 | sylancl 586 |
. . . . . . 7
⊢ (𝜑 → (𝐹‘0) ∈ Fin) |
7 | | heibor.8 |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑛 ∈ ℕ0 𝑋 = ∪ 𝑦 ∈ (𝐹‘𝑛)(𝑦𝐵𝑛)) |
8 | | fveq2 6783 |
. . . . . . . . . . . 12
⊢ (𝑛 = 0 → (𝐹‘𝑛) = (𝐹‘0)) |
9 | | oveq2 7292 |
. . . . . . . . . . . 12
⊢ (𝑛 = 0 → (𝑦𝐵𝑛) = (𝑦𝐵0)) |
10 | 8, 9 | iuneq12d 4953 |
. . . . . . . . . . 11
⊢ (𝑛 = 0 → ∪ 𝑦 ∈ (𝐹‘𝑛)(𝑦𝐵𝑛) = ∪ 𝑦 ∈ (𝐹‘0)(𝑦𝐵0)) |
11 | 10 | eqeq2d 2750 |
. . . . . . . . . 10
⊢ (𝑛 = 0 → (𝑋 = ∪ 𝑦 ∈ (𝐹‘𝑛)(𝑦𝐵𝑛) ↔ 𝑋 = ∪ 𝑦 ∈ (𝐹‘0)(𝑦𝐵0))) |
12 | 11 | rspccva 3561 |
. . . . . . . . 9
⊢
((∀𝑛 ∈
ℕ0 𝑋 =
∪ 𝑦 ∈ (𝐹‘𝑛)(𝑦𝐵𝑛) ∧ 0 ∈ ℕ0) →
𝑋 = ∪ 𝑦 ∈ (𝐹‘0)(𝑦𝐵0)) |
13 | 7, 2, 12 | sylancl 586 |
. . . . . . . 8
⊢ (𝜑 → 𝑋 = ∪ 𝑦 ∈ (𝐹‘0)(𝑦𝐵0)) |
14 | | eqimss 3978 |
. . . . . . . 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 7317 |
. . . . . . . . . 10
⊢ (𝑦𝐵0) ∈ V |
19 | 16, 17, 18 | heiborlem1 35978 |
. . . . . . . . 9
⊢ (((𝐹‘0) ∈ Fin ∧ 𝑋 ⊆ ∪ 𝑦 ∈ (𝐹‘0)(𝑦𝐵0) ∧ 𝑋 ∈ 𝐾) → ∃𝑦 ∈ (𝐹‘0)(𝑦𝐵0) ∈ 𝐾) |
20 | | oveq1 7291 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑥 → (𝑦𝐵0) = (𝑥𝐵0)) |
21 | 20 | eleq1d 2824 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑥 → ((𝑦𝐵0) ∈ 𝐾 ↔ (𝑥𝐵0) ∈ 𝐾)) |
22 | 21 | cbvrexvw 3385 |
. . . . . . . . 9
⊢
(∃𝑦 ∈
(𝐹‘0)(𝑦𝐵0) ∈ 𝐾 ↔ ∃𝑥 ∈ (𝐹‘0)(𝑥𝐵0) ∈ 𝐾) |
23 | 19, 22 | sylib 217 |
. . . . . . . 8
⊢ (((𝐹‘0) ∈ Fin ∧ 𝑋 ⊆ ∪ 𝑦 ∈ (𝐹‘0)(𝑦𝐵0) ∧ 𝑋 ∈ 𝐾) → ∃𝑥 ∈ (𝐹‘0)(𝑥𝐵0) ∈ 𝐾) |
24 | 23 | 3expia 1120 |
. . . . . . 7
⊢ (((𝐹‘0) ∈ Fin ∧ 𝑋 ⊆ ∪ 𝑦 ∈ (𝐹‘0)(𝑦𝐵0)) → (𝑋 ∈ 𝐾 → ∃𝑥 ∈ (𝐹‘0)(𝑥𝐵0) ∈ 𝐾)) |
25 | 6, 15, 24 | syl2anc 584 |
. . . . . 6
⊢ (𝜑 → (𝑋 ∈ 𝐾 → ∃𝑥 ∈ (𝐹‘0)(𝑥𝐵0) ∈ 𝐾)) |
26 | 25 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ (𝑈 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪
𝑈)) → (𝑋 ∈ 𝐾 → ∃𝑥 ∈ (𝐹‘0)(𝑥𝐵0) ∈ 𝐾)) |
27 | | heibor.4 |
. . . . . . . . . 10
⊢ 𝐺 = {〈𝑦, 𝑛〉 ∣ (𝑛 ∈ ℕ0 ∧ 𝑦 ∈ (𝐹‘𝑛) ∧ (𝑦𝐵𝑛) ∈ 𝐾)} |
28 | | vex 3437 |
. . . . . . . . . 10
⊢ 𝑥 ∈ V |
29 | | c0ex 10978 |
. . . . . . . . . 10
⊢ 0 ∈
V |
30 | 16, 17, 27, 28, 29 | heiborlem2 35979 |
. . . . . . . . 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 35980 |
. . . . . . . . . . 11
⊢ (𝜑 → ∃𝑔∀𝑥 ∈ 𝐺 ((𝑔‘𝑥)𝐺((2nd ‘𝑥) + 1) ∧ ((𝐵‘𝑥) ∩ ((𝑔‘𝑥)𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾)) |
34 | 33 | ad2antrr 723 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑈 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪
𝑈)) ∧ 𝑥𝐺0) → ∃𝑔∀𝑥 ∈ 𝐺 ((𝑔‘𝑥)𝐺((2nd ‘𝑥) + 1) ∧ ((𝐵‘𝑥) ∩ ((𝑔‘𝑥)𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾)) |
35 | 32 | ad2antrr 723 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑈 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪
𝑈)) ∧ (𝑥𝐺0 ∧ ∀𝑥 ∈ 𝐺 ((𝑔‘𝑥)𝐺((2nd ‘𝑥) + 1) ∧ ((𝐵‘𝑥) ∩ ((𝑔‘𝑥)𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾))) → 𝐷 ∈ (CMet‘𝑋)) |
36 | 1 | ad2antrr 723 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑈 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪
𝑈)) ∧ (𝑥𝐺0 ∧ ∀𝑥 ∈ 𝐺 ((𝑔‘𝑥)𝐺((2nd ‘𝑥) + 1) ∧ ((𝐵‘𝑥) ∩ ((𝑔‘𝑥)𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾))) → 𝐹:ℕ0⟶(𝒫 𝑋 ∩ Fin)) |
37 | 7 | ad2antrr 723 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑈 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪
𝑈)) ∧ (𝑥𝐺0 ∧ ∀𝑥 ∈ 𝐺 ((𝑔‘𝑥)𝐺((2nd ‘𝑥) + 1) ∧ ((𝐵‘𝑥) ∩ ((𝑔‘𝑥)𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾))) → ∀𝑛 ∈ ℕ0 𝑋 = ∪ 𝑦 ∈ (𝐹‘𝑛)(𝑦𝐵𝑛)) |
38 | | simprr 770 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑈 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪
𝑈)) ∧ (𝑥𝐺0 ∧ ∀𝑥 ∈ 𝐺 ((𝑔‘𝑥)𝐺((2nd ‘𝑥) + 1) ∧ ((𝐵‘𝑥) ∩ ((𝑔‘𝑥)𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾))) → ∀𝑥 ∈ 𝐺 ((𝑔‘𝑥)𝐺((2nd ‘𝑥) + 1) ∧ ((𝐵‘𝑥) ∩ ((𝑔‘𝑥)𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾)) |
39 | | fveq2 6783 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑡 → (𝑔‘𝑥) = (𝑔‘𝑡)) |
40 | | fveq2 6783 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑡 → (2nd ‘𝑥) = (2nd ‘𝑡)) |
41 | 40 | oveq1d 7299 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑡 → ((2nd ‘𝑥) + 1) = ((2nd
‘𝑡) +
1)) |
42 | 39, 41 | breq12d 5088 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑡 → ((𝑔‘𝑥)𝐺((2nd ‘𝑥) + 1) ↔ (𝑔‘𝑡)𝐺((2nd ‘𝑡) + 1))) |
43 | | fveq2 6783 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑡 → (𝐵‘𝑥) = (𝐵‘𝑡)) |
44 | 39, 41 | oveq12d 7302 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑡 → ((𝑔‘𝑥)𝐵((2nd ‘𝑥) + 1)) = ((𝑔‘𝑡)𝐵((2nd ‘𝑡) + 1))) |
45 | 43, 44 | ineq12d 4148 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑡 → ((𝐵‘𝑥) ∩ ((𝑔‘𝑥)𝐵((2nd ‘𝑥) + 1))) = ((𝐵‘𝑡) ∩ ((𝑔‘𝑡)𝐵((2nd ‘𝑡) + 1)))) |
46 | 45 | eleq1d 2824 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑡 → (((𝐵‘𝑥) ∩ ((𝑔‘𝑥)𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾 ↔ ((𝐵‘𝑡) ∩ ((𝑔‘𝑡)𝐵((2nd ‘𝑡) + 1))) ∈ 𝐾)) |
47 | 42, 46 | anbi12d 631 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑡 → (((𝑔‘𝑥)𝐺((2nd ‘𝑥) + 1) ∧ ((𝐵‘𝑥) ∩ ((𝑔‘𝑥)𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾) ↔ ((𝑔‘𝑡)𝐺((2nd ‘𝑡) + 1) ∧ ((𝐵‘𝑡) ∩ ((𝑔‘𝑡)𝐵((2nd ‘𝑡) + 1))) ∈ 𝐾))) |
48 | 47 | cbvralvw 3384 |
. . . . . . . . . . . . . 14
⊢
(∀𝑥 ∈
𝐺 ((𝑔‘𝑥)𝐺((2nd ‘𝑥) + 1) ∧ ((𝐵‘𝑥) ∩ ((𝑔‘𝑥)𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾) ↔ ∀𝑡 ∈ 𝐺 ((𝑔‘𝑡)𝐺((2nd ‘𝑡) + 1) ∧ ((𝐵‘𝑡) ∩ ((𝑔‘𝑡)𝐵((2nd ‘𝑡) + 1))) ∈ 𝐾)) |
49 | 38, 48 | sylib 217 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑈 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪
𝑈)) ∧ (𝑥𝐺0 ∧ ∀𝑥 ∈ 𝐺 ((𝑔‘𝑥)𝐺((2nd ‘𝑥) + 1) ∧ ((𝐵‘𝑥) ∩ ((𝑔‘𝑥)𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾))) → ∀𝑡 ∈ 𝐺 ((𝑔‘𝑡)𝐺((2nd ‘𝑡) + 1) ∧ ((𝐵‘𝑡) ∩ ((𝑔‘𝑡)𝐵((2nd ‘𝑡) + 1))) ∈ 𝐾)) |
50 | | simprl 768 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑈 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪
𝑈)) ∧ (𝑥𝐺0 ∧ ∀𝑥 ∈ 𝐺 ((𝑔‘𝑥)𝐺((2nd ‘𝑥) + 1) ∧ ((𝐵‘𝑥) ∩ ((𝑔‘𝑥)𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾))) → 𝑥𝐺0) |
51 | | eqeq1 2743 |
. . . . . . . . . . . . . . . 16
⊢ (𝑔 = 𝑚 → (𝑔 = 0 ↔ 𝑚 = 0)) |
52 | | oveq1 7291 |
. . . . . . . . . . . . . . . 16
⊢ (𝑔 = 𝑚 → (𝑔 − 1) = (𝑚 − 1)) |
53 | 51, 52 | ifbieq2d 4486 |
. . . . . . . . . . . . . . 15
⊢ (𝑔 = 𝑚 → if(𝑔 = 0, 𝑥, (𝑔 − 1)) = if(𝑚 = 0, 𝑥, (𝑚 − 1))) |
54 | 53 | cbvmptv 5188 |
. . . . . . . . . . . . . 14
⊢ (𝑔 ∈ ℕ0
↦ if(𝑔 = 0, 𝑥, (𝑔 − 1))) = (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝑥, (𝑚 − 1))) |
55 | | seqeq3 13735 |
. . . . . . . . . . . . . 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 2739 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ ↦
〈(seq0(𝑔, (𝑔 ∈ ℕ0
↦ if(𝑔 = 0, 𝑥, (𝑔 − 1))))‘𝑛), (3 / (2↑𝑛))〉) = (𝑛 ∈ ℕ ↦ 〈(seq0(𝑔, (𝑔 ∈ ℕ0 ↦ if(𝑔 = 0, 𝑥, (𝑔 − 1))))‘𝑛), (3 / (2↑𝑛))〉) |
58 | | simplrl 774 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑈 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪
𝑈)) ∧ (𝑥𝐺0 ∧ ∀𝑥 ∈ 𝐺 ((𝑔‘𝑥)𝐺((2nd ‘𝑥) + 1) ∧ ((𝐵‘𝑥) ∩ ((𝑔‘𝑥)𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾))) → 𝑈 ⊆ 𝐽) |
59 | | cmetmet 24459 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐷 ∈ (CMet‘𝑋) → 𝐷 ∈ (Met‘𝑋)) |
60 | | metxmet 23496 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐷 ∈ (Met‘𝑋) → 𝐷 ∈ (∞Met‘𝑋)) |
61 | 16 | mopnuni 23603 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝑋 = ∪ 𝐽) |
62 | 32, 59, 60, 61 | 4syl 19 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑋 = ∪ 𝐽) |
63 | 62 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑈 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪
𝑈)) → 𝑋 = ∪
𝐽) |
64 | | simprr 770 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑈 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪
𝑈)) → ∪ 𝐽 =
∪ 𝑈) |
65 | 63, 64 | eqtr2d 2780 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑈 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪
𝑈)) → ∪ 𝑈 =
𝑋) |
66 | 65 | adantr 481 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑈 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪
𝑈)) ∧ (𝑥𝐺0 ∧ ∀𝑥 ∈ 𝐺 ((𝑔‘𝑥)𝐺((2nd ‘𝑥) + 1) ∧ ((𝐵‘𝑥) ∩ ((𝑔‘𝑥)𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾))) → ∪
𝑈 = 𝑋) |
67 | 16, 17, 27, 31, 35, 36, 37, 49, 50, 56, 57, 58, 66 | heiborlem9 35986 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑈 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪
𝑈)) ∧ (𝑥𝐺0 ∧ ∀𝑥 ∈ 𝐺 ((𝑔‘𝑥)𝐺((2nd ‘𝑥) + 1) ∧ ((𝐵‘𝑥) ∩ ((𝑔‘𝑥)𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾))) → ¬ 𝑋 ∈ 𝐾) |
68 | 67 | expr 457 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑈 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪
𝑈)) ∧ 𝑥𝐺0) → (∀𝑥 ∈ 𝐺 ((𝑔‘𝑥)𝐺((2nd ‘𝑥) + 1) ∧ ((𝐵‘𝑥) ∩ ((𝑔‘𝑥)𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾) → ¬ 𝑋 ∈ 𝐾)) |
69 | 68 | exlimdv 1937 |
. . . . . . . . . 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 1353 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑈 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪
𝑈)) → (0 ∈
ℕ0 → (𝑥 ∈ (𝐹‘0) → ((𝑥𝐵0) ∈ 𝐾 → ¬ 𝑋 ∈ 𝐾)))) |
73 | 2, 72 | mpi 20 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑈 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪
𝑈)) → (𝑥 ∈ (𝐹‘0) → ((𝑥𝐵0) ∈ 𝐾 → ¬ 𝑋 ∈ 𝐾))) |
74 | 73 | rexlimdv 3213 |
. . . . 5
⊢ ((𝜑 ∧ (𝑈 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪
𝑈)) → (∃𝑥 ∈ (𝐹‘0)(𝑥𝐵0) ∈ 𝐾 → ¬ 𝑋 ∈ 𝐾)) |
75 | 26, 74 | syld 47 |
. . . 4
⊢ ((𝜑 ∧ (𝑈 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪
𝑈)) → (𝑋 ∈ 𝐾 → ¬ 𝑋 ∈ 𝐾)) |
76 | 75 | pm2.01d 189 |
. . 3
⊢ ((𝜑 ∧ (𝑈 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪
𝑈)) → ¬ 𝑋 ∈ 𝐾) |
77 | | elfvdm 6815 |
. . . . . 6
⊢ (𝐷 ∈ (CMet‘𝑋) → 𝑋 ∈ dom CMet) |
78 | | sseq1 3947 |
. . . . . . . . 9
⊢ (𝑢 = 𝑋 → (𝑢 ⊆ ∪ 𝑣 ↔ 𝑋 ⊆ ∪ 𝑣)) |
79 | 78 | rexbidv 3227 |
. . . . . . . 8
⊢ (𝑢 = 𝑋 → (∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)𝑢 ⊆ ∪ 𝑣 ↔ ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)𝑋 ⊆ ∪ 𝑣)) |
80 | 79 | notbid 318 |
. . . . . . 7
⊢ (𝑢 = 𝑋 → (¬ ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)𝑢 ⊆ ∪ 𝑣 ↔ ¬ ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)𝑋 ⊆ ∪ 𝑣)) |
81 | 80, 17 | elab2g 3612 |
. . . . . 6
⊢ (𝑋 ∈ dom CMet → (𝑋 ∈ 𝐾 ↔ ¬ ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)𝑋 ⊆ ∪ 𝑣)) |
82 | 32, 77, 81 | 3syl 18 |
. . . . 5
⊢ (𝜑 → (𝑋 ∈ 𝐾 ↔ ¬ ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)𝑋 ⊆ ∪ 𝑣)) |
83 | 82 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ (𝑈 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪
𝑈)) → (𝑋 ∈ 𝐾 ↔ ¬ ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)𝑋 ⊆ ∪ 𝑣)) |
84 | 83 | con2bid 355 |
. . 3
⊢ ((𝜑 ∧ (𝑈 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪
𝑈)) → (∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)𝑋 ⊆ ∪ 𝑣 ↔ ¬ 𝑋 ∈ 𝐾)) |
85 | 76, 84 | mpbird 256 |
. 2
⊢ ((𝜑 ∧ (𝑈 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪
𝑈)) → ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)𝑋 ⊆ ∪ 𝑣) |
86 | 62 | ad2antrr 723 |
. . . . 5
⊢ (((𝜑 ∧ (𝑈 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪
𝑈)) ∧ 𝑣 ∈ (𝒫 𝑈 ∩ Fin)) → 𝑋 = ∪
𝐽) |
87 | 86 | sseq1d 3953 |
. . . 4
⊢ (((𝜑 ∧ (𝑈 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪
𝑈)) ∧ 𝑣 ∈ (𝒫 𝑈 ∩ Fin)) → (𝑋 ⊆ ∪ 𝑣
↔ ∪ 𝐽 ⊆ ∪ 𝑣)) |
88 | | inss1 4163 |
. . . . . . . . 9
⊢
(𝒫 𝑈 ∩
Fin) ⊆ 𝒫 𝑈 |
89 | 88 | sseli 3918 |
. . . . . . . 8
⊢ (𝑣 ∈ (𝒫 𝑈 ∩ Fin) → 𝑣 ∈ 𝒫 𝑈) |
90 | 89 | elpwid 4545 |
. . . . . . 7
⊢ (𝑣 ∈ (𝒫 𝑈 ∩ Fin) → 𝑣 ⊆ 𝑈) |
91 | | simprl 768 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑈 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪
𝑈)) → 𝑈 ⊆ 𝐽) |
92 | | sstr 3930 |
. . . . . . . 8
⊢ ((𝑣 ⊆ 𝑈 ∧ 𝑈 ⊆ 𝐽) → 𝑣 ⊆ 𝐽) |
93 | 92 | unissd 4850 |
. . . . . . 7
⊢ ((𝑣 ⊆ 𝑈 ∧ 𝑈 ⊆ 𝐽) → ∪ 𝑣 ⊆ ∪ 𝐽) |
94 | 90, 91, 93 | syl2anr 597 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑈 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪
𝑈)) ∧ 𝑣 ∈ (𝒫 𝑈 ∩ Fin)) → ∪ 𝑣
⊆ ∪ 𝐽) |
95 | 94 | biantrud 532 |
. . . . 5
⊢ (((𝜑 ∧ (𝑈 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪
𝑈)) ∧ 𝑣 ∈ (𝒫 𝑈 ∩ Fin)) → (∪ 𝐽
⊆ ∪ 𝑣 ↔ (∪ 𝐽 ⊆ ∪ 𝑣
∧ ∪ 𝑣 ⊆ ∪ 𝐽))) |
96 | | eqss 3937 |
. . . . 5
⊢ (∪ 𝐽 =
∪ 𝑣 ↔ (∪ 𝐽 ⊆ ∪ 𝑣
∧ ∪ 𝑣 ⊆ ∪ 𝐽)) |
97 | 95, 96 | bitr4di 289 |
. . . 4
⊢ (((𝜑 ∧ (𝑈 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪
𝑈)) ∧ 𝑣 ∈ (𝒫 𝑈 ∩ Fin)) → (∪ 𝐽
⊆ ∪ 𝑣 ↔ ∪ 𝐽 = ∪
𝑣)) |
98 | 87, 97 | bitrd 278 |
. . 3
⊢ (((𝜑 ∧ (𝑈 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪
𝑈)) ∧ 𝑣 ∈ (𝒫 𝑈 ∩ Fin)) → (𝑋 ⊆ ∪ 𝑣
↔ ∪ 𝐽 = ∪ 𝑣)) |
99 | 98 | rexbidva 3226 |
. 2
⊢ ((𝜑 ∧ (𝑈 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪
𝑈)) → (∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)𝑋 ⊆ ∪ 𝑣 ↔ ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)∪ 𝐽 =
∪ 𝑣)) |
100 | 85, 99 | mpbid 231 |
1
⊢ ((𝜑 ∧ (𝑈 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪
𝑈)) → ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)∪ 𝐽 =
∪ 𝑣) |