Theorem acni3

Description: The property of being a choice set of length A . (Contributed by Mario Carneiro, 31-Aug-2015)

	Ref	Expression
Hypothesis	acni3.1	⊢ ( 𝑦 = ( 𝑔 ‘ 𝑥 ) → ( 𝜑 ↔ 𝜓 ) )
Assertion	acni3	⊢ ( ( 𝑋 ∈ AC 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝑋 𝜑 ) → ∃ 𝑔 ( 𝑔 : 𝐴 ⟶ 𝑋 ∧ ∀ 𝑥 ∈ 𝐴 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		acni3.1	⊢ ( 𝑦 = ( 𝑔 ‘ 𝑥 ) → ( 𝜑 ↔ 𝜓 ) )
2		rabn0	⊢ ( { 𝑦 ∈ 𝑋 ∣ 𝜑 } ≠ ∅ ↔ ∃ 𝑦 ∈ 𝑋 𝜑 )
3	2	biimpri	⊢ ( ∃ 𝑦 ∈ 𝑋 𝜑 → { 𝑦 ∈ 𝑋 ∣ 𝜑 } ≠ ∅ )
4		ssrab2	⊢ { 𝑦 ∈ 𝑋 ∣ 𝜑 } ⊆ 𝑋
5	3 4	jctil	⊢ ( ∃ 𝑦 ∈ 𝑋 𝜑 → ( { 𝑦 ∈ 𝑋 ∣ 𝜑 } ⊆ 𝑋 ∧ { 𝑦 ∈ 𝑋 ∣ 𝜑 } ≠ ∅ ) )
6	5	ralimi	⊢ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝑋 𝜑 → ∀ 𝑥 ∈ 𝐴 ( { 𝑦 ∈ 𝑋 ∣ 𝜑 } ⊆ 𝑋 ∧ { 𝑦 ∈ 𝑋 ∣ 𝜑 } ≠ ∅ ) )
7		acni2	⊢ ( ( 𝑋 ∈ AC 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( { 𝑦 ∈ 𝑋 ∣ 𝜑 } ⊆ 𝑋 ∧ { 𝑦 ∈ 𝑋 ∣ 𝜑 } ≠ ∅ ) ) → ∃ 𝑔 ( 𝑔 : 𝐴 ⟶ 𝑋 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑔 ‘ 𝑥 ) ∈ { 𝑦 ∈ 𝑋 ∣ 𝜑 } ) )
8	6 7	sylan2	⊢ ( ( 𝑋 ∈ AC 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝑋 𝜑 ) → ∃ 𝑔 ( 𝑔 : 𝐴 ⟶ 𝑋 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑔 ‘ 𝑥 ) ∈ { 𝑦 ∈ 𝑋 ∣ 𝜑 } ) )
9	1	elrab	⊢ ( ( 𝑔 ‘ 𝑥 ) ∈ { 𝑦 ∈ 𝑋 ∣ 𝜑 } ↔ ( ( 𝑔 ‘ 𝑥 ) ∈ 𝑋 ∧ 𝜓 ) )
10	9	simprbi	⊢ ( ( 𝑔 ‘ 𝑥 ) ∈ { 𝑦 ∈ 𝑋 ∣ 𝜑 } → 𝜓 )
11	10	ralimi	⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝑔 ‘ 𝑥 ) ∈ { 𝑦 ∈ 𝑋 ∣ 𝜑 } → ∀ 𝑥 ∈ 𝐴 𝜓 )
12	11	anim2i	⊢ ( ( 𝑔 : 𝐴 ⟶ 𝑋 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑔 ‘ 𝑥 ) ∈ { 𝑦 ∈ 𝑋 ∣ 𝜑 } ) → ( 𝑔 : 𝐴 ⟶ 𝑋 ∧ ∀ 𝑥 ∈ 𝐴 𝜓 ) )
13	12	eximi	⊢ ( ∃ 𝑔 ( 𝑔 : 𝐴 ⟶ 𝑋 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑔 ‘ 𝑥 ) ∈ { 𝑦 ∈ 𝑋 ∣ 𝜑 } ) → ∃ 𝑔 ( 𝑔 : 𝐴 ⟶ 𝑋 ∧ ∀ 𝑥 ∈ 𝐴 𝜓 ) )
14	8 13	syl	⊢ ( ( 𝑋 ∈ AC 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝑋 𝜑 ) → ∃ 𝑔 ( 𝑔 : 𝐴 ⟶ 𝑋 ∧ ∀ 𝑥 ∈ 𝐴 𝜓 ) )