Theorem ac9

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. (Contributed by Mario Carneiro, 22-Mar-2013)

	Ref	Expression
Hypotheses	ac6c4.1	⊢ 𝐴 ∈ V
	ac6c4.2	⊢ 𝐵 ∈ V
Assertion	ac9	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ≠ ∅ ↔ X 𝑥 ∈ 𝐴 𝐵 ≠ ∅ )

Proof

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