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

Metamath Proof Explorer

Theorem ixpn0

Description: The infinite Cartesian product of a family B ( x ) with an empty member is empty. The converse of this theorem is equivalent to the Axiom of Choice, see ac9 . (Contributed by Mario Carneiro, 22-Jun-2016)

Ref Expression
Assertion ixpn0 
|- ( X_ x e. A B =/= (/) -> A. x e. A B =/= (/) )

Proof

Step Hyp Ref Expression
1 n0 
 |-  ( X_ x e. A B =/= (/) <-> E. f f e. X_ x e. A B )
2 df-ixp 
 |-  X_ x e. A B = { f | ( f Fn { x | x e. A } /\ A. x e. A ( f ` x ) e. B ) }
3 2 eqabri 
 |-  ( f e. X_ x e. A B <-> ( f Fn { x | x e. A } /\ A. x e. A ( f ` x ) e. B ) )
4 ne0i 
 |-  ( ( f ` x ) e. B -> B =/= (/) )
5 4 ralimi 
 |-  ( A. x e. A ( f ` x ) e. B -> A. x e. A B =/= (/) )
6 3 5 simplbiim 
 |-  ( f e. X_ x e. A B -> A. x e. A B =/= (/) )
7 6 exlimiv 
 |-  ( E. f f e. X_ x e. A B -> A. x e. A B =/= (/) )
8 1 7 sylbi 
 |-  ( X_ x e. A B =/= (/) -> A. x e. A B =/= (/) )