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	⊢ 𝐴 ∈ V
	Assertion	ac9s	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ≠ ∅ ↔ X 𝑥 ∈ 𝐴 𝐵 ≠ ∅ )

Proof

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

Metamath Proof Explorer

Theorem ac9s

Proof