Metamath Proof Explorer


Theorem acni

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

Ref Expression
Assertion acni X AC _ A F : A 𝒫 X g x A g x F x

Proof

Step Hyp Ref Expression
1 fveq1 f = F f x = F x
2 1 eleq2d f = F g x f x g x F x
3 2 ralbidv f = F x A g x f x x A g x F x
4 3 exbidv f = F g x A g x f x g x A g x F x
5 acnrcl X AC _ A A V
6 isacn X AC _ A A V X AC _ A f 𝒫 X A g x A g x f x
7 5 6 mpdan X AC _ A X AC _ A f 𝒫 X A g x A g x f x
8 7 ibi X AC _ A f 𝒫 X A g x A g x f x
9 8 adantr X AC _ A F : A 𝒫 X f 𝒫 X A g x A g x f x
10 pwexg X AC _ A 𝒫 X V
11 10 difexd X AC _ A 𝒫 X V
12 11 5 elmapd X AC _ A F 𝒫 X A F : A 𝒫 X
13 12 biimpar X AC _ A F : A 𝒫 X F 𝒫 X A
14 4 9 13 rspcdva X AC _ A F : A 𝒫 X g x A g x F x