Step | Hyp | Ref
| Expression |
1 | | eqid 2759 |
. . . . 5
⊢ ∪ 𝐽 =
∪ 𝐽 |
2 | 1 | ist0 22005 |
. . . 4
⊢ (𝐽 ∈ Kol2 ↔ (𝐽 ∈ Top ∧ ∀𝑥 ∈ ∪ 𝐽∀𝑦 ∈ ∪ 𝐽(∀𝑜 ∈ 𝐽 (𝑥 ∈ 𝑜 ↔ 𝑦 ∈ 𝑜) → 𝑥 = 𝑦))) |
3 | 2 | simplbi 502 |
. . 3
⊢ (𝐽 ∈ Kol2 → 𝐽 ∈ Top) |
4 | 3 | adantl 486 |
. 2
⊢ ((𝜑 ∧ 𝐽 ∈ Kol2) → 𝐽 ∈ Top) |
5 | 2 | baib 540 |
. . . 4
⊢ (𝐽 ∈ Top → (𝐽 ∈ Kol2 ↔
∀𝑥 ∈ ∪ 𝐽∀𝑦 ∈ ∪ 𝐽(∀𝑜 ∈ 𝐽 (𝑥 ∈ 𝑜 ↔ 𝑦 ∈ 𝑜) → 𝑥 = 𝑦))) |
6 | 5 | adantl 486 |
. . 3
⊢ ((𝜑 ∧ 𝐽 ∈ Top) → (𝐽 ∈ Kol2 ↔ ∀𝑥 ∈ ∪ 𝐽∀𝑦 ∈ ∪ 𝐽(∀𝑜 ∈ 𝐽 (𝑥 ∈ 𝑜 ↔ 𝑦 ∈ 𝑜) → 𝑥 = 𝑦))) |
7 | | ist0cls.1 |
. . . . . 6
⊢ (𝜑 → 𝐵 = ∪ 𝐽) |
8 | 7 | adantr 485 |
. . . . 5
⊢ ((𝜑 ∧ 𝐽 ∈ Top) → 𝐵 = ∪ 𝐽) |
9 | 8 | eqcomd 2765 |
. . . 4
⊢ ((𝜑 ∧ 𝐽 ∈ Top) → ∪ 𝐽 =
𝐵) |
10 | 9 | adantr 485 |
. . . . 5
⊢ (((𝜑 ∧ 𝐽 ∈ Top) ∧ 𝑥 ∈ ∪ 𝐽) → ∪ 𝐽 =
𝐵) |
11 | | simp-4r 784 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝐽 ∈ Top) ∧ 𝑥 ∈ ∪ 𝐽)
∧ 𝑦 ∈ ∪ 𝐽)
∧ 𝑜 ∈ 𝐽) → 𝐽 ∈ Top) |
12 | | uniexg 7457 |
. . . . . . . . 9
⊢ (𝐽 ∈ Top → ∪ 𝐽
∈ V) |
13 | | difexg 5190 |
. . . . . . . . 9
⊢ (∪ 𝐽
∈ V → (∪ 𝐽 ∖ 𝑜) ∈ V) |
14 | 11, 12, 13 | 3syl 18 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝐽 ∈ Top) ∧ 𝑥 ∈ ∪ 𝐽)
∧ 𝑦 ∈ ∪ 𝐽)
∧ 𝑜 ∈ 𝐽) → (∪ 𝐽
∖ 𝑜) ∈
V) |
15 | 1 | iscld 21712 |
. . . . . . . . . . 11
⊢ (𝐽 ∈ Top → (𝑑 ∈ (Clsd‘𝐽) ↔ (𝑑 ⊆ ∪ 𝐽 ∧ (∪ 𝐽
∖ 𝑑) ∈ 𝐽))) |
16 | 15 | adantl 486 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐽 ∈ Top) → (𝑑 ∈ (Clsd‘𝐽) ↔ (𝑑 ⊆ ∪ 𝐽 ∧ (∪ 𝐽
∖ 𝑑) ∈ 𝐽))) |
17 | | ist0cls.2 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐷 = (Clsd‘𝐽)) |
18 | 17 | eleq2d 2836 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑑 ∈ 𝐷 ↔ 𝑑 ∈ (Clsd‘𝐽))) |
19 | 18 | adantr 485 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐽 ∈ Top) → (𝑑 ∈ 𝐷 ↔ 𝑑 ∈ (Clsd‘𝐽))) |
20 | | simpr 489 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝐽 ∈ Top) ∧ 𝑜 ∈ 𝐽) ∧ 𝑑 = (∪ 𝐽 ∖ 𝑜)) → 𝑑 = (∪ 𝐽 ∖ 𝑜)) |
21 | | difssd 4034 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝐽 ∈ Top) ∧ 𝑜 ∈ 𝐽) ∧ 𝑑 = (∪ 𝐽 ∖ 𝑜)) → (∪ 𝐽 ∖ 𝑜) ⊆ ∪ 𝐽) |
22 | 20, 21 | eqsstrd 3926 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝐽 ∈ Top) ∧ 𝑜 ∈ 𝐽) ∧ 𝑑 = (∪ 𝐽 ∖ 𝑜)) → 𝑑 ⊆ ∪ 𝐽) |
23 | 22 | r19.29an 3210 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐽 ∈ Top) ∧ ∃𝑜 ∈ 𝐽 𝑑 = (∪ 𝐽 ∖ 𝑜)) → 𝑑 ⊆ ∪ 𝐽) |
24 | | simpr 489 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝐽 ∈ Top) ∧ 𝑑 ⊆ ∪ 𝐽)
∧ 𝑜 ∈ 𝐽) ∧ 𝑑 = (∪ 𝐽 ∖ 𝑜)) → 𝑑 = (∪ 𝐽 ∖ 𝑜)) |
25 | 24 | difeq2d 4024 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝐽 ∈ Top) ∧ 𝑑 ⊆ ∪ 𝐽)
∧ 𝑜 ∈ 𝐽) ∧ 𝑑 = (∪ 𝐽 ∖ 𝑜)) → (∪ 𝐽 ∖ 𝑑) = (∪ 𝐽 ∖ (∪ 𝐽
∖ 𝑜))) |
26 | 1 | eltopss 21592 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐽 ∈ Top ∧ 𝑜 ∈ 𝐽) → 𝑜 ⊆ ∪ 𝐽) |
27 | 26 | ad5ant24 761 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝐽 ∈ Top) ∧ 𝑑 ⊆ ∪ 𝐽)
∧ 𝑜 ∈ 𝐽) ∧ 𝑑 = (∪ 𝐽 ∖ 𝑜)) → 𝑜 ⊆ ∪ 𝐽) |
28 | | dfss4 4159 |
. . . . . . . . . . . . . . . 16
⊢ (𝑜 ⊆ ∪ 𝐽
↔ (∪ 𝐽 ∖ (∪ 𝐽 ∖ 𝑜)) = 𝑜) |
29 | 27, 28 | sylib 221 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝐽 ∈ Top) ∧ 𝑑 ⊆ ∪ 𝐽)
∧ 𝑜 ∈ 𝐽) ∧ 𝑑 = (∪ 𝐽 ∖ 𝑜)) → (∪ 𝐽 ∖ (∪ 𝐽
∖ 𝑜)) = 𝑜) |
30 | | simplr 769 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝐽 ∈ Top) ∧ 𝑑 ⊆ ∪ 𝐽)
∧ 𝑜 ∈ 𝐽) ∧ 𝑑 = (∪ 𝐽 ∖ 𝑜)) → 𝑜 ∈ 𝐽) |
31 | 29, 30 | eqeltrd 2851 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝐽 ∈ Top) ∧ 𝑑 ⊆ ∪ 𝐽)
∧ 𝑜 ∈ 𝐽) ∧ 𝑑 = (∪ 𝐽 ∖ 𝑜)) → (∪ 𝐽 ∖ (∪ 𝐽
∖ 𝑜)) ∈ 𝐽) |
32 | 25, 31 | eqeltrd 2851 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝐽 ∈ Top) ∧ 𝑑 ⊆ ∪ 𝐽)
∧ 𝑜 ∈ 𝐽) ∧ 𝑑 = (∪ 𝐽 ∖ 𝑜)) → (∪ 𝐽 ∖ 𝑑) ∈ 𝐽) |
33 | 32 | r19.29an 3210 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝐽 ∈ Top) ∧ 𝑑 ⊆ ∪ 𝐽) ∧ ∃𝑜 ∈ 𝐽 𝑑 = (∪ 𝐽 ∖ 𝑜)) → (∪ 𝐽 ∖ 𝑑) ∈ 𝐽) |
34 | | simpr 489 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝐽 ∈ Top) ∧ 𝑑 ⊆ ∪ 𝐽) ∧ (∪ 𝐽
∖ 𝑑) ∈ 𝐽) → (∪ 𝐽
∖ 𝑑) ∈ 𝐽) |
35 | | simpr 489 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝐽 ∈ Top) ∧ 𝑑 ⊆ ∪ 𝐽)
∧ (∪ 𝐽 ∖ 𝑑) ∈ 𝐽) ∧ 𝑜 = (∪ 𝐽 ∖ 𝑑)) → 𝑜 = (∪ 𝐽 ∖ 𝑑)) |
36 | 35 | difeq2d 4024 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝐽 ∈ Top) ∧ 𝑑 ⊆ ∪ 𝐽)
∧ (∪ 𝐽 ∖ 𝑑) ∈ 𝐽) ∧ 𝑜 = (∪ 𝐽 ∖ 𝑑)) → (∪ 𝐽 ∖ 𝑜) = (∪ 𝐽 ∖ (∪ 𝐽
∖ 𝑑))) |
37 | 36 | eqeq2d 2770 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝐽 ∈ Top) ∧ 𝑑 ⊆ ∪ 𝐽)
∧ (∪ 𝐽 ∖ 𝑑) ∈ 𝐽) ∧ 𝑜 = (∪ 𝐽 ∖ 𝑑)) → (𝑑 = (∪ 𝐽 ∖ 𝑜) ↔ 𝑑 = (∪ 𝐽 ∖ (∪ 𝐽
∖ 𝑑)))) |
38 | | simplr 769 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝐽 ∈ Top) ∧ 𝑑 ⊆ ∪ 𝐽) ∧ (∪ 𝐽
∖ 𝑑) ∈ 𝐽) → 𝑑 ⊆ ∪ 𝐽) |
39 | | dfss4 4159 |
. . . . . . . . . . . . . . 15
⊢ (𝑑 ⊆ ∪ 𝐽
↔ (∪ 𝐽 ∖ (∪ 𝐽 ∖ 𝑑)) = 𝑑) |
40 | 38, 39 | sylib 221 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝐽 ∈ Top) ∧ 𝑑 ⊆ ∪ 𝐽) ∧ (∪ 𝐽
∖ 𝑑) ∈ 𝐽) → (∪ 𝐽
∖ (∪ 𝐽 ∖ 𝑑)) = 𝑑) |
41 | 40 | eqcomd 2765 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝐽 ∈ Top) ∧ 𝑑 ⊆ ∪ 𝐽) ∧ (∪ 𝐽
∖ 𝑑) ∈ 𝐽) → 𝑑 = (∪ 𝐽 ∖ (∪ 𝐽
∖ 𝑑))) |
42 | 34, 37, 41 | rspcedvd 3542 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝐽 ∈ Top) ∧ 𝑑 ⊆ ∪ 𝐽) ∧ (∪ 𝐽
∖ 𝑑) ∈ 𝐽) → ∃𝑜 ∈ 𝐽 𝑑 = (∪ 𝐽 ∖ 𝑜)) |
43 | 33, 42 | impbida 801 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐽 ∈ Top) ∧ 𝑑 ⊆ ∪ 𝐽) → (∃𝑜 ∈ 𝐽 𝑑 = (∪ 𝐽 ∖ 𝑜) ↔ (∪ 𝐽 ∖ 𝑑) ∈ 𝐽)) |
44 | 23, 43 | biadanid 30320 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐽 ∈ Top) → (∃𝑜 ∈ 𝐽 𝑑 = (∪ 𝐽 ∖ 𝑜) ↔ (𝑑 ⊆ ∪ 𝐽 ∧ (∪ 𝐽
∖ 𝑑) ∈ 𝐽))) |
45 | 16, 19, 44 | 3bitr4d 315 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐽 ∈ Top) → (𝑑 ∈ 𝐷 ↔ ∃𝑜 ∈ 𝐽 𝑑 = (∪ 𝐽 ∖ 𝑜))) |
46 | 45 | ad2antrr 726 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝐽 ∈ Top) ∧ 𝑥 ∈ ∪ 𝐽) ∧ 𝑦 ∈ ∪ 𝐽) → (𝑑 ∈ 𝐷 ↔ ∃𝑜 ∈ 𝐽 𝑑 = (∪ 𝐽 ∖ 𝑜))) |
47 | | simpr 489 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝐽 ∈ Top) ∧ 𝑥 ∈ ∪ 𝐽)
∧ 𝑦 ∈ ∪ 𝐽)
∧ 𝑑 = (∪ 𝐽
∖ 𝑜)) → 𝑑 = (∪
𝐽 ∖ 𝑜)) |
48 | 47 | eleq2d 2836 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝐽 ∈ Top) ∧ 𝑥 ∈ ∪ 𝐽)
∧ 𝑦 ∈ ∪ 𝐽)
∧ 𝑑 = (∪ 𝐽
∖ 𝑜)) → (𝑥 ∈ 𝑑 ↔ 𝑥 ∈ (∪ 𝐽 ∖ 𝑜))) |
49 | | eldif 3864 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (∪ 𝐽
∖ 𝑜) ↔ (𝑥 ∈ ∪ 𝐽
∧ ¬ 𝑥 ∈ 𝑜)) |
50 | 49 | baib 540 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ∪ 𝐽
→ (𝑥 ∈ (∪ 𝐽
∖ 𝑜) ↔ ¬
𝑥 ∈ 𝑜)) |
51 | 50 | ad3antlr 731 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝐽 ∈ Top) ∧ 𝑥 ∈ ∪ 𝐽)
∧ 𝑦 ∈ ∪ 𝐽)
∧ 𝑑 = (∪ 𝐽
∖ 𝑜)) → (𝑥 ∈ (∪ 𝐽
∖ 𝑜) ↔ ¬
𝑥 ∈ 𝑜)) |
52 | 48, 51 | bitrd 282 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝐽 ∈ Top) ∧ 𝑥 ∈ ∪ 𝐽)
∧ 𝑦 ∈ ∪ 𝐽)
∧ 𝑑 = (∪ 𝐽
∖ 𝑜)) → (𝑥 ∈ 𝑑 ↔ ¬ 𝑥 ∈ 𝑜)) |
53 | 47 | eleq2d 2836 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝐽 ∈ Top) ∧ 𝑥 ∈ ∪ 𝐽)
∧ 𝑦 ∈ ∪ 𝐽)
∧ 𝑑 = (∪ 𝐽
∖ 𝑜)) → (𝑦 ∈ 𝑑 ↔ 𝑦 ∈ (∪ 𝐽 ∖ 𝑜))) |
54 | | eldif 3864 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ (∪ 𝐽
∖ 𝑜) ↔ (𝑦 ∈ ∪ 𝐽
∧ ¬ 𝑦 ∈ 𝑜)) |
55 | 54 | baib 540 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ∪ 𝐽
→ (𝑦 ∈ (∪ 𝐽
∖ 𝑜) ↔ ¬
𝑦 ∈ 𝑜)) |
56 | 55 | ad2antlr 727 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝐽 ∈ Top) ∧ 𝑥 ∈ ∪ 𝐽)
∧ 𝑦 ∈ ∪ 𝐽)
∧ 𝑑 = (∪ 𝐽
∖ 𝑜)) → (𝑦 ∈ (∪ 𝐽
∖ 𝑜) ↔ ¬
𝑦 ∈ 𝑜)) |
57 | 53, 56 | bitrd 282 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝐽 ∈ Top) ∧ 𝑥 ∈ ∪ 𝐽)
∧ 𝑦 ∈ ∪ 𝐽)
∧ 𝑑 = (∪ 𝐽
∖ 𝑜)) → (𝑦 ∈ 𝑑 ↔ ¬ 𝑦 ∈ 𝑜)) |
58 | 52, 57 | bibi12d 350 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝐽 ∈ Top) ∧ 𝑥 ∈ ∪ 𝐽)
∧ 𝑦 ∈ ∪ 𝐽)
∧ 𝑑 = (∪ 𝐽
∖ 𝑜)) → ((𝑥 ∈ 𝑑 ↔ 𝑦 ∈ 𝑑) ↔ (¬ 𝑥 ∈ 𝑜 ↔ ¬ 𝑦 ∈ 𝑜))) |
59 | | notbi 323 |
. . . . . . . . 9
⊢ ((𝑥 ∈ 𝑜 ↔ 𝑦 ∈ 𝑜) ↔ (¬ 𝑥 ∈ 𝑜 ↔ ¬ 𝑦 ∈ 𝑜)) |
60 | 58, 59 | bitr4di 293 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝐽 ∈ Top) ∧ 𝑥 ∈ ∪ 𝐽)
∧ 𝑦 ∈ ∪ 𝐽)
∧ 𝑑 = (∪ 𝐽
∖ 𝑜)) → ((𝑥 ∈ 𝑑 ↔ 𝑦 ∈ 𝑑) ↔ (𝑥 ∈ 𝑜 ↔ 𝑦 ∈ 𝑜))) |
61 | 14, 46, 60 | ralxfr2d 5272 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝐽 ∈ Top) ∧ 𝑥 ∈ ∪ 𝐽) ∧ 𝑦 ∈ ∪ 𝐽) → (∀𝑑 ∈ 𝐷 (𝑥 ∈ 𝑑 ↔ 𝑦 ∈ 𝑑) ↔ ∀𝑜 ∈ 𝐽 (𝑥 ∈ 𝑜 ↔ 𝑦 ∈ 𝑜))) |
62 | 61 | bicomd 226 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝐽 ∈ Top) ∧ 𝑥 ∈ ∪ 𝐽) ∧ 𝑦 ∈ ∪ 𝐽) → (∀𝑜 ∈ 𝐽 (𝑥 ∈ 𝑜 ↔ 𝑦 ∈ 𝑜) ↔ ∀𝑑 ∈ 𝐷 (𝑥 ∈ 𝑑 ↔ 𝑦 ∈ 𝑑))) |
63 | 62 | imbi1d 346 |
. . . . 5
⊢ ((((𝜑 ∧ 𝐽 ∈ Top) ∧ 𝑥 ∈ ∪ 𝐽) ∧ 𝑦 ∈ ∪ 𝐽) → ((∀𝑜 ∈ 𝐽 (𝑥 ∈ 𝑜 ↔ 𝑦 ∈ 𝑜) → 𝑥 = 𝑦) ↔ (∀𝑑 ∈ 𝐷 (𝑥 ∈ 𝑑 ↔ 𝑦 ∈ 𝑑) → 𝑥 = 𝑦))) |
64 | 10, 63 | raleqbidva 3333 |
. . . 4
⊢ (((𝜑 ∧ 𝐽 ∈ Top) ∧ 𝑥 ∈ ∪ 𝐽) → (∀𝑦 ∈ ∪ 𝐽(∀𝑜 ∈ 𝐽 (𝑥 ∈ 𝑜 ↔ 𝑦 ∈ 𝑜) → 𝑥 = 𝑦) ↔ ∀𝑦 ∈ 𝐵 (∀𝑑 ∈ 𝐷 (𝑥 ∈ 𝑑 ↔ 𝑦 ∈ 𝑑) → 𝑥 = 𝑦))) |
65 | 9, 64 | raleqbidva 3333 |
. . 3
⊢ ((𝜑 ∧ 𝐽 ∈ Top) → (∀𝑥 ∈ ∪ 𝐽∀𝑦 ∈ ∪ 𝐽(∀𝑜 ∈ 𝐽 (𝑥 ∈ 𝑜 ↔ 𝑦 ∈ 𝑜) → 𝑥 = 𝑦) ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (∀𝑑 ∈ 𝐷 (𝑥 ∈ 𝑑 ↔ 𝑦 ∈ 𝑑) → 𝑥 = 𝑦))) |
66 | 6, 65 | bitrd 282 |
. 2
⊢ ((𝜑 ∧ 𝐽 ∈ Top) → (𝐽 ∈ Kol2 ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (∀𝑑 ∈ 𝐷 (𝑥 ∈ 𝑑 ↔ 𝑦 ∈ 𝑑) → 𝑥 = 𝑦))) |
67 | 4, 66 | biadanid 30320 |
1
⊢ (𝜑 → (𝐽 ∈ Kol2 ↔ (𝐽 ∈ Top ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (∀𝑑 ∈ 𝐷 (𝑥 ∈ 𝑑 ↔ 𝑦 ∈ 𝑑) → 𝑥 = 𝑦)))) |