아래는 단순 예시입니다.(아래 수정한 수식이 있습니다)

alpha가 한 ordinal일때
모든 zeta in alpha + 1에 대하여 아래의 성질을 갖는 non-empty set A_{zeta}이 잘 정의되어 있다고 합시다.
(1) forall{zeta in (alpha + 1)} A_{zeta + 1} subsetneq A_{zeta} ;
(2) forall{zeta} (zeta는 limit oridinal이다.) rightarrow (forall{xi
x가 한 sequence of length alpha일 때, x를 다음과 같이 정의하려고 합니다.
forall{zeta in alpha} x(zeta) = a such that a in A_{zeta} setminus A_{zeta + 1};

즉 emptyset이 아닌 disjoint sets에서 하나씩 원소를 뽑아서 sequence를 정의하려하는데, 이때 필요한 것이 axiom of choice인가요?

지금 제가 공부하고 있는 부분이 집합론 초반부이고 axiom of choice는 교재 뒷부분에 있어서 이 공리를 공부하지 않았는데
위 sequence를 정의할 때 이 공리가 필요하다면 먼저 공부하고 넘어가려고 해요.

모바일 환경이라 특수문자 삽입이 어려워 글을 이렇게 쓰긴 했는데 알아보기 힘드시다면 나중에 데스크톱 환경에서 다시 글을 올리겠습니다. 감사합니다.

-수정본-

α가 한 ordinal일때
모든 ζ ∈ α + 1에 대하여 아래의 성질을 갖는 non-empty set A_ζ이 잘 정의되어 있다고 합시다.
(1) ∀(ζ ∈ α + 1) A_(ζ+1) ⊊ A_ζ ;
(2) ∀(ζ ∈ α) (ζ is limit oridinal) → (∀{ξ < ζ} A_ζ ⊊ A_ξ);

x가 한 sequence of length α일 때, x를 다음과 같이 정의하려고 합니다.
∀(ζ ∈ α) x(ζ) = y such that y ∈ A_ζ∖A_(ζ+1);