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 NM, 1-Oct-2006) (Proof shortened by Mario Carneiro, 22-Jun-2016)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | ixp0 | ⊢ ( ∃ 𝑥 ∈ 𝐴 𝐵 = ∅ → X 𝑥 ∈ 𝐴 𝐵 = ∅ ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | nne | ⊢ ( ¬ 𝐵 ≠ ∅ ↔ 𝐵 = ∅ ) | |
| 2 | 1 | rexbii | ⊢ ( ∃ 𝑥 ∈ 𝐴 ¬ 𝐵 ≠ ∅ ↔ ∃ 𝑥 ∈ 𝐴 𝐵 = ∅ ) |
| 3 | rexnal | ⊢ ( ∃ 𝑥 ∈ 𝐴 ¬ 𝐵 ≠ ∅ ↔ ¬ ∀ 𝑥 ∈ 𝐴 𝐵 ≠ ∅ ) | |
| 4 | 2 3 | bitr3i | ⊢ ( ∃ 𝑥 ∈ 𝐴 𝐵 = ∅ ↔ ¬ ∀ 𝑥 ∈ 𝐴 𝐵 ≠ ∅ ) |
| 5 | ixpn0 | ⊢ ( X 𝑥 ∈ 𝐴 𝐵 ≠ ∅ → ∀ 𝑥 ∈ 𝐴 𝐵 ≠ ∅ ) | |
| 6 | 5 | necon1bi | ⊢ ( ¬ ∀ 𝑥 ∈ 𝐴 𝐵 ≠ ∅ → X 𝑥 ∈ 𝐴 𝐵 = ∅ ) |
| 7 | 4 6 | sylbi | ⊢ ( ∃ 𝑥 ∈ 𝐴 𝐵 = ∅ → X 𝑥 ∈ 𝐴 𝐵 = ∅ ) |