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 ⊢ A ∈ V
ac6c4.2 ⊢ B ∈ V
Assertion ac9 ⊢ ∀ x ∈ A B ≠ ∅ ↔ ⨉ x ∈ A B ≠ ∅

Proof

Step Hyp Ref Expression
1 ac6c4.1 ⊢ A ∈ V
2 ac6c4.2 ⊢ B ∈ V
3 1 2 ac6c4 ⊢ ∀ x ∈ A B ≠ ∅ → ∃ f f Fn A ∧ ∀ x ∈ A f ⁡ x ∈ B
4 n0 ⊢ ⨉ x ∈ A B ≠ ∅ ↔ ∃ f f ∈ ⨉ x ∈ A B
5 vex ⊢ f ∈ V
6 5 elixp ⊢ f ∈ ⨉ x ∈ A B ↔ f Fn A ∧ ∀ x ∈ A f ⁡ x ∈ B
7 6 exbii ⊢ ∃ f f ∈ ⨉ x ∈ A B ↔ ∃ f f Fn A ∧ ∀ x ∈ A f ⁡ x ∈ B
8 4 7 bitr2i ⊢ ∃ f f Fn A ∧ ∀ x ∈ A f ⁡ x ∈ B ↔ ⨉ x ∈ A B ≠ ∅
9 3 8 sylib ⊢ ∀ x ∈ A B ≠ ∅ → ⨉ x ∈ A B ≠ ∅
10 ixpn0 ⊢ ⨉ x ∈ A B ≠ ∅ → ∀ x ∈ A B ≠ ∅
11 9 10 impbii ⊢ ∀ x ∈ A B ≠ ∅ ↔ ⨉ x ∈ A B ≠ ∅