Metamath Proof Explorer

Theorem fiunelros

Description: A ring of sets is closed under finite union. (Contributed by Thierry Arnoux, 19-Jul-2020)

Ref Expression
Hypotheses isros.1 ⊢ 𝑄 = { 𝑠 ∈ 𝒫 𝒫 𝑂 ∣ ( ∅ ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑠 ( ( 𝑥 ∪ 𝑦 ) ∈ 𝑠 ∧ ( 𝑥 ∖ 𝑦 ) ∈ 𝑠 ) ) }
fiunelros.1 ⊢ ( 𝜑 → 𝑆 ∈ 𝑄 )
fiunelros.2 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
fiunelros.3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ..^ 𝑁 ) ) → 𝐵 ∈ 𝑆 )
Assertion fiunelros ( 𝜑 → ∪ 𝑘 ∈ ( 1 ..^ 𝑁 ) 𝐵 ∈ 𝑆 )

Proof

Step Hyp Ref Expression
1 isros.1 ⊢ 𝑄 = { 𝑠 ∈ 𝒫 𝒫 𝑂 ∣ ( ∅ ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑠 ( ( 𝑥 ∪ 𝑦 ) ∈ 𝑠 ∧ ( 𝑥 ∖ 𝑦 ) ∈ 𝑠 ) ) }
2 fiunelros.1 ⊢ ( 𝜑 → 𝑆 ∈ 𝑄 )
3 fiunelros.2 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
4 fiunelros.3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ..^ 𝑁 ) ) → 𝐵 ∈ 𝑆 )
5 simpr ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ℕ ) → 𝑁 ∈ ℕ )
6 5 nnred ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ℕ ) → 𝑁 ∈ ℝ )
7 6 leidd ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ℕ ) → 𝑁 ≤ 𝑁 )
8 breq1 ⊢ ( 𝑛 = 1 → ( 𝑛 ≤ 𝑁 ↔ 1 ≤ 𝑁 ) )
9 oveq2 ⊢ ( 𝑛 = 1 → ( 1 ..^ 𝑛 ) = ( 1 ..^ 1 ) )
10 9 iuneq1d ⊢ ( 𝑛 = 1 → ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 = ∪ 𝑘 ∈ ( 1 ..^ 1 ) 𝐵 )
11 10 eleq1d ⊢ ( 𝑛 = 1 → ( ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 ∈ 𝑆 ↔ ∪ 𝑘 ∈ ( 1 ..^ 1 ) 𝐵 ∈ 𝑆 ) )
12 8 11 imbi12d ⊢ ( 𝑛 = 1 → ( ( 𝑛 ≤ 𝑁 → ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 ∈ 𝑆 ) ↔ ( 1 ≤ 𝑁 → ∪ 𝑘 ∈ ( 1 ..^ 1 ) 𝐵 ∈ 𝑆 ) ) )
13 breq1 ⊢ ( 𝑛 = 𝑖 → ( 𝑛 ≤ 𝑁 ↔ 𝑖 ≤ 𝑁 ) )
14 oveq2 ⊢ ( 𝑛 = 𝑖 → ( 1 ..^ 𝑛 ) = ( 1 ..^ 𝑖 ) )
15 14 iuneq1d ⊢ ( 𝑛 = 𝑖 → ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 = ∪ 𝑘 ∈ ( 1 ..^ 𝑖 ) 𝐵 )
16 15 eleq1d ⊢ ( 𝑛 = 𝑖 → ( ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 ∈ 𝑆 ↔ ∪ 𝑘 ∈ ( 1 ..^ 𝑖 ) 𝐵 ∈ 𝑆 ) )
17 13 16 imbi12d ⊢ ( 𝑛 = 𝑖 → ( ( 𝑛 ≤ 𝑁 → ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 ∈ 𝑆 ) ↔ ( 𝑖 ≤ 𝑁 → ∪ 𝑘 ∈ ( 1 ..^ 𝑖 ) 𝐵 ∈ 𝑆 ) ) )
18 breq1 ⊢ ( 𝑛 = ( 𝑖 + 1 ) → ( 𝑛 ≤ 𝑁 ↔ ( 𝑖 + 1 ) ≤ 𝑁 ) )
19 oveq2 ⊢ ( 𝑛 = ( 𝑖 + 1 ) → ( 1 ..^ 𝑛 ) = ( 1 ..^ ( 𝑖 + 1 ) ) )
20 19 iuneq1d ⊢ ( 𝑛 = ( 𝑖 + 1 ) → ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 = ∪ 𝑘 ∈ ( 1 ..^ ( 𝑖 + 1 ) ) 𝐵 )
21 20 eleq1d ⊢ ( 𝑛 = ( 𝑖 + 1 ) → ( ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 ∈ 𝑆 ↔ ∪ 𝑘 ∈ ( 1 ..^ ( 𝑖 + 1 ) ) 𝐵 ∈ 𝑆 ) )
22 18 21 imbi12d ⊢ ( 𝑛 = ( 𝑖 + 1 ) → ( ( 𝑛 ≤ 𝑁 → ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 ∈ 𝑆 ) ↔ ( ( 𝑖 + 1 ) ≤ 𝑁 → ∪ 𝑘 ∈ ( 1 ..^ ( 𝑖 + 1 ) ) 𝐵 ∈ 𝑆 ) ) )
23 breq1 ⊢ ( 𝑛 = 𝑁 → ( 𝑛 ≤ 𝑁 ↔ 𝑁 ≤ 𝑁 ) )
24 oveq2 ⊢ ( 𝑛 = 𝑁 → ( 1 ..^ 𝑛 ) = ( 1 ..^ 𝑁 ) )
25 24 iuneq1d ⊢ ( 𝑛 = 𝑁 → ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 = ∪ 𝑘 ∈ ( 1 ..^ 𝑁 ) 𝐵 )
26 25 eleq1d ⊢ ( 𝑛 = 𝑁 → ( ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 ∈ 𝑆 ↔ ∪ 𝑘 ∈ ( 1 ..^ 𝑁 ) 𝐵 ∈ 𝑆 ) )
27 23 26 imbi12d ⊢ ( 𝑛 = 𝑁 → ( ( 𝑛 ≤ 𝑁 → ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 ∈ 𝑆 ) ↔ ( 𝑁 ≤ 𝑁 → ∪ 𝑘 ∈ ( 1 ..^ 𝑁 ) 𝐵 ∈ 𝑆 ) ) )
28 fzo0 ⊢ ( 1 ..^ 1 ) = ∅
29 iuneq1 ⊢ ( ( 1 ..^ 1 ) = ∅ → ∪ 𝑘 ∈ ( 1 ..^ 1 ) 𝐵 = ∪ 𝑘 ∈ ∅ 𝐵 )
30 28 29 ax-mp ⊢ ∪ 𝑘 ∈ ( 1 ..^ 1 ) 𝐵 = ∪ 𝑘 ∈ ∅ 𝐵
31 0iun ⊢ ∪ 𝑘 ∈ ∅ 𝐵 = ∅
32 30 31 eqtri ⊢ ∪ 𝑘 ∈ ( 1 ..^ 1 ) 𝐵 = ∅
33 1 0elros ⊢ ( 𝑆 ∈ 𝑄 → ∅ ∈ 𝑆 )
34 2 33 syl ⊢ ( 𝜑 → ∅ ∈ 𝑆 )
35 32 34 eqeltrid ⊢ ( 𝜑 → ∪ 𝑘 ∈ ( 1 ..^ 1 ) 𝐵 ∈ 𝑆 )
36 35 a1d ⊢ ( 𝜑 → ( 1 ≤ 𝑁 → ∪ 𝑘 ∈ ( 1 ..^ 1 ) 𝐵 ∈ 𝑆 ) )
37 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) ∧ ( 𝑖 ≤ 𝑁 → ∪ 𝑘 ∈ ( 1 ..^ 𝑖 ) 𝐵 ∈ 𝑆 ) ) ∧ ( 𝑖 + 1 ) ≤ 𝑁 ) → 𝑖 ∈ ℕ )
38 fzosplitsn ⊢ ( 𝑖 ∈ ( ℤ≥ ‘ 1 ) → ( 1 ..^ ( 𝑖 + 1 ) ) = ( ( 1 ..^ 𝑖 ) ∪ { 𝑖 } ) )
39 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
40 38 39 eleq2s ⊢ ( 𝑖 ∈ ℕ → ( 1 ..^ ( 𝑖 + 1 ) ) = ( ( 1 ..^ 𝑖 ) ∪ { 𝑖 } ) )
41 40 iuneq1d ⊢ ( 𝑖 ∈ ℕ → ∪ 𝑘 ∈ ( 1 ..^ ( 𝑖 + 1 ) ) 𝐵 = ∪ 𝑘 ∈ ( ( 1 ..^ 𝑖 ) ∪ { 𝑖 } ) 𝐵 )
42 37 41 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) ∧ ( 𝑖 ≤ 𝑁 → ∪ 𝑘 ∈ ( 1 ..^ 𝑖 ) 𝐵 ∈ 𝑆 ) ) ∧ ( 𝑖 + 1 ) ≤ 𝑁 ) → ∪ 𝑘 ∈ ( 1 ..^ ( 𝑖 + 1 ) ) 𝐵 = ∪ 𝑘 ∈ ( ( 1 ..^ 𝑖 ) ∪ { 𝑖 } ) 𝐵 )
43 iunxun ⊢ ∪ 𝑘 ∈ ( ( 1 ..^ 𝑖 ) ∪ { 𝑖 } ) 𝐵 = ( ∪ 𝑘 ∈ ( 1 ..^ 𝑖 ) 𝐵 ∪ ∪ 𝑘 ∈ { 𝑖 } 𝐵 )
44 42 43 eqtrdi ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) ∧ ( 𝑖 ≤ 𝑁 → ∪ 𝑘 ∈ ( 1 ..^ 𝑖 ) 𝐵 ∈ 𝑆 ) ) ∧ ( 𝑖 + 1 ) ≤ 𝑁 ) → ∪ 𝑘 ∈ ( 1 ..^ ( 𝑖 + 1 ) ) 𝐵 = ( ∪ 𝑘 ∈ ( 1 ..^ 𝑖 ) 𝐵 ∪ ∪ 𝑘 ∈ { 𝑖 } 𝐵 ) )
45 2 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) ∧ ( 𝑖 ≤ 𝑁 → ∪ 𝑘 ∈ ( 1 ..^ 𝑖 ) 𝐵 ∈ 𝑆 ) ) ∧ ( 𝑖 + 1 ) ≤ 𝑁 ) → 𝑆 ∈ 𝑄 )
46 37 nnred ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) ∧ ( 𝑖 ≤ 𝑁 → ∪ 𝑘 ∈ ( 1 ..^ 𝑖 ) 𝐵 ∈ 𝑆 ) ) ∧ ( 𝑖 + 1 ) ≤ 𝑁 ) → 𝑖 ∈ ℝ )
47 3 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) ∧ ( 𝑖 ≤ 𝑁 → ∪ 𝑘 ∈ ( 1 ..^ 𝑖 ) 𝐵 ∈ 𝑆 ) ) ∧ ( 𝑖 + 1 ) ≤ 𝑁 ) → 𝑁 ∈ ℕ )
48 47 nnred ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) ∧ ( 𝑖 ≤ 𝑁 → ∪ 𝑘 ∈ ( 1 ..^ 𝑖 ) 𝐵 ∈ 𝑆 ) ) ∧ ( 𝑖 + 1 ) ≤ 𝑁 ) → 𝑁 ∈ ℝ )
49 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) ∧ ( 𝑖 ≤ 𝑁 → ∪ 𝑘 ∈ ( 1 ..^ 𝑖 ) 𝐵 ∈ 𝑆 ) ) ∧ ( 𝑖 + 1 ) ≤ 𝑁 ) → ( 𝑖 + 1 ) ≤ 𝑁 )
50 nnltp1le ⊢ ( ( 𝑖 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 𝑖 < 𝑁 ↔ ( 𝑖 + 1 ) ≤ 𝑁 ) )
51 37 47 50 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) ∧ ( 𝑖 ≤ 𝑁 → ∪ 𝑘 ∈ ( 1 ..^ 𝑖 ) 𝐵 ∈ 𝑆 ) ) ∧ ( 𝑖 + 1 ) ≤ 𝑁 ) → ( 𝑖 < 𝑁 ↔ ( 𝑖 + 1 ) ≤ 𝑁 ) )
52 49 51 mpbird ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) ∧ ( 𝑖 ≤ 𝑁 → ∪ 𝑘 ∈ ( 1 ..^ 𝑖 ) 𝐵 ∈ 𝑆 ) ) ∧ ( 𝑖 + 1 ) ≤ 𝑁 ) → 𝑖 < 𝑁 )
53 46 48 52 ltled ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) ∧ ( 𝑖 ≤ 𝑁 → ∪ 𝑘 ∈ ( 1 ..^ 𝑖 ) 𝐵 ∈ 𝑆 ) ) ∧ ( 𝑖 + 1 ) ≤ 𝑁 ) → 𝑖 ≤ 𝑁 )
54 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) ∧ ( 𝑖 ≤ 𝑁 → ∪ 𝑘 ∈ ( 1 ..^ 𝑖 ) 𝐵 ∈ 𝑆 ) ) ∧ ( 𝑖 + 1 ) ≤ 𝑁 ) → ( 𝑖 ≤ 𝑁 → ∪ 𝑘 ∈ ( 1 ..^ 𝑖 ) 𝐵 ∈ 𝑆 ) )
55 53 54 mpd ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) ∧ ( 𝑖 ≤ 𝑁 → ∪ 𝑘 ∈ ( 1 ..^ 𝑖 ) 𝐵 ∈ 𝑆 ) ) ∧ ( 𝑖 + 1 ) ≤ 𝑁 ) → ∪ 𝑘 ∈ ( 1 ..^ 𝑖 ) 𝐵 ∈ 𝑆 )
56 nfcsb1v ⊢ Ⅎ 𝑘 ⦋ 𝑖 / 𝑘 ⦌ 𝐵
57 csbeq1a ⊢ ( 𝑘 = 𝑖 → 𝐵 = ⦋ 𝑖 / 𝑘 ⦌ 𝐵 )
58 56 57 iunxsngf ⊢ ( 𝑖 ∈ ℕ → ∪ 𝑘 ∈ { 𝑖 } 𝐵 = ⦋ 𝑖 / 𝑘 ⦌ 𝐵 )
59 37 58 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) ∧ ( 𝑖 ≤ 𝑁 → ∪ 𝑘 ∈ ( 1 ..^ 𝑖 ) 𝐵 ∈ 𝑆 ) ) ∧ ( 𝑖 + 1 ) ≤ 𝑁 ) → ∪ 𝑘 ∈ { 𝑖 } 𝐵 = ⦋ 𝑖 / 𝑘 ⦌ 𝐵 )
60 simplll ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) ∧ ( 𝑖 ≤ 𝑁 → ∪ 𝑘 ∈ ( 1 ..^ 𝑖 ) 𝐵 ∈ 𝑆 ) ) ∧ ( 𝑖 + 1 ) ≤ 𝑁 ) → 𝜑 )
61 elfzo1 ⊢ ( 𝑖 ∈ ( 1 ..^ 𝑁 ) ↔ ( 𝑖 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑖 < 𝑁 ) )
62 37 47 52 61 syl3anbrc ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) ∧ ( 𝑖 ≤ 𝑁 → ∪ 𝑘 ∈ ( 1 ..^ 𝑖 ) 𝐵 ∈ 𝑆 ) ) ∧ ( 𝑖 + 1 ) ≤ 𝑁 ) → 𝑖 ∈ ( 1 ..^ 𝑁 ) )
63 nfv ⊢ Ⅎ 𝑘 ( 𝜑 ∧ 𝑖 ∈ ( 1 ..^ 𝑁 ) )
64 nfcv ⊢ Ⅎ 𝑘 𝑆
65 56 64 nfel ⊢ Ⅎ 𝑘 ⦋ 𝑖 / 𝑘 ⦌ 𝐵 ∈ 𝑆
66 63 65 nfim ⊢ Ⅎ 𝑘 ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ..^ 𝑁 ) ) → ⦋ 𝑖 / 𝑘 ⦌ 𝐵 ∈ 𝑆 )
67 eleq1w ⊢ ( 𝑘 = 𝑖 → ( 𝑘 ∈ ( 1 ..^ 𝑁 ) ↔ 𝑖 ∈ ( 1 ..^ 𝑁 ) ) )
68 67 anbi2d ⊢ ( 𝑘 = 𝑖 → ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ..^ 𝑁 ) ) ↔ ( 𝜑 ∧ 𝑖 ∈ ( 1 ..^ 𝑁 ) ) ) )
69 57 eleq1d ⊢ ( 𝑘 = 𝑖 → ( 𝐵 ∈ 𝑆 ↔ ⦋ 𝑖 / 𝑘 ⦌ 𝐵 ∈ 𝑆 ) )
70 68 69 imbi12d ⊢ ( 𝑘 = 𝑖 → ( ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ..^ 𝑁 ) ) → 𝐵 ∈ 𝑆 ) ↔ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ..^ 𝑁 ) ) → ⦋ 𝑖 / 𝑘 ⦌ 𝐵 ∈ 𝑆 ) ) )
71 66 70 4 chvarfv ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ..^ 𝑁 ) ) → ⦋ 𝑖 / 𝑘 ⦌ 𝐵 ∈ 𝑆 )
72 60 62 71 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) ∧ ( 𝑖 ≤ 𝑁 → ∪ 𝑘 ∈ ( 1 ..^ 𝑖 ) 𝐵 ∈ 𝑆 ) ) ∧ ( 𝑖 + 1 ) ≤ 𝑁 ) → ⦋ 𝑖 / 𝑘 ⦌ 𝐵 ∈ 𝑆 )
73 59 72 eqeltrd ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) ∧ ( 𝑖 ≤ 𝑁 → ∪ 𝑘 ∈ ( 1 ..^ 𝑖 ) 𝐵 ∈ 𝑆 ) ) ∧ ( 𝑖 + 1 ) ≤ 𝑁 ) → ∪ 𝑘 ∈ { 𝑖 } 𝐵 ∈ 𝑆 )
74 1 unelros ⊢ ( ( 𝑆 ∈ 𝑄 ∧ ∪ 𝑘 ∈ ( 1 ..^ 𝑖 ) 𝐵 ∈ 𝑆 ∧ ∪ 𝑘 ∈ { 𝑖 } 𝐵 ∈ 𝑆 ) → ( ∪ 𝑘 ∈ ( 1 ..^ 𝑖 ) 𝐵 ∪ ∪ 𝑘 ∈ { 𝑖 } 𝐵 ) ∈ 𝑆 )
75 45 55 73 74 syl3anc ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) ∧ ( 𝑖 ≤ 𝑁 → ∪ 𝑘 ∈ ( 1 ..^ 𝑖 ) 𝐵 ∈ 𝑆 ) ) ∧ ( 𝑖 + 1 ) ≤ 𝑁 ) → ( ∪ 𝑘 ∈ ( 1 ..^ 𝑖 ) 𝐵 ∪ ∪ 𝑘 ∈ { 𝑖 } 𝐵 ) ∈ 𝑆 )
76 44 75 eqeltrd ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) ∧ ( 𝑖 ≤ 𝑁 → ∪ 𝑘 ∈ ( 1 ..^ 𝑖 ) 𝐵 ∈ 𝑆 ) ) ∧ ( 𝑖 + 1 ) ≤ 𝑁 ) → ∪ 𝑘 ∈ ( 1 ..^ ( 𝑖 + 1 ) ) 𝐵 ∈ 𝑆 )
77 76 ex ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) ∧ ( 𝑖 ≤ 𝑁 → ∪ 𝑘 ∈ ( 1 ..^ 𝑖 ) 𝐵 ∈ 𝑆 ) ) → ( ( 𝑖 + 1 ) ≤ 𝑁 → ∪ 𝑘 ∈ ( 1 ..^ ( 𝑖 + 1 ) ) 𝐵 ∈ 𝑆 ) )
78 12 17 22 27 36 77 nnindd ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ℕ ) → ( 𝑁 ≤ 𝑁 → ∪ 𝑘 ∈ ( 1 ..^ 𝑁 ) 𝐵 ∈ 𝑆 ) )
79 7 78 mpd ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ℕ ) → ∪ 𝑘 ∈ ( 1 ..^ 𝑁 ) 𝐵 ∈ 𝑆 )
80 3 79 mpdan ⊢ ( 𝜑 → ∪ 𝑘 ∈ ( 1 ..^ 𝑁 ) 𝐵 ∈ 𝑆 )