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

Metamath Proof Explorer

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