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	abeq2i	|- ( 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 =/= (/) )