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

Metamath Proof Explorer

Theorem ac6mapd

Description: Axiom of choice equivalent, deduction form. (Contributed by Thierry Arnoux, 13-Oct-2025)

Ref Expression
Hypotheses ac6mapd.1 ⊢ ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝜓 ↔ 𝜒 ) )
ac6mapd.2 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
ac6mapd.3 ⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
ac6mapd.4 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ∃ 𝑦 ∈ 𝐵 𝜓 )
Assertion ac6mapd ( 𝜑 → ∃ 𝑓 ∈ ( 𝐵 ↑m 𝐴 ) ∀ 𝑥 ∈ 𝐴 𝜒 )

Proof

Step Hyp Ref Expression
1 ac6mapd.1 ⊢ ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝜓 ↔ 𝜒 ) )
2 ac6mapd.2 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
3 ac6mapd.3 ⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
4 ac6mapd.4 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ∃ 𝑦 ∈ 𝐵 𝜓 )
5 4 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜓 )
6 1 ac6sg ⊢ ( 𝐴 ∈ 𝑉 → ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜓 → ∃ 𝑓 ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 𝜒 ) ) )
7 2 5 6 sylc ⊢ ( 𝜑 → ∃ 𝑓 ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 𝜒 ) )
8 3 2 elmapd ⊢ ( 𝜑 → ( 𝑓 ∈ ( 𝐵 ↑m 𝐴 ) ↔ 𝑓 : 𝐴 ⟶ 𝐵 ) )
9 8 biimprd ⊢ ( 𝜑 → ( 𝑓 : 𝐴 ⟶ 𝐵 → 𝑓 ∈ ( 𝐵 ↑m 𝐴 ) ) )
10 9 anim1d ⊢ ( 𝜑 → ( ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 𝜒 ) → ( 𝑓 ∈ ( 𝐵 ↑m 𝐴 ) ∧ ∀ 𝑥 ∈ 𝐴 𝜒 ) ) )
11 10 eximdv ⊢ ( 𝜑 → ( ∃ 𝑓 ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 𝜒 ) → ∃ 𝑓 ( 𝑓 ∈ ( 𝐵 ↑m 𝐴 ) ∧ ∀ 𝑥 ∈ 𝐴 𝜒 ) ) )
12 7 11 mpd ⊢ ( 𝜑 → ∃ 𝑓 ( 𝑓 ∈ ( 𝐵 ↑m 𝐴 ) ∧ ∀ 𝑥 ∈ 𝐴 𝜒 ) )
13 df-rex ⊢ ( ∃ 𝑓 ∈ ( 𝐵 ↑m 𝐴 ) ∀ 𝑥 ∈ 𝐴 𝜒 ↔ ∃ 𝑓 ( 𝑓 ∈ ( 𝐵 ↑m 𝐴 ) ∧ ∀ 𝑥 ∈ 𝐴 𝜒 ) )
14 12 13 sylibr ⊢ ( 𝜑 → ∃ 𝑓 ∈ ( 𝐵 ↑m 𝐴 ) ∀ 𝑥 ∈ 𝐴 𝜒 )