| Step | Hyp | Ref
| Expression |
| 1 | | locfincmp.1 |
. . . . . . . . . 10
⊢ 𝑋 = ∪
𝐽 |
| 2 | 1 | locfinnei 23531 |
. . . . . . . . 9
⊢ ((𝐶 ∈ (LocFin‘𝐽) ∧ 𝑥 ∈ 𝑋) → ∃𝑜 ∈ 𝐽 (𝑥 ∈ 𝑜 ∧ {𝑠 ∈ 𝐶 ∣ (𝑠 ∩ 𝑜) ≠ ∅} ∈ Fin)) |
| 3 | 2 | ralrimiva 3146 |
. . . . . . . 8
⊢ (𝐶 ∈ (LocFin‘𝐽) → ∀𝑥 ∈ 𝑋 ∃𝑜 ∈ 𝐽 (𝑥 ∈ 𝑜 ∧ {𝑠 ∈ 𝐶 ∣ (𝑠 ∩ 𝑜) ≠ ∅} ∈ Fin)) |
| 4 | 1 | cmpcov2 23398 |
. . . . . . . 8
⊢ ((𝐽 ∈ Comp ∧ ∀𝑥 ∈ 𝑋 ∃𝑜 ∈ 𝐽 (𝑥 ∈ 𝑜 ∧ {𝑠 ∈ 𝐶 ∣ (𝑠 ∩ 𝑜) ≠ ∅} ∈ Fin)) →
∃𝑐 ∈ (𝒫
𝐽 ∩ Fin)(𝑋 = ∪
𝑐 ∧ ∀𝑜 ∈ 𝑐 {𝑠 ∈ 𝐶 ∣ (𝑠 ∩ 𝑜) ≠ ∅} ∈ Fin)) |
| 5 | 3, 4 | sylan2 593 |
. . . . . . 7
⊢ ((𝐽 ∈ Comp ∧ 𝐶 ∈ (LocFin‘𝐽)) → ∃𝑐 ∈ (𝒫 𝐽 ∩ Fin)(𝑋 = ∪ 𝑐 ∧ ∀𝑜 ∈ 𝑐 {𝑠 ∈ 𝐶 ∣ (𝑠 ∩ 𝑜) ≠ ∅} ∈ Fin)) |
| 6 | | elfpw 9394 |
. . . . . . . . 9
⊢ (𝑐 ∈ (𝒫 𝐽 ∩ Fin) ↔ (𝑐 ⊆ 𝐽 ∧ 𝑐 ∈ Fin)) |
| 7 | | simplrr 778 |
. . . . . . . . . . 11
⊢ ((((𝐽 ∈ Comp ∧ 𝐶 ∈ (LocFin‘𝐽)) ∧ (𝑐 ⊆ 𝐽 ∧ 𝑐 ∈ Fin)) ∧ 𝑋 = ∪ 𝑐) → 𝑐 ∈ Fin) |
| 8 | | eldifsn 4786 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (𝐶 ∖ {∅}) ↔ (𝑥 ∈ 𝐶 ∧ 𝑥 ≠ ∅)) |
| 9 | | ineq1 4213 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑠 = 𝑥 → (𝑠 ∩ 𝑜) = (𝑥 ∩ 𝑜)) |
| 10 | 9 | neeq1d 3000 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑠 = 𝑥 → ((𝑠 ∩ 𝑜) ≠ ∅ ↔ (𝑥 ∩ 𝑜) ≠ ∅)) |
| 11 | | simplrl 777 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝐽 ∈ Comp
∧ 𝐶 ∈
(LocFin‘𝐽)) ∧
(𝑐 ⊆ 𝐽 ∧ 𝑐 ∈ Fin)) ∧ 𝑋 = ∪ 𝑐) ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝑥)) ∧ (𝑜 ∈ 𝑐 ∧ 𝑦 ∈ 𝑜)) → 𝑥 ∈ 𝐶) |
| 12 | | simplrr 778 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝐽 ∈ Comp
∧ 𝐶 ∈
(LocFin‘𝐽)) ∧
(𝑐 ⊆ 𝐽 ∧ 𝑐 ∈ Fin)) ∧ 𝑋 = ∪ 𝑐) ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝑥)) ∧ (𝑜 ∈ 𝑐 ∧ 𝑦 ∈ 𝑜)) → 𝑦 ∈ 𝑥) |
| 13 | | simprr 773 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝐽 ∈ Comp
∧ 𝐶 ∈
(LocFin‘𝐽)) ∧
(𝑐 ⊆ 𝐽 ∧ 𝑐 ∈ Fin)) ∧ 𝑋 = ∪ 𝑐) ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝑥)) ∧ (𝑜 ∈ 𝑐 ∧ 𝑦 ∈ 𝑜)) → 𝑦 ∈ 𝑜) |
| 14 | | inelcm 4465 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑦 ∈ 𝑥 ∧ 𝑦 ∈ 𝑜) → (𝑥 ∩ 𝑜) ≠ ∅) |
| 15 | 12, 13, 14 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝐽 ∈ Comp
∧ 𝐶 ∈
(LocFin‘𝐽)) ∧
(𝑐 ⊆ 𝐽 ∧ 𝑐 ∈ Fin)) ∧ 𝑋 = ∪ 𝑐) ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝑥)) ∧ (𝑜 ∈ 𝑐 ∧ 𝑦 ∈ 𝑜)) → (𝑥 ∩ 𝑜) ≠ ∅) |
| 16 | 10, 11, 15 | elrabd 3694 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝐽 ∈ Comp
∧ 𝐶 ∈
(LocFin‘𝐽)) ∧
(𝑐 ⊆ 𝐽 ∧ 𝑐 ∈ Fin)) ∧ 𝑋 = ∪ 𝑐) ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝑥)) ∧ (𝑜 ∈ 𝑐 ∧ 𝑦 ∈ 𝑜)) → 𝑥 ∈ {𝑠 ∈ 𝐶 ∣ (𝑠 ∩ 𝑜) ≠ ∅}) |
| 17 | | elunii 4912 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐶) → 𝑦 ∈ ∪ 𝐶) |
| 18 | | locfincmp.2 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 𝑌 = ∪
𝐶 |
| 19 | 17, 18 | eleqtrrdi 2852 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐶) → 𝑦 ∈ 𝑌) |
| 20 | 19 | ancoms 458 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ 𝑌) |
| 21 | 20 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝐽 ∈ Comp
∧ 𝐶 ∈
(LocFin‘𝐽)) ∧
(𝑐 ⊆ 𝐽 ∧ 𝑐 ∈ Fin)) ∧ 𝑋 = ∪ 𝑐) ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝑥)) → 𝑦 ∈ 𝑌) |
| 22 | 1, 18 | locfinbas 23530 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐶 ∈ (LocFin‘𝐽) → 𝑋 = 𝑌) |
| 23 | 22 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐽 ∈ Comp ∧ 𝐶 ∈ (LocFin‘𝐽)) → 𝑋 = 𝑌) |
| 24 | 23 | ad3antrrr 730 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝐽 ∈ Comp
∧ 𝐶 ∈
(LocFin‘𝐽)) ∧
(𝑐 ⊆ 𝐽 ∧ 𝑐 ∈ Fin)) ∧ 𝑋 = ∪ 𝑐) ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝑥)) → 𝑋 = 𝑌) |
| 25 | 21, 24 | eleqtrrd 2844 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝐽 ∈ Comp
∧ 𝐶 ∈
(LocFin‘𝐽)) ∧
(𝑐 ⊆ 𝐽 ∧ 𝑐 ∈ Fin)) ∧ 𝑋 = ∪ 𝑐) ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝑥)) → 𝑦 ∈ 𝑋) |
| 26 | | simplr 769 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝐽 ∈ Comp
∧ 𝐶 ∈
(LocFin‘𝐽)) ∧
(𝑐 ⊆ 𝐽 ∧ 𝑐 ∈ Fin)) ∧ 𝑋 = ∪ 𝑐) ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝑥)) → 𝑋 = ∪ 𝑐) |
| 27 | 25, 26 | eleqtrd 2843 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐽 ∈ Comp
∧ 𝐶 ∈
(LocFin‘𝐽)) ∧
(𝑐 ⊆ 𝐽 ∧ 𝑐 ∈ Fin)) ∧ 𝑋 = ∪ 𝑐) ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝑥)) → 𝑦 ∈ ∪ 𝑐) |
| 28 | | eluni2 4911 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 ∈ ∪ 𝑐
↔ ∃𝑜 ∈
𝑐 𝑦 ∈ 𝑜) |
| 29 | 27, 28 | sylib 218 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝐽 ∈ Comp
∧ 𝐶 ∈
(LocFin‘𝐽)) ∧
(𝑐 ⊆ 𝐽 ∧ 𝑐 ∈ Fin)) ∧ 𝑋 = ∪ 𝑐) ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝑥)) → ∃𝑜 ∈ 𝑐 𝑦 ∈ 𝑜) |
| 30 | 16, 29 | reximddv 3171 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐽 ∈ Comp
∧ 𝐶 ∈
(LocFin‘𝐽)) ∧
(𝑐 ⊆ 𝐽 ∧ 𝑐 ∈ Fin)) ∧ 𝑋 = ∪ 𝑐) ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝑥)) → ∃𝑜 ∈ 𝑐 𝑥 ∈ {𝑠 ∈ 𝐶 ∣ (𝑠 ∩ 𝑜) ≠ ∅}) |
| 31 | 30 | expr 456 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐽 ∈ Comp
∧ 𝐶 ∈
(LocFin‘𝐽)) ∧
(𝑐 ⊆ 𝐽 ∧ 𝑐 ∈ Fin)) ∧ 𝑋 = ∪ 𝑐) ∧ 𝑥 ∈ 𝐶) → (𝑦 ∈ 𝑥 → ∃𝑜 ∈ 𝑐 𝑥 ∈ {𝑠 ∈ 𝐶 ∣ (𝑠 ∩ 𝑜) ≠ ∅})) |
| 32 | 31 | exlimdv 1933 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐽 ∈ Comp
∧ 𝐶 ∈
(LocFin‘𝐽)) ∧
(𝑐 ⊆ 𝐽 ∧ 𝑐 ∈ Fin)) ∧ 𝑋 = ∪ 𝑐) ∧ 𝑥 ∈ 𝐶) → (∃𝑦 𝑦 ∈ 𝑥 → ∃𝑜 ∈ 𝑐 𝑥 ∈ {𝑠 ∈ 𝐶 ∣ (𝑠 ∩ 𝑜) ≠ ∅})) |
| 33 | | n0 4353 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ≠ ∅ ↔
∃𝑦 𝑦 ∈ 𝑥) |
| 34 | | eliun 4995 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ∪ 𝑜 ∈ 𝑐 {𝑠 ∈ 𝐶 ∣ (𝑠 ∩ 𝑜) ≠ ∅} ↔ ∃𝑜 ∈ 𝑐 𝑥 ∈ {𝑠 ∈ 𝐶 ∣ (𝑠 ∩ 𝑜) ≠ ∅}) |
| 35 | 32, 33, 34 | 3imtr4g 296 |
. . . . . . . . . . . . . 14
⊢
(((((𝐽 ∈ Comp
∧ 𝐶 ∈
(LocFin‘𝐽)) ∧
(𝑐 ⊆ 𝐽 ∧ 𝑐 ∈ Fin)) ∧ 𝑋 = ∪ 𝑐) ∧ 𝑥 ∈ 𝐶) → (𝑥 ≠ ∅ → 𝑥 ∈ ∪
𝑜 ∈ 𝑐 {𝑠 ∈ 𝐶 ∣ (𝑠 ∩ 𝑜) ≠ ∅})) |
| 36 | 35 | expimpd 453 |
. . . . . . . . . . . . 13
⊢ ((((𝐽 ∈ Comp ∧ 𝐶 ∈ (LocFin‘𝐽)) ∧ (𝑐 ⊆ 𝐽 ∧ 𝑐 ∈ Fin)) ∧ 𝑋 = ∪ 𝑐) → ((𝑥 ∈ 𝐶 ∧ 𝑥 ≠ ∅) → 𝑥 ∈ ∪
𝑜 ∈ 𝑐 {𝑠 ∈ 𝐶 ∣ (𝑠 ∩ 𝑜) ≠ ∅})) |
| 37 | 8, 36 | biimtrid 242 |
. . . . . . . . . . . 12
⊢ ((((𝐽 ∈ Comp ∧ 𝐶 ∈ (LocFin‘𝐽)) ∧ (𝑐 ⊆ 𝐽 ∧ 𝑐 ∈ Fin)) ∧ 𝑋 = ∪ 𝑐) → (𝑥 ∈ (𝐶 ∖ {∅}) → 𝑥 ∈ ∪ 𝑜 ∈ 𝑐 {𝑠 ∈ 𝐶 ∣ (𝑠 ∩ 𝑜) ≠ ∅})) |
| 38 | 37 | ssrdv 3989 |
. . . . . . . . . . 11
⊢ ((((𝐽 ∈ Comp ∧ 𝐶 ∈ (LocFin‘𝐽)) ∧ (𝑐 ⊆ 𝐽 ∧ 𝑐 ∈ Fin)) ∧ 𝑋 = ∪ 𝑐) → (𝐶 ∖ {∅}) ⊆ ∪ 𝑜 ∈ 𝑐 {𝑠 ∈ 𝐶 ∣ (𝑠 ∩ 𝑜) ≠ ∅}) |
| 39 | | iunfi 9383 |
. . . . . . . . . . . . 13
⊢ ((𝑐 ∈ Fin ∧ ∀𝑜 ∈ 𝑐 {𝑠 ∈ 𝐶 ∣ (𝑠 ∩ 𝑜) ≠ ∅} ∈ Fin) → ∪ 𝑜 ∈ 𝑐 {𝑠 ∈ 𝐶 ∣ (𝑠 ∩ 𝑜) ≠ ∅} ∈ Fin) |
| 40 | 39 | ex 412 |
. . . . . . . . . . . 12
⊢ (𝑐 ∈ Fin →
(∀𝑜 ∈ 𝑐 {𝑠 ∈ 𝐶 ∣ (𝑠 ∩ 𝑜) ≠ ∅} ∈ Fin → ∪ 𝑜 ∈ 𝑐 {𝑠 ∈ 𝐶 ∣ (𝑠 ∩ 𝑜) ≠ ∅} ∈ Fin)) |
| 41 | | ssfi 9213 |
. . . . . . . . . . . . 13
⊢
((∪ 𝑜 ∈ 𝑐 {𝑠 ∈ 𝐶 ∣ (𝑠 ∩ 𝑜) ≠ ∅} ∈ Fin ∧ (𝐶 ∖ {∅}) ⊆
∪ 𝑜 ∈ 𝑐 {𝑠 ∈ 𝐶 ∣ (𝑠 ∩ 𝑜) ≠ ∅}) → (𝐶 ∖ {∅}) ∈
Fin) |
| 42 | 41 | expcom 413 |
. . . . . . . . . . . 12
⊢ ((𝐶 ∖ {∅}) ⊆
∪ 𝑜 ∈ 𝑐 {𝑠 ∈ 𝐶 ∣ (𝑠 ∩ 𝑜) ≠ ∅} → (∪ 𝑜 ∈ 𝑐 {𝑠 ∈ 𝐶 ∣ (𝑠 ∩ 𝑜) ≠ ∅} ∈ Fin → (𝐶 ∖ {∅}) ∈
Fin)) |
| 43 | 40, 42 | sylan9 507 |
. . . . . . . . . . 11
⊢ ((𝑐 ∈ Fin ∧ (𝐶 ∖ {∅}) ⊆
∪ 𝑜 ∈ 𝑐 {𝑠 ∈ 𝐶 ∣ (𝑠 ∩ 𝑜) ≠ ∅}) → (∀𝑜 ∈ 𝑐 {𝑠 ∈ 𝐶 ∣ (𝑠 ∩ 𝑜) ≠ ∅} ∈ Fin → (𝐶 ∖ {∅}) ∈
Fin)) |
| 44 | 7, 38, 43 | syl2anc 584 |
. . . . . . . . . 10
⊢ ((((𝐽 ∈ Comp ∧ 𝐶 ∈ (LocFin‘𝐽)) ∧ (𝑐 ⊆ 𝐽 ∧ 𝑐 ∈ Fin)) ∧ 𝑋 = ∪ 𝑐) → (∀𝑜 ∈ 𝑐 {𝑠 ∈ 𝐶 ∣ (𝑠 ∩ 𝑜) ≠ ∅} ∈ Fin → (𝐶 ∖ {∅}) ∈
Fin)) |
| 45 | 44 | expimpd 453 |
. . . . . . . . 9
⊢ (((𝐽 ∈ Comp ∧ 𝐶 ∈ (LocFin‘𝐽)) ∧ (𝑐 ⊆ 𝐽 ∧ 𝑐 ∈ Fin)) → ((𝑋 = ∪ 𝑐 ∧ ∀𝑜 ∈ 𝑐 {𝑠 ∈ 𝐶 ∣ (𝑠 ∩ 𝑜) ≠ ∅} ∈ Fin) → (𝐶 ∖ {∅}) ∈
Fin)) |
| 46 | 6, 45 | sylan2b 594 |
. . . . . . . 8
⊢ (((𝐽 ∈ Comp ∧ 𝐶 ∈ (LocFin‘𝐽)) ∧ 𝑐 ∈ (𝒫 𝐽 ∩ Fin)) → ((𝑋 = ∪ 𝑐 ∧ ∀𝑜 ∈ 𝑐 {𝑠 ∈ 𝐶 ∣ (𝑠 ∩ 𝑜) ≠ ∅} ∈ Fin) → (𝐶 ∖ {∅}) ∈
Fin)) |
| 47 | 46 | rexlimdva 3155 |
. . . . . . 7
⊢ ((𝐽 ∈ Comp ∧ 𝐶 ∈ (LocFin‘𝐽)) → (∃𝑐 ∈ (𝒫 𝐽 ∩ Fin)(𝑋 = ∪ 𝑐 ∧ ∀𝑜 ∈ 𝑐 {𝑠 ∈ 𝐶 ∣ (𝑠 ∩ 𝑜) ≠ ∅} ∈ Fin) → (𝐶 ∖ {∅}) ∈
Fin)) |
| 48 | 5, 47 | mpd 15 |
. . . . . 6
⊢ ((𝐽 ∈ Comp ∧ 𝐶 ∈ (LocFin‘𝐽)) → (𝐶 ∖ {∅}) ∈
Fin) |
| 49 | | snfi 9083 |
. . . . . 6
⊢ {∅}
∈ Fin |
| 50 | | unfi 9211 |
. . . . . 6
⊢ (((𝐶 ∖ {∅}) ∈ Fin
∧ {∅} ∈ Fin) → ((𝐶 ∖ {∅}) ∪ {∅}) ∈
Fin) |
| 51 | 48, 49, 50 | sylancl 586 |
. . . . 5
⊢ ((𝐽 ∈ Comp ∧ 𝐶 ∈ (LocFin‘𝐽)) → ((𝐶 ∖ {∅}) ∪ {∅}) ∈
Fin) |
| 52 | | ssun1 4178 |
. . . . . 6
⊢ 𝐶 ⊆ (𝐶 ∪ {∅}) |
| 53 | | undif1 4476 |
. . . . . 6
⊢ ((𝐶 ∖ {∅}) ∪
{∅}) = (𝐶 ∪
{∅}) |
| 54 | 52, 53 | sseqtrri 4033 |
. . . . 5
⊢ 𝐶 ⊆ ((𝐶 ∖ {∅}) ∪
{∅}) |
| 55 | | ssfi 9213 |
. . . . 5
⊢ ((((𝐶 ∖ {∅}) ∪
{∅}) ∈ Fin ∧ 𝐶 ⊆ ((𝐶 ∖ {∅}) ∪ {∅})) →
𝐶 ∈
Fin) |
| 56 | 51, 54, 55 | sylancl 586 |
. . . 4
⊢ ((𝐽 ∈ Comp ∧ 𝐶 ∈ (LocFin‘𝐽)) → 𝐶 ∈ Fin) |
| 57 | 56, 23 | jca 511 |
. . 3
⊢ ((𝐽 ∈ Comp ∧ 𝐶 ∈ (LocFin‘𝐽)) → (𝐶 ∈ Fin ∧ 𝑋 = 𝑌)) |
| 58 | 57 | ex 412 |
. 2
⊢ (𝐽 ∈ Comp → (𝐶 ∈ (LocFin‘𝐽) → (𝐶 ∈ Fin ∧ 𝑋 = 𝑌))) |
| 59 | | cmptop 23403 |
. . 3
⊢ (𝐽 ∈ Comp → 𝐽 ∈ Top) |
| 60 | 1, 18 | finlocfin 23528 |
. . . 4
⊢ ((𝐽 ∈ Top ∧ 𝐶 ∈ Fin ∧ 𝑋 = 𝑌) → 𝐶 ∈ (LocFin‘𝐽)) |
| 61 | 60 | 3expib 1123 |
. . 3
⊢ (𝐽 ∈ Top → ((𝐶 ∈ Fin ∧ 𝑋 = 𝑌) → 𝐶 ∈ (LocFin‘𝐽))) |
| 62 | 59, 61 | syl 17 |
. 2
⊢ (𝐽 ∈ Comp → ((𝐶 ∈ Fin ∧ 𝑋 = 𝑌) → 𝐶 ∈ (LocFin‘𝐽))) |
| 63 | 58, 62 | impbid 212 |
1
⊢ (𝐽 ∈ Comp → (𝐶 ∈ (LocFin‘𝐽) ↔ (𝐶 ∈ Fin ∧ 𝑋 = 𝑌))) |