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

Metamath Proof Explorer

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