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 𝐴 ∈ V
Assertion ac9s ( ∀ 𝑥𝐴 𝐵 ≠ ∅ ↔ X 𝑥𝐴 𝐵 ≠ ∅ )

Proof

Step Hyp Ref Expression
1 ac9.1 𝐴 ∈ V
2 1 ac6s4 ( ∀ 𝑥𝐴 𝐵 ≠ ∅ → ∃ 𝑓 ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥𝐴 ( 𝑓𝑥 ) ∈ 𝐵 ) )
3 n0 ( X 𝑥𝐴 𝐵 ≠ ∅ ↔ ∃ 𝑓 𝑓X 𝑥𝐴 𝐵 )
4 vex 𝑓 ∈ V
5 4 elixp ( 𝑓X 𝑥𝐴 𝐵 ↔ ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥𝐴 ( 𝑓𝑥 ) ∈ 𝐵 ) )
6 5 exbii ( ∃ 𝑓 𝑓X 𝑥𝐴 𝐵 ↔ ∃ 𝑓 ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥𝐴 ( 𝑓𝑥 ) ∈ 𝐵 ) )
7 3 6 bitr2i ( ∃ 𝑓 ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥𝐴 ( 𝑓𝑥 ) ∈ 𝐵 ) ↔ X 𝑥𝐴 𝐵 ≠ ∅ )
8 2 7 sylib ( ∀ 𝑥𝐴 𝐵 ≠ ∅ → X 𝑥𝐴 𝐵 ≠ ∅ )
9 ixpn0 ( X 𝑥𝐴 𝐵 ≠ ∅ → ∀ 𝑥𝐴 𝐵 ≠ ∅ )
10 8 9 impbii ( ∀ 𝑥𝐴 𝐵 ≠ ∅ ↔ X 𝑥𝐴 𝐵 ≠ ∅ )