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

Metamath Proof Explorer

Theorem axacnd

Description: A version of the Axiom of Choice with no distinct variable conditions. (New usage is discouraged.) (Contributed by NM, 3-Jan-2002) (Proof shortened by Mario Carneiro, 10-Dec-2016)

Ref Expression
Assertion axacnd 
|- E. x A. y A. z ( A. x ( y e. z /\ z e. w ) -> E. w A. y ( E. w ( ( y e. z /\ z e. w ) /\ ( y e. w /\ w e. x ) ) <-> y = w ) )

Proof

Step Hyp Ref Expression
1 axacndlem5 
 |-  E. x A. y A. v ( A. x ( y e. v /\ v e. w ) -> E. w A. y ( E. w ( ( y e. v /\ v e. w ) /\ ( y e. w /\ w e. x ) ) <-> y = w ) )
2 nfnae 
 |-  F/ x -. A. z z = x
3 nfnae 
 |-  F/ x -. A. z z = y
4 nfnae 
 |-  F/ x -. A. z z = w
5 2 3 4 nf3an 
 |-  F/ x ( -. A. z z = x /\ -. A. z z = y /\ -. A. z z = w )
6 nfnae 
 |-  F/ y -. A. z z = x
7 nfnae 
 |-  F/ y -. A. z z = y
8 nfnae 
 |-  F/ y -. A. z z = w
9 6 7 8 nf3an 
 |-  F/ y ( -. A. z z = x /\ -. A. z z = y /\ -. A. z z = w )
10 nfnae 
 |-  F/ z -. A. z z = x
11 nfnae 
 |-  F/ z -. A. z z = y
12 nfnae 
 |-  F/ z -. A. z z = w
13 10 11 12 nf3an 
 |-  F/ z ( -. A. z z = x /\ -. A. z z = y /\ -. A. z z = w )
14 nfcvf 
 |-  ( -. A. z z = y -> F/_ z y )
15 14 3ad2ant2 
 |-  ( ( -. A. z z = x /\ -. A. z z = y /\ -. A. z z = w ) -> F/_ z y )
16 nfcvd 
 |-  ( ( -. A. z z = x /\ -. A. z z = y /\ -. A. z z = w ) -> F/_ z v )
17 15 16 nfeld 
 |-  ( ( -. A. z z = x /\ -. A. z z = y /\ -. A. z z = w ) -> F/ z y e. v )
18 nfcvf 
 |-  ( -. A. z z = w -> F/_ z w )
19 18 3ad2ant3 
 |-  ( ( -. A. z z = x /\ -. A. z z = y /\ -. A. z z = w ) -> F/_ z w )
20 16 19 nfeld 
 |-  ( ( -. A. z z = x /\ -. A. z z = y /\ -. A. z z = w ) -> F/ z v e. w )
21 17 20 nfand 
 |-  ( ( -. A. z z = x /\ -. A. z z = y /\ -. A. z z = w ) -> F/ z ( y e. v /\ v e. w ) )
22 5 21 nfald 
 |-  ( ( -. A. z z = x /\ -. A. z z = y /\ -. A. z z = w ) -> F/ z A. x ( y e. v /\ v e. w ) )
23 nfnae 
 |-  F/ w -. A. z z = x
24 nfnae 
 |-  F/ w -. A. z z = y
25 nfnae 
 |-  F/ w -. A. z z = w
26 23 24 25 nf3an 
 |-  F/ w ( -. A. z z = x /\ -. A. z z = y /\ -. A. z z = w )
27 15 19 nfeld 
 |-  ( ( -. A. z z = x /\ -. A. z z = y /\ -. A. z z = w ) -> F/ z y e. w )
28 nfcvf 
 |-  ( -. A. z z = x -> F/_ z x )
29 28 3ad2ant1 
 |-  ( ( -. A. z z = x /\ -. A. z z = y /\ -. A. z z = w ) -> F/_ z x )
30 19 29 nfeld 
 |-  ( ( -. A. z z = x /\ -. A. z z = y /\ -. A. z z = w ) -> F/ z w e. x )
31 27 30 nfand 
 |-  ( ( -. A. z z = x /\ -. A. z z = y /\ -. A. z z = w ) -> F/ z ( y e. w /\ w e. x ) )
32 21 31 nfand 
 |-  ( ( -. A. z z = x /\ -. A. z z = y /\ -. A. z z = w ) -> F/ z ( ( y e. v /\ v e. w ) /\ ( y e. w /\ w e. x ) ) )
33 26 32 nfexd 
 |-  ( ( -. A. z z = x /\ -. A. z z = y /\ -. A. z z = w ) -> F/ z E. w ( ( y e. v /\ v e. w ) /\ ( y e. w /\ w e. x ) ) )
34 15 19 nfeqd 
 |-  ( ( -. A. z z = x /\ -. A. z z = y /\ -. A. z z = w ) -> F/ z y = w )
35 33 34 nfbid 
 |-  ( ( -. A. z z = x /\ -. A. z z = y /\ -. A. z z = w ) -> F/ z ( E. w ( ( y e. v /\ v e. w ) /\ ( y e. w /\ w e. x ) ) <-> y = w ) )
36 9 35 nfald 
 |-  ( ( -. A. z z = x /\ -. A. z z = y /\ -. A. z z = w ) -> F/ z A. y ( E. w ( ( y e. v /\ v e. w ) /\ ( y e. w /\ w e. x ) ) <-> y = w ) )
37 26 36 nfexd 
 |-  ( ( -. A. z z = x /\ -. A. z z = y /\ -. A. z z = w ) -> F/ z E. w A. y ( E. w ( ( y e. v /\ v e. w ) /\ ( y e. w /\ w e. x ) ) <-> y = w ) )
38 22 37 nfimd 
 |-  ( ( -. A. z z = x /\ -. A. z z = y /\ -. A. z z = w ) -> F/ z ( A. x ( y e. v /\ v e. w ) -> E. w A. y ( E. w ( ( y e. v /\ v e. w ) /\ ( y e. w /\ w e. x ) ) <-> y = w ) ) )
39 nfcvd 
 |-  ( ( -. A. z z = x /\ -. A. z z = y /\ -. A. z z = w ) -> F/_ x v )
40 nfcvf2 
 |-  ( -. A. z z = x -> F/_ x z )
41 40 3ad2ant1 
 |-  ( ( -. A. z z = x /\ -. A. z z = y /\ -. A. z z = w ) -> F/_ x z )
42 39 41 nfeqd 
 |-  ( ( -. A. z z = x /\ -. A. z z = y /\ -. A. z z = w ) -> F/ x v = z )
43 5 42 nfan1 
 |-  F/ x ( ( -. A. z z = x /\ -. A. z z = y /\ -. A. z z = w ) /\ v = z )
44 simpr 
 |-  ( ( ( -. A. z z = x /\ -. A. z z = y /\ -. A. z z = w ) /\ v = z ) -> v = z )
45 44 eleq2d 
 |-  ( ( ( -. A. z z = x /\ -. A. z z = y /\ -. A. z z = w ) /\ v = z ) -> ( y e. v <-> y e. z ) )
46 44 eleq1d 
 |-  ( ( ( -. A. z z = x /\ -. A. z z = y /\ -. A. z z = w ) /\ v = z ) -> ( v e. w <-> z e. w ) )
47 45 46 anbi12d 
 |-  ( ( ( -. A. z z = x /\ -. A. z z = y /\ -. A. z z = w ) /\ v = z ) -> ( ( y e. v /\ v e. w ) <-> ( y e. z /\ z e. w ) ) )
48 43 47 albid 
 |-  ( ( ( -. A. z z = x /\ -. A. z z = y /\ -. A. z z = w ) /\ v = z ) -> ( A. x ( y e. v /\ v e. w ) <-> A. x ( y e. z /\ z e. w ) ) )
49 nfcvd 
 |-  ( ( -. A. z z = x /\ -. A. z z = y /\ -. A. z z = w ) -> F/_ w v )
50 nfcvf2 
 |-  ( -. A. z z = w -> F/_ w z )
51 50 3ad2ant3 
 |-  ( ( -. A. z z = x /\ -. A. z z = y /\ -. A. z z = w ) -> F/_ w z )
52 49 51 nfeqd 
 |-  ( ( -. A. z z = x /\ -. A. z z = y /\ -. A. z z = w ) -> F/ w v = z )
53 26 52 nfan1 
 |-  F/ w ( ( -. A. z z = x /\ -. A. z z = y /\ -. A. z z = w ) /\ v = z )
54 nfcvd 
 |-  ( ( -. A. z z = x /\ -. A. z z = y /\ -. A. z z = w ) -> F/_ y v )
55 nfcvf2 
 |-  ( -. A. z z = y -> F/_ y z )
56 55 3ad2ant2 
 |-  ( ( -. A. z z = x /\ -. A. z z = y /\ -. A. z z = w ) -> F/_ y z )
57 54 56 nfeqd 
 |-  ( ( -. A. z z = x /\ -. A. z z = y /\ -. A. z z = w ) -> F/ y v = z )
58 9 57 nfan1 
 |-  F/ y ( ( -. A. z z = x /\ -. A. z z = y /\ -. A. z z = w ) /\ v = z )
59 47 anbi1d 
 |-  ( ( ( -. A. z z = x /\ -. A. z z = y /\ -. A. z z = w ) /\ v = z ) -> ( ( ( y e. v /\ v e. w ) /\ ( y e. w /\ w e. x ) ) <-> ( ( y e. z /\ z e. w ) /\ ( y e. w /\ w e. x ) ) ) )
60 53 59 exbid 
 |-  ( ( ( -. A. z z = x /\ -. A. z z = y /\ -. A. z z = w ) /\ v = z ) -> ( E. w ( ( y e. v /\ v e. w ) /\ ( y e. w /\ w e. x ) ) <-> E. w ( ( y e. z /\ z e. w ) /\ ( y e. w /\ w e. x ) ) ) )
61 60 bibi1d 
 |-  ( ( ( -. A. z z = x /\ -. A. z z = y /\ -. A. z z = w ) /\ v = z ) -> ( ( E. w ( ( y e. v /\ v e. w ) /\ ( y e. w /\ w e. x ) ) <-> y = w ) <-> ( E. w ( ( y e. z /\ z e. w ) /\ ( y e. w /\ w e. x ) ) <-> y = w ) ) )
62 58 61 albid 
 |-  ( ( ( -. A. z z = x /\ -. A. z z = y /\ -. A. z z = w ) /\ v = z ) -> ( A. y ( E. w ( ( y e. v /\ v e. w ) /\ ( y e. w /\ w e. x ) ) <-> y = w ) <-> A. y ( E. w ( ( y e. z /\ z e. w ) /\ ( y e. w /\ w e. x ) ) <-> y = w ) ) )
63 53 62 exbid 
 |-  ( ( ( -. A. z z = x /\ -. A. z z = y /\ -. A. z z = w ) /\ v = z ) -> ( E. w A. y ( E. w ( ( y e. v /\ v e. w ) /\ ( y e. w /\ w e. x ) ) <-> y = w ) <-> E. w A. y ( E. w ( ( y e. z /\ z e. w ) /\ ( y e. w /\ w e. x ) ) <-> y = w ) ) )
64 48 63 imbi12d 
 |-  ( ( ( -. A. z z = x /\ -. A. z z = y /\ -. A. z z = w ) /\ v = z ) -> ( ( A. x ( y e. v /\ v e. w ) -> E. w A. y ( E. w ( ( y e. v /\ v e. w ) /\ ( y e. w /\ w e. x ) ) <-> y = w ) ) <-> ( A. x ( y e. z /\ z e. w ) -> E. w A. y ( E. w ( ( y e. z /\ z e. w ) /\ ( y e. w /\ w e. x ) ) <-> y = w ) ) ) )
65 64 ex 
 |-  ( ( -. A. z z = x /\ -. A. z z = y /\ -. A. z z = w ) -> ( v = z -> ( ( A. x ( y e. v /\ v e. w ) -> E. w A. y ( E. w ( ( y e. v /\ v e. w ) /\ ( y e. w /\ w e. x ) ) <-> y = w ) ) <-> ( A. x ( y e. z /\ z e. w ) -> E. w A. y ( E. w ( ( y e. z /\ z e. w ) /\ ( y e. w /\ w e. x ) ) <-> y = w ) ) ) ) )
66 13 38 65 cbvald 
 |-  ( ( -. A. z z = x /\ -. A. z z = y /\ -. A. z z = w ) -> ( A. v ( A. x ( y e. v /\ v e. w ) -> E. w A. y ( E. w ( ( y e. v /\ v e. w ) /\ ( y e. w /\ w e. x ) ) <-> y = w ) ) <-> A. z ( A. x ( y e. z /\ z e. w ) -> E. w A. y ( E. w ( ( y e. z /\ z e. w ) /\ ( y e. w /\ w e. x ) ) <-> y = w ) ) ) )
67 9 66 albid 
 |-  ( ( -. A. z z = x /\ -. A. z z = y /\ -. A. z z = w ) -> ( A. y A. v ( A. x ( y e. v /\ v e. w ) -> E. w A. y ( E. w ( ( y e. v /\ v e. w ) /\ ( y e. w /\ w e. x ) ) <-> y = w ) ) <-> A. y A. z ( A. x ( y e. z /\ z e. w ) -> E. w A. y ( E. w ( ( y e. z /\ z e. w ) /\ ( y e. w /\ w e. x ) ) <-> y = w ) ) ) )
68 5 67 exbid 
 |-  ( ( -. A. z z = x /\ -. A. z z = y /\ -. A. z z = w ) -> ( E. x A. y A. v ( A. x ( y e. v /\ v e. w ) -> E. w A. y ( E. w ( ( y e. v /\ v e. w ) /\ ( y e. w /\ w e. x ) ) <-> y = w ) ) <-> E. x A. y A. z ( A. x ( y e. z /\ z e. w ) -> E. w A. y ( E. w ( ( y e. z /\ z e. w ) /\ ( y e. w /\ w e. x ) ) <-> y = w ) ) ) )
69 1 68 mpbii 
 |-  ( ( -. A. z z = x /\ -. A. z z = y /\ -. A. z z = w ) -> E. x A. y A. z ( A. x ( y e. z /\ z e. w ) -> E. w A. y ( E. w ( ( y e. z /\ z e. w ) /\ ( y e. w /\ w e. x ) ) <-> y = w ) ) )
70 69 3exp 
 |-  ( -. A. z z = x -> ( -. A. z z = y -> ( -. A. z z = w -> E. x A. y A. z ( A. x ( y e. z /\ z e. w ) -> E. w A. y ( E. w ( ( y e. z /\ z e. w ) /\ ( y e. w /\ w e. x ) ) <-> y = w ) ) ) ) )
71 axacndlem2 
 |-  ( A. x x = z -> E. x A. y A. z ( A. x ( y e. z /\ z e. w ) -> E. w A. y ( E. w ( ( y e. z /\ z e. w ) /\ ( y e. w /\ w e. x ) ) <-> y = w ) ) )
72 71 aecoms 
 |-  ( A. z z = x -> E. x A. y A. z ( A. x ( y e. z /\ z e. w ) -> E. w A. y ( E. w ( ( y e. z /\ z e. w ) /\ ( y e. w /\ w e. x ) ) <-> y = w ) ) )
73 axacndlem3 
 |-  ( A. y y = z -> E. x A. y A. z ( A. x ( y e. z /\ z e. w ) -> E. w A. y ( E. w ( ( y e. z /\ z e. w ) /\ ( y e. w /\ w e. x ) ) <-> y = w ) ) )
74 73 aecoms 
 |-  ( A. z z = y -> E. x A. y A. z ( A. x ( y e. z /\ z e. w ) -> E. w A. y ( E. w ( ( y e. z /\ z e. w ) /\ ( y e. w /\ w e. x ) ) <-> y = w ) ) )
75 nfae 
 |-  F/ y A. z z = w
76 simpr 
 |-  ( ( y e. z /\ z e. w ) -> z e. w )
77 76 alimi 
 |-  ( A. x ( y e. z /\ z e. w ) -> A. x z e. w )
78 nd3 
 |-  ( A. z z = w -> -. A. x z e. w )
79 78 pm2.21d 
 |-  ( A. z z = w -> ( A. x z e. w -> E. w A. y ( E. w ( ( y e. z /\ z e. w ) /\ ( y e. w /\ w e. x ) ) <-> y = w ) ) )
80 77 79 syl5 
 |-  ( A. z z = w -> ( A. x ( y e. z /\ z e. w ) -> E. w A. y ( E. w ( ( y e. z /\ z e. w ) /\ ( y e. w /\ w e. x ) ) <-> y = w ) ) )
81 80 axc4i 
 |-  ( A. z z = w -> A. z ( A. x ( y e. z /\ z e. w ) -> E. w A. y ( E. w ( ( y e. z /\ z e. w ) /\ ( y e. w /\ w e. x ) ) <-> y = w ) ) )
82 75 81 alrimi 
 |-  ( A. z z = w -> A. y A. z ( A. x ( y e. z /\ z e. w ) -> E. w A. y ( E. w ( ( y e. z /\ z e. w ) /\ ( y e. w /\ w e. x ) ) <-> y = w ) ) )
83 82 19.8ad 
 |-  ( A. z z = w -> E. x A. y A. z ( A. x ( y e. z /\ z e. w ) -> E. w A. y ( E. w ( ( y e. z /\ z e. w ) /\ ( y e. w /\ w e. x ) ) <-> y = w ) ) )
84 70 72 74 83 pm2.61iii 
 |-  E. x A. y A. z ( A. x ( y e. z /\ z e. w ) -> E. w A. y ( E. w ( ( y e. z /\ z e. w ) /\ ( y e. w /\ w e. x ) ) <-> y = w ) )