Metamath Proof Explorer

Theorem acnrcl

Description: Reverse closure for the choice set predicate. (Contributed by Mario Carneiro, 31-Aug-2015)

Ref Expression
Assertion acnrcl ⊢ X ∈ AC _ A → A ∈ V

Proof

Step Hyp Ref Expression
1 ne0i ⊢ X ∈ x | A ∈ V ∧ ∀ f ∈ 𝒫 x ∖ ∅ A ∃ g ∀ y ∈ A g ⁡ y ∈ f ⁡ y → x | A ∈ V ∧ ∀ f ∈ 𝒫 x ∖ ∅ A ∃ g ∀ y ∈ A g ⁡ y ∈ f ⁡ y ≠ ∅
2 abn0 ⊢ x | A ∈ V ∧ ∀ f ∈ 𝒫 x ∖ ∅ A ∃ g ∀ y ∈ A g ⁡ y ∈ f ⁡ y ≠ ∅ ↔ ∃ x A ∈ V ∧ ∀ f ∈ 𝒫 x ∖ ∅ A ∃ g ∀ y ∈ A g ⁡ y ∈ f ⁡ y
3 simpl ⊢ A ∈ V ∧ ∀ f ∈ 𝒫 x ∖ ∅ A ∃ g ∀ y ∈ A g ⁡ y ∈ f ⁡ y → A ∈ V
4 3 exlimiv ⊢ ∃ x A ∈ V ∧ ∀ f ∈ 𝒫 x ∖ ∅ A ∃ g ∀ y ∈ A g ⁡ y ∈ f ⁡ y → A ∈ V
5 2 4 sylbi ⊢ x | A ∈ V ∧ ∀ f ∈ 𝒫 x ∖ ∅ A ∃ g ∀ y ∈ A g ⁡ y ∈ f ⁡ y ≠ ∅ → A ∈ V
6 1 5 syl ⊢ X ∈ x | A ∈ V ∧ ∀ f ∈ 𝒫 x ∖ ∅ A ∃ g ∀ y ∈ A g ⁡ y ∈ f ⁡ y → A ∈ V
7 df-acn ⊢ AC _ A = x | A ∈ V ∧ ∀ f ∈ 𝒫 x ∖ ∅ A ∃ g ∀ y ∈ A g ⁡ y ∈ f ⁡ y
8 6 7 eleq2s ⊢ X ∈ AC _ A → A ∈ V