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 ( ∀ 𝑓 ( 𝑓 : 𝐴𝐵 → ∃ 𝑥𝐴 𝜓 ) → ∃ 𝑥𝐴𝑦𝐵 𝜑 )