Metamath Proof Explorer

Theorem axacndlem4

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

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