Theorem ac6s

Description: Equivalent of Axiom of Choice. Using the Boundedness Axiom bnd2 , we derive this strong version of ac6 that doesn't require B to be a set. (Contributed by NM, 4-Feb-2004)

	Ref	Expression
Hypotheses	ac6s.1	⊢ 𝐴 ∈ V
	ac6s.2	⊢ ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝜑 ↔ 𝜓 ) )
Assertion	ac6s	⊢ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 → ∃ 𝑓 ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		ac6s.1	⊢ 𝐴 ∈ V
2		ac6s.2	⊢ ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝜑 ↔ 𝜓 ) )
3	1	bnd2	⊢ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 → ∃ 𝑧 ( 𝑧 ⊆ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝑧 𝜑 ) )
4		vex	⊢ 𝑧 ∈ V
5	1 4 2	ac6	⊢ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝑧 𝜑 → ∃ 𝑓 ( 𝑓 : 𝐴 ⟶ 𝑧 ∧ ∀ 𝑥 ∈ 𝐴 𝜓 ) )
6	5	anim2i	⊢ ( ( 𝑧 ⊆ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝑧 𝜑 ) → ( 𝑧 ⊆ 𝐵 ∧ ∃ 𝑓 ( 𝑓 : 𝐴 ⟶ 𝑧 ∧ ∀ 𝑥 ∈ 𝐴 𝜓 ) ) )
7	6	eximi	⊢ ( ∃ 𝑧 ( 𝑧 ⊆ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝑧 𝜑 ) → ∃ 𝑧 ( 𝑧 ⊆ 𝐵 ∧ ∃ 𝑓 ( 𝑓 : 𝐴 ⟶ 𝑧 ∧ ∀ 𝑥 ∈ 𝐴 𝜓 ) ) )
8		fss	⊢ ( ( 𝑓 : 𝐴 ⟶ 𝑧 ∧ 𝑧 ⊆ 𝐵 ) → 𝑓 : 𝐴 ⟶ 𝐵 )
9	8	expcom	⊢ ( 𝑧 ⊆ 𝐵 → ( 𝑓 : 𝐴 ⟶ 𝑧 → 𝑓 : 𝐴 ⟶ 𝐵 ) )
10	9	anim1d	⊢ ( 𝑧 ⊆ 𝐵 → ( ( 𝑓 : 𝐴 ⟶ 𝑧 ∧ ∀ 𝑥 ∈ 𝐴 𝜓 ) → ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 𝜓 ) ) )
11	10	eximdv	⊢ ( 𝑧 ⊆ 𝐵 → ( ∃ 𝑓 ( 𝑓 : 𝐴 ⟶ 𝑧 ∧ ∀ 𝑥 ∈ 𝐴 𝜓 ) → ∃ 𝑓 ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 𝜓 ) ) )
12	11	imp	⊢ ( ( 𝑧 ⊆ 𝐵 ∧ ∃ 𝑓 ( 𝑓 : 𝐴 ⟶ 𝑧 ∧ ∀ 𝑥 ∈ 𝐴 𝜓 ) ) → ∃ 𝑓 ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 𝜓 ) )
13	12	exlimiv	⊢ ( ∃ 𝑧 ( 𝑧 ⊆ 𝐵 ∧ ∃ 𝑓 ( 𝑓 : 𝐴 ⟶ 𝑧 ∧ ∀ 𝑥 ∈ 𝐴 𝜓 ) ) → ∃ 𝑓 ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 𝜓 ) )
14	3 7 13	3syl	⊢ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 → ∃ 𝑓 ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 𝜓 ) )