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