Metamath Proof Explorer

Theorem nolesgn2o

Description: Given A less-than or equal to B , equal to B up to X , and A ( X ) = 2o , then B ( X ) = 2o . (Contributed by Scott Fenton, 6-Dec-2021)

Ref Expression
Assertion nolesgn2o ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ ( 𝐴 ‘ 𝑋 ) = 2o ) ∧ ¬ 𝐵 <s 𝐴 ) → ( 𝐵 ‘ 𝑋 ) = 2o )

Proof

Step Hyp Ref Expression
1 simpl2 ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ ( 𝐴 ‘ 𝑋 ) = 2o ) ) → 𝐵 ∈ No )
2 nofv ⊢ ( 𝐵 ∈ No → ( ( 𝐵 ‘ 𝑋 ) = ∅ ∨ ( 𝐵 ‘ 𝑋 ) = 1o ∨ ( 𝐵 ‘ 𝑋 ) = 2o ) )
3 1 2 syl ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ ( 𝐴 ‘ 𝑋 ) = 2o ) ) → ( ( 𝐵 ‘ 𝑋 ) = ∅ ∨ ( 𝐵 ‘ 𝑋 ) = 1o ∨ ( 𝐵 ‘ 𝑋 ) = 2o ) )
4 3orel3 ⊢ ( ¬ ( 𝐵 ‘ 𝑋 ) = 2o → ( ( ( 𝐵 ‘ 𝑋 ) = ∅ ∨ ( 𝐵 ‘ 𝑋 ) = 1o ∨ ( 𝐵 ‘ 𝑋 ) = 2o ) → ( ( 𝐵 ‘ 𝑋 ) = ∅ ∨ ( 𝐵 ‘ 𝑋 ) = 1o ) ) )
5 3 4 syl5com ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ ( 𝐴 ‘ 𝑋 ) = 2o ) ) → ( ¬ ( 𝐵 ‘ 𝑋 ) = 2o → ( ( 𝐵 ‘ 𝑋 ) = ∅ ∨ ( 𝐵 ‘ 𝑋 ) = 1o ) ) )
6 simp13 ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ ( 𝐴 ‘ 𝑋 ) = 2o ) ∧ ( ( 𝐵 ‘ 𝑋 ) = ∅ ∨ ( 𝐵 ‘ 𝑋 ) = 1o ) ) → 𝑋 ∈ On )
7 fveq1 ⊢ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) → ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑦 ) = ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑦 ) )
8 7 eqcomd ⊢ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) → ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑦 ) = ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑦 ) )
9 8 adantr ⊢ ( ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) → ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑦 ) = ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑦 ) )
10 simpr ⊢ ( ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) → 𝑦 ∈ 𝑋 )
11 10 fvresd ⊢ ( ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) → ( ( 𝐵 ↾ 𝑋 ) ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) )
12 10 fvresd ⊢ ( ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) → ( ( 𝐴 ↾ 𝑋 ) ‘ 𝑦 ) = ( 𝐴 ‘ 𝑦 ) )
13 9 11 12 3eqtr3d ⊢ ( ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) → ( 𝐵 ‘ 𝑦 ) = ( 𝐴 ‘ 𝑦 ) )
14 13 ralrimiva ⊢ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) → ∀ 𝑦 ∈ 𝑋 ( 𝐵 ‘ 𝑦 ) = ( 𝐴 ‘ 𝑦 ) )
15 14 adantr ⊢ ( ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ ( 𝐴 ‘ 𝑋 ) = 2o ) → ∀ 𝑦 ∈ 𝑋 ( 𝐵 ‘ 𝑦 ) = ( 𝐴 ‘ 𝑦 ) )
16 15 3ad2ant2 ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ ( 𝐴 ‘ 𝑋 ) = 2o ) ∧ ( ( 𝐵 ‘ 𝑋 ) = ∅ ∨ ( 𝐵 ‘ 𝑋 ) = 1o ) ) → ∀ 𝑦 ∈ 𝑋 ( 𝐵 ‘ 𝑦 ) = ( 𝐴 ‘ 𝑦 ) )
17 simprr ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ ( 𝐴 ‘ 𝑋 ) = 2o ) ) → ( 𝐴 ‘ 𝑋 ) = 2o )
18 17 a1d ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ ( 𝐴 ‘ 𝑋 ) = 2o ) ) → ( ( 𝐵 ‘ 𝑋 ) = ∅ → ( 𝐴 ‘ 𝑋 ) = 2o ) )
19 18 ancld ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ ( 𝐴 ‘ 𝑋 ) = 2o ) ) → ( ( 𝐵 ‘ 𝑋 ) = ∅ → ( ( 𝐵 ‘ 𝑋 ) = ∅ ∧ ( 𝐴 ‘ 𝑋 ) = 2o ) ) )
20 17 a1d ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ ( 𝐴 ‘ 𝑋 ) = 2o ) ) → ( ( 𝐵 ‘ 𝑋 ) = 1o → ( 𝐴 ‘ 𝑋 ) = 2o ) )
21 20 ancld ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ ( 𝐴 ‘ 𝑋 ) = 2o ) ) → ( ( 𝐵 ‘ 𝑋 ) = 1o → ( ( 𝐵 ‘ 𝑋 ) = 1o ∧ ( 𝐴 ‘ 𝑋 ) = 2o ) ) )
22 19 21 orim12d ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ ( 𝐴 ‘ 𝑋 ) = 2o ) ) → ( ( ( 𝐵 ‘ 𝑋 ) = ∅ ∨ ( 𝐵 ‘ 𝑋 ) = 1o ) → ( ( ( 𝐵 ‘ 𝑋 ) = ∅ ∧ ( 𝐴 ‘ 𝑋 ) = 2o ) ∨ ( ( 𝐵 ‘ 𝑋 ) = 1o ∧ ( 𝐴 ‘ 𝑋 ) = 2o ) ) ) )
23 22 3impia ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ ( 𝐴 ‘ 𝑋 ) = 2o ) ∧ ( ( 𝐵 ‘ 𝑋 ) = ∅ ∨ ( 𝐵 ‘ 𝑋 ) = 1o ) ) → ( ( ( 𝐵 ‘ 𝑋 ) = ∅ ∧ ( 𝐴 ‘ 𝑋 ) = 2o ) ∨ ( ( 𝐵 ‘ 𝑋 ) = 1o ∧ ( 𝐴 ‘ 𝑋 ) = 2o ) ) )
24 3mix3 ⊢ ( ( ( 𝐵 ‘ 𝑋 ) = ∅ ∧ ( 𝐴 ‘ 𝑋 ) = 2o ) → ( ( ( 𝐵 ‘ 𝑋 ) = 1o ∧ ( 𝐴 ‘ 𝑋 ) = ∅ ) ∨ ( ( 𝐵 ‘ 𝑋 ) = 1o ∧ ( 𝐴 ‘ 𝑋 ) = 2o ) ∨ ( ( 𝐵 ‘ 𝑋 ) = ∅ ∧ ( 𝐴 ‘ 𝑋 ) = 2o ) ) )
25 3mix2 ⊢ ( ( ( 𝐵 ‘ 𝑋 ) = 1o ∧ ( 𝐴 ‘ 𝑋 ) = 2o ) → ( ( ( 𝐵 ‘ 𝑋 ) = 1o ∧ ( 𝐴 ‘ 𝑋 ) = ∅ ) ∨ ( ( 𝐵 ‘ 𝑋 ) = 1o ∧ ( 𝐴 ‘ 𝑋 ) = 2o ) ∨ ( ( 𝐵 ‘ 𝑋 ) = ∅ ∧ ( 𝐴 ‘ 𝑋 ) = 2o ) ) )
26 24 25 jaoi ⊢ ( ( ( ( 𝐵 ‘ 𝑋 ) = ∅ ∧ ( 𝐴 ‘ 𝑋 ) = 2o ) ∨ ( ( 𝐵 ‘ 𝑋 ) = 1o ∧ ( 𝐴 ‘ 𝑋 ) = 2o ) ) → ( ( ( 𝐵 ‘ 𝑋 ) = 1o ∧ ( 𝐴 ‘ 𝑋 ) = ∅ ) ∨ ( ( 𝐵 ‘ 𝑋 ) = 1o ∧ ( 𝐴 ‘ 𝑋 ) = 2o ) ∨ ( ( 𝐵 ‘ 𝑋 ) = ∅ ∧ ( 𝐴 ‘ 𝑋 ) = 2o ) ) )
27 23 26 syl ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ ( 𝐴 ‘ 𝑋 ) = 2o ) ∧ ( ( 𝐵 ‘ 𝑋 ) = ∅ ∨ ( 𝐵 ‘ 𝑋 ) = 1o ) ) → ( ( ( 𝐵 ‘ 𝑋 ) = 1o ∧ ( 𝐴 ‘ 𝑋 ) = ∅ ) ∨ ( ( 𝐵 ‘ 𝑋 ) = 1o ∧ ( 𝐴 ‘ 𝑋 ) = 2o ) ∨ ( ( 𝐵 ‘ 𝑋 ) = ∅ ∧ ( 𝐴 ‘ 𝑋 ) = 2o ) ) )
28 fvex ⊢ ( 𝐵 ‘ 𝑋 ) ∈ V
29 fvex ⊢ ( 𝐴 ‘ 𝑋 ) ∈ V
30 28 29 brtp ⊢ ( ( 𝐵 ‘ 𝑋 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐴 ‘ 𝑋 ) ↔ ( ( ( 𝐵 ‘ 𝑋 ) = 1o ∧ ( 𝐴 ‘ 𝑋 ) = ∅ ) ∨ ( ( 𝐵 ‘ 𝑋 ) = 1o ∧ ( 𝐴 ‘ 𝑋 ) = 2o ) ∨ ( ( 𝐵 ‘ 𝑋 ) = ∅ ∧ ( 𝐴 ‘ 𝑋 ) = 2o ) ) )
31 27 30 sylibr ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ ( 𝐴 ‘ 𝑋 ) = 2o ) ∧ ( ( 𝐵 ‘ 𝑋 ) = ∅ ∨ ( 𝐵 ‘ 𝑋 ) = 1o ) ) → ( 𝐵 ‘ 𝑋 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐴 ‘ 𝑋 ) )
32 raleq ⊢ ( 𝑥 = 𝑋 → ( ∀ 𝑦 ∈ 𝑥 ( 𝐵 ‘ 𝑦 ) = ( 𝐴 ‘ 𝑦 ) ↔ ∀ 𝑦 ∈ 𝑋 ( 𝐵 ‘ 𝑦 ) = ( 𝐴 ‘ 𝑦 ) ) )
33 fveq2 ⊢ ( 𝑥 = 𝑋 → ( 𝐵 ‘ 𝑥 ) = ( 𝐵 ‘ 𝑋 ) )
34 fveq2 ⊢ ( 𝑥 = 𝑋 → ( 𝐴 ‘ 𝑥 ) = ( 𝐴 ‘ 𝑋 ) )
35 33 34 breq12d ⊢ ( 𝑥 = 𝑋 → ( ( 𝐵 ‘ 𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐴 ‘ 𝑥 ) ↔ ( 𝐵 ‘ 𝑋 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐴 ‘ 𝑋 ) ) )
36 32 35 anbi12d ⊢ ( 𝑥 = 𝑋 → ( ( ∀ 𝑦 ∈ 𝑥 ( 𝐵 ‘ 𝑦 ) = ( 𝐴 ‘ 𝑦 ) ∧ ( 𝐵 ‘ 𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐴 ‘ 𝑥 ) ) ↔ ( ∀ 𝑦 ∈ 𝑋 ( 𝐵 ‘ 𝑦 ) = ( 𝐴 ‘ 𝑦 ) ∧ ( 𝐵 ‘ 𝑋 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐴 ‘ 𝑋 ) ) ) )
37 36 rspcev ⊢ ( ( 𝑋 ∈ On ∧ ( ∀ 𝑦 ∈ 𝑋 ( 𝐵 ‘ 𝑦 ) = ( 𝐴 ‘ 𝑦 ) ∧ ( 𝐵 ‘ 𝑋 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐴 ‘ 𝑋 ) ) ) → ∃ 𝑥 ∈ On ( ∀ 𝑦 ∈ 𝑥 ( 𝐵 ‘ 𝑦 ) = ( 𝐴 ‘ 𝑦 ) ∧ ( 𝐵 ‘ 𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐴 ‘ 𝑥 ) ) )
38 6 16 31 37 syl12anc ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ ( 𝐴 ‘ 𝑋 ) = 2o ) ∧ ( ( 𝐵 ‘ 𝑋 ) = ∅ ∨ ( 𝐵 ‘ 𝑋 ) = 1o ) ) → ∃ 𝑥 ∈ On ( ∀ 𝑦 ∈ 𝑥 ( 𝐵 ‘ 𝑦 ) = ( 𝐴 ‘ 𝑦 ) ∧ ( 𝐵 ‘ 𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐴 ‘ 𝑥 ) ) )
39 simp12 ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ ( 𝐴 ‘ 𝑋 ) = 2o ) ∧ ( ( 𝐵 ‘ 𝑋 ) = ∅ ∨ ( 𝐵 ‘ 𝑋 ) = 1o ) ) → 𝐵 ∈ No )
40 simp11 ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ ( 𝐴 ‘ 𝑋 ) = 2o ) ∧ ( ( 𝐵 ‘ 𝑋 ) = ∅ ∨ ( 𝐵 ‘ 𝑋 ) = 1o ) ) → 𝐴 ∈ No )
41 ltsval ⊢ ( ( 𝐵 ∈ No ∧ 𝐴 ∈ No ) → ( 𝐵 <s 𝐴 ↔ ∃ 𝑥 ∈ On ( ∀ 𝑦 ∈ 𝑥 ( 𝐵 ‘ 𝑦 ) = ( 𝐴 ‘ 𝑦 ) ∧ ( 𝐵 ‘ 𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐴 ‘ 𝑥 ) ) ) )
42 39 40 41 syl2anc ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ ( 𝐴 ‘ 𝑋 ) = 2o ) ∧ ( ( 𝐵 ‘ 𝑋 ) = ∅ ∨ ( 𝐵 ‘ 𝑋 ) = 1o ) ) → ( 𝐵 <s 𝐴 ↔ ∃ 𝑥 ∈ On ( ∀ 𝑦 ∈ 𝑥 ( 𝐵 ‘ 𝑦 ) = ( 𝐴 ‘ 𝑦 ) ∧ ( 𝐵 ‘ 𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐴 ‘ 𝑥 ) ) ) )
43 38 42 mpbird ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ ( 𝐴 ‘ 𝑋 ) = 2o ) ∧ ( ( 𝐵 ‘ 𝑋 ) = ∅ ∨ ( 𝐵 ‘ 𝑋 ) = 1o ) ) → 𝐵 <s 𝐴 )
44 43 3expia ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ ( 𝐴 ‘ 𝑋 ) = 2o ) ) → ( ( ( 𝐵 ‘ 𝑋 ) = ∅ ∨ ( 𝐵 ‘ 𝑋 ) = 1o ) → 𝐵 <s 𝐴 ) )
45 5 44 syld ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ ( 𝐴 ‘ 𝑋 ) = 2o ) ) → ( ¬ ( 𝐵 ‘ 𝑋 ) = 2o → 𝐵 <s 𝐴 ) )
46 45 con1d ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ ( 𝐴 ‘ 𝑋 ) = 2o ) ) → ( ¬ 𝐵 <s 𝐴 → ( 𝐵 ‘ 𝑋 ) = 2o ) )
47 46 3impia ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On ) ∧ ( ( 𝐴 ↾ 𝑋 ) = ( 𝐵 ↾ 𝑋 ) ∧ ( 𝐴 ‘ 𝑋 ) = 2o ) ∧ ¬ 𝐵 <s 𝐴 ) → ( 𝐵 ‘ 𝑋 ) = 2o )