Metamath Proof Explorer

Theorem isacn

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

Ref Expression
Assertion isacn ⊢ X ∈ V ∧ A ∈ W → X ∈ AC _ A ↔ ∀ f ∈ 𝒫 X ∖ ∅ A ∃ g ∀ x ∈ A g ⁡ x ∈ f ⁡ x

Proof

Step Hyp Ref Expression
1 pweq ⊢ y = X → 𝒫 y = 𝒫 X
2 1 difeq1d ⊢ y = X → 𝒫 y ∖ ∅ = 𝒫 X ∖ ∅
3 2 oveq1d ⊢ y = X → 𝒫 y ∖ ∅ A = 𝒫 X ∖ ∅ A
4 3 raleqdv ⊢ y = X → ∀ f ∈ 𝒫 y ∖ ∅ A ∃ g ∀ x ∈ A g ⁡ x ∈ f ⁡ x ↔ ∀ f ∈ 𝒫 X ∖ ∅ A ∃ g ∀ x ∈ A g ⁡ x ∈ f ⁡ x
5 4 anbi2d ⊢ y = X → A ∈ V ∧ ∀ f ∈ 𝒫 y ∖ ∅ A ∃ g ∀ x ∈ A g ⁡ x ∈ f ⁡ x ↔ A ∈ V ∧ ∀ f ∈ 𝒫 X ∖ ∅ A ∃ g ∀ x ∈ A g ⁡ x ∈ f ⁡ x
6 df-acn ⊢ AC _ A = y | A ∈ V ∧ ∀ f ∈ 𝒫 y ∖ ∅ A ∃ g ∀ x ∈ A g ⁡ x ∈ f ⁡ x
7 5 6 elab2g ⊢ X ∈ V → X ∈ AC _ A ↔ A ∈ V ∧ ∀ f ∈ 𝒫 X ∖ ∅ A ∃ g ∀ x ∈ A g ⁡ x ∈ f ⁡ x
8 elex ⊢ A ∈ W → A ∈ V
9 biid ⊢ A ∈ V ∧ ∀ f ∈ 𝒫 X ∖ ∅ A ∃ g ∀ x ∈ A g ⁡ x ∈ f ⁡ x ↔ A ∈ V ∧ ∀ f ∈ 𝒫 X ∖ ∅ A ∃ g ∀ x ∈ A g ⁡ x ∈ f ⁡ x
10 9 baib ⊢ A ∈ V → A ∈ V ∧ ∀ f ∈ 𝒫 X ∖ ∅ A ∃ g ∀ x ∈ A g ⁡ x ∈ f ⁡ x ↔ ∀ f ∈ 𝒫 X ∖ ∅ A ∃ g ∀ x ∈ A g ⁡ x ∈ f ⁡ x
11 8 10 syl ⊢ A ∈ W → A ∈ V ∧ ∀ f ∈ 𝒫 X ∖ ∅ A ∃ g ∀ x ∈ A g ⁡ x ∈ f ⁡ x ↔ ∀ f ∈ 𝒫 X ∖ ∅ A ∃ g ∀ x ∈ A g ⁡ x ∈ f ⁡ x
12 7 11 sylan9bb ⊢ X ∈ V ∧ A ∈ W → X ∈ AC _ A ↔ ∀ f ∈ 𝒫 X ∖ ∅ A ∃ g ∀ x ∈ A g ⁡ x ∈ f ⁡ x