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 ⊢ y = g ⁡ x → φ ↔ ψ
Assertion acni3 ⊢ X ∈ AC _ A ∧ ∀ x ∈ A ∃ y ∈ X φ → ∃ g g : A ⟶ X ∧ ∀ x ∈ A ψ

Proof

Step Hyp Ref Expression
1 acni3.1 ⊢ y = g ⁡ x → φ ↔ ψ
2 rabn0 ⊢ y ∈ X | φ ≠ ∅ ↔ ∃ y ∈ X φ
3 2 biimpri ⊢ ∃ y ∈ X φ → y ∈ X | φ ≠ ∅
4 ssrab2 ⊢ y ∈ X | φ ⊆ X
5 3 4 jctil ⊢ ∃ y ∈ X φ → y ∈ X | φ ⊆ X ∧ y ∈ X | φ ≠ ∅
6 5 ralimi ⊢ ∀ x ∈ A ∃ y ∈ X φ → ∀ x ∈ A y ∈ X | φ ⊆ X ∧ y ∈ X | φ ≠ ∅
7 acni2 ⊢ X ∈ AC _ A ∧ ∀ x ∈ A y ∈ X | φ ⊆ X ∧ y ∈ X | φ ≠ ∅ → ∃ g g : A ⟶ X ∧ ∀ x ∈ A g ⁡ x ∈ y ∈ X | φ
8 6 7 sylan2 ⊢ X ∈ AC _ A ∧ ∀ x ∈ A ∃ y ∈ X φ → ∃ g g : A ⟶ X ∧ ∀ x ∈ A g ⁡ x ∈ y ∈ X | φ
9 1 elrab ⊢ g ⁡ x ∈ y ∈ X | φ ↔ g ⁡ x ∈ X ∧ ψ
10 9 simprbi ⊢ g ⁡ x ∈ y ∈ X | φ → ψ
11 10 ralimi ⊢ ∀ x ∈ A g ⁡ x ∈ y ∈ X | φ → ∀ x ∈ A ψ
12 11 anim2i ⊢ g : A ⟶ X ∧ ∀ x ∈ A g ⁡ x ∈ y ∈ X | φ → g : A ⟶ X ∧ ∀ x ∈ A ψ
13 12 eximi ⊢ ∃ g g : A ⟶ X ∧ ∀ x ∈ A g ⁡ x ∈ y ∈ X | φ → ∃ g g : A ⟶ X ∧ ∀ x ∈ A ψ
14 8 13 syl ⊢ X ∈ AC _ A ∧ ∀ x ∈ A ∃ y ∈ X φ → ∃ g g : A ⟶ X ∧ ∀ x ∈ A ψ