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 ( ( 𝑋𝑉𝐴𝑊 ) → ( 𝑋AC 𝐴 ↔ ∀ 𝑓 ∈ ( ( 𝒫 𝑋 ∖ { ∅ } ) ↑m 𝐴 ) ∃ 𝑔𝑥𝐴 ( 𝑔𝑥 ) ∈ ( 𝑓𝑥 ) ) )

Proof

Step Hyp Ref Expression
1 pweq ( 𝑦 = 𝑋 → 𝒫 𝑦 = 𝒫 𝑋 )
2 1 difeq1d ( 𝑦 = 𝑋 → ( 𝒫 𝑦 ∖ { ∅ } ) = ( 𝒫 𝑋 ∖ { ∅ } ) )
3 2 oveq1d ( 𝑦 = 𝑋 → ( ( 𝒫 𝑦 ∖ { ∅ } ) ↑m 𝐴 ) = ( ( 𝒫 𝑋 ∖ { ∅ } ) ↑m 𝐴 ) )
4 3 raleqdv ( 𝑦 = 𝑋 → ( ∀ 𝑓 ∈ ( ( 𝒫 𝑦 ∖ { ∅ } ) ↑m 𝐴 ) ∃ 𝑔𝑥𝐴 ( 𝑔𝑥 ) ∈ ( 𝑓𝑥 ) ↔ ∀ 𝑓 ∈ ( ( 𝒫 𝑋 ∖ { ∅ } ) ↑m 𝐴 ) ∃ 𝑔𝑥𝐴 ( 𝑔𝑥 ) ∈ ( 𝑓𝑥 ) ) )
5 4 anbi2d ( 𝑦 = 𝑋 → ( ( 𝐴 ∈ V ∧ ∀ 𝑓 ∈ ( ( 𝒫 𝑦 ∖ { ∅ } ) ↑m 𝐴 ) ∃ 𝑔𝑥𝐴 ( 𝑔𝑥 ) ∈ ( 𝑓𝑥 ) ) ↔ ( 𝐴 ∈ V ∧ ∀ 𝑓 ∈ ( ( 𝒫 𝑋 ∖ { ∅ } ) ↑m 𝐴 ) ∃ 𝑔𝑥𝐴 ( 𝑔𝑥 ) ∈ ( 𝑓𝑥 ) ) ) )
6 df-acn AC 𝐴 = { 𝑦 ∣ ( 𝐴 ∈ V ∧ ∀ 𝑓 ∈ ( ( 𝒫 𝑦 ∖ { ∅ } ) ↑m 𝐴 ) ∃ 𝑔𝑥𝐴 ( 𝑔𝑥 ) ∈ ( 𝑓𝑥 ) ) }
7 5 6 elab2g ( 𝑋𝑉 → ( 𝑋AC 𝐴 ↔ ( 𝐴 ∈ V ∧ ∀ 𝑓 ∈ ( ( 𝒫 𝑋 ∖ { ∅ } ) ↑m 𝐴 ) ∃ 𝑔𝑥𝐴 ( 𝑔𝑥 ) ∈ ( 𝑓𝑥 ) ) ) )
8 elex ( 𝐴𝑊𝐴 ∈ V )
9 biid ( ( 𝐴 ∈ V ∧ ∀ 𝑓 ∈ ( ( 𝒫 𝑋 ∖ { ∅ } ) ↑m 𝐴 ) ∃ 𝑔𝑥𝐴 ( 𝑔𝑥 ) ∈ ( 𝑓𝑥 ) ) ↔ ( 𝐴 ∈ V ∧ ∀ 𝑓 ∈ ( ( 𝒫 𝑋 ∖ { ∅ } ) ↑m 𝐴 ) ∃ 𝑔𝑥𝐴 ( 𝑔𝑥 ) ∈ ( 𝑓𝑥 ) ) )
10 9 baib ( 𝐴 ∈ V → ( ( 𝐴 ∈ V ∧ ∀ 𝑓 ∈ ( ( 𝒫 𝑋 ∖ { ∅ } ) ↑m 𝐴 ) ∃ 𝑔𝑥𝐴 ( 𝑔𝑥 ) ∈ ( 𝑓𝑥 ) ) ↔ ∀ 𝑓 ∈ ( ( 𝒫 𝑋 ∖ { ∅ } ) ↑m 𝐴 ) ∃ 𝑔𝑥𝐴 ( 𝑔𝑥 ) ∈ ( 𝑓𝑥 ) ) )
11 8 10 syl ( 𝐴𝑊 → ( ( 𝐴 ∈ V ∧ ∀ 𝑓 ∈ ( ( 𝒫 𝑋 ∖ { ∅ } ) ↑m 𝐴 ) ∃ 𝑔𝑥𝐴 ( 𝑔𝑥 ) ∈ ( 𝑓𝑥 ) ) ↔ ∀ 𝑓 ∈ ( ( 𝒫 𝑋 ∖ { ∅ } ) ↑m 𝐴 ) ∃ 𝑔𝑥𝐴 ( 𝑔𝑥 ) ∈ ( 𝑓𝑥 ) ) )
12 7 11 sylan9bb ( ( 𝑋𝑉𝐴𝑊 ) → ( 𝑋AC 𝐴 ↔ ∀ 𝑓 ∈ ( ( 𝒫 𝑋 ∖ { ∅ } ) ↑m 𝐴 ) ∃ 𝑔𝑥𝐴 ( 𝑔𝑥 ) ∈ ( 𝑓𝑥 ) ) )