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 𝑥 ∈ 𝐴 𝐵 ≠ ∅ → ∀ 𝑥 ∈ 𝐴 𝐵 ≠ ∅ )

Proof

Step	Hyp	Ref	Expression
1		n0	⊢ ( X 𝑥 ∈ 𝐴 𝐵 ≠ ∅ ↔ ∃ 𝑓 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 )
2		df-ixp	⊢ X 𝑥 ∈ 𝐴 𝐵 = { 𝑓 ∣ ( 𝑓 Fn { 𝑥 ∣ 𝑥 ∈ 𝐴 } ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 ) }
3	2	eqabri	⊢ ( 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 ↔ ( 𝑓 Fn { 𝑥 ∣ 𝑥 ∈ 𝐴 } ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 ) )
4		ne0i	⊢ ( ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 → 𝐵 ≠ ∅ )
5	4	ralimi	⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 → ∀ 𝑥 ∈ 𝐴 𝐵 ≠ ∅ )
6	3 5	simplbiim	⊢ ( 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 → ∀ 𝑥 ∈ 𝐴 𝐵 ≠ ∅ )
7	6	exlimiv	⊢ ( ∃ 𝑓 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 → ∀ 𝑥 ∈ 𝐴 𝐵 ≠ ∅ )
8	1 7	sylbi	⊢ ( X 𝑥 ∈ 𝐴 𝐵 ≠ ∅ → ∀ 𝑥 ∈ 𝐴 𝐵 ≠ ∅ )