How to prove well ordering principle => axiom of choice

Stream: mathlib4

[Santiago Mourenza Rivero]

I have already done the definitions of wop and aoc. The problem I had is that I need to extract the relation R for choosing one function s that $s(X i) = min (X i) \in X i$.

variable (γ : Type _)
variable {β I : Type _}
variable (X : I → Set β)

variable (A : Set γ)
variable (S : Set α)

open Set

def well_ordered_principle : Prop := (isPartialOrder R : γ  → γ → Prop) →  (∀ (A : Set γ), Nonempty A) → ∃ n ∈ A, ∀ m ∈ A, R n m

def axiom_of_choice : Prop := (∀ (i : I), Nonempty (X i)) → ∃ (f : (I → ⋃ i, X i)), ∀ (i : I), (f i).1 ∈ X i

theorem wop_aoc : well_ordered_principle γ A → axiom_of_choice X := by
  intro wop nempty