This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 e. _V
Assertion ac9s 
|- ( A. x e. A B =/= (/) <-> X_ x e. A B =/= (/) )

Proof

Step Hyp Ref Expression
1 ac9.1 
 |-  A e. _V
2 1 ac6s4 
 |-  ( A. x e. A B =/= (/) -> E. f ( f Fn A /\ A. x e. A ( f ` x ) e. B ) )
3 n0 
 |-  ( X_ x e. A B =/= (/) <-> E. f f e. X_ x e. A B )
4 vex 
 |-  f e. _V
5 4 elixp 
 |-  ( f e. X_ x e. A B <-> ( f Fn A /\ A. x e. A ( f ` x ) e. B ) )
6 5 exbii 
 |-  ( E. f f e. X_ x e. A B <-> E. f ( f Fn A /\ A. x e. A ( f ` x ) e. B ) )
7 3 6 bitr2i 
 |-  ( E. f ( f Fn A /\ A. x e. A ( f ` x ) e. B ) <-> X_ x e. A B =/= (/) )
8 2 7 sylib 
 |-  ( A. x e. A B =/= (/) -> X_ x e. A B =/= (/) )
9 ixpn0 
 |-  ( X_ x e. A B =/= (/) -> A. x e. A B =/= (/) )
10 8 9 impbii 
 |-  ( A. x e. A B =/= (/) <-> X_ x e. A B =/= (/) )