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

Metamath Proof Explorer

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