Metamath Proof Explorer


Theorem ac6

Description: Equivalent of Axiom of Choice. This is useful for proving that there exists, for example, a sequence mapping natural numbers to members of a larger set B , where ph depends on x (the natural number) and y (to specify a member of B ). A stronger version of this theorem, ac6s , allows B to be a proper class. (Contributed by NM, 18-Oct-1999) (Revised by Mario Carneiro, 27-Aug-2015)

Ref Expression
Hypotheses ac6.1 𝐴 ∈ V
ac6.2 𝐵 ∈ V
ac6.3 ( 𝑦 = ( 𝑓𝑥 ) → ( 𝜑𝜓 ) )
Assertion ac6 ( ∀ 𝑥𝐴𝑦𝐵 𝜑 → ∃ 𝑓 ( 𝑓 : 𝐴𝐵 ∧ ∀ 𝑥𝐴 𝜓 ) )

Proof

Step Hyp Ref Expression
1 ac6.1 𝐴 ∈ V
2 ac6.2 𝐵 ∈ V
3 ac6.3 ( 𝑦 = ( 𝑓𝑥 ) → ( 𝜑𝜓 ) )
4 ssrab2 { 𝑦𝐵𝜑 } ⊆ 𝐵
5 4 rgenw 𝑥𝐴 { 𝑦𝐵𝜑 } ⊆ 𝐵
6 iunss ( 𝑥𝐴 { 𝑦𝐵𝜑 } ⊆ 𝐵 ↔ ∀ 𝑥𝐴 { 𝑦𝐵𝜑 } ⊆ 𝐵 )
7 5 6 mpbir 𝑥𝐴 { 𝑦𝐵𝜑 } ⊆ 𝐵
8 2 7 ssexi 𝑥𝐴 { 𝑦𝐵𝜑 } ∈ V
9 numth3 ( 𝑥𝐴 { 𝑦𝐵𝜑 } ∈ V → 𝑥𝐴 { 𝑦𝐵𝜑 } ∈ dom card )
10 8 9 ax-mp 𝑥𝐴 { 𝑦𝐵𝜑 } ∈ dom card
11 3 ac6num ( ( 𝐴 ∈ V ∧ 𝑥𝐴 { 𝑦𝐵𝜑 } ∈ dom card ∧ ∀ 𝑥𝐴𝑦𝐵 𝜑 ) → ∃ 𝑓 ( 𝑓 : 𝐴𝐵 ∧ ∀ 𝑥𝐴 𝜓 ) )
12 1 10 11 mp3an12 ( ∀ 𝑥𝐴𝑦𝐵 𝜑 → ∃ 𝑓 ( 𝑓 : 𝐴𝐵 ∧ ∀ 𝑥𝐴 𝜓 ) )