Metamath Proof Explorer

Theorem acni

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

Ref Expression
Assertion acni ⊢ X ∈ AC _ A ∧ F : A ⟶ 𝒫 X ∖ ∅ → ∃ g ∀ x ∈ A g ⁡ x ∈ F ⁡ x

Proof

Step Hyp Ref Expression
1 fveq1 ⊢ f = F → f ⁡ x = F ⁡ x
2 1 eleq2d ⊢ f = F → g ⁡ x ∈ f ⁡ x ↔ g ⁡ x ∈ F ⁡ x
3 2 ralbidv ⊢ f = F → ∀ x ∈ A g ⁡ x ∈ f ⁡ x ↔ ∀ x ∈ A g ⁡ x ∈ F ⁡ x
4 3 exbidv ⊢ f = F → ∃ g ∀ x ∈ A g ⁡ x ∈ f ⁡ x ↔ ∃ g ∀ x ∈ A g ⁡ x ∈ F ⁡ x
5 acnrcl ⊢ X ∈ AC _ A → A ∈ V
6 isacn ⊢ X ∈ AC _ A ∧ A ∈ V → X ∈ AC _ A ↔ ∀ f ∈ 𝒫 X ∖ ∅ A ∃ g ∀ x ∈ A g ⁡ x ∈ f ⁡ x
7 5 6 mpdan ⊢ X ∈ AC _ A → X ∈ AC _ A ↔ ∀ f ∈ 𝒫 X ∖ ∅ A ∃ g ∀ x ∈ A g ⁡ x ∈ f ⁡ x
8 7 ibi ⊢ X ∈ AC _ A → ∀ f ∈ 𝒫 X ∖ ∅ A ∃ g ∀ x ∈ A g ⁡ x ∈ f ⁡ x
9 8 adantr ⊢ X ∈ AC _ A ∧ F : A ⟶ 𝒫 X ∖ ∅ → ∀ f ∈ 𝒫 X ∖ ∅ A ∃ g ∀ x ∈ A g ⁡ x ∈ f ⁡ x
10 pwexg ⊢ X ∈ AC _ A → 𝒫 X ∈ V
11 difexg ⊢ 𝒫 X ∈ V → 𝒫 X ∖ ∅ ∈ V
12 10 11 syl ⊢ X ∈ AC _ A → 𝒫 X ∖ ∅ ∈ V
13 12 5 elmapd ⊢ X ∈ AC _ A → F ∈ 𝒫 X ∖ ∅ A ↔ F : A ⟶ 𝒫 X ∖ ∅
14 13 biimpar ⊢ X ∈ AC _ A ∧ F : A ⟶ 𝒫 X ∖ ∅ → F ∈ 𝒫 X ∖ ∅ A
15 4 9 14 rspcdva ⊢ X ∈ AC _ A ∧ F : A ⟶ 𝒫 X ∖ ∅ → ∃ g ∀ x ∈ A g ⁡ x ∈ F ⁡ x