This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 𝐴 ) ∃ 𝑔 ∀ 𝑥 ∈ 𝐴 ( 𝑔 ‘ 𝑥 ) ∈ ( 𝑓 ‘ 𝑥 ) ) )