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

Metamath Proof Explorer

Theorem ac6

Proof