Metamath Proof Explorer


Theorem dfac3

Description: Equivalence of two versions of the Axiom of Choice. The left-hand side is defined as the Axiom of Choice (first form) of Enderton p. 49. The right-hand side is the Axiom of Choice of TakeutiZaring p. 83. The proof does not depend on AC. (Contributed by NM, 24-Mar-2004) (Revised by Stefan O'Rear, 22-Feb-2015)

Ref Expression
Assertion dfac3 CHOICE x f z x z f z z

Proof

Step Hyp Ref Expression
1 df-ac CHOICE y f f y f Fn dom y
2 vex x V
3 vuniex x V
4 2 3 xpex x × x V
5 simpl w x v w w x
6 elunii v w w x v x
7 6 ancoms w x v w v x
8 5 7 jca w x v w w x v x
9 8 ssopab2i w v | w x v w w v | w x v x
10 df-xp x × x = w v | w x v x
11 9 10 sseqtrri w v | w x v w x × x
12 4 11 ssexi w v | w x v w V
13 sseq2 y = w v | w x v w f y f w v | w x v w
14 dmeq y = w v | w x v w dom y = dom w v | w x v w
15 14 fneq2d y = w v | w x v w f Fn dom y f Fn dom w v | w x v w
16 13 15 anbi12d y = w v | w x v w f y f Fn dom y f w v | w x v w f Fn dom w v | w x v w
17 16 exbidv y = w v | w x v w f f y f Fn dom y f f w v | w x v w f Fn dom w v | w x v w
18 12 17 spcv y f f y f Fn dom y f f w v | w x v w f Fn dom w v | w x v w
19 fndm f Fn dom w v | w x v w dom f = dom w v | w x v w
20 dmopab dom w v | w x v w = w | v w x v w
21 20 eleq2i z dom w v | w x v w z w | v w x v w
22 vex z V
23 elequ1 w = z w x z x
24 eleq2 w = z v w v z
25 23 24 anbi12d w = z w x v w z x v z
26 25 exbidv w = z v w x v w v z x v z
27 22 26 elab z w | v w x v w v z x v z
28 19.42v v z x v z z x v v z
29 n0 z v v z
30 29 anbi2i z x z z x v v z
31 28 30 bitr4i v z x v z z x z
32 21 27 31 3bitrri z x z z dom w v | w x v w
33 eleq2 dom f = dom w v | w x v w z dom f z dom w v | w x v w
34 32 33 bitr4id dom f = dom w v | w x v w z x z z dom f
35 19 34 syl f Fn dom w v | w x v w z x z z dom f
36 35 adantl f w v | w x v w f Fn dom w v | w x v w z x z z dom f
37 fnfun f Fn dom w v | w x v w Fun f
38 funfvima3 Fun f f w v | w x v w z dom f f z w v | w x v w z
39 38 ancoms f w v | w x v w Fun f z dom f f z w v | w x v w z
40 37 39 sylan2 f w v | w x v w f Fn dom w v | w x v w z dom f f z w v | w x v w z
41 36 40 sylbid f w v | w x v w f Fn dom w v | w x v w z x z f z w v | w x v w z
42 41 imp f w v | w x v w f Fn dom w v | w x v w z x z f z w v | w x v w z
43 imasng z V w v | w x v w z = u | z w v | w x v w u
44 43 elv w v | w x v w z = u | z w v | w x v w u
45 vex u V
46 elequ1 v = u v z u z
47 46 anbi2d v = u z x v z z x u z
48 eqid w v | w x v w = w v | w x v w
49 22 45 25 47 48 brab z w v | w x v w u z x u z
50 49 abbii u | z w v | w x v w u = u | z x u z
51 44 50 eqtri w v | w x v w z = u | z x u z
52 ibar z x u z z x u z
53 52 abbi2dv z x z = u | z x u z
54 51 53 eqtr4id z x w v | w x v w z = z
55 54 eleq2d z x f z w v | w x v w z f z z
56 55 ad2antrl f w v | w x v w f Fn dom w v | w x v w z x z f z w v | w x v w z f z z
57 42 56 mpbid f w v | w x v w f Fn dom w v | w x v w z x z f z z
58 57 exp32 f w v | w x v w f Fn dom w v | w x v w z x z f z z
59 58 ralrimiv f w v | w x v w f Fn dom w v | w x v w z x z f z z
60 59 eximi f f w v | w x v w f Fn dom w v | w x v w f z x z f z z
61 18 60 syl y f f y f Fn dom y f z x z f z z
62 61 alrimiv y f f y f Fn dom y x f z x z f z z
63 eqid w dom y f u | w y u = w dom y f u | w y u
64 63 aceq3lem x f z x z f z z f f y f Fn dom y
65 64 alrimiv x f z x z f z z y f f y f Fn dom y
66 62 65 impbii y f f y f Fn dom y x f z x z f z z
67 1 66 bitri CHOICE x f z x z f z z