Metamath Proof Explorer

Theorem ac9s

Description: An Axiom of Choice equivalent: the infinite Cartesian product of nonempty classes is nonempty. Axiom of Choice (second form) of Enderton p. 55 and its converse. This is a stronger version of the axiom in Enderton, with no existence requirement for the family of classes B ( x ) (achieved via the Collection Principle cp ). (Contributed by NM, 29-Sep-2006)

Ref Expression
Hypothesis ac9.1 ⊢A∈V
Assertion ac9s ⊢∀x∈AB≠∅↔⨉x∈AB≠∅

Proof

Step Hyp Ref Expression
1 ac9.1 ⊢A∈V
2 1 ac6s4 ⊢∀x∈AB≠∅→∃ffFnA∧∀x∈Af⁡x∈B
3 n0 ⊢⨉x∈AB≠∅↔∃ff∈⨉x∈AB
4 vex ⊢f∈V
5 4 elixp ⊢f∈⨉x∈AB↔fFnA∧∀x∈Af⁡x∈B
6 5 exbii ⊢∃ff∈⨉x∈AB↔∃ffFnA∧∀x∈Af⁡x∈B
7 3 6 bitr2i ⊢∃ffFnA∧∀x∈Af⁡x∈B↔⨉x∈AB≠∅
8 2 7 sylib ⊢∀x∈AB≠∅→⨉x∈AB≠∅
9 ixpn0 ⊢⨉x∈AB≠∅→∀x∈AB≠∅
10 8 9 impbii ⊢∀x∈AB≠∅↔⨉x∈AB≠∅