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∈Ag⁡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∈Ag⁡x∈f⁡x↔∀f∈𝒫X∖∅A∃g∀x∈Ag⁡x∈f⁡x
5 4 anbi2d ⊢y=X→A∈V∧∀f∈𝒫y∖∅A∃g∀x∈Ag⁡x∈f⁡x↔A∈V∧∀f∈𝒫X∖∅A∃g∀x∈Ag⁡x∈f⁡x
6 df-acn ⊢AC_A=y|A∈V∧∀f∈𝒫y∖∅A∃g∀x∈Ag⁡x∈f⁡x
7 5 6 elab2g ⊢X∈V→X∈AC_A↔A∈V∧∀f∈𝒫X∖∅A∃g∀x∈Ag⁡x∈f⁡x
8 elex ⊢A∈W→A∈V
9 biid ⊢A∈V∧∀f∈𝒫X∖∅A∃g∀x∈Ag⁡x∈f⁡x↔A∈V∧∀f∈𝒫X∖∅A∃g∀x∈Ag⁡x∈f⁡x
10 9 baib ⊢A∈V→A∈V∧∀f∈𝒫X∖∅A∃g∀x∈Ag⁡x∈f⁡x↔∀f∈𝒫X∖∅A∃g∀x∈Ag⁡x∈f⁡x
11 8 10 syl ⊢A∈W→A∈V∧∀f∈𝒫X∖∅A∃g∀x∈Ag⁡x∈f⁡x↔∀f∈𝒫X∖∅A∃g∀x∈Ag⁡x∈f⁡x
12 7 11 sylan9bb ⊢X∈V∧A∈W→X∈AC_A↔∀f∈𝒫X∖∅A∃g∀x∈Ag⁡x∈f⁡x