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