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

Metamath Proof Explorer

Theorem ac6n

Description: Equivalent of Axiom of Choice. Contrapositive of ac6s . (Contributed by NM, 10-Jun-2007)

Ref Expression
Hypotheses ac6s.1 ⊢ A ∈ V
ac6s.2 ⊢ y = f ⁡ x → φ ↔ ψ
Assertion ac6n ⊢ ∀ f f : A ⟶ B → ∃ x ∈ A ψ → ∃ x ∈ A ∀ y ∈ B φ

Proof

Step Hyp Ref Expression
1 ac6s.1 ⊢ A ∈ V
2 ac6s.2 ⊢ y = f ⁡ x → φ ↔ ψ
3 2 notbid ⊢ y = f ⁡ x → ¬ φ ↔ ¬ ψ
4 1 3 ac6s ⊢ ∀ x ∈ A ∃ y ∈ B ¬ φ → ∃ f f : A ⟶ B ∧ ∀ x ∈ A ¬ ψ
5 4 con3i ⊢ ¬ ∃ f f : A ⟶ B ∧ ∀ x ∈ A ¬ ψ → ¬ ∀ x ∈ A ∃ y ∈ B ¬ φ
6 dfrex2 ⊢ ∃ x ∈ A ψ ↔ ¬ ∀ x ∈ A ¬ ψ
7 6 imbi2i ⊢ f : A ⟶ B → ∃ x ∈ A ψ ↔ f : A ⟶ B → ¬ ∀ x ∈ A ¬ ψ
8 7 albii ⊢ ∀ f f : A ⟶ B → ∃ x ∈ A ψ ↔ ∀ f f : A ⟶ B → ¬ ∀ x ∈ A ¬ ψ
9 alinexa ⊢ ∀ f f : A ⟶ B → ¬ ∀ x ∈ A ¬ ψ ↔ ¬ ∃ f f : A ⟶ B ∧ ∀ x ∈ A ¬ ψ
10 8 9 bitri ⊢ ∀ f f : A ⟶ B → ∃ x ∈ A ψ ↔ ¬ ∃ f f : A ⟶ B ∧ ∀ x ∈ A ¬ ψ
11 dfral2 ⊢ ∀ y ∈ B φ ↔ ¬ ∃ y ∈ B ¬ φ
12 11 rexbii ⊢ ∃ x ∈ A ∀ y ∈ B φ ↔ ∃ x ∈ A ¬ ∃ y ∈ B ¬ φ
13 rexnal ⊢ ∃ x ∈ A ¬ ∃ y ∈ B ¬ φ ↔ ¬ ∀ x ∈ A ∃ y ∈ B ¬ φ
14 12 13 bitri ⊢ ∃ x ∈ A ∀ y ∈ B φ ↔ ¬ ∀ x ∈ A ∃ y ∈ B ¬ φ
15 5 10 14 3imtr4i ⊢ ∀ f f : A ⟶ B → ∃ x ∈ A ψ → ∃ x ∈ A ∀ y ∈ B φ