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 ⊢ 𝐴 ∈ V
ac6s.2 ⊢ ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝜑 ↔ 𝜓 ) )
Assertion ac6n ( ∀ 𝑓 ( 𝑓 : 𝐴 ⟶ 𝐵 → ∃ 𝑥 ∈ 𝐴 𝜓 ) → ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝜑 )

Proof

Step Hyp Ref Expression
1 ac6s.1 ⊢ 𝐴 ∈ V
2 ac6s.2 ⊢ ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝜑 ↔ 𝜓 ) )
3 2 notbid ⊢ ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( ¬ 𝜑 ↔ ¬ 𝜓 ) )
4 1 3 ac6s ⊢ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ¬ 𝜑 → ∃ 𝑓 ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ¬ 𝜓 ) )
5 4 con3i ⊢ ( ¬ ∃ 𝑓 ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ¬ 𝜓 ) → ¬ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ¬ 𝜑 )
6 dfrex2 ⊢ ( ∃ 𝑥 ∈ 𝐴 𝜓 ↔ ¬ ∀ 𝑥 ∈ 𝐴 ¬ 𝜓 )
7 6 imbi2i ⊢ ( ( 𝑓 : 𝐴 ⟶ 𝐵 → ∃ 𝑥 ∈ 𝐴 𝜓 ) ↔ ( 𝑓 : 𝐴 ⟶ 𝐵 → ¬ ∀ 𝑥 ∈ 𝐴 ¬ 𝜓 ) )
8 7 albii ⊢ ( ∀ 𝑓 ( 𝑓 : 𝐴 ⟶ 𝐵 → ∃ 𝑥 ∈ 𝐴 𝜓 ) ↔ ∀ 𝑓 ( 𝑓 : 𝐴 ⟶ 𝐵 → ¬ ∀ 𝑥 ∈ 𝐴 ¬ 𝜓 ) )
9 alinexa ⊢ ( ∀ 𝑓 ( 𝑓 : 𝐴 ⟶ 𝐵 → ¬ ∀ 𝑥 ∈ 𝐴 ¬ 𝜓 ) ↔ ¬ ∃ 𝑓 ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ¬ 𝜓 ) )
10 8 9 bitri ⊢ ( ∀ 𝑓 ( 𝑓 : 𝐴 ⟶ 𝐵 → ∃ 𝑥 ∈ 𝐴 𝜓 ) ↔ ¬ ∃ 𝑓 ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ¬ 𝜓 ) )
11 dfral2 ⊢ ( ∀ 𝑦 ∈ 𝐵 𝜑 ↔ ¬ ∃ 𝑦 ∈ 𝐵 ¬ 𝜑 )
12 11 rexbii ⊢ ( ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝜑 ↔ ∃ 𝑥 ∈ 𝐴 ¬ ∃ 𝑦 ∈ 𝐵 ¬ 𝜑 )
13 rexnal ⊢ ( ∃ 𝑥 ∈ 𝐴 ¬ ∃ 𝑦 ∈ 𝐵 ¬ 𝜑 ↔ ¬ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ¬ 𝜑 )
14 12 13 bitri ⊢ ( ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝜑 ↔ ¬ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ¬ 𝜑 )
15 5 10 14 3imtr4i ⊢ ( ∀ 𝑓 ( 𝑓 : 𝐴 ⟶ 𝐵 → ∃ 𝑥 ∈ 𝐴 𝜓 ) → ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝜑 )