Metamath Proof Explorer

Theorem ac6c4

Description: Equivalent of Axiom of Choice. B is a collection B ( x ) of nonempty sets. (Contributed by Mario Carneiro, 22-Mar-2013)

Ref Expression
Hypotheses ac6c4.1 
|- A e. _V
ac6c4.2 
|- B e. _V
Assertion ac6c4 
|- ( A. x e. A B =/= (/) -> E. f ( f Fn A /\ A. x e. A ( f ` x ) e. B ) )

Proof

Step Hyp Ref Expression
1 ac6c4.1 
 |-  A e. _V
2 ac6c4.2 
 |-  B e. _V
3 nfv 
 |-  F/ z B =/= (/)
4 nfcsb1v 
 |-  F/_ x [_ z / x ]_ B
5 nfcv 
 |-  F/_ x (/)
6 4 5 nfne 
 |-  F/ x [_ z / x ]_ B =/= (/)
7 csbeq1a 
 |-  ( x = z -> B = [_ z / x ]_ B )
8 7 neeq1d 
 |-  ( x = z -> ( B =/= (/) <-> [_ z / x ]_ B =/= (/) ) )
9 3 6 8 cbvralw 
 |-  ( A. x e. A B =/= (/) <-> A. z e. A [_ z / x ]_ B =/= (/) )
10 n0 
 |-  ( [_ z / x ]_ B =/= (/) <-> E. y y e. [_ z / x ]_ B )
11 nfv 
 |-  F/ y z e. A
12 nfre1 
 |-  F/ y E. y e. U_ x e. A B y e. [_ z / x ]_ B
13 4 nfel2 
 |-  F/ x y e. [_ z / x ]_ B
14 7 eleq2d 
 |-  ( x = z -> ( y e. B <-> y e. [_ z / x ]_ B ) )
15 13 14 rspce 
 |-  ( ( z e. A /\ y e. [_ z / x ]_ B ) -> E. x e. A y e. B )
16 eliun 
 |-  ( y e. U_ x e. A B <-> E. x e. A y e. B )
17 15 16 sylibr 
 |-  ( ( z e. A /\ y e. [_ z / x ]_ B ) -> y e. U_ x e. A B )
18 rspe 
 |-  ( ( y e. U_ x e. A B /\ y e. [_ z / x ]_ B ) -> E. y e. U_ x e. A B y e. [_ z / x ]_ B )
19 17 18 sylancom 
 |-  ( ( z e. A /\ y e. [_ z / x ]_ B ) -> E. y e. U_ x e. A B y e. [_ z / x ]_ B )
20 19 ex 
 |-  ( z e. A -> ( y e. [_ z / x ]_ B -> E. y e. U_ x e. A B y e. [_ z / x ]_ B ) )
21 11 12 20 exlimd 
 |-  ( z e. A -> ( E. y y e. [_ z / x ]_ B -> E. y e. U_ x e. A B y e. [_ z / x ]_ B ) )
22 10 21 biimtrid 
 |-  ( z e. A -> ( [_ z / x ]_ B =/= (/) -> E. y e. U_ x e. A B y e. [_ z / x ]_ B ) )
23 22 ralimia 
 |-  ( A. z e. A [_ z / x ]_ B =/= (/) -> A. z e. A E. y e. U_ x e. A B y e. [_ z / x ]_ B )
24 9 23 sylbi 
 |-  ( A. x e. A B =/= (/) -> A. z e. A E. y e. U_ x e. A B y e. [_ z / x ]_ B )
25 1 2 iunex 
 |-  U_ x e. A B e. _V
26 eleq1 
 |-  ( y = ( f ` z ) -> ( y e. [_ z / x ]_ B <-> ( f ` z ) e. [_ z / x ]_ B ) )
27 1 25 26 ac6 
 |-  ( A. z e. A E. y e. U_ x e. A B y e. [_ z / x ]_ B -> E. f ( f : A --> U_ x e. A B /\ A. z e. A ( f ` z ) e. [_ z / x ]_ B ) )
28 ffn 
 |-  ( f : A --> U_ x e. A B -> f Fn A )
29 nfv 
 |-  F/ z ( f ` x ) e. B
30 4 nfel2 
 |-  F/ x ( f ` z ) e. [_ z / x ]_ B
31 fveq2 
 |-  ( x = z -> ( f ` x ) = ( f ` z ) )
32 31 7 eleq12d 
 |-  ( x = z -> ( ( f ` x ) e. B <-> ( f ` z ) e. [_ z / x ]_ B ) )
33 29 30 32 cbvralw 
 |-  ( A. x e. A ( f ` x ) e. B <-> A. z e. A ( f ` z ) e. [_ z / x ]_ B )
34 33 biimpri 
 |-  ( A. z e. A ( f ` z ) e. [_ z / x ]_ B -> A. x e. A ( f ` x ) e. B )
35 28 34 anim12i 
 |-  ( ( f : A --> U_ x e. A B /\ A. z e. A ( f ` z ) e. [_ z / x ]_ B ) -> ( f Fn A /\ A. x e. A ( f ` x ) e. B ) )
36 35 eximi 
 |-  ( E. f ( f : A --> U_ x e. A B /\ A. z e. A ( f ` z ) e. [_ z / x ]_ B ) -> E. f ( f Fn A /\ A. x e. A ( f ` x ) e. B ) )
37 24 27 36 3syl 
 |-  ( A. x e. A B =/= (/) -> E. f ( f Fn A /\ A. x e. A ( f ` x ) e. B ) )